Metamath Proof Explorer


Theorem tendo0co2

Description: The additive identity trace-preserving endormorphism preserves composition of translations. TODO: why isn't this a special case of tendospdi1 ? (Contributed by NM, 11-Jun-2013)

Ref Expression
Hypotheses tendo0.b B = Base K
tendo0.h H = LHyp K
tendo0.t T = LTrn K W
tendo0.e E = TEndo K W
tendo0.o O = f T I B
Assertion tendo0co2 K HL W H F T G T O F G = O F O G

Proof

Step Hyp Ref Expression
1 tendo0.b B = Base K
2 tendo0.h H = LHyp K
3 tendo0.t T = LTrn K W
4 tendo0.e E = TEndo K W
5 tendo0.o O = f T I B
6 2 3 ltrnco K HL W H F T G T F G T
7 5 1 tendo02 F G T O F G = I B
8 6 7 syl K HL W H F T G T O F G = I B
9 5 1 tendo02 F T O F = I B
10 9 3ad2ant2 K HL W H F T G T O F = I B
11 5 1 tendo02 G T O G = I B
12 11 3ad2ant3 K HL W H F T G T O G = I B
13 10 12 coeq12d K HL W H F T G T O F O G = I B I B
14 f1oi I B : B 1-1 onto B
15 f1of I B : B 1-1 onto B I B : B B
16 fcoi1 I B : B B I B I B = I B
17 14 15 16 mp2b I B I B = I B
18 13 17 eqtr2di K HL W H F T G T I B = O F O G
19 8 18 eqtrd K HL W H F T G T O F G = O F O G