# Metamath Proof Explorer

## 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 )`