# 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 : ~H --> ~H /\ T : ~H --> ~H ) /\ A e. ~H ) -> ( ( S -op T ) ` A ) e. ~H )`

### Proof

Step Hyp Ref Expression
1 hodval
` |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ A e. ~H ) -> ( ( S -op T ) ` A ) = ( ( S ` A ) -h ( T ` A ) ) )`
2 ffvelrn
` |-  ( ( S : ~H --> ~H /\ A e. ~H ) -> ( S ` A ) e. ~H )`
` |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ A e. ~H ) -> ( S ` A ) e. ~H )`
` |-  ( ( T : ~H --> ~H /\ A e. ~H ) -> ( T ` A ) e. ~H )`
` |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ A e. ~H ) -> ( T ` A ) e. ~H )`
` |-  ( ( ( S ` A ) e. ~H /\ ( T ` A ) e. ~H ) -> ( ( S ` A ) -h ( T ` A ) ) e. ~H )`
` |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ A e. ~H ) -> ( ( S ` A ) -h ( T ` A ) ) e. ~H )`
` |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ A e. ~H ) -> ( ( S -op T ) ` A ) e. ~H )`
` |-  ( ( ( S : ~H --> ~H /\ T : ~H --> ~H ) /\ A e. ~H ) -> ( ( S -op T ) ` A ) e. ~H )`