Metamath Proof Explorer


Theorem cdlemkuu

Description: Convert between function and operation forms of Y . TODO: Use operation form everywhere. (Contributed by NM, 6-Jul-2013)

Ref Expression
Hypotheses cdlemk3.b B = Base K
cdlemk3.l ˙ = K
cdlemk3.j ˙ = join K
cdlemk3.m ˙ = meet K
cdlemk3.a A = Atoms K
cdlemk3.h H = LHyp K
cdlemk3.t T = LTrn K W
cdlemk3.r R = trL K W
cdlemk3.s S = f T ι i T | i P = P ˙ R f ˙ N P ˙ R f F -1
cdlemk3.u1 Y = d T , e T ι j T | j P = P ˙ R e ˙ S d P ˙ R e d -1
cdlemk3.o2 Q = S D
cdlemk3.u2 Z = e T ι j T | j P = P ˙ R e ˙ Q P ˙ R e D -1
Assertion cdlemkuu D T G T D Y G = Z G

Proof

Step Hyp Ref Expression
1 cdlemk3.b B = Base K
2 cdlemk3.l ˙ = K
3 cdlemk3.j ˙ = join K
4 cdlemk3.m ˙ = meet K
5 cdlemk3.a A = Atoms K
6 cdlemk3.h H = LHyp K
7 cdlemk3.t T = LTrn K W
8 cdlemk3.r R = trL K W
9 cdlemk3.s S = f T ι i T | i P = P ˙ R f ˙ N P ˙ R f F -1
10 cdlemk3.u1 Y = d T , e T ι j T | j P = P ˙ R e ˙ S d P ˙ R e d -1
11 cdlemk3.o2 Q = S D
12 cdlemk3.u2 Z = e T ι j T | j P = P ˙ R e ˙ Q P ˙ R e D -1
13 fveq2 d = D S d = S D
14 13 11 eqtr4di d = D S d = Q
15 14 fveq1d d = D S d P = Q P
16 cnveq d = D d -1 = D -1
17 16 coeq2d d = D e d -1 = e D -1
18 17 fveq2d d = D R e d -1 = R e D -1
19 15 18 oveq12d d = D S d P ˙ R e d -1 = Q P ˙ R e D -1
20 19 oveq2d d = D P ˙ R e ˙ S d P ˙ R e d -1 = P ˙ R e ˙ Q P ˙ R e D -1
21 20 eqeq2d d = D j P = P ˙ R e ˙ S d P ˙ R e d -1 j P = P ˙ R e ˙ Q P ˙ R e D -1
22 21 riotabidv d = D ι j T | j P = P ˙ R e ˙ S d P ˙ R e d -1 = ι j T | j P = P ˙ R e ˙ Q P ˙ R e D -1
23 fveq2 e = G R e = R G
24 23 oveq2d e = G P ˙ R e = P ˙ R G
25 coeq1 e = G e D -1 = G D -1
26 25 fveq2d e = G R e D -1 = R G D -1
27 26 oveq2d e = G Q P ˙ R e D -1 = Q P ˙ R G D -1
28 24 27 oveq12d e = G P ˙ R e ˙ Q P ˙ R e D -1 = P ˙ R G ˙ Q P ˙ R G D -1
29 28 eqeq2d e = G j P = P ˙ R e ˙ Q P ˙ R e D -1 j P = P ˙ R G ˙ Q P ˙ R G D -1
30 29 riotabidv e = G ι j T | j P = P ˙ R e ˙ Q P ˙ R e D -1 = ι j T | j P = P ˙ R G ˙ Q P ˙ R G D -1
31 riotaex ι j T | j P = P ˙ R G ˙ Q P ˙ R G D -1 V
32 22 30 10 31 ovmpo D T G T D Y G = ι j T | j P = P ˙ R G ˙ Q P ˙ R G D -1
33 1 2 3 5 6 7 8 4 12 cdlemksv G T Z G = ι j T | j P = P ˙ R G ˙ Q P ˙ R G D -1
34 33 adantl D T G T Z G = ι j T | j P = P ˙ R G ˙ Q P ˙ R G D -1
35 32 34 eqtr4d D T G T D Y G = Z G