Metamath Proof Explorer

Theorem adjcl

Description: Closure of the adjoint of a Hilbert space operator. (Contributed by NM, 17-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion adjcl 
|- ( ( T e. dom adjh /\ A e. ~H ) -> ( ( adjh ` T ) ` A ) e. ~H )

Proof

Step Hyp Ref Expression
1 dmadjrn 
 |-  ( T e. dom adjh -> ( adjh ` T ) e. dom adjh )
2 dmadjop 
 |-  ( ( adjh ` T ) e. dom adjh -> ( adjh ` T ) : ~H --> ~H )
3 1 2 syl 
 |-  ( T e. dom adjh -> ( adjh ` T ) : ~H --> ~H )
4 3 ffvelrnda 
 |-  ( ( T e. dom adjh /\ A e. ~H ) -> ( ( adjh ` T ) ` A ) e. ~H )