Metamath Proof Explorer


Theorem cdlemefr44

Description: Value of f(r) when r is an atom not under pq, using more compact hypotheses. TODO: eliminate and use cdlemefr45 instead? TODO: FIX COMMENT. (Contributed by NM, 31-Mar-2013)

Ref Expression
Hypotheses cdlemef44.b B = Base K
cdlemef44.l ˙ = K
cdlemef44.j ˙ = join K
cdlemef44.m ˙ = meet K
cdlemef44.a A = Atoms K
cdlemef44.h H = LHyp K
cdlemef44.u U = P ˙ Q ˙ W
cdlemef44.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdlemef44.o O = ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q I s / t D ˙ x ˙ W
cdlemef44.f F = x B if P Q ¬ x ˙ W O x
Assertion cdlemefr44 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q F R = R / t D

Proof

Step Hyp Ref Expression
1 cdlemef44.b B = Base K
2 cdlemef44.l ˙ = K
3 cdlemef44.j ˙ = join K
4 cdlemef44.m ˙ = meet K
5 cdlemef44.a A = Atoms K
6 cdlemef44.h H = LHyp K
7 cdlemef44.u U = P ˙ Q ˙ W
8 cdlemef44.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
9 cdlemef44.o O = ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q I s / t D ˙ x ˙ W
10 cdlemef44.f F = x B if P Q ¬ x ˙ W O x
11 eqid s ˙ U ˙ Q ˙ P ˙ s ˙ W = s ˙ U ˙ Q ˙ P ˙ s ˙ W
12 biid s ˙ P ˙ Q s ˙ P ˙ Q
13 vex s V
14 8 11 cdleme31sc s V s / t D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
15 13 14 ax-mp s / t D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
16 12 15 ifbieq2i if s ˙ P ˙ Q I s / t D = if s ˙ P ˙ Q I s ˙ U ˙ Q ˙ P ˙ s ˙ W
17 eqid R ˙ U ˙ Q ˙ P ˙ R ˙ W = R ˙ U ˙ Q ˙ P ˙ R ˙ W
18 1 2 3 4 5 6 7 11 16 9 10 17 cdlemefr31fv1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q F R = R ˙ U ˙ Q ˙ P ˙ R ˙ W
19 simp2rl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q R A
20 8 17 cdleme31sc R A R / t D = R ˙ U ˙ Q ˙ P ˙ R ˙ W
21 19 20 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q R / t D = R ˙ U ˙ Q ˙ P ˙ R ˙ W
22 18 21 eqtr4d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q F R = R / t D