Metamath Proof Explorer

Theorem idhmop

Description: The Hilbert space identity operator is a Hermitian operator. (Contributed by NM, 22-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion idhmop 
|- Iop e. HrmOp

Proof

Step Hyp Ref Expression
1 hoif 
 |-  Iop : ~H -1-1-onto-> ~H
2 f1of 
 |-  ( Iop : ~H -1-1-onto-> ~H -> Iop : ~H --> ~H )
3 1 2 ax-mp 
 |-  Iop : ~H --> ~H
4 hoival 
 |-  ( x e. ~H -> ( Iop ` x ) = x )
5 4 eqcomd 
 |-  ( x e. ~H -> x = ( Iop ` x ) )
6 hoival 
 |-  ( y e. ~H -> ( Iop ` y ) = y )
7 5 6 oveqan12d 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( x .ih ( Iop ` y ) ) = ( ( Iop ` x ) .ih y ) )
8 7 rgen2 
 |-  A. x e. ~H A. y e. ~H ( x .ih ( Iop ` y ) ) = ( ( Iop ` x ) .ih y )
9 elhmop 
 |-  ( Iop e. HrmOp <-> ( Iop : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( Iop ` y ) ) = ( ( Iop ` x ) .ih y ) ) )
10 3 8 9 mpbir2an 
 |-  Iop e. HrmOp