Metamath Proof Explorer


Theorem cdlemg2cN

Description: Any translation belongs to the set of functions constructed for cdleme . TODO: Fix comment. (Contributed by NM, 22-Apr-2013) (New usage is discouraged.)

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
cdlemg2.u U = P ˙ Q ˙ W
cdlemg2.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdlemg2.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
cdlemg2.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 cdlemg2cN K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F P = Q F T 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 cdlemg2.u U = P ˙ Q ˙ W
9 cdlemg2.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
10 cdlemg2.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
11 cdlemg2.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 cdlemg1cN K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F P = Q F T F = ι f T | f P = Q
13 eqid ι f T | f P = Q = ι f T | f P = Q
14 1 2 3 4 5 6 8 9 10 11 7 13 cdlemg1b2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W ι f T | f P = Q = G
15 14 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F P = Q ι f T | f P = Q = G
16 15 eqeq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F P = Q F = ι f T | f P = Q F = G
17 12 16 bitrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F P = Q F T F = G