Theorem dmadjrnb

Description: The adjoint of an operator belongs to the adjoint function's domain. (Note: the converse is dependent on our definition of function value, since it uses ndmfv .) (Contributed by NM, 19-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	dmadjrnb	⊢ ( 𝑇 ∈ dom adjℎ ↔ ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ )

Proof

Step	Hyp	Ref	Expression
1		dmadjrn	⊢ ( 𝑇 ∈ dom adjℎ → ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ )
2		ax-hv0cl	⊢ 0ℎ ∈ ℋ
3	2	n0ii	⊢ ¬ ℋ = ∅
4		eqcom	⊢ ( ∅ = ℋ ↔ ℋ = ∅ )
5	3 4	mtbir	⊢ ¬ ∅ = ℋ
6		dm0	⊢ dom ∅ = ∅
7	6	eqeq1i	⊢ ( dom ∅ = ℋ ↔ ∅ = ℋ )
8	5 7	mtbir	⊢ ¬ dom ∅ = ℋ
9		fdm	⊢ ( ∅ : ℋ ⟶ ℋ → dom ∅ = ℋ )
10	8 9	mto	⊢ ¬ ∅ : ℋ ⟶ ℋ
11		dmadjop	⊢ ( ∅ ∈ dom adjℎ → ∅ : ℋ ⟶ ℋ )
12	10 11	mto	⊢ ¬ ∅ ∈ dom adjℎ
13		ndmfv	⊢ ( ¬ 𝑇 ∈ dom adjℎ → ( adjℎ ‘ 𝑇 ) = ∅ )
14	13	eleq1d	⊢ ( ¬ 𝑇 ∈ dom adjℎ → ( ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ ↔ ∅ ∈ dom adjℎ ) )
15	12 14	mtbiri	⊢ ( ¬ 𝑇 ∈ dom adjℎ → ¬ ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ )
16	15	con4i	⊢ ( ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ → 𝑇 ∈ dom adjℎ )
17	1 16	impbii	⊢ ( 𝑇 ∈ dom adjℎ ↔ ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ )