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

Metamath Proof Explorer

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