Theorem idleop

Description: The identity operator is a positive operator. Part of Example 12.2(i) in Young p. 142. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	idleop	|- 0hop <_op Iop

Proof

Step	Hyp	Ref	Expression
1		0hmop	|- 0hop e. HrmOp
2		idhmop	|- Iop e. HrmOp
3		leop2	|- ( ( 0hop e. HrmOp /\ Iop e. HrmOp ) -> ( 0hop <_op Iop <-> A. x e. ~H ( ( 0hop ` x ) .ih x ) <_ ( ( Iop ` x ) .ih x ) ) )
4	1 2 3	mp2an	|- ( 0hop <_op Iop <-> A. x e. ~H ( ( 0hop ` x ) .ih x ) <_ ( ( Iop ` x ) .ih x ) )
5		hiidge0	|- ( x e. ~H -> 0 <_ ( x .ih x ) )
6		ho0val	|- ( x e. ~H -> ( 0hop ` x ) = 0h )
7	6	oveq1d	|- ( x e. ~H -> ( ( 0hop ` x ) .ih x ) = ( 0h .ih x ) )
8		hi01	|- ( x e. ~H -> ( 0h .ih x ) = 0 )
9	7 8	eqtrd	|- ( x e. ~H -> ( ( 0hop ` x ) .ih x ) = 0 )
10		hoival	|- ( x e. ~H -> ( Iop ` x ) = x )
11	10	oveq1d	|- ( x e. ~H -> ( ( Iop ` x ) .ih x ) = ( x .ih x ) )
12	5 9 11	3brtr4d	|- ( x e. ~H -> ( ( 0hop ` x ) .ih x ) <_ ( ( Iop ` x ) .ih x ) )
13	4 12	mprgbir	|- 0hop <_op Iop