Metamath Proof Explorer


Theorem cdleme01N

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 5-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 cdleme01N K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q U P U Q U ˙ P ˙ Q 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 simp1l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q K HL
8 7 hllatd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q K Lat
9 simp2ll K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q P A
10 simp2rl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q Q A
11 eqid Base K = Base K
12 11 2 4 hlatjcl K HL P A Q A P ˙ Q Base K
13 7 9 10 12 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q P ˙ Q Base K
14 simp1r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q W H
15 11 5 lhpbase W H W Base K
16 14 15 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q W Base K
17 11 1 3 latmle2 K Lat P ˙ Q Base K W Base K P ˙ Q ˙ W ˙ W
18 8 13 16 17 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q P ˙ Q ˙ W ˙ W
19 6 18 eqbrtrid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q U ˙ W
20 simp2lr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ P ˙ W
21 nbrne2 U ˙ W ¬ P ˙ W U P
22 19 20 21 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q U P
23 simp2rr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ Q ˙ W
24 nbrne2 U ˙ W ¬ Q ˙ W U Q
25 19 23 24 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q U Q
26 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q K HL W H
27 1 2 3 4 5 6 cdlemeulpq K HL W H P A Q A U ˙ P ˙ Q
28 26 9 10 27 syl12anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q U ˙ P ˙ Q
29 22 25 28 3jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q U P U Q U ˙ P ˙ Q
30 29 19 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q U P U Q U ˙ P ˙ Q U ˙ W