Theorem hosmval

Description: Value of the sum of two Hilbert space operators. (Contributed by NM, 9-Nov-2000) (Revised by Mario Carneiro, 23-Aug-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	hosmval	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑆 +op 𝑇 ) = ( 𝑥 ∈ ℋ ↦ ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) ) )

Proof

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