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

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 ⊢ S : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ → S - op T = x ∈ ℋ ⟼ S ⁡ x - ℎ T ⁡ x

Proof

Step Hyp Ref Expression
1 ax-hilex ⊢ ℋ ∈ V
2 1 1 elmap ⊢ S ∈ ℋ ℋ ↔ S : ℋ ⟶ ℋ
3 1 1 elmap ⊢ T ∈ ℋ ℋ ↔ T : ℋ ⟶ ℋ
4 fveq1 ⊢ f = S → f ⁡ x = S ⁡ x
5 4 oveq1d ⊢ f = S → f ⁡ x - ℎ g ⁡ x = S ⁡ x - ℎ g ⁡ x
6 5 mpteq2dv ⊢ f = S → x ∈ ℋ ⟼ f ⁡ x - ℎ g ⁡ x = x ∈ ℋ ⟼ S ⁡ x - ℎ g ⁡ x
7 fveq1 ⊢ g = T → g ⁡ x = T ⁡ x
8 7 oveq2d ⊢ g = T → S ⁡ x - ℎ g ⁡ x = S ⁡ x - ℎ T ⁡ x
9 8 mpteq2dv ⊢ g = T → x ∈ ℋ ⟼ S ⁡ x - ℎ g ⁡ x = x ∈ ℋ ⟼ S ⁡ x - ℎ T ⁡ x
10 df-hodif ⊢ - op = f ∈ ℋ ℋ , g ∈ ℋ ℋ ⟼ x ∈ ℋ ⟼ f ⁡ x - ℎ g ⁡ x
11 1 mptex ⊢ x ∈ ℋ ⟼ S ⁡ x - ℎ T ⁡ x ∈ V
12 6 9 10 11 ovmpo ⊢ S ∈ ℋ ℋ ∧ T ∈ ℋ ℋ → S - op T = x ∈ ℋ ⟼ S ⁡ x - ℎ T ⁡ x
13 2 3 12 syl2anbr ⊢ S : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ → S - op T = x ∈ ℋ ⟼ S ⁡ x - ℎ T ⁡ x