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 )
3 2 3adant2 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ A e. ~H ) -> ( S ` A ) e. ~H )
4 ffvelrn 
 |-  ( ( T : ~H --> ~H /\ A e. ~H ) -> ( T ` A ) e. ~H )
5 4 3adant1 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ A e. ~H ) -> ( T ` A ) e. ~H )
6 hvsubcl 
 |-  ( ( ( S ` A ) e. ~H /\ ( T ` A ) e. ~H ) -> ( ( S ` A ) -h ( T ` A ) ) e. ~H )
7 3 5 6 syl2anc 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ A e. ~H ) -> ( ( S ` A ) -h ( T ` A ) ) e. ~H )
8 1 7 eqeltrd 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ A e. ~H ) -> ( ( S -op T ) ` A ) e. ~H )
9 8 3expa 
 |-  ( ( ( S : ~H --> ~H /\ T : ~H --> ~H ) /\ A e. ~H ) -> ( ( S -op T ) ` A ) e. ~H )