Metamath Proof Explorer


Theorem cdlemc5

Description: Lemma for cdlemc . (Contributed by NM, 26-May-2012)

Ref Expression
Hypotheses cdlemc3.l ˙ = K
cdlemc3.j ˙ = join K
cdlemc3.m ˙ = meet K
cdlemc3.a A = Atoms K
cdlemc3.h H = LHyp K
cdlemc3.t T = LTrn K W
cdlemc3.r R = trL K W
Assertion cdlemc5 K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P F Q = Q ˙ R F ˙ F P ˙ P ˙ Q ˙ W

Proof

Step Hyp Ref Expression
1 cdlemc3.l ˙ = K
2 cdlemc3.j ˙ = join K
3 cdlemc3.m ˙ = meet K
4 cdlemc3.a A = Atoms K
5 cdlemc3.h H = LHyp K
6 cdlemc3.t T = LTrn K W
7 cdlemc3.r R = trL K W
8 simp1l K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P K HL
9 simp23l K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P Q A
10 simp1 K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P K HL W H
11 simp21 K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P F T
12 1 4 5 6 ltrnat K HL W H F T Q A F Q A
13 10 11 9 12 syl3anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P F Q A
14 1 2 4 hlatlej2 K HL Q A F Q A F Q ˙ Q ˙ F Q
15 8 9 13 14 syl3anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P F Q ˙ Q ˙ F Q
16 simp23 K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P Q A ¬ Q ˙ W
17 1 2 4 5 6 7 trljat1 K HL W H F T Q A ¬ Q ˙ W Q ˙ R F = Q ˙ F Q
18 10 11 16 17 syl3anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P Q ˙ R F = Q ˙ F Q
19 15 18 breqtrrd K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P F Q ˙ Q ˙ R F
20 simp22 K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P P A ¬ P ˙ W
21 1 2 3 4 5 6 cdlemc2 K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W F Q ˙ F P ˙ P ˙ Q ˙ W
22 10 11 20 16 21 syl112anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P F Q ˙ F P ˙ P ˙ Q ˙ W
23 8 hllatd K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P K Lat
24 eqid Base K = Base K
25 24 4 atbase Q A Q Base K
26 9 25 syl K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P Q Base K
27 24 5 6 ltrncl K HL W H F T Q Base K F Q Base K
28 10 11 26 27 syl3anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P F Q Base K
29 24 5 6 7 trlcl K HL W H F T R F Base K
30 10 11 29 syl2anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P R F Base K
31 24 2 latjcl K Lat Q Base K R F Base K Q ˙ R F Base K
32 23 26 30 31 syl3anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P Q ˙ R F Base K
33 simp22l K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P P A
34 24 4 atbase P A P Base K
35 33 34 syl K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P P Base K
36 24 5 6 ltrncl K HL W H F T P Base K F P Base K
37 10 11 35 36 syl3anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P F P Base K
38 24 2 4 hlatjcl K HL P A Q A P ˙ Q Base K
39 8 33 9 38 syl3anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P P ˙ Q Base K
40 simp1r K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P W H
41 24 5 lhpbase W H W Base K
42 40 41 syl K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P W Base K
43 24 3 latmcl K Lat P ˙ Q Base K W Base K P ˙ Q ˙ W Base K
44 23 39 42 43 syl3anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P P ˙ Q ˙ W Base K
45 24 2 latjcl K Lat F P Base K P ˙ Q ˙ W Base K F P ˙ P ˙ Q ˙ W Base K
46 23 37 44 45 syl3anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P F P ˙ P ˙ Q ˙ W Base K
47 24 1 3 latlem12 K Lat F Q Base K Q ˙ R F Base K F P ˙ P ˙ Q ˙ W Base K F Q ˙ Q ˙ R F F Q ˙ F P ˙ P ˙ Q ˙ W F Q ˙ Q ˙ R F ˙ F P ˙ P ˙ Q ˙ W
48 23 28 32 46 47 syl13anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P F Q ˙ Q ˙ R F F Q ˙ F P ˙ P ˙ Q ˙ W F Q ˙ Q ˙ R F ˙ F P ˙ P ˙ Q ˙ W
49 19 22 48 mpbi2and K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P F Q ˙ Q ˙ R F ˙ F P ˙ P ˙ Q ˙ W
50 hlatl K HL K AtLat
51 8 50 syl K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P K AtLat
52 simp3r K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P F P P
53 1 4 5 6 7 trlat K HL W H P A ¬ P ˙ W F T F P P R F A
54 10 20 11 52 53 syl112anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P R F A
55 1 5 6 7 trlle K HL W H F T R F ˙ W
56 10 11 55 syl2anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P R F ˙ W
57 simp23r K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P ¬ Q ˙ W
58 nbrne2 R F ˙ W ¬ Q ˙ W R F Q
59 58 necomd R F ˙ W ¬ Q ˙ W Q R F
60 56 57 59 syl2anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P Q R F
61 eqid LLines K = LLines K
62 2 4 61 llni2 K HL Q A R F A Q R F Q ˙ R F LLines K
63 8 9 54 60 62 syl31anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P Q ˙ R F LLines K
64 1 4 5 6 ltrnat K HL W H F T P A F P A
65 10 11 33 64 syl3anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P F P A
66 1 2 4 hlatlej1 K HL P A F P A P ˙ P ˙ F P
67 8 33 65 66 syl3anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P P ˙ P ˙ F P
68 simp3l K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P ¬ Q ˙ P ˙ F P
69 nbrne2 P ˙ P ˙ F P ¬ Q ˙ P ˙ F P P Q
70 67 68 69 syl2anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P P Q
71 1 2 3 4 5 lhpat K HL W H P A ¬ P ˙ W Q A P Q P ˙ Q ˙ W A
72 10 20 9 70 71 syl112anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P P ˙ Q ˙ W A
73 24 1 3 latmle2 K Lat P ˙ Q Base K W Base K P ˙ Q ˙ W ˙ W
74 23 39 42 73 syl3anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P P ˙ Q ˙ W ˙ W
75 1 4 5 6 ltrnel K HL W H F T P A ¬ P ˙ W F P A ¬ F P ˙ W
76 75 simprd K HL W H F T P A ¬ P ˙ W ¬ F P ˙ W
77 10 11 20 76 syl3anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P ¬ F P ˙ W
78 nbrne2 P ˙ Q ˙ W ˙ W ¬ F P ˙ W P ˙ Q ˙ W F P
79 78 necomd P ˙ Q ˙ W ˙ W ¬ F P ˙ W F P P ˙ Q ˙ W
80 74 77 79 syl2anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P F P P ˙ Q ˙ W
81 2 4 61 llni2 K HL F P A P ˙ Q ˙ W A F P P ˙ Q ˙ W F P ˙ P ˙ Q ˙ W LLines K
82 8 65 72 80 81 syl31anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P F P ˙ P ˙ Q ˙ W LLines K
83 1 2 3 4 5 6 7 cdlemc4 K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P Q ˙ R F F P ˙ P ˙ Q ˙ W
84 83 3adant3r K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P Q ˙ R F F P ˙ P ˙ Q ˙ W
85 24 3 latmcl K Lat Q ˙ R F Base K F P ˙ P ˙ Q ˙ W Base K Q ˙ R F ˙ F P ˙ P ˙ Q ˙ W Base K
86 23 32 46 85 syl3anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P Q ˙ R F ˙ F P ˙ P ˙ Q ˙ W Base K
87 eqid 0. K = 0. K
88 24 1 87 4 atlen0 K AtLat Q ˙ R F ˙ F P ˙ P ˙ Q ˙ W Base K F Q A F Q ˙ Q ˙ R F ˙ F P ˙ P ˙ Q ˙ W Q ˙ R F ˙ F P ˙ P ˙ Q ˙ W 0. K
89 51 86 13 49 88 syl31anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P Q ˙ R F ˙ F P ˙ P ˙ Q ˙ W 0. K
90 3 87 4 61 2llnmat K HL Q ˙ R F LLines K F P ˙ P ˙ Q ˙ W LLines K Q ˙ R F F P ˙ P ˙ Q ˙ W Q ˙ R F ˙ F P ˙ P ˙ Q ˙ W 0. K Q ˙ R F ˙ F P ˙ P ˙ Q ˙ W A
91 8 63 82 84 89 90 syl32anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P Q ˙ R F ˙ F P ˙ P ˙ Q ˙ W A
92 1 4 atcmp K AtLat F Q A Q ˙ R F ˙ F P ˙ P ˙ Q ˙ W A F Q ˙ Q ˙ R F ˙ F P ˙ P ˙ Q ˙ W F Q = Q ˙ R F ˙ F P ˙ P ˙ Q ˙ W
93 51 13 91 92 syl3anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P F Q ˙ Q ˙ R F ˙ F P ˙ P ˙ Q ˙ W F Q = Q ˙ R F ˙ F P ˙ P ˙ Q ˙ W
94 49 93 mpbid K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W ¬ Q ˙ P ˙ F P F P P F Q = Q ˙ R F ˙ F P ˙ P ˙ Q ˙ W