Metamath Proof Explorer


Theorem cdleme0c

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 12-Jun-2012)

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

Proof

Step Hyp Ref Expression
1 cdleme0.l ˙ = K
2 cdleme0.j ˙ = join K
3 cdleme0.m ˙ = meet K
4 cdleme0.a A = Atoms K
5 cdleme0.h H = LHyp K
6 cdleme0.u U = P ˙ Q ˙ W
7 simp1l K HL W H P A Q A R A ¬ R ˙ W K HL
8 7 hllatd K HL W H P A Q A R A ¬ R ˙ W K Lat
9 simp2l K HL W H P A Q A R A ¬ R ˙ W P A
10 eqid Base K = Base K
11 10 4 atbase P A P Base K
12 9 11 syl K HL W H P A Q A R A ¬ R ˙ W P Base K
13 simp2r K HL W H P A Q A R A ¬ R ˙ W Q A
14 10 4 atbase Q A Q Base K
15 13 14 syl K HL W H P A Q A R A ¬ R ˙ W Q Base K
16 10 2 latjcl K Lat P Base K Q Base K P ˙ Q Base K
17 8 12 15 16 syl3anc K HL W H P A Q A R A ¬ R ˙ W P ˙ Q Base K
18 simp1r K HL W H P A Q A R A ¬ R ˙ W W H
19 10 5 lhpbase W H W Base K
20 18 19 syl K HL W H P A Q A R A ¬ R ˙ W W Base K
21 10 1 3 latmle2 K Lat P ˙ Q Base K W Base K P ˙ Q ˙ W ˙ W
22 8 17 20 21 syl3anc K HL W H P A Q A R A ¬ R ˙ W P ˙ Q ˙ W ˙ W
23 6 22 eqbrtrid K HL W H P A Q A R A ¬ R ˙ W U ˙ W
24 simp3r K HL W H P A Q A R A ¬ R ˙ W ¬ R ˙ W
25 nbrne2 U ˙ W ¬ R ˙ W U R
26 23 24 25 syl2anc K HL W H P A Q A R A ¬ R ˙ W U R