Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dvh4dimat Unicode version

Theorem dvh4dimat 31628
 Description: There is an atom that is outside the subspace sum of 3 others. (Contributed by NM, 25-Apr-2015.)
Hypotheses
Ref Expression
dvh4dimat.h
dvh4dimat.u
dvh4dimat.s
dvh4dimat.a LSAtoms
dvh4dimat.k
dvh4dimat.p
dvh4dimat.q
dvh4dimat.r
Assertion
Ref Expression
dvh4dimat
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem dvh4dimat
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 dvh4dimat.k . . . . 5
21simpld 445 . . . 4
3 dvh4dimat.p . . . . 5
4 eqid 2283 . . . . . 6
5 dvh4dimat.h . . . . . 6
6 dvh4dimat.u . . . . . 6
7 eqid 2283 . . . . . 6
8 dvh4dimat.a . . . . . 6 LSAtoms
94, 5, 6, 7, 8dihlatat 31527 . . . . 5
101, 3, 9syl2anc 642 . . . 4
11 dvh4dimat.q . . . . 5
124, 5, 6, 7, 8dihlatat 31527 . . . . 5
131, 11, 12syl2anc 642 . . . 4
14 dvh4dimat.r . . . . 5
154, 5, 6, 7, 8dihlatat 31527 . . . . 5
161, 14, 15syl2anc 642 . . . 4
17 eqid 2283 . . . . 5
18 eqid 2283 . . . . 5
1917, 18, 43dim3 29658 . . . 4
202, 10, 13, 16, 19syl13anc 1184 . . 3
21 dvh4dimat.s . . . . . . . . 9
221adantr 451 . . . . . . . . 9
235, 6, 7, 8dih1dimat 31520 . . . . . . . . . . . 12
241, 3, 23syl2anc 642 . . . . . . . . . . 11
255, 7, 6, 21, 8, 1, 24, 11dihsmatrn 31626 . . . . . . . . . 10
2625adantr 451 . . . . . . . . 9
2714adantr 451 . . . . . . . . 9
2817, 5, 7, 6, 21, 8, 22, 26, 27dihjat4 31623 . . . . . . . 8
2924adantr 451 . . . . . . . . . . 11
3011adantr 451 . . . . . . . . . . 11
3117, 5, 7, 6, 21, 8, 22, 29, 30dihjat6 31624 . . . . . . . . . 10
3231oveq1d 5873 . . . . . . . . 9
3332fveq2d 5529 . . . . . . . 8
3428, 33eqtrd 2315 . . . . . . 7
3534sseq2d 3206 . . . . . 6
36 eqid 2283 . . . . . . . . 9
3736, 4atbase 29479 . . . . . . . 8
3837adantl 452 . . . . . . 7
39 hllat 29553 . . . . . . . . . 10
402, 39syl 15 . . . . . . . . 9
4136, 17, 4hlatjcl 29556 . . . . . . . . . 10
422, 10, 13, 41syl3anc 1182 . . . . . . . . 9
4336, 4atbase 29479 . . . . . . . . . 10
4416, 43syl 15 . . . . . . . . 9
4536, 17latjcl 14156 . . . . . . . . 9
4640, 42, 44, 45syl3anc 1182 . . . . . . . 8
4746adantr 451 . . . . . . 7
4836, 18, 5, 7dihord 31454 . . . . . . 7
4922, 38, 47, 48syl3anc 1182 . . . . . 6
5035, 49bitr2d 245 . . . . 5
5150notbid 285 . . . 4
5251rexbidva 2560 . . 3
5320, 52mpbid 201 . 2
544, 5, 6, 7, 8dihatlat 31524 . . . 4
551, 54sylan 457 . . 3
564, 5, 6, 7, 8dihlatat 31527 . . . . 5
571, 56sylan 457 . . . 4
581adantr 451 . . . . . 6
595, 6, 7, 8dih1dimat 31520 . . . . . . 7
601, 59sylan 457 . . . . . 6
615, 7dihcnvid2 31463 . . . . . 6
6258, 60, 61syl2anc 642 . . . . 5
6362eqcomd 2288 . . . 4
64 fveq2 5525 . . . . . 6
6564eqeq2d 2294 . . . . 5
6665rspcev 2884 . . . 4
6757, 63, 66syl2anc 642 . . 3
68 sseq1 3199 . . . . 5
6968notbid 285 . . . 4