Metamath Proof Explorer


Theorem tendo1mulr

Description: Multiplicative identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 20-Nov-2013)

Ref Expression
Hypotheses tendof.h
|- H = ( LHyp ` K )
tendof.t
|- T = ( ( LTrn ` K ) ` W )
tendof.e
|- E = ( ( TEndo ` K ) ` W )
Assertion tendo1mulr
|- ( ( ( K e. HL /\ W e. H ) /\ U e. E ) -> ( U o. ( _I |` T ) ) = U )

Proof

Step Hyp Ref Expression
1 tendof.h
 |-  H = ( LHyp ` K )
2 tendof.t
 |-  T = ( ( LTrn ` K ) ` W )
3 tendof.e
 |-  E = ( ( TEndo ` K ) ` W )
4 1 2 3 tendof
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E ) -> U : T --> T )
5 fcoi1
 |-  ( U : T --> T -> ( U o. ( _I |` T ) ) = U )
6 4 5 syl
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E ) -> ( U o. ( _I |` T ) ) = U )