Metamath Proof Explorer

Theorem leoprf

Description: The ordering relation for operators is reflexive. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion leoprf 
|- ( T e. HrmOp -> T <_op T )

Proof

Step Hyp Ref Expression
1 0le0 
 |-  0 <_ 0
2 hmopf 
 |-  ( T e. HrmOp -> T : ~H --> ~H )
3 hodid 
 |-  ( T : ~H --> ~H -> ( T -op T ) = 0hop )
4 2 3 syl 
 |-  ( T e. HrmOp -> ( T -op T ) = 0hop )
5 4 adantr 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( T -op T ) = 0hop )
6 5 fveq1d 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( ( T -op T ) ` x ) = ( 0hop ` x ) )
7 ho0val 
 |-  ( x e. ~H -> ( 0hop ` x ) = 0h )
8 7 adantl 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( 0hop ` x ) = 0h )
9 6 8 eqtrd 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( ( T -op T ) ` x ) = 0h )
10 9 oveq1d 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( ( ( T -op T ) ` x ) .ih x ) = ( 0h .ih x ) )
11 hi01 
 |-  ( x e. ~H -> ( 0h .ih x ) = 0 )
12 11 adantl 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( 0h .ih x ) = 0 )
13 10 12 eqtr2d 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> 0 = ( ( ( T -op T ) ` x ) .ih x ) )
14 1 13 breqtrid 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> 0 <_ ( ( ( T -op T ) ` x ) .ih x ) )
15 14 ralrimiva 
 |-  ( T e. HrmOp -> A. x e. ~H 0 <_ ( ( ( T -op T ) ` x ) .ih x ) )
16 leop 
 |-  ( ( T e. HrmOp /\ T e. HrmOp ) -> ( T <_op T <-> A. x e. ~H 0 <_ ( ( ( T -op T ) ` x ) .ih x ) ) )
17 16 anidms 
 |-  ( T e. HrmOp -> ( T <_op T <-> A. x e. ~H 0 <_ ( ( ( T -op T ) ` x ) .ih x ) ) )
18 15 17 mpbird 
 |-  ( T e. HrmOp -> T <_op T )