Metamath Proof Explorer

Theorem hmdmadj

Description: Every Hermitian operator has an adjoint. (Contributed by NM, 24-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion hmdmadj 
|- ( T e. HrmOp -> T e. dom adjh )

Proof

Step Hyp Ref Expression
1 hmopf 
 |-  ( T e. HrmOp -> T : ~H --> ~H )
2 hon0 
 |-  ( T : ~H --> ~H -> -. T = (/) )
3 1 2 syl 
 |-  ( T e. HrmOp -> -. T = (/) )
4 hmopadj 
 |-  ( T e. HrmOp -> ( adjh ` T ) = T )
5 4 eqeq1d 
 |-  ( T e. HrmOp -> ( ( adjh ` T ) = (/) <-> T = (/) ) )
6 3 5 mtbird 
 |-  ( T e. HrmOp -> -. ( adjh ` T ) = (/) )
7 ndmfv 
 |-  ( -. T e. dom adjh -> ( adjh ` T ) = (/) )
8 6 7 nsyl2 
 |-  ( T e. HrmOp -> T e. dom adjh )