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 e. dom adjh <-> ( adjh ` T ) e. dom adjh )

Proof

Step	Hyp	Ref	Expression
1		dmadjrn	|- ( T e. dom adjh -> ( adjh ` T ) e. dom adjh )
2		ax-hv0cl	|- 0h e. ~H
3	2	n0ii	|- -. ~H = (/)
4		eqcom	|- ( (/) = ~H <-> ~H = (/) )
5	3 4	mtbir	|- -. (/) = ~H
6		dm0	|- dom (/) = (/)
7	6	eqeq1i	|- ( dom (/) = ~H <-> (/) = ~H )
8	5 7	mtbir	|- -. dom (/) = ~H
9		fdm	|- ( (/) : ~H --> ~H -> dom (/) = ~H )
10	8 9	mto	|- -. (/) : ~H --> ~H
11		dmadjop	|- ( (/) e. dom adjh -> (/) : ~H --> ~H )
12	10 11	mto	|- -. (/) e. dom adjh
13		ndmfv	|- ( -. T e. dom adjh -> ( adjh ` T ) = (/) )
14	13	eleq1d	|- ( -. T e. dom adjh -> ( ( adjh ` T ) e. dom adjh <-> (/) e. dom adjh ) )
15	12 14	mtbiri	|- ( -. T e. dom adjh -> -. ( adjh ` T ) e. dom adjh )
16	15	con4i	|- ( ( adjh ` T ) e. dom adjh -> T e. dom adjh )
17	1 16	impbii	|- ( T e. dom adjh <-> ( adjh ` T ) e. dom adjh )