Metamath Proof Explorer

Theorem 0hmop

Description: The identically zero function is a Hermitian operator. (Contributed by NM, 8-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion 0hmop 
|- 0hop e. HrmOp

Proof

Step Hyp Ref Expression
1 ho0f 
 |-  0hop : ~H --> ~H
2 ho0val 
 |-  ( y e. ~H -> ( 0hop ` y ) = 0h )
3 2 oveq2d 
 |-  ( y e. ~H -> ( x .ih ( 0hop ` y ) ) = ( x .ih 0h ) )
4 hi02 
 |-  ( x e. ~H -> ( x .ih 0h ) = 0 )
5 3 4 sylan9eqr 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( x .ih ( 0hop ` y ) ) = 0 )
6 ho0val 
 |-  ( x e. ~H -> ( 0hop ` x ) = 0h )
7 6 oveq1d 
 |-  ( x e. ~H -> ( ( 0hop ` x ) .ih y ) = ( 0h .ih y ) )
8 hi01 
 |-  ( y e. ~H -> ( 0h .ih y ) = 0 )
9 7 8 sylan9eq 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( 0hop ` x ) .ih y ) = 0 )
10 5 9 eqtr4d 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( x .ih ( 0hop ` y ) ) = ( ( 0hop ` x ) .ih y ) )
11 10 rgen2 
 |-  A. x e. ~H A. y e. ~H ( x .ih ( 0hop ` y ) ) = ( ( 0hop ` x ) .ih y )
12 elhmop 
 |-  ( 0hop e. HrmOp <-> ( 0hop : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( 0hop ` y ) ) = ( ( 0hop ` x ) .ih y ) ) )
13 1 11 12 mpbir2an 
 |-  0hop e. HrmOp