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 𝑇 ) = 𝑇 )