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 𝑇 ) = ( 𝑥 ∈ ℋ ↦ ( ( 𝑆 ‘ 𝑥 ) + ( 𝑇 ‘ 𝑥 ) ) ) )