Metamath Proof Explorer


Theorem cdlemg2cex

Description: Any translation is one of our F s. TODO: fix comment, move to its own block maybe? Would this help for cdlemf ? (Contributed by NM, 22-Apr-2013)

Ref Expression
Hypotheses cdlemg2.b B = Base K
cdlemg2.l ˙ = K
cdlemg2.j ˙ = join K
cdlemg2.m ˙ = meet K
cdlemg2.a A = Atoms K
cdlemg2.h H = LHyp K
cdlemg2.t T = LTrn K W
cdlemg2ex.u U = p ˙ q ˙ W
cdlemg2ex.d D = t ˙ U ˙ q ˙ p ˙ t ˙ W
cdlemg2ex.e E = p ˙ q ˙ D ˙ s ˙ t ˙ W
cdlemg2ex.g G = 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 cdlemg2cex K HL W H F T p A q A ¬ p ˙ W ¬ q ˙ W F = G

Proof

Step Hyp Ref Expression
1 cdlemg2.b B = Base K
2 cdlemg2.l ˙ = K
3 cdlemg2.j ˙ = join K
4 cdlemg2.m ˙ = meet K
5 cdlemg2.a A = Atoms K
6 cdlemg2.h H = LHyp K
7 cdlemg2.t T = LTrn K W
8 cdlemg2ex.u U = p ˙ q ˙ W
9 cdlemg2ex.d D = t ˙ U ˙ q ˙ p ˙ t ˙ W
10 cdlemg2ex.e E = p ˙ q ˙ D ˙ s ˙ t ˙ W
11 cdlemg2ex.g G = 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
12 2 5 6 7 cdlemg1cex K HL W H F T p A q A ¬ p ˙ W ¬ q ˙ W F = ι f T | f p = q
13 simplll K HL W H p A q A ¬ p ˙ W ¬ q ˙ W K HL
14 simpllr K HL W H p A q A ¬ p ˙ W ¬ q ˙ W W H
15 simplrl K HL W H p A q A ¬ p ˙ W ¬ q ˙ W p A
16 simprl K HL W H p A q A ¬ p ˙ W ¬ q ˙ W ¬ p ˙ W
17 simplrr K HL W H p A q A ¬ p ˙ W ¬ q ˙ W q A
18 simprr K HL W H p A q A ¬ p ˙ W ¬ q ˙ W ¬ q ˙ W
19 eqid ι f T | f p = q = ι f T | f p = q
20 1 2 3 4 5 6 8 9 10 11 7 19 cdlemg1b2 K HL W H p A ¬ p ˙ W q A ¬ q ˙ W ι f T | f p = q = G
21 13 14 15 16 17 18 20 syl222anc K HL W H p A q A ¬ p ˙ W ¬ q ˙ W ι f T | f p = q = G
22 21 eqeq2d K HL W H p A q A ¬ p ˙ W ¬ q ˙ W F = ι f T | f p = q F = G
23 22 pm5.32da K HL W H p A q A ¬ p ˙ W ¬ q ˙ W F = ι f T | f p = q ¬ p ˙ W ¬ q ˙ W F = G
24 df-3an ¬ p ˙ W ¬ q ˙ W F = ι f T | f p = q ¬ p ˙ W ¬ q ˙ W F = ι f T | f p = q
25 df-3an ¬ p ˙ W ¬ q ˙ W F = G ¬ p ˙ W ¬ q ˙ W F = G
26 23 24 25 3bitr4g K HL W H p A q A ¬ p ˙ W ¬ q ˙ W F = ι f T | f p = q ¬ p ˙ W ¬ q ˙ W F = G
27 26 2rexbidva K HL W H p A q A ¬ p ˙ W ¬ q ˙ W F = ι f T | f p = q p A q A ¬ p ˙ W ¬ q ˙ W F = G
28 12 27 bitrd K HL W H F T p A q A ¬ p ˙ W ¬ q ˙ W F = G