Metamath Proof Explorer

Theorem homullid

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

Ref Expression
Assertion homullid ⊢ T : ℋ ⟶ ℋ → 1 · op T = T

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 homval ⊢ 1 ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → 1 · op T ⁡ x = 1 ⋅ ℎ T ⁡ x
3 1 2 mp3an1 ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → 1 · op T ⁡ x = 1 ⋅ ℎ T ⁡ x
4 ffvelcdm ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → T ⁡ x ∈ ℋ
5 ax-hvmulid ⊢ T ⁡ x ∈ ℋ → 1 ⋅ ℎ T ⁡ x = T ⁡ x
6 4 5 syl ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → 1 ⋅ ℎ T ⁡ x = T ⁡ x
7 3 6 eqtrd ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → 1 · op T ⁡ x = T ⁡ x
8 7 ralrimiva ⊢ T : ℋ ⟶ ℋ → ∀ x ∈ ℋ 1 · op T ⁡ x = T ⁡ x
9 homulcl ⊢ 1 ∈ ℂ ∧ T : ℋ ⟶ ℋ → 1 · op T : ℋ ⟶ ℋ
10 1 9 mpan ⊢ T : ℋ ⟶ ℋ → 1 · op T : ℋ ⟶ ℋ
11 hoeq ⊢ 1 · op T : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ → ∀ x ∈ ℋ 1 · op T ⁡ x = T ⁡ x ↔ 1 · op T = T
12 10 11 mpancom ⊢ T : ℋ ⟶ ℋ → ∀ x ∈ ℋ 1 · op T ⁡ x = T ⁡ x ↔ 1 · op T = T
13 8 12 mpbid ⊢ T : ℋ ⟶ ℋ → 1 · op T = T