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	⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ) → ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ∈ ℋ )

Proof

Step	Hyp	Ref	Expression
1		dmadjrn	⊢ ( 𝑇 ∈ dom adjℎ → ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ )
2		dmadjop	⊢ ( ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ → ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ )
3	1 2	syl	⊢ ( 𝑇 ∈ dom adjℎ → ( adjℎ ‘ 𝑇 ) : ℋ ⟶ ℋ )
4	3	ffvelrnda	⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ) → ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ∈ ℋ )