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 𝐻 = ( LHyp ‘ 𝐾 )
tendof.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tendof.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
Assertion tendo1mul ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸 ) → ( ( I ↾ 𝑇 ) ∘ 𝑈 ) = 𝑈 )

Proof

Step Hyp Ref Expression
1 tendof.h 𝐻 = ( LHyp ‘ 𝐾 )
2 tendof.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 tendof.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 1 2 3 tendof ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸 ) → 𝑈 : 𝑇𝑇 )
5 fcoi2 ( 𝑈 : 𝑇𝑇 → ( ( I ↾ 𝑇 ) ∘ 𝑈 ) = 𝑈 )
6 4 5 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸 ) → ( ( I ↾ 𝑇 ) ∘ 𝑈 ) = 𝑈 )