Metamath Proof Explorer


Theorem cdleme50trn2

Description: Part of proof that F is a translation. Remove S hypotheses no longer needed from cdleme50trn2a . 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 cdleme50trn2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ 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 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q K HL W H
12 simp12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q P A ¬ P ˙ W
13 simp13 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q Q A ¬ Q ˙ W
14 simp2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q P Q
15 2 3 5 6 cdlemb2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q e A ¬ e ˙ W ¬ e ˙ P ˙ Q
16 11 12 13 14 15 syl121anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q e A ¬ e ˙ W ¬ e ˙ P ˙ Q
17 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q e A ¬ e ˙ W ¬ e ˙ P ˙ Q K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
18 simp2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q e A ¬ e ˙ W ¬ e ˙ P ˙ Q P Q
19 simp2r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q e A ¬ e ˙ W ¬ e ˙ P ˙ Q R A ¬ R ˙ W
20 simp3rl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q e A ¬ e ˙ W ¬ e ˙ P ˙ Q e A
21 simprrl R ˙ P ˙ Q e A ¬ e ˙ W ¬ e ˙ P ˙ Q ¬ e ˙ W
22 21 3ad2ant3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q e A ¬ e ˙ W ¬ e ˙ P ˙ Q ¬ e ˙ W
23 20 22 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q e A ¬ e ˙ W ¬ e ˙ P ˙ Q e A ¬ e ˙ W
24 simp3l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q e A ¬ e ˙ W ¬ e ˙ P ˙ Q R ˙ P ˙ Q
25 simprrr R ˙ P ˙ Q e A ¬ e ˙ W ¬ e ˙ P ˙ Q ¬ e ˙ P ˙ Q
26 25 3ad2ant3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q e A ¬ e ˙ W ¬ e ˙ P ˙ Q ¬ e ˙ P ˙ Q
27 1 2 3 4 5 6 7 8 9 10 cdleme50trn2a K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W e A ¬ e ˙ W R ˙ P ˙ Q ¬ e ˙ P ˙ Q R ˙ F R ˙ W = U
28 17 18 19 23 24 26 27 syl132anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q e A ¬ e ˙ W ¬ e ˙ P ˙ Q R ˙ F R ˙ W = U
29 28 3exp K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q e A ¬ e ˙ W ¬ e ˙ P ˙ Q R ˙ F R ˙ W = U
30 29 exp4a K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q e A ¬ e ˙ W ¬ e ˙ P ˙ Q R ˙ F R ˙ W = U
31 30 3imp K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q e A ¬ e ˙ W ¬ e ˙ P ˙ Q R ˙ F R ˙ W = U
32 31 expd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q e A ¬ e ˙ W ¬ e ˙ P ˙ Q R ˙ F R ˙ W = U
33 32 rexlimdv K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q e A ¬ e ˙ W ¬ e ˙ P ˙ Q R ˙ F R ˙ W = U
34 16 33 mpd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q R ˙ F R ˙ W = U