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

Metamath Proof Explorer

Theorem hodval

Description: Value of the difference of two Hilbert space operators. (Contributed by NM, 10-Nov-2000) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion hodval ⊢ S : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ ∧ A ∈ ℋ → S - op T ⁡ A = S ⁡ A - ℎ T ⁡ A

Proof

Step Hyp Ref Expression
1 hodmval ⊢ S : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ → S - op T = x ∈ ℋ ⟼ S ⁡ x - ℎ T ⁡ x
2 1 fveq1d ⊢ S : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ → S - op T ⁡ A = x ∈ ℋ ⟼ S ⁡ x - ℎ T ⁡ x ⁡ A
3 fveq2 ⊢ x = A → S ⁡ x = S ⁡ A
4 fveq2 ⊢ x = A → T ⁡ x = T ⁡ A
5 3 4 oveq12d ⊢ x = A → S ⁡ x - ℎ T ⁡ x = S ⁡ A - ℎ T ⁡ A
6 eqid ⊢ x ∈ ℋ ⟼ S ⁡ x - ℎ T ⁡ x = x ∈ ℋ ⟼ S ⁡ x - ℎ T ⁡ x
7 ovex ⊢ S ⁡ A - ℎ T ⁡ A ∈ V
8 5 6 7 fvmpt ⊢ A ∈ ℋ → x ∈ ℋ ⟼ S ⁡ x - ℎ T ⁡ x ⁡ A = S ⁡ A - ℎ T ⁡ A
9 2 8 sylan9eq ⊢ S : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ ∧ A ∈ ℋ → S - op T ⁡ A = S ⁡ A - ℎ T ⁡ A
10 9 3impa ⊢ S : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ ∧ A ∈ ℋ → S - op T ⁡ A = S ⁡ A - ℎ T ⁡ A