Metamath Proof Explorer


Theorem cdleme7d

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

Ref Expression
Hypotheses cdleme4.l ˙ = K
cdleme4.j ˙ = join K
cdleme4.m ˙ = meet K
cdleme4.a A = Atoms K
cdleme4.h H = LHyp K
cdleme4.u U = P ˙ Q ˙ W
cdleme4.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
cdleme4.g G = P ˙ Q ˙ F ˙ R ˙ S ˙ W
cdleme7.v V = R ˙ S ˙ W
Assertion cdleme7d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q G U

Proof

Step Hyp Ref Expression
1 cdleme4.l ˙ = K
2 cdleme4.j ˙ = join K
3 cdleme4.m ˙ = meet K
4 cdleme4.a A = Atoms K
5 cdleme4.h H = LHyp K
6 cdleme4.u U = P ˙ Q ˙ W
7 cdleme4.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
8 cdleme4.g G = P ˙ Q ˙ F ˙ R ˙ S ˙ W
9 cdleme7.v V = R ˙ S ˙ W
10 1 2 3 4 5 6 7 8 9 cdleme7a G = P ˙ Q ˙ F ˙ V
11 simp11l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q K HL
12 11 hllatd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q K Lat
13 simp12l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q P A
14 simp13l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q Q A
15 eqid Base K = Base K
16 15 2 4 hlatjcl K HL P A Q A P ˙ Q Base K
17 11 13 14 16 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q P ˙ Q Base K
18 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q K HL W H
19 simp12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q P A ¬ P ˙ W
20 simp13 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q Q A ¬ Q ˙ W
21 simp2r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q S A ¬ S ˙ W
22 simp31 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q P Q
23 simp33 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q ¬ S ˙ P ˙ Q
24 1 2 3 4 5 6 7 cdleme3fa K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q F A
25 18 19 20 21 22 23 24 syl132anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q F A
26 simp2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q R A ¬ R ˙ W
27 simp2rl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q S A
28 simp32 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ P ˙ Q
29 1 2 3 4 5 6 7 8 9 cdleme7b K HL W H R A ¬ R ˙ W S A ¬ S ˙ P ˙ Q R ˙ P ˙ Q V A
30 18 26 27 23 28 29 syl113anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q V A
31 15 2 4 hlatjcl K HL F A V A F ˙ V Base K
32 11 25 30 31 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q F ˙ V Base K
33 15 1 3 latmle2 K Lat P ˙ Q Base K F ˙ V Base K P ˙ Q ˙ F ˙ V ˙ F ˙ V
34 12 17 32 33 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q P ˙ Q ˙ F ˙ V ˙ F ˙ V
35 10 34 eqbrtrid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q G ˙ F ˙ V
36 1 2 3 4 5 6 7 cdleme3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q ¬ S ˙ P ˙ Q ¬ F ˙ W
37 18 19 20 21 22 23 36 syl132anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q ¬ F ˙ W
38 1 2 3 4 5 6 lhpat2 K HL W H P A ¬ P ˙ W Q A P Q U A
39 18 19 14 22 38 syl112anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q U A
40 simp2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q R A ¬ R ˙ W S A ¬ S ˙ W
41 simp3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q
42 1 2 3 4 5 6 7 8 9 cdleme7c K HL W H P A ¬ P ˙ W Q A R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q U V
43 18 19 14 40 41 42 syl311anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q U V
44 1 2 4 hlatexch2 K HL U A F A V A U V U ˙ F ˙ V F ˙ U ˙ V
45 11 39 25 30 43 44 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q U ˙ F ˙ V F ˙ U ˙ V
46 simp11r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q W H
47 15 5 lhpbase W H W Base K
48 46 47 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q W Base K
49 15 1 3 latmle2 K Lat P ˙ Q Base K W Base K P ˙ Q ˙ W ˙ W
50 12 17 48 49 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q P ˙ Q ˙ W ˙ W
51 6 50 eqbrtrid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q U ˙ W
52 simp2ll K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q R A
53 15 2 4 hlatjcl K HL R A S A R ˙ S Base K
54 11 52 27 53 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S Base K
55 15 1 3 latmle2 K Lat R ˙ S Base K W Base K R ˙ S ˙ W ˙ W
56 12 54 48 55 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ W ˙ W
57 9 56 eqbrtrid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q V ˙ W
58 15 4 atbase U A U Base K
59 39 58 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q U Base K
60 15 4 atbase V A V Base K
61 30 60 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q V Base K
62 15 1 2 latjle12 K Lat U Base K V Base K W Base K U ˙ W V ˙ W U ˙ V ˙ W
63 12 59 61 48 62 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q U ˙ W V ˙ W U ˙ V ˙ W
64 51 57 63 mpbi2and K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q U ˙ V ˙ W
65 15 4 atbase F A F Base K
66 25 65 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q F Base K
67 15 2 4 hlatjcl K HL U A V A U ˙ V Base K
68 11 39 30 67 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q U ˙ V Base K
69 15 1 lattr K Lat F Base K U ˙ V Base K W Base K F ˙ U ˙ V U ˙ V ˙ W F ˙ W
70 12 66 68 48 69 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q F ˙ U ˙ V U ˙ V ˙ W F ˙ W
71 64 70 mpan2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q F ˙ U ˙ V F ˙ W
72 45 71 syld K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q U ˙ F ˙ V F ˙ W
73 37 72 mtod K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q ¬ U ˙ F ˙ V
74 nbrne2 G ˙ F ˙ V ¬ U ˙ F ˙ V G U
75 35 73 74 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W P Q R ˙ P ˙ Q ¬ S ˙ P ˙ Q G U