Metamath Proof Explorer


Theorem tendo1mul

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