Metamath Proof Explorer


Theorem cdlemefs45eN

Description: Explicit expansion of cdlemefs45 . TODO: use to shorten cdlemefs45 uses? TODO: FIX COMMENT. (Contributed by NM, 10-Apr-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemef45.b B = Base K
cdlemef45.l ˙ = K
cdlemef45.j ˙ = join K
cdlemef45.m ˙ = meet K
cdlemef45.a A = Atoms K
cdlemef45.h H = LHyp K
cdlemef45.u U = P ˙ Q ˙ W
cdlemef45.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdlemef45.f F = x B if P Q ¬ x ˙ W ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W x
cdlemefs45.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
Assertion cdlemefs45eN K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R ˙ P ˙ Q ¬ S ˙ P ˙ Q F R = P ˙ Q ˙ F S ˙ R ˙ S ˙ W

Proof

Step Hyp Ref Expression
1 cdlemef45.b B = Base K
2 cdlemef45.l ˙ = K
3 cdlemef45.j ˙ = join K
4 cdlemef45.m ˙ = meet K
5 cdlemef45.a A = Atoms K
6 cdlemef45.h H = LHyp K
7 cdlemef45.u U = P ˙ Q ˙ W
8 cdlemef45.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
9 cdlemef45.f F = x B if P Q ¬ x ˙ W ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W x
10 cdlemefs45.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
11 1 2 3 4 5 6 7 8 9 10 cdlemefs45ee K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R ˙ P ˙ Q ¬ S ˙ P ˙ Q F R = P ˙ Q ˙ S ˙ U ˙ Q ˙ P ˙ S ˙ W ˙ R ˙ S ˙ W
12 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R ˙ P ˙ Q ¬ S ˙ P ˙ Q K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
13 simp21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R ˙ P ˙ Q ¬ S ˙ P ˙ Q P Q
14 simp23 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R ˙ P ˙ Q ¬ S ˙ P ˙ Q S A ¬ S ˙ W
15 simp3r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R ˙ P ˙ Q ¬ S ˙ P ˙ Q ¬ S ˙ P ˙ Q
16 1 2 3 4 5 6 7 8 9 cdlemefr45e K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q F S = S ˙ U ˙ Q ˙ P ˙ S ˙ W
17 12 13 14 15 16 syl121anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R ˙ P ˙ Q ¬ S ˙ P ˙ Q F S = S ˙ U ˙ Q ˙ P ˙ S ˙ W
18 17 oveq1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R ˙ P ˙ Q ¬ S ˙ P ˙ Q F S ˙ R ˙ S ˙ W = S ˙ U ˙ Q ˙ P ˙ S ˙ W ˙ R ˙ S ˙ W
19 18 oveq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R ˙ P ˙ Q ¬ S ˙ P ˙ Q P ˙ Q ˙ F S ˙ R ˙ S ˙ W = P ˙ Q ˙ S ˙ U ˙ Q ˙ P ˙ S ˙ W ˙ R ˙ S ˙ W
20 11 19 eqtr4d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R ˙ P ˙ Q ¬ S ˙ P ˙ Q F R = P ˙ Q ˙ F S ˙ R ˙ S ˙ W