Metamath Proof Explorer


Theorem cdleme50trn2a

Description: Part of proof that F is a translation. R .<_ ( P .\/ Q ) case. TODO: fix comment. (Contributed by NM, 10-Apr-2013)

Ref Expression
Hypotheses cdlemef50.b B = Base K
cdlemef50.l ˙ = K
cdlemef50.j ˙ = join K
cdlemef50.m ˙ = meet K
cdlemef50.a A = Atoms K
cdlemef50.h H = LHyp K
cdlemef50.u U = P ˙ Q ˙ W
cdlemef50.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdlemefs50.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
cdlemef50.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
Assertion cdleme50trn2a 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 R ˙ F R ˙ W = U

Proof

Step Hyp Ref Expression
1 cdlemef50.b B = Base K
2 cdlemef50.l ˙ = K
3 cdlemef50.j ˙ = join K
4 cdlemef50.m ˙ = meet K
5 cdlemef50.a A = Atoms K
6 cdlemef50.h H = LHyp K
7 cdlemef50.u U = P ˙ Q ˙ W
8 cdlemef50.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
9 cdlemefs50.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
10 cdlemef50.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
11 1 2 3 4 5 6 7 8 10 9 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 11 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 R ˙ F R = R ˙ P ˙ Q ˙ S ˙ U ˙ Q ˙ P ˙ S ˙ W ˙ R ˙ S ˙ W
13 12 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 R ˙ F R ˙ W = R ˙ P ˙ Q ˙ S ˙ U ˙ Q ˙ P ˙ S ˙ W ˙ R ˙ S ˙ W ˙ W
14 simp11 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
15 simp12l 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 A
16 simp13l 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 Q A
17 simp22 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 R A ¬ R ˙ W
18 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
19 simp3l 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 R ˙ P ˙ Q
20 eqid S ˙ U ˙ Q ˙ P ˙ S ˙ W = S ˙ U ˙ Q ˙ P ˙ S ˙ W
21 eqid P ˙ Q ˙ S ˙ U ˙ Q ˙ P ˙ S ˙ W ˙ R ˙ S ˙ W = P ˙ Q ˙ S ˙ U ˙ Q ˙ P ˙ S ˙ W ˙ R ˙ S ˙ W
22 2 3 4 5 6 7 20 21 cdleme5 K HL W H P A Q A R A ¬ R ˙ W S A ¬ S ˙ W R ˙ P ˙ Q R ˙ P ˙ Q ˙ S ˙ U ˙ Q ˙ P ˙ S ˙ W ˙ R ˙ S ˙ W = P ˙ Q
23 14 15 16 17 18 19 22 syl132anc 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 R ˙ P ˙ Q ˙ S ˙ U ˙ Q ˙ P ˙ S ˙ W ˙ R ˙ S ˙ W = P ˙ Q
24 23 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 R ˙ P ˙ Q ˙ S ˙ U ˙ Q ˙ P ˙ S ˙ W ˙ R ˙ S ˙ W ˙ W = P ˙ Q ˙ W
25 24 7 eqtr4di 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 R ˙ P ˙ Q ˙ S ˙ U ˙ Q ˙ P ˙ S ˙ W ˙ R ˙ S ˙ W ˙ W = U
26 13 25 eqtrd 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 R ˙ F R ˙ W = U