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 ∈ dom ⁡ adj h ∧ A ∈ ℋ → adj h ⁡ T ⁡ A ∈ ℋ

Proof

Step Hyp Ref Expression
1 dmadjrn ⊢ T ∈ dom ⁡ adj h → adj h ⁡ T ∈ dom ⁡ adj h
2 dmadjop ⊢ adj h ⁡ T ∈ dom ⁡ adj h → adj h ⁡ T : ℋ ⟶ ℋ
3 1 2 syl ⊢ T ∈ dom ⁡ adj h → adj h ⁡ T : ℋ ⟶ ℋ
4 3 ffvelrnda ⊢ T ∈ dom ⁡ adj h ∧ A ∈ ℋ → adj h ⁡ T ⁡ A ∈ ℋ