# Metamath Proof Explorer

## Theorem homulid2

Description: An operator equals its scalar product with one. (Contributed by NM, 12-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion homulid2 ( 𝑇 : ℋ ⟶ ℋ → ( 1 ·op 𝑇 ) = 𝑇 )

### Proof

Step Hyp Ref Expression
1 ax-1cn 1 ∈ ℂ
2 homval ( ( 1 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 1 ·op 𝑇 ) ‘ 𝑥 ) = ( 1 · ( 𝑇𝑥 ) ) )
3 1 2 mp3an1 ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 1 ·op 𝑇 ) ‘ 𝑥 ) = ( 1 · ( 𝑇𝑥 ) ) )
4 ffvelrn ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑇𝑥 ) ∈ ℋ )
5 ax-hvmulid ( ( 𝑇𝑥 ) ∈ ℋ → ( 1 · ( 𝑇𝑥 ) ) = ( 𝑇𝑥 ) )
6 4 5 syl ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( 1 · ( 𝑇𝑥 ) ) = ( 𝑇𝑥 ) )
7 3 6 eqtrd ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 1 ·op 𝑇 ) ‘ 𝑥 ) = ( 𝑇𝑥 ) )
8 7 ralrimiva ( 𝑇 : ℋ ⟶ ℋ → ∀ 𝑥 ∈ ℋ ( ( 1 ·op 𝑇 ) ‘ 𝑥 ) = ( 𝑇𝑥 ) )
9 homulcl ( ( 1 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 1 ·op 𝑇 ) : ℋ ⟶ ℋ )
10 1 9 mpan ( 𝑇 : ℋ ⟶ ℋ → ( 1 ·op 𝑇 ) : ℋ ⟶ ℋ )
11 hoeq ( ( ( 1 ·op 𝑇 ) : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( ( 1 ·op 𝑇 ) ‘ 𝑥 ) = ( 𝑇𝑥 ) ↔ ( 1 ·op 𝑇 ) = 𝑇 ) )
12 10 11 mpancom ( 𝑇 : ℋ ⟶ ℋ → ( ∀ 𝑥 ∈ ℋ ( ( 1 ·op 𝑇 ) ‘ 𝑥 ) = ( 𝑇𝑥 ) ↔ ( 1 ·op 𝑇 ) = 𝑇 ) )
13 8 12 mpbid ( 𝑇 : ℋ ⟶ ℋ → ( 1 ·op 𝑇 ) = 𝑇 )