Description: Multiplicative identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 20-Nov-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tendof.h | ||
tendof.t | |||
tendof.e | |||
Assertion | tendo1mul |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tendof.h | ||
2 | tendof.t | ||
3 | tendof.e | ||
4 | 1 2 3 | tendof | |
5 | fcoi2 | ||
6 | 4 5 | syl |