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

Theorem dvh4dimat 32238
 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 447 . . . 4
3 dvh4dimat.p . . . . 5
4 eqid 2438 . . . . . 6
5 dvh4dimat.h . . . . . 6
6 dvh4dimat.u . . . . . 6
7 eqid 2438 . . . . . 6
8 dvh4dimat.a . . . . . 6 LSAtoms
94, 5, 6, 7, 8dihlatat 32137 . . . . 5
101, 3, 9syl2anc 644 . . . 4
11 dvh4dimat.q . . . . 5
124, 5, 6, 7, 8dihlatat 32137 . . . . 5
131, 11, 12syl2anc 644 . . . 4
14 dvh4dimat.r . . . . 5
154, 5, 6, 7, 8dihlatat 32137 . . . . 5
161, 14, 15syl2anc 644 . . . 4
17 eqid 2438 . . . . 5
18 eqid 2438 . . . . 5
1917, 18, 43dim3 30268 . . . 4
202, 10, 13, 16, 19syl13anc 1187 . . 3
21 dvh4dimat.s . . . . . . . . 9
221adantr 453 . . . . . . . . 9
235, 6, 7, 8dih1dimat 32130 . . . . . . . . . . . 12
241, 3, 23syl2anc 644 . . . . . . . . . . 11
255, 7, 6, 21, 8, 1, 24, 11dihsmatrn 32236 . . . . . . . . . 10
2625adantr 453 . . . . . . . . 9
2714adantr 453 . . . . . . . . 9
2817, 5, 7, 6, 21, 8, 22, 26, 27dihjat4 32233 . . . . . . . 8
2924adantr 453 . . . . . . . . . . 11
3011adantr 453 . . . . . . . . . . 11
3117, 5, 7, 6, 21, 8, 22, 29, 30dihjat6 32234 . . . . . . . . . 10
3231oveq1d 6098 . . . . . . . . 9
3332fveq2d 5734 . . . . . . . 8
3428, 33eqtrd 2470 . . . . . . 7
3534sseq2d 3378 . . . . . 6
36 eqid 2438 . . . . . . . . 9
3736, 4atbase 30089 . . . . . . . 8
3837adantl 454 . . . . . . 7
39 hllat 30163 . . . . . . . . . 10
402, 39syl 16 . . . . . . . . 9
4136, 17, 4hlatjcl 30166 . . . . . . . . . 10
422, 10, 13, 41syl3anc 1185 . . . . . . . . 9
4336, 4atbase 30089 . . . . . . . . . 10
4416, 43syl 16 . . . . . . . . 9
4536, 17latjcl 14481 . . . . . . . . 9
4640, 42, 44, 45syl3anc 1185 . . . . . . . 8
4746adantr 453 . . . . . . 7
4836, 18, 5, 7dihord 32064 . . . . . . 7
4922, 38, 47, 48syl3anc 1185 . . . . . 6
5035, 49bitr2d 247 . . . . 5
5150notbid 287 . . . 4
5251rexbidva 2724 . . 3
5320, 52mpbid 203 . 2
544, 5, 6, 7, 8dihatlat 32134 . . . 4
551, 54sylan 459 . . 3
564, 5, 6, 7, 8dihlatat 32137 . . . . 5
571, 56sylan 459 . . . 4
581adantr 453 . . . . . 6
595, 6, 7, 8dih1dimat 32130 . . . . . . 7
601, 59sylan 459 . . . . . 6
615, 7dihcnvid2 32073 . . . . . 6
6258, 60, 61syl2anc 644 . . . . 5
6362eqcomd 2443 . . . 4
64 fveq2 5730 . . . . . 6
6564eqeq2d 2449 . . . . 5
6665rspcev 3054 . . . 4
6757, 63, 66syl2anc 644 . . 3
68 sseq1 3371 . . . . 5
6968notbid 287 . . . 4