This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑆 : ℋ ⟶ ℂ ∧ 𝑇 : ℋ ⟶ ℂ ) → ( 𝑆 +fn 𝑇 ) = ( 𝑥 ∈ ℋ ↦ ( ( 𝑆 ‘ 𝑥 ) + ( 𝑇 ‘ 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 cnex ⊢ ℂ ∈ V
2 ax-hilex ⊢ ℋ ∈ V
3 1 2 elmap ⊢ ( 𝑆 ∈ ( ℂ ↑m ℋ ) ↔ 𝑆 : ℋ ⟶ ℂ )
4 1 2 elmap ⊢ ( 𝑇 ∈ ( ℂ ↑m ℋ ) ↔ 𝑇 : ℋ ⟶ ℂ )
5 fveq1 ⊢ ( 𝑓 = 𝑆 → ( 𝑓 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
6 5 oveq1d ⊢ ( 𝑓 = 𝑆 → ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑆 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) )
7 6 mpteq2dv ⊢ ( 𝑓 = 𝑆 → ( 𝑥 ∈ ℋ ↦ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℋ ↦ ( ( 𝑆 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ) )
8 fveq1 ⊢ ( 𝑔 = 𝑇 → ( 𝑔 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) )
9 8 oveq2d ⊢ ( 𝑔 = 𝑇 → ( ( 𝑆 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑆 ‘ 𝑥 ) + ( 𝑇 ‘ 𝑥 ) ) )
10 9 mpteq2dv ⊢ ( 𝑔 = 𝑇 → ( 𝑥 ∈ ℋ ↦ ( ( 𝑆 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℋ ↦ ( ( 𝑆 ‘ 𝑥 ) + ( 𝑇 ‘ 𝑥 ) ) ) )
11 df-hfsum ⊢ +fn = ( 𝑓 ∈ ( ℂ ↑m ℋ ) , 𝑔 ∈ ( ℂ ↑m ℋ ) ↦ ( 𝑥 ∈ ℋ ↦ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑔 ‘ 𝑥 ) ) ) )
12 2 mptex ⊢ ( 𝑥 ∈ ℋ ↦ ( ( 𝑆 ‘ 𝑥 ) + ( 𝑇 ‘ 𝑥 ) ) ) ∈ V
13 7 10 11 12 ovmpo ⊢ ( ( 𝑆 ∈ ( ℂ ↑m ℋ ) ∧ 𝑇 ∈ ( ℂ ↑m ℋ ) ) → ( 𝑆 +fn 𝑇 ) = ( 𝑥 ∈ ℋ ↦ ( ( 𝑆 ‘ 𝑥 ) + ( 𝑇 ‘ 𝑥 ) ) ) )
14 3 4 13 syl2anbr ⊢ ( ( 𝑆 : ℋ ⟶ ℂ ∧ 𝑇 : ℋ ⟶ ℂ ) → ( 𝑆 +fn 𝑇 ) = ( 𝑥 ∈ ℋ ↦ ( ( 𝑆 ‘ 𝑥 ) + ( 𝑇 ‘ 𝑥 ) ) ) )