Metamath Proof Explorer


Theorem cdlemeda

Description: Part of proof of Lemma E in Crawley p. 113. Utility lemma. D represents s_2. (Contributed by NM, 13-Nov-2012)

Ref Expression
Hypotheses cdlemeda.l ˙ = K
cdlemeda.j ˙ = join K
cdlemeda.m ˙ = meet K
cdlemeda.a A = Atoms K
cdlemeda.h H = LHyp K
cdlemeda.d D = R ˙ S ˙ W
Assertion cdlemeda K HL W H S A ¬ S ˙ W R A R ˙ P ˙ Q ¬ S ˙ P ˙ Q D A

Proof

Step Hyp Ref Expression
1 cdlemeda.l ˙ = K
2 cdlemeda.j ˙ = join K
3 cdlemeda.m ˙ = meet K
4 cdlemeda.a A = Atoms K
5 cdlemeda.h H = LHyp K
6 cdlemeda.d D = R ˙ S ˙ W
7 simp1l K HL W H S A ¬ S ˙ W R A R ˙ P ˙ Q ¬ S ˙ P ˙ Q K HL
8 simp31 K HL W H S A ¬ S ˙ W R A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R A
9 simp2l K HL W H S A ¬ S ˙ W R A R ˙ P ˙ Q ¬ S ˙ P ˙ Q S A
10 2 4 hlatjcom K HL R A S A R ˙ S = S ˙ R
11 7 8 9 10 syl3anc K HL W H S A ¬ S ˙ W R A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S = S ˙ R
12 11 oveq1d K HL W H S A ¬ S ˙ W R A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ W = S ˙ R ˙ W
13 simp1r K HL W H S A ¬ S ˙ W R A R ˙ P ˙ Q ¬ S ˙ P ˙ Q W H
14 simp2r K HL W H S A ¬ S ˙ W R A R ˙ P ˙ Q ¬ S ˙ P ˙ Q ¬ S ˙ W
15 simp32 K HL W H S A ¬ S ˙ W R A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ P ˙ Q
16 simp33 K HL W H S A ¬ S ˙ W R A R ˙ P ˙ Q ¬ S ˙ P ˙ Q ¬ S ˙ P ˙ Q
17 1 2 4 5 cdlemesner K HL R A S A R ˙ P ˙ Q ¬ S ˙ P ˙ Q S R
18 7 8 9 15 16 17 syl122anc K HL W H S A ¬ S ˙ W R A R ˙ P ˙ Q ¬ S ˙ P ˙ Q S R
19 1 2 3 4 5 lhpat K HL W H S A ¬ S ˙ W R A S R S ˙ R ˙ W A
20 7 13 9 14 8 18 19 syl222anc K HL W H S A ¬ S ˙ W R A R ˙ P ˙ Q ¬ S ˙ P ˙ Q S ˙ R ˙ W A
21 12 20 eqeltrd K HL W H S A ¬ S ˙ W R A R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ S ˙ W A
22 6 21 eqeltrid K HL W H S A ¬ S ˙ W R A R ˙ P ˙ Q ¬ S ˙ P ˙ Q D A