Metamath Proof Explorer


Theorem cdleme02N

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 9-Nov-2012) (New usage is discouraged.)

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 cdleme02N K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q P ˙ U = Q ˙ U U ˙ W

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 1 2 3 4 5 6 cdleme01N K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q U P U Q U ˙ P ˙ Q U ˙ W
8 simp1l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q K HL
9 hlcvl K HL K CvLat
10 8 9 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q K CvLat
11 simp2ll K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q P A
12 simp2rl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q Q A
13 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q K HL W H
14 simp2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q P A ¬ P ˙ W
15 simp3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q P Q
16 1 2 3 4 5 6 lhpat2 K HL W H P A ¬ P ˙ W Q A P Q U A
17 13 14 12 15 16 syl112anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q U A
18 4 1 2 cvlsupr2 K CvLat P A Q A U A P Q P ˙ U = Q ˙ U U P U Q U ˙ P ˙ Q
19 10 11 12 17 15 18 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q P ˙ U = Q ˙ U U P U Q U ˙ P ˙ Q
20 19 anbi1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q P ˙ U = Q ˙ U U ˙ W U P U Q U ˙ P ˙ Q U ˙ W
21 7 20 mpbird K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q P ˙ U = Q ˙ U U ˙ W