Metamath Proof Explorer


Theorem cdleme3h

Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme3fa and cdleme3 . (Contributed by NM, 6-Jun-2012)

Ref Expression
Hypotheses cdleme1.l ˙ = K
cdleme1.j ˙ = join K
cdleme1.m ˙ = meet K
cdleme1.a A = Atoms K
cdleme1.h H = LHyp K
cdleme1.u U = P ˙ Q ˙ W
cdleme1.f F = R ˙ U ˙ Q ˙ P ˙ R ˙ W
cdleme3.3 V = P ˙ R ˙ W
Assertion cdleme3h K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q F A

Proof

Step Hyp Ref Expression
1 cdleme1.l ˙ = K
2 cdleme1.j ˙ = join K
3 cdleme1.m ˙ = meet K
4 cdleme1.a A = Atoms K
5 cdleme1.h H = LHyp K
6 cdleme1.u U = P ˙ Q ˙ W
7 cdleme1.f F = R ˙ U ˙ Q ˙ P ˙ R ˙ W
8 cdleme3.3 V = P ˙ R ˙ W
9 1 2 3 4 5 6 7 8 cdleme3d F = R ˙ U ˙ Q ˙ V
10 simp1l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q K HL
11 simp23l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q R A
12 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q K HL W H
13 simp21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q P A ¬ P ˙ W
14 simp22l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q Q A
15 simp3l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q P Q
16 1 2 3 4 5 6 lhpat2 K HL W H P A ¬ P ˙ W Q A P Q U A
17 12 13 14 15 16 syl112anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q U A
18 eqid Base K = Base K
19 18 2 4 hlatjcl K HL R A U A R ˙ U Base K
20 10 11 17 19 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q R ˙ U Base K
21 simp3r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q ¬ R ˙ P ˙ Q
22 11 21 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q R A ¬ R ˙ P ˙ Q
23 1 2 3 4 5 6 7 8 cdleme3e K HL W H P A ¬ P ˙ W Q A R A ¬ R ˙ P ˙ Q V A
24 12 13 14 22 23 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q V A
25 18 2 4 hlatjcl K HL Q A V A Q ˙ V Base K
26 10 14 24 25 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q Q ˙ V Base K
27 10 hllatd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q K Lat
28 simp21l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q P A
29 18 2 4 hlatjcl K HL P A Q A P ˙ Q Base K
30 10 28 14 29 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q P ˙ Q Base K
31 simp1r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q W H
32 18 5 lhpbase W H W Base K
33 31 32 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q W Base K
34 18 1 3 latmle2 K Lat P ˙ Q Base K W Base K P ˙ Q ˙ W ˙ W
35 27 30 33 34 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q P ˙ Q ˙ W ˙ W
36 6 35 eqbrtrid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q U ˙ W
37 simp23r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q ¬ R ˙ W
38 nbrne2 U ˙ W ¬ R ˙ W U R
39 36 37 38 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q U R
40 39 necomd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q R U
41 eqid Lines K = Lines K
42 eqid pmap K = pmap K
43 2 4 41 42 linepmap K Lat R A U A R U pmap K R ˙ U Lines K
44 27 11 17 40 43 syl31anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q pmap K R ˙ U Lines K
45 18 2 4 hlatjcl K HL P A R A P ˙ R Base K
46 10 28 11 45 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q P ˙ R Base K
47 18 1 3 latmle2 K Lat P ˙ R Base K W Base K P ˙ R ˙ W ˙ W
48 27 46 33 47 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q P ˙ R ˙ W ˙ W
49 8 48 eqbrtrid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q V ˙ W
50 simp22r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q ¬ Q ˙ W
51 nbrne2 V ˙ W ¬ Q ˙ W V Q
52 49 50 51 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q V Q
53 52 necomd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q Q V
54 2 4 41 42 linepmap K Lat Q A V A Q V pmap K Q ˙ V Lines K
55 27 14 24 53 54 syl31anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q pmap K Q ˙ V Lines K
56 1 2 4 hlatlej1 K HL R A U A R ˙ R ˙ U
57 10 11 17 56 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q R ˙ R ˙ U
58 nbrne2 V ˙ W ¬ R ˙ W V R
59 49 37 58 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q V R
60 59 necomd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q R V
61 1 2 4 hlatexch2 K HL R A Q A V A R V R ˙ Q ˙ V Q ˙ R ˙ V
62 10 11 14 24 60 61 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q R ˙ Q ˙ V Q ˙ R ˙ V
63 8 oveq2i R ˙ V = R ˙ P ˙ R ˙ W
64 1 2 4 hlatlej2 K HL P A R A R ˙ P ˙ R
65 10 28 11 64 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q R ˙ P ˙ R
66 18 1 3 latmle1 K Lat P ˙ R Base K W Base K P ˙ R ˙ W ˙ P ˙ R
67 27 46 33 66 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q P ˙ R ˙ W ˙ P ˙ R
68 18 4 atbase R A R Base K
69 11 68 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q R Base K
70 18 3 latmcl K Lat P ˙ R Base K W Base K P ˙ R ˙ W Base K
71 27 46 33 70 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q P ˙ R ˙ W Base K
72 18 1 2 latjle12 K Lat R Base K P ˙ R ˙ W Base K P ˙ R Base K R ˙ P ˙ R P ˙ R ˙ W ˙ P ˙ R R ˙ P ˙ R ˙ W ˙ P ˙ R
73 27 69 71 46 72 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q R ˙ P ˙ R P ˙ R ˙ W ˙ P ˙ R R ˙ P ˙ R ˙ W ˙ P ˙ R
74 65 67 73 mpbi2and K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q R ˙ P ˙ R ˙ W ˙ P ˙ R
75 63 74 eqbrtrid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q R ˙ V ˙ P ˙ R
76 18 4 atbase Q A Q Base K
77 14 76 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q Q Base K
78 18 2 4 hlatjcl K HL R A V A R ˙ V Base K
79 10 11 24 78 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q R ˙ V Base K
80 18 1 lattr K Lat Q Base K R ˙ V Base K P ˙ R Base K Q ˙ R ˙ V R ˙ V ˙ P ˙ R Q ˙ P ˙ R
81 27 77 79 46 80 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q Q ˙ R ˙ V R ˙ V ˙ P ˙ R Q ˙ P ˙ R
82 75 81 mpan2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q Q ˙ R ˙ V Q ˙ P ˙ R
83 15 necomd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q Q P
84 1 2 4 hlatexch1 K HL Q A R A P A Q P Q ˙ P ˙ R R ˙ P ˙ Q
85 10 14 11 28 83 84 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q Q ˙ P ˙ R R ˙ P ˙ Q
86 62 82 85 3syld K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q R ˙ Q ˙ V R ˙ P ˙ Q
87 21 86 mtod K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q ¬ R ˙ Q ˙ V
88 nbrne1 R ˙ R ˙ U ¬ R ˙ Q ˙ V R ˙ U Q ˙ V
89 57 87 88 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q R ˙ U Q ˙ V
90 14 15 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q Q A P Q
91 simp23 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q R A ¬ R ˙ W
92 eqid 0. K = 0. K
93 1 2 3 4 5 6 7 92 cdleme3c K HL W H P A ¬ P ˙ W Q A P Q R A ¬ R ˙ W F 0. K
94 12 13 90 91 93 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q F 0. K
95 9 94 eqnetrrid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q R ˙ U ˙ Q ˙ V 0. K
96 18 3 92 4 41 42 2lnat K HL R ˙ U Base K Q ˙ V Base K pmap K R ˙ U Lines K pmap K Q ˙ V Lines K R ˙ U Q ˙ V R ˙ U ˙ Q ˙ V 0. K R ˙ U ˙ Q ˙ V A
97 10 20 26 44 55 89 95 96 syl322anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q R ˙ U ˙ Q ˙ V A
98 9 97 eqeltrid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ R ˙ P ˙ Q F A