Metamath Proof Explorer


Theorem cdleme11k

Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme11 . (Contributed by NM, 15-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 cdleme11k K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q C = Q ˙ F ˙ W

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 1 2 3 4 5 6 7 6 9 cdleme11j K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q C ˙ Q ˙ F
11 simp1l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q K HL
12 11 hllatd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q K Lat
13 simp21l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q P A
14 eqid Base K = Base K
15 14 4 atbase P A P Base K
16 13 15 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q P Base K
17 simp23l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q S A
18 14 4 atbase S A S Base K
19 17 18 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q S Base K
20 14 2 latjcl K Lat P Base K S Base K P ˙ S Base K
21 12 16 19 20 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q P ˙ S Base K
22 simp1r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q W H
23 14 5 lhpbase W H W Base K
24 22 23 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q W Base K
25 14 1 3 latmle2 K Lat P ˙ S Base K W Base K P ˙ S ˙ W ˙ W
26 12 21 24 25 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q P ˙ S ˙ W ˙ W
27 7 26 eqbrtrid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q C ˙ W
28 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q K HL W H
29 simp21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q P A ¬ P ˙ W
30 simp22l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q Q A
31 simp3r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ S ˙ P ˙ Q
32 1 2 3 4 cdleme00a K HL P A Q A S A ¬ S ˙ P ˙ Q S P
33 11 13 30 17 31 32 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q S P
34 33 necomd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q P S
35 1 2 3 4 5 7 cdleme9a K HL W H P A ¬ P ˙ W S A P S C A
36 28 29 17 34 35 syl112anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q C A
37 14 4 atbase C A C Base K
38 36 37 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q C Base K
39 14 4 atbase Q A Q Base K
40 30 39 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q Q Base K
41 1 2 3 4 5 6 9 cdleme3fa K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q F A
42 14 4 atbase F A F Base K
43 41 42 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q F Base K
44 14 2 latjcl K Lat Q Base K F Base K Q ˙ F Base K
45 12 40 43 44 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q Q ˙ F Base K
46 14 1 3 latlem12 K Lat C Base K Q ˙ F Base K W Base K C ˙ Q ˙ F C ˙ W C ˙ Q ˙ F ˙ W
47 12 38 45 24 46 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q C ˙ Q ˙ F C ˙ W C ˙ Q ˙ F ˙ W
48 10 27 47 mpbi2and K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q C ˙ Q ˙ F ˙ W
49 hlatl K HL K AtLat
50 11 49 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q K AtLat
51 simp22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q Q A ¬ Q ˙ W
52 simp3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q P Q ¬ S ˙ P ˙ Q
53 1 2 3 4 5 6 7 6 9 cdleme11h K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A P Q ¬ S ˙ P ˙ Q F Q
54 28 29 51 17 52 53 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q F Q
55 54 necomd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q Q F
56 1 2 3 4 5 lhpat K HL W H Q A ¬ Q ˙ W F A Q F Q ˙ F ˙ W A
57 28 51 41 55 56 syl112anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q Q ˙ F ˙ W A
58 1 4 atcmp K AtLat C A Q ˙ F ˙ W A C ˙ Q ˙ F ˙ W C = Q ˙ F ˙ W
59 50 36 57 58 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q C ˙ Q ˙ F ˙ W C = Q ˙ F ˙ W
60 48 59 mpbid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q C = Q ˙ F ˙ W