Metamath Proof Explorer


Theorem cdleme35sn3a

Description: Part of proof of Lemma E in Crawley p. 113. TODO: FIX COMMENT. (Contributed by NM, 19-Mar-2013)

Ref Expression
Hypotheses cdleme32s.b B = Base K
cdleme32s.l ˙ = K
cdleme32s.j ˙ = join K
cdleme32s.m ˙ = meet K
cdleme32s.a A = Atoms K
cdleme32s.h H = LHyp K
cdleme32s.u U = P ˙ Q ˙ W
cdleme32s.d D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
cdleme32s.n N = if s ˙ P ˙ Q I D
Assertion cdleme35sn3a K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q ¬ R / s N ˙ P ˙ Q

Proof

Step Hyp Ref Expression
1 cdleme32s.b B = Base K
2 cdleme32s.l ˙ = K
3 cdleme32s.j ˙ = join K
4 cdleme32s.m ˙ = meet K
5 cdleme32s.a A = Atoms K
6 cdleme32s.h H = LHyp K
7 cdleme32s.u U = P ˙ Q ˙ W
8 cdleme32s.d D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
9 cdleme32s.n N = if s ˙ P ˙ Q I D
10 eqid R ˙ U ˙ Q ˙ P ˙ R ˙ W = R ˙ U ˙ Q ˙ P ˙ R ˙ W
11 2 3 4 5 6 7 10 cdleme35fnpq K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q ¬ R ˙ U ˙ Q ˙ P ˙ R ˙ W ˙ P ˙ Q
12 simp2rl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q R A
13 simp3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q ¬ R ˙ P ˙ Q
14 8 9 10 cdleme31sn2 R A ¬ R ˙ P ˙ Q R / s N = R ˙ U ˙ Q ˙ P ˙ R ˙ W
15 12 13 14 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q R / s N = R ˙ U ˙ Q ˙ P ˙ R ˙ W
16 15 breq1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q R / s N ˙ P ˙ Q R ˙ U ˙ Q ˙ P ˙ R ˙ W ˙ P ˙ Q
17 11 16 mtbird K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q ¬ R / s N ˙ P ˙ Q