Metamath Proof Explorer


Theorem cdleme35c

Description: Part of proof of Lemma E in Crawley p. 113. TODO: FIX COMMENT. (Contributed by NM, 10-Mar-2013)

Ref Expression
Hypotheses cdleme35.l ˙ = K
cdleme35.j ˙ = join K
cdleme35.m ˙ = meet K
cdleme35.a A = Atoms K
cdleme35.h H = LHyp K
cdleme35.u U = P ˙ Q ˙ W
cdleme35.f F = R ˙ U ˙ Q ˙ P ˙ R ˙ W
Assertion cdleme35c K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q Q ˙ F = Q ˙ P ˙ R ˙ W

Proof

Step Hyp Ref Expression
1 cdleme35.l ˙ = K
2 cdleme35.j ˙ = join K
3 cdleme35.m ˙ = meet K
4 cdleme35.a A = Atoms K
5 cdleme35.h H = LHyp K
6 cdleme35.u U = P ˙ Q ˙ W
7 cdleme35.f F = R ˙ U ˙ Q ˙ P ˙ R ˙ W
8 7 oveq2i Q ˙ F = Q ˙ R ˙ U ˙ Q ˙ P ˙ R ˙ W
9 simp11l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q K HL
10 simp13l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q Q A
11 simp2rl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q R A
12 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q K HL W H
13 simp12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q P A ¬ P ˙ W
14 simp2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q P Q
15 1 2 3 4 5 6 cdleme0a K HL W H P A ¬ P ˙ W Q A P Q U A
16 12 13 10 14 15 syl112anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q U A
17 eqid Base K = Base K
18 17 2 4 hlatjcl K HL R A U A R ˙ U Base K
19 9 11 16 18 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q R ˙ U Base K
20 9 hllatd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q K Lat
21 17 4 atbase Q A Q Base K
22 10 21 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q Q Base K
23 simp12l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q P A
24 17 2 4 hlatjcl K HL P A R A P ˙ R Base K
25 9 23 11 24 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q P ˙ R Base K
26 simp11r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q W H
27 17 5 lhpbase W H W Base K
28 26 27 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q W Base K
29 17 3 latmcl K Lat P ˙ R Base K W Base K P ˙ R ˙ W Base K
30 20 25 28 29 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q P ˙ R ˙ W Base K
31 17 2 latjcl K Lat Q Base K P ˙ R ˙ W Base K Q ˙ P ˙ R ˙ W Base K
32 20 22 30 31 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q Q ˙ P ˙ R ˙ W Base K
33 17 1 2 latlej1 K Lat Q Base K P ˙ R ˙ W Base K Q ˙ Q ˙ P ˙ R ˙ W
34 20 22 30 33 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q Q ˙ Q ˙ P ˙ R ˙ W
35 17 1 2 3 4 atmod1i1 K HL Q A R ˙ U Base K Q ˙ P ˙ R ˙ W Base K Q ˙ Q ˙ P ˙ R ˙ W Q ˙ R ˙ U ˙ Q ˙ P ˙ R ˙ W = Q ˙ R ˙ U ˙ Q ˙ P ˙ R ˙ W
36 9 10 19 32 34 35 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q Q ˙ R ˙ U ˙ Q ˙ P ˙ R ˙ W = Q ˙ R ˙ U ˙ Q ˙ P ˙ R ˙ W
37 1 2 3 4 5 6 7 cdleme35b K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q Q ˙ P ˙ R ˙ W ˙ Q ˙ R ˙ U
38 17 2 latjcl K Lat Q Base K R ˙ U Base K Q ˙ R ˙ U Base K
39 20 22 19 38 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q Q ˙ R ˙ U Base K
40 17 1 3 latleeqm2 K Lat Q ˙ P ˙ R ˙ W Base K Q ˙ R ˙ U Base K Q ˙ P ˙ R ˙ W ˙ Q ˙ R ˙ U Q ˙ R ˙ U ˙ Q ˙ P ˙ R ˙ W = Q ˙ P ˙ R ˙ W
41 20 32 39 40 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q Q ˙ P ˙ R ˙ W ˙ Q ˙ R ˙ U Q ˙ R ˙ U ˙ Q ˙ P ˙ R ˙ W = Q ˙ P ˙ R ˙ W
42 37 41 mpbid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q Q ˙ R ˙ U ˙ Q ˙ P ˙ R ˙ W = Q ˙ P ˙ R ˙ W
43 36 42 eqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q Q ˙ R ˙ U ˙ Q ˙ P ˙ R ˙ W = Q ˙ P ˙ R ˙ W
44 8 43 syl5eq K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q Q ˙ F = Q ˙ P ˙ R ˙ W