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

Proof

Step Hyp Ref Expression
` |-  ( 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`
` |-  ( (/) e. dom adjh -> (/) : ~H --> ~H )`
` |-  -. (/) e. dom adjh`
` |-  ( -. T e. dom adjh -> ( adjh ` T ) = (/) )`
` |-  ( -. T e. dom adjh -> ( ( adjh ` T ) e. dom adjh <-> (/) e. dom adjh ) )`
` |-  ( -. T e. dom adjh -> -. ( adjh ` T ) e. dom adjh )`
` |-  ( ( adjh ` T ) e. dom adjh -> T e. dom adjh )`
` |-  ( T e. dom adjh <-> ( adjh ` T ) e. dom adjh )`