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	$$⊢T\in \mathrm{dom}{adj}_h\leftrightarrow {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 \mathscr{H}$$
3	2	n0ii	$$⊢\neg \mathscr{H}=\varnothing$$
4		eqcom	$$⊢\varnothing =\mathscr{H}\leftrightarrow \mathscr{H}=\varnothing$$
5	3 4	mtbir	$$⊢\neg \varnothing =\mathscr{H}$$
6		dm0	$$⊢\mathrm{dom}\varnothing =\varnothing$$
7	6	eqeq1i	$$⊢\mathrm{dom}\varnothing =\mathscr{H}\leftrightarrow \varnothing =\mathscr{H}$$
8	5 7	mtbir	$$⊢\neg \mathrm{dom}\varnothing =\mathscr{H}$$
9		fdm	$$⊢\varnothing :\mathscr{H}⟶\mathscr{H}\to \mathrm{dom}\varnothing =\mathscr{H}$$
10	8 9	mto	$$⊢\neg \varnothing :\mathscr{H}⟶\mathscr{H}$$
11		dmadjop	$$⊢\varnothing \in \mathrm{dom}{adj}_h\to \varnothing :\mathscr{H}⟶\mathscr{H}$$
12	10 11	mto	$$⊢\neg \varnothing \in \mathrm{dom}{adj}_h$$
13		ndmfv	$$⊢\neg T\in \mathrm{dom}{adj}_h\to {adj}_h\left(T\right)=\varnothing$$
14	13	eleq1d	$$⊢\neg T\in \mathrm{dom}{adj}_h\to \left({adj}_h\left(T\right)\in \mathrm{dom}{adj}_h\leftrightarrow \varnothing \in \mathrm{dom}{adj}_h\right)$$
15	12 14	mtbiri	$$⊢\neg T\in \mathrm{dom}{adj}_h\to \neg {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\leftrightarrow {adj}_h\left(T\right)\in \mathrm{dom}{adj}_h$$