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 e. T |-> ( _I |` B ) )
Assertion	tendo0co2	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( O ` ( F o. G ) ) = ( ( O ` F ) o. ( 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 e. T |-> ( _I |` B ) )
6	2 3	ltrnco	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( F o. G ) e. T )
7	5 1	tendo02	|- ( ( F o. G ) e. T -> ( O ` ( F o. G ) ) = ( _I |` B ) )
8	6 7	syl	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( O ` ( F o. G ) ) = ( _I |` B ) )
9	5 1	tendo02	|- ( F e. T -> ( O ` F ) = ( _I |` B ) )
10	9	3ad2ant2	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( O ` F ) = ( _I |` B ) )
11	5 1	tendo02	|- ( G e. T -> ( O ` G ) = ( _I |` B ) )
12	11	3ad2ant3	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( O ` G ) = ( _I |` B ) )
13	10 12	coeq12d	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( ( O ` F ) o. ( O ` G ) ) = ( ( _I |` B ) o. ( _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 ) o. ( _I |` B ) ) = ( _I |` B ) )
17	14 15 16	mp2b	|- ( ( _I |` B ) o. ( _I |` B ) ) = ( _I |` B )
18	13 17	eqtr2di	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( _I |` B ) = ( ( O ` F ) o. ( O ` G ) ) )
19	8 18	eqtrd	|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( O ` ( F o. G ) ) = ( ( O ` F ) o. ( O ` G ) ) )