Metamath Proof Explorer

Theorem hfsmval

Description: Value of the sum of two Hilbert space functionals. (Contributed by NM, 23-May-2006) (Revised by Mario Carneiro, 23-Aug-2014) (New usage is discouraged.)

Ref Expression
Assertion hfsmval ⊢ S : ℋ ⟶ ℂ ∧ T : ℋ ⟶ ℂ → S + fn T = x ∈ ℋ ⟼ S ⁡ x + T ⁡ x

Proof

Step Hyp Ref Expression
1 cnex ⊢ ℂ ∈ V
2 ax-hilex ⊢ ℋ ∈ V
3 1 2 elmap ⊢ S ∈ ℂ ℋ ↔ S : ℋ ⟶ ℂ
4 1 2 elmap ⊢ T ∈ ℂ ℋ ↔ T : ℋ ⟶ ℂ
5 fveq1 ⊢ f = S → f ⁡ x = S ⁡ x
6 5 oveq1d ⊢ f = S → f ⁡ x + g ⁡ x = S ⁡ x + g ⁡ x
7 6 mpteq2dv ⊢ f = S → x ∈ ℋ ⟼ f ⁡ x + g ⁡ x = x ∈ ℋ ⟼ S ⁡ x + g ⁡ x
8 fveq1 ⊢ g = T → g ⁡ x = T ⁡ x
9 8 oveq2d ⊢ g = T → S ⁡ x + g ⁡ x = S ⁡ x + T ⁡ x
10 9 mpteq2dv ⊢ g = T → x ∈ ℋ ⟼ S ⁡ x + g ⁡ x = x ∈ ℋ ⟼ S ⁡ x + T ⁡ x
11 df-hfsum ⊢ + fn = f ∈ ℂ ℋ , g ∈ ℂ ℋ ⟼ x ∈ ℋ ⟼ f ⁡ x + g ⁡ x
12 2 mptex ⊢ x ∈ ℋ ⟼ S ⁡ x + T ⁡ x ∈ V
13 7 10 11 12 ovmpo ⊢ S ∈ ℂ ℋ ∧ T ∈ ℂ ℋ → S + fn T = x ∈ ℋ ⟼ S ⁡ x + T ⁡ x
14 3 4 13 syl2anbr ⊢ S : ℋ ⟶ ℂ ∧ T : ℋ ⟶ ℂ → S + fn T = x ∈ ℋ ⟼ S ⁡ x + T ⁡ x