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 ↾ 𝑇 ) ∘ 𝑈 ) = 𝑈 ) |
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 ↾ 𝑇 ) ∘ 𝑈 ) = 𝑈 ) |