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

Metamath Proof Explorer

Theorem homcl

Description: Closure of the scalar product of a Hilbert space operator. (Contributed by NM, 20-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion homcl 
|- ( ( A e. CC /\ T : ~H --> ~H /\ B e. ~H ) -> ( ( A .op T ) ` B ) e. ~H )

Proof

Step Hyp Ref Expression
1 homval 
 |-  ( ( A e. CC /\ T : ~H --> ~H /\ B e. ~H ) -> ( ( A .op T ) ` B ) = ( A .h ( T ` B ) ) )
2 ffvelcdm 
 |-  ( ( T : ~H --> ~H /\ B e. ~H ) -> ( T ` B ) e. ~H )
3 2 anim2i 
 |-  ( ( A e. CC /\ ( T : ~H --> ~H /\ B e. ~H ) ) -> ( A e. CC /\ ( T ` B ) e. ~H ) )
4 3 3impb 
 |-  ( ( A e. CC /\ T : ~H --> ~H /\ B e. ~H ) -> ( A e. CC /\ ( T ` B ) e. ~H ) )
5 hvmulcl 
 |-  ( ( A e. CC /\ ( T ` B ) e. ~H ) -> ( A .h ( T ` B ) ) e. ~H )
6 4 5 syl 
 |-  ( ( A e. CC /\ T : ~H --> ~H /\ B e. ~H ) -> ( A .h ( T ` B ) ) e. ~H )
7 1 6 eqeltrd 
 |-  ( ( A e. CC /\ T : ~H --> ~H /\ B e. ~H ) -> ( ( A .op T ) ` B ) e. ~H )