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 )