Metamath Proof Explorer

Theorem lnfnaddi

Description: Additive property of a linear Hilbert space functional. (Contributed by NM, 11-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypothesis lnfnl.1 ⊢ T ∈ LinFn
Assertion lnfnaddi ⊢ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A + ℎ B = T ⁡ A + T ⁡ B

Proof

Step Hyp Ref Expression
1 lnfnl.1 ⊢ T ∈ LinFn
2 ax-1cn ⊢ 1 ∈ ℂ
3 1 lnfnli ⊢ 1 ∈ ℂ ∧ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ 1 ⋅ ℎ A + ℎ B = 1 ⁢ T ⁡ A + T ⁡ B
4 2 3 mp3an1 ⊢ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ 1 ⋅ ℎ A + ℎ B = 1 ⁢ T ⁡ A + T ⁡ B
5 ax-hvmulid ⊢ A ∈ ℋ → 1 ⋅ ℎ A = A
6 5 fvoveq1d ⊢ A ∈ ℋ → T ⁡ 1 ⋅ ℎ A + ℎ B = T ⁡ A + ℎ B
7 6 adantr ⊢ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ 1 ⋅ ℎ A + ℎ B = T ⁡ A + ℎ B
8 1 lnfnfi ⊢ T : ℋ ⟶ ℂ
9 8 ffvelrni ⊢ A ∈ ℋ → T ⁡ A ∈ ℂ
10 9 mulid2d ⊢ A ∈ ℋ → 1 ⁢ T ⁡ A = T ⁡ A
11 10 adantr ⊢ A ∈ ℋ ∧ B ∈ ℋ → 1 ⁢ T ⁡ A = T ⁡ A
12 11 oveq1d ⊢ A ∈ ℋ ∧ B ∈ ℋ → 1 ⁢ T ⁡ A + T ⁡ B = T ⁡ A + T ⁡ B
13 4 7 12 3eqtr3d ⊢ A ∈ ℋ ∧ B ∈ ℋ → T ⁡ A + ℎ B = T ⁡ A + T ⁡ B