Metamath Proof Explorer


Theorem cdleme7aa

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
Assertion 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

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 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
10 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
11 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
12 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
13 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
14 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
15 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
16 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
17 1 2 3 4 5 6 lhpat2 K HL W H P A ¬ P ˙ W Q A P Q U A
18 13 14 15 16 17 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
19 10 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
20 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
21 eqid Base K = Base K
22 21 2 4 hlatjcl K HL P A Q A P ˙ Q Base K
23 10 20 15 22 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
24 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
25 21 5 lhpbase W H W Base K
26 24 25 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
27 21 1 3 latmle2 K Lat P ˙ Q Base K W Base K P ˙ Q ˙ W ˙ W
28 19 23 26 27 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
29 6 28 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
30 simp2lr 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
31 nbrne2 U ˙ W ¬ R ˙ W U R
32 31 necomd U ˙ W ¬ R ˙ W R U
33 29 30 32 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 U
34 1 2 4 hlatexch1 K HL R A S A U A R U R ˙ U ˙ S S ˙ U ˙ R
35 10 11 12 18 33 34 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 R ˙ U ˙ S S ˙ U ˙ R
36 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
37 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
38 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
39 13 20 15 36 37 38 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
40 2 4 hlatjcom K HL R A U A R ˙ U = U ˙ R
41 10 11 18 40 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 ˙ U = U ˙ R
42 39 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 = U ˙ R
43 42 breq2d 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 S ˙ U ˙ R
44 35 43 sylibrd 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 S ˙ P ˙ Q
45 9 44 mtod 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