Theorem homulcl

Description: The scalar product of a Hilbert space operator is an operator. (Contributed by NM, 21-Feb-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ffvelrn	|- ( ( T : ~H --> ~H /\ x e. ~H ) -> ( T ` x ) e. ~H )
2		hvmulcl	|- ( ( A e. CC /\ ( T ` x ) e. ~H ) -> ( A .h ( T ` x ) ) e. ~H )
3	1 2	sylan2	|- ( ( A e. CC /\ ( T : ~H --> ~H /\ x e. ~H ) ) -> ( A .h ( T ` x ) ) e. ~H )
4	3	anassrs	|- ( ( ( A e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( A .h ( T ` x ) ) e. ~H )
5	4	fmpttd	|- ( ( A e. CC /\ T : ~H --> ~H ) -> ( x e. ~H |-> ( A .h ( T ` x ) ) ) : ~H --> ~H )
6		hommval	|- ( ( A e. CC /\ T : ~H --> ~H ) -> ( A .op T ) = ( x e. ~H |-> ( A .h ( T ` x ) ) ) )
7	6	feq1d	|- ( ( A e. CC /\ T : ~H --> ~H ) -> ( ( A .op T ) : ~H --> ~H <-> ( x e. ~H |-> ( A .h ( T ` x ) ) ) : ~H --> ~H ) )
8	5 7	mpbird	|- ( ( A e. CC /\ T : ~H --> ~H ) -> ( A .op T ) : ~H --> ~H )