Metamath Proof Explorer

Theorem dmadjrn

Description: The adjoint of an operator belongs to the adjoint function's domain. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion dmadjrn ⊢ T ∈ dom ⁡ adj h → adj h ⁡ T ∈ dom ⁡ adj h

Proof

Step Hyp Ref Expression
1 adj1o ⊢ adj h : dom ⁡ adj h ⟶ 1-1 onto dom ⁡ adj h
2 f1of ⊢ adj h : dom ⁡ adj h ⟶ 1-1 onto dom ⁡ adj h → adj h : dom ⁡ adj h ⟶ dom ⁡ adj h
3 1 2 ax-mp ⊢ adj h : dom ⁡ adj h ⟶ dom ⁡ adj h
4 3 ffvelcdmi ⊢ T ∈ dom ⁡ adj h → adj h ⁡ T ∈ dom ⁡ adj h