Metamath Proof Explorer

Theorem hoscl

Description: Closure of the sum of two Hilbert space operators. (Contributed by NM, 12-Nov-2000) (New usage is discouraged.)

Ref Expression
Assertion hoscl 
|- ( ( ( S : ~H --> ~H /\ T : ~H --> ~H ) /\ A e. ~H ) -> ( ( S +op T ) ` A ) e. ~H )

Proof

Step Hyp Ref Expression
1 hosval 
 |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ A e. ~H ) -> ( ( S +op T ) ` A ) = ( ( S ` A ) +h ( T ` A ) ) )
2 1 3expa 
 |-  ( ( ( S : ~H --> ~H /\ T : ~H --> ~H ) /\ A e. ~H ) -> ( ( S +op T ) ` A ) = ( ( S ` A ) +h ( T ` A ) ) )
3 ffvelrn 
 |-  ( ( S : ~H --> ~H /\ A e. ~H ) -> ( S ` A ) e. ~H )
4 ffvelrn 
 |-  ( ( T : ~H --> ~H /\ A e. ~H ) -> ( T ` A ) e. ~H )
5 3 4 anim12i 
 |-  ( ( ( S : ~H --> ~H /\ A e. ~H ) /\ ( T : ~H --> ~H /\ A e. ~H ) ) -> ( ( S ` A ) e. ~H /\ ( T ` A ) e. ~H ) )
6 5 anandirs 
 |-  ( ( ( S : ~H --> ~H /\ T : ~H --> ~H ) /\ A e. ~H ) -> ( ( S ` A ) e. ~H /\ ( T ` A ) e. ~H ) )
7 hvaddcl 
 |-  ( ( ( S ` A ) e. ~H /\ ( T ` A ) e. ~H ) -> ( ( S ` A ) +h ( T ` A ) ) e. ~H )
8 6 7 syl 
 |-  ( ( ( S : ~H --> ~H /\ T : ~H --> ~H ) /\ A e. ~H ) -> ( ( S ` A ) +h ( T ` A ) ) e. ~H )
9 2 8 eqeltrd 
 |-  ( ( ( S : ~H --> ~H /\ T : ~H --> ~H ) /\ A e. ~H ) -> ( ( S +op T ) ` A ) e. ~H )