Metamath Proof Explorer


Theorem cdlemefr29bpre0N

Description: TODO fix comment. (Contributed by NM, 28-Mar-2013) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cdlemefr27.b B = Base K
2 cdlemefr27.l ˙ = K
3 cdlemefr27.j ˙ = join K
4 cdlemefr27.m ˙ = meet K
5 cdlemefr27.a A = Atoms K
6 cdlemefr27.h H = LHyp K
7 cdlemefr27.u U = P ˙ Q ˙ W
8 cdlemefr27.c C = s ˙ U ˙ Q ˙ P ˙ s ˙ W
9 cdlemefr27.n N = if s ˙ P ˙ Q I C
10 breq1 s = R s ˙ P ˙ Q R ˙ P ˙ Q
11 10 notbid s = R ¬ s ˙ P ˙ Q ¬ R ˙ P ˙ Q
12 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q K HL W H
13 simp12l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q P A
14 simp13l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q Q A
15 simp3l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q s A
16 simp3rr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q ¬ s ˙ P ˙ Q
17 simp2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q P Q
18 1 2 3 4 5 6 7 8 9 cdlemefr27cl K HL W H P A Q A s A ¬ s ˙ P ˙ Q P Q N B
19 12 13 14 15 16 17 18 syl33anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q N B
20 1 2 3 4 5 6 11 19 cdlemefrs29bpre0 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q s ˙ R ˙ W = R z = N ˙ R ˙ W z = R / s N