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 HL W H U E U 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 HL W H U E U : T T
5 fcoi1 U : T T U I T = U
6 4 5 syl K HL W H U E U I T = U