Metamath Proof Explorer


Theorem hodmval

Description: Value of the difference 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 hodmval ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑆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-hodif op = ( 𝑓 ∈ ( ℋ ↑m ℋ ) , 𝑔 ∈ ( ℋ ↑m ℋ ) ↦ ( 𝑥 ∈ ℋ ↦ ( ( 𝑓𝑥 ) − ( 𝑔𝑥 ) ) ) )
11 1 mptex ( 𝑥 ∈ ℋ ↦ ( ( 𝑆𝑥 ) − ( 𝑇𝑥 ) ) ) ∈ V
12 6 9 10 11 ovmpo ( ( 𝑆 ∈ ( ℋ ↑m ℋ ) ∧ 𝑇 ∈ ( ℋ ↑m ℋ ) ) → ( 𝑆op 𝑇 ) = ( 𝑥 ∈ ℋ ↦ ( ( 𝑆𝑥 ) − ( 𝑇𝑥 ) ) ) )
13 2 3 12 syl2anbr ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑆op 𝑇 ) = ( 𝑥 ∈ ℋ ↦ ( ( 𝑆𝑥 ) − ( 𝑇𝑥 ) ) ) )