Metamath Proof Explorer


Theorem cdleme35d

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 cdleme35d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q Q ˙ F ˙ W = 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 1 2 3 4 5 6 7 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
9 8 oveq1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q Q ˙ F ˙ W = Q ˙ P ˙ R ˙ W ˙ W
10 simp11l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q K HL
11 simp13l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q Q A
12 10 hllatd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q K Lat
13 simp12l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q P A
14 simp2rl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q R A
15 eqid Base K = Base K
16 15 2 4 hlatjcl K HL P A R A P ˙ R Base K
17 10 13 14 16 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
18 simp11r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q W H
19 15 5 lhpbase W H W Base K
20 18 19 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
21 15 3 latmcl K Lat P ˙ R Base K W Base K P ˙ R ˙ W Base K
22 12 17 20 21 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
23 15 1 3 latmle2 K Lat P ˙ R Base K W Base K P ˙ R ˙ W ˙ W
24 12 17 20 23 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 ˙ W
25 15 1 2 3 4 atmod4i2 K HL Q A P ˙ R ˙ W Base K W Base K P ˙ R ˙ W ˙ W Q ˙ W ˙ P ˙ R ˙ W = Q ˙ P ˙ R ˙ W ˙ W
26 10 11 22 20 24 25 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q Q ˙ W ˙ P ˙ R ˙ W = Q ˙ P ˙ R ˙ W ˙ W
27 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
28 simp13 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q Q A ¬ Q ˙ W
29 eqid 0. K = 0. K
30 1 3 29 4 5 lhpmat K HL W H Q A ¬ Q ˙ W Q ˙ W = 0. K
31 27 28 30 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q Q ˙ W = 0. K
32 31 oveq1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q Q ˙ W ˙ P ˙ R ˙ W = 0. K ˙ P ˙ R ˙ W
33 hlol K HL K OL
34 10 33 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q K OL
35 15 2 29 olj02 K OL P ˙ R ˙ W Base K 0. K ˙ P ˙ R ˙ W = P ˙ R ˙ W
36 34 22 35 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q 0. K ˙ P ˙ R ˙ W = P ˙ R ˙ W
37 32 36 eqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q Q ˙ W ˙ P ˙ R ˙ W = P ˙ R ˙ W
38 9 26 37 3eqtr2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q Q ˙ F ˙ W = P ˙ R ˙ W