Metamath Proof Explorer


Theorem cdleme11g

Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme11 . (Contributed by NM, 14-Jun-2012)

Ref Expression
Hypotheses cdleme11.l ˙ = K
cdleme11.j ˙ = join K
cdleme11.m ˙ = meet K
cdleme11.a A = Atoms K
cdleme11.h H = LHyp K
cdleme11.u U = P ˙ Q ˙ W
cdleme11.c C = P ˙ S ˙ W
cdleme11.d D = P ˙ T ˙ W
cdleme11.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
Assertion cdleme11g K HL W H P A Q A ¬ Q ˙ W S A P Q Q ˙ F = Q ˙ C

Proof

Step Hyp Ref Expression
1 cdleme11.l ˙ = K
2 cdleme11.j ˙ = join K
3 cdleme11.m ˙ = meet K
4 cdleme11.a A = Atoms K
5 cdleme11.h H = LHyp K
6 cdleme11.u U = P ˙ Q ˙ W
7 cdleme11.c C = P ˙ S ˙ W
8 cdleme11.d D = P ˙ T ˙ W
9 cdleme11.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
10 9 oveq2i Q ˙ F = Q ˙ S ˙ U ˙ Q ˙ P ˙ S ˙ W
11 simp1l K HL W H P A Q A ¬ Q ˙ W S A P Q K HL
12 simp22l K HL W H P A Q A ¬ Q ˙ W S A P Q Q A
13 11 hllatd K HL W H P A Q A ¬ Q ˙ W S A P Q K Lat
14 simp23 K HL W H P A Q A ¬ Q ˙ W S A P Q S A
15 eqid Base K = Base K
16 15 4 atbase S A S Base K
17 14 16 syl K HL W H P A Q A ¬ Q ˙ W S A P Q S Base K
18 simp1 K HL W H P A Q A ¬ Q ˙ W S A P Q K HL W H
19 simp21 K HL W H P A Q A ¬ Q ˙ W S A P Q P A
20 1 2 3 4 5 6 15 cdleme0aa K HL W H P A Q A U Base K
21 18 19 12 20 syl3anc K HL W H P A Q A ¬ Q ˙ W S A P Q U Base K
22 15 2 latjcl K Lat S Base K U Base K S ˙ U Base K
23 13 17 21 22 syl3anc K HL W H P A Q A ¬ Q ˙ W S A P Q S ˙ U Base K
24 15 4 atbase Q A Q Base K
25 12 24 syl K HL W H P A Q A ¬ Q ˙ W S A P Q Q Base K
26 15 4 atbase P A P Base K
27 19 26 syl K HL W H P A Q A ¬ Q ˙ W S A P Q P Base K
28 15 2 latjcl K Lat P Base K S Base K P ˙ S Base K
29 13 27 17 28 syl3anc K HL W H P A Q A ¬ Q ˙ W S A P Q P ˙ S Base K
30 simp1r K HL W H P A Q A ¬ Q ˙ W S A P Q W H
31 15 5 lhpbase W H W Base K
32 30 31 syl K HL W H P A Q A ¬ Q ˙ W S A P Q W Base K
33 15 3 latmcl K Lat P ˙ S Base K W Base K P ˙ S ˙ W Base K
34 13 29 32 33 syl3anc K HL W H P A Q A ¬ Q ˙ W S A P Q P ˙ S ˙ W Base K
35 15 2 latjcl K Lat Q Base K P ˙ S ˙ W Base K Q ˙ P ˙ S ˙ W Base K
36 13 25 34 35 syl3anc K HL W H P A Q A ¬ Q ˙ W S A P Q Q ˙ P ˙ S ˙ W Base K
37 15 1 2 latlej1 K Lat Q Base K P ˙ S ˙ W Base K Q ˙ Q ˙ P ˙ S ˙ W
38 13 25 34 37 syl3anc K HL W H P A Q A ¬ Q ˙ W S A P Q Q ˙ Q ˙ P ˙ S ˙ W
39 15 1 2 3 4 atmod1i1 K HL Q A S ˙ U Base K Q ˙ P ˙ S ˙ W Base K Q ˙ Q ˙ P ˙ S ˙ W Q ˙ S ˙ U ˙ Q ˙ P ˙ S ˙ W = Q ˙ S ˙ U ˙ Q ˙ P ˙ S ˙ W
40 11 12 23 36 38 39 syl131anc K HL W H P A Q A ¬ Q ˙ W S A P Q Q ˙ S ˙ U ˙ Q ˙ P ˙ S ˙ W = Q ˙ S ˙ U ˙ Q ˙ P ˙ S ˙ W
41 10 40 syl5eq K HL W H P A Q A ¬ Q ˙ W S A P Q Q ˙ F = Q ˙ S ˙ U ˙ Q ˙ P ˙ S ˙ W
42 simp22 K HL W H P A Q A ¬ Q ˙ W S A P Q Q A ¬ Q ˙ W
43 1 2 3 4 5 6 cdleme0cq K HL W H P A Q A ¬ Q ˙ W Q ˙ U = P ˙ Q
44 18 19 42 43 syl12anc K HL W H P A Q A ¬ Q ˙ W S A P Q Q ˙ U = P ˙ Q
45 44 oveq2d K HL W H P A Q A ¬ Q ˙ W S A P Q S ˙ Q ˙ U = S ˙ P ˙ Q
46 15 2 latj12 K Lat Q Base K S Base K U Base K Q ˙ S ˙ U = S ˙ Q ˙ U
47 13 25 17 21 46 syl13anc K HL W H P A Q A ¬ Q ˙ W S A P Q Q ˙ S ˙ U = S ˙ Q ˙ U
48 15 2 latj13 K Lat Q Base K P Base K S Base K Q ˙ P ˙ S = S ˙ P ˙ Q
49 13 25 27 17 48 syl13anc K HL W H P A Q A ¬ Q ˙ W S A P Q Q ˙ P ˙ S = S ˙ P ˙ Q
50 45 47 49 3eqtr4d K HL W H P A Q A ¬ Q ˙ W S A P Q Q ˙ S ˙ U = Q ˙ P ˙ S
51 50 oveq1d K HL W H P A Q A ¬ Q ˙ W S A P Q Q ˙ S ˙ U ˙ Q ˙ P ˙ S ˙ W = Q ˙ P ˙ S ˙ Q ˙ P ˙ S ˙ W
52 15 1 3 latmle1 K Lat P ˙ S Base K W Base K P ˙ S ˙ W ˙ P ˙ S
53 13 29 32 52 syl3anc K HL W H P A Q A ¬ Q ˙ W S A P Q P ˙ S ˙ W ˙ P ˙ S
54 15 1 2 latjlej2 K Lat P ˙ S ˙ W Base K P ˙ S Base K Q Base K P ˙ S ˙ W ˙ P ˙ S Q ˙ P ˙ S ˙ W ˙ Q ˙ P ˙ S
55 13 34 29 25 54 syl13anc K HL W H P A Q A ¬ Q ˙ W S A P Q P ˙ S ˙ W ˙ P ˙ S Q ˙ P ˙ S ˙ W ˙ Q ˙ P ˙ S
56 53 55 mpd K HL W H P A Q A ¬ Q ˙ W S A P Q Q ˙ P ˙ S ˙ W ˙ Q ˙ P ˙ S
57 15 2 latjcl K Lat Q Base K P ˙ S Base K Q ˙ P ˙ S Base K
58 13 25 29 57 syl3anc K HL W H P A Q A ¬ Q ˙ W S A P Q Q ˙ P ˙ S Base K
59 15 1 3 latleeqm2 K Lat Q ˙ P ˙ S ˙ W Base K Q ˙ P ˙ S Base K Q ˙ P ˙ S ˙ W ˙ Q ˙ P ˙ S Q ˙ P ˙ S ˙ Q ˙ P ˙ S ˙ W = Q ˙ P ˙ S ˙ W
60 13 36 58 59 syl3anc K HL W H P A Q A ¬ Q ˙ W S A P Q Q ˙ P ˙ S ˙ W ˙ Q ˙ P ˙ S Q ˙ P ˙ S ˙ Q ˙ P ˙ S ˙ W = Q ˙ P ˙ S ˙ W
61 56 60 mpbid K HL W H P A Q A ¬ Q ˙ W S A P Q Q ˙ P ˙ S ˙ Q ˙ P ˙ S ˙ W = Q ˙ P ˙ S ˙ W
62 7 oveq2i Q ˙ C = Q ˙ P ˙ S ˙ W
63 61 62 eqtr4di K HL W H P A Q A ¬ Q ˙ W S A P Q Q ˙ P ˙ S ˙ Q ˙ P ˙ S ˙ W = Q ˙ C
64 41 51 63 3eqtrd K HL W H P A Q A ¬ Q ˙ W S A P Q Q ˙ F = Q ˙ C