This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )