# Metamath Proof Explorer

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 ${⊢}{T}\in \mathrm{dom}{adj}_{h}↔{adj}_{h}\left({T}\right)\in \mathrm{dom}{adj}_{h}$

### Proof

Step Hyp Ref Expression
1 dmadjrn ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to {adj}_{h}\left({T}\right)\in \mathrm{dom}{adj}_{h}$
2 ax-hv0cl ${⊢}{0}_{ℎ}\in ℋ$
3 2 n0ii ${⊢}¬ℋ=\varnothing$
4 eqcom ${⊢}\varnothing =ℋ↔ℋ=\varnothing$
5 3 4 mtbir ${⊢}¬\varnothing =ℋ$
6 dm0 ${⊢}\mathrm{dom}\varnothing =\varnothing$
7 6 eqeq1i ${⊢}\mathrm{dom}\varnothing =ℋ↔\varnothing =ℋ$
8 5 7 mtbir ${⊢}¬\mathrm{dom}\varnothing =ℋ$
9 fdm ${⊢}\varnothing :ℋ⟶ℋ\to \mathrm{dom}\varnothing =ℋ$
10 8 9 mto ${⊢}¬\varnothing :ℋ⟶ℋ$
11 dmadjop ${⊢}\varnothing \in \mathrm{dom}{adj}_{h}\to \varnothing :ℋ⟶ℋ$
12 10 11 mto ${⊢}¬\varnothing \in \mathrm{dom}{adj}_{h}$
13 ndmfv ${⊢}¬{T}\in \mathrm{dom}{adj}_{h}\to {adj}_{h}\left({T}\right)=\varnothing$
14 13 eleq1d ${⊢}¬{T}\in \mathrm{dom}{adj}_{h}\to \left({adj}_{h}\left({T}\right)\in \mathrm{dom}{adj}_{h}↔\varnothing \in \mathrm{dom}{adj}_{h}\right)$
15 12 14 mtbiri ${⊢}¬{T}\in \mathrm{dom}{adj}_{h}\to ¬{adj}_{h}\left({T}\right)\in \mathrm{dom}{adj}_{h}$
16 15 con4i ${⊢}{adj}_{h}\left({T}\right)\in \mathrm{dom}{adj}_{h}\to {T}\in \mathrm{dom}{adj}_{h}$
17 1 16 impbii ${⊢}{T}\in \mathrm{dom}{adj}_{h}↔{adj}_{h}\left({T}\right)\in \mathrm{dom}{adj}_{h}$