Metamath Proof Explorer


Theorem cdleme7c

Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme7ga and cdleme7 . (Contributed by NM, 7-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 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

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 6 9 oveq12i U ˙ V = P ˙ Q ˙ W ˙ R ˙ S ˙ W
11 simp11 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 K HL W H
12 simp12l 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 P A
13 simp13 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 Q A
14 simp2l 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 R A ¬ R ˙ W
15 simp32 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 R ˙ P ˙ Q
16 1 2 3 4 5 6 cdleme4 K HL W H P A Q A R A ¬ R ˙ W R ˙ P ˙ Q P ˙ Q = R ˙ U
17 11 12 13 14 15 16 syl131anc 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 P ˙ Q = R ˙ U
18 17 oveq1d 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 P ˙ Q ˙ R ˙ S = R ˙ U ˙ R ˙ S
19 simp11l 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 K HL
20 simp12 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 P A ¬ P ˙ W
21 simp31 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 P Q
22 1 2 3 4 5 6 lhpat2 K HL W H P A ¬ P ˙ W Q A P Q U A
23 11 20 13 21 22 syl112anc 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 A
24 simp2rl 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 S A
25 simp2ll 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 R A
26 19 hllatd 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 K Lat
27 eqid Base K = Base K
28 27 2 4 hlatjcl K HL P A Q A P ˙ Q Base K
29 19 12 13 28 syl3anc 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 P ˙ Q Base K
30 simp11r 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 W H
31 27 5 lhpbase W H W Base K
32 30 31 syl 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 W Base K
33 27 1 3 latmle2 K Lat P ˙ Q Base K W Base K P ˙ Q ˙ W ˙ W
34 26 29 32 33 syl3anc 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 P ˙ Q ˙ W ˙ W
35 6 34 eqbrtrid 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 ˙ W
36 simp2rr 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 ¬ S ˙ W
37 nbrne2 U ˙ W ¬ S ˙ W U S
38 35 36 37 syl2anc 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 S
39 1 2 3 4 5 6 7 8 cdleme7aa 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 ¬ R ˙ U ˙ S
40 1 2 3 4 2llnma2 K HL U A S A R A U S ¬ R ˙ U ˙ S R ˙ U ˙ R ˙ S = R
41 19 23 24 25 38 39 40 syl132anc 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 R ˙ U ˙ R ˙ S = R
42 18 41 eqtrd 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 P ˙ Q ˙ R ˙ S = R
43 42 oveq1d 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 P ˙ Q ˙ R ˙ S ˙ W = R ˙ W
44 hlol K HL K OL
45 19 44 syl 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 K OL
46 27 2 4 hlatjcl K HL R A S A R ˙ S Base K
47 19 25 24 46 syl3anc 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 R ˙ S Base K
48 27 3 latmmdir K OL P ˙ Q Base K R ˙ S Base K W Base K P ˙ Q ˙ R ˙ S ˙ W = P ˙ Q ˙ W ˙ R ˙ S ˙ W
49 45 29 47 32 48 syl13anc 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 P ˙ Q ˙ R ˙ S ˙ W = P ˙ Q ˙ W ˙ R ˙ S ˙ W
50 eqid 0. K = 0. K
51 1 3 50 4 5 lhpmat K HL W H R A ¬ R ˙ W R ˙ W = 0. K
52 11 14 51 syl2anc 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 R ˙ W = 0. K
53 43 49 52 3eqtr3d 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 P ˙ Q ˙ W ˙ R ˙ S ˙ W = 0. K
54 10 53 syl5eq 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 = 0. K
55 hlatl K HL K AtLat
56 19 55 syl 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 K AtLat
57 simp33 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 ¬ S ˙ P ˙ Q
58 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
59 11 14 24 57 15 58 syl113anc 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 V A
60 3 50 4 atnem0 K AtLat U A V A U V U ˙ V = 0. K
61 56 23 59 60 syl3anc 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 U ˙ V = 0. K
62 54 61 mpbird 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