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

Metamath Proof Explorer

Theorem hodcl

Description: Closure of the difference of two Hilbert space operators. (Contributed by NM, 15-Nov-2002) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 hodval ⊢ S : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ ∧ A ∈ ℋ → S - op T ⁡ A = S ⁡ A - ℎ T ⁡ A
2 ffvelcdm ⊢ S : ℋ ⟶ ℋ ∧ A ∈ ℋ → S ⁡ A ∈ ℋ
3 2 3adant2 ⊢ S : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ ∧ A ∈ ℋ → S ⁡ A ∈ ℋ
4 ffvelcdm ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℋ → T ⁡ A ∈ ℋ
5 4 3adant1 ⊢ S : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ ∧ A ∈ ℋ → T ⁡ A ∈ ℋ
6 hvsubcl ⊢ S ⁡ A ∈ ℋ ∧ T ⁡ A ∈ ℋ → S ⁡ A - ℎ T ⁡ A ∈ ℋ
7 3 5 6 syl2anc ⊢ S : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ ∧ A ∈ ℋ → S ⁡ A - ℎ T ⁡ A ∈ ℋ
8 1 7 eqeltrd ⊢ S : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ ∧ A ∈ ℋ → S - op T ⁡ A ∈ ℋ
9 8 3expa ⊢ S : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ ∧ A ∈ ℋ → S - op T ⁡ A ∈ ℋ