Metamath Proof Explorer

Theorem adj0

Description: Adjoint of the zero operator. (Contributed by NM, 20-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adj0 
|- ( adjh ` 0hop ) = 0hop

Proof

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