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

Proof

Step	Hyp	Ref	Expression
1		adj1o	⊢ adjℎ : dom adjℎ –1-1-onto→ dom adjℎ
2		f1of	⊢ ( adjℎ : dom adjℎ –1-1-onto→ dom adjℎ → adjℎ : dom adjℎ ⟶ dom adjℎ )
3	1 2	ax-mp	⊢ adjℎ : dom adjℎ ⟶ dom adjℎ
4	3	ffvelrni	⊢ ( 𝑇 ∈ dom adjℎ → ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ )