Metamath Proof Explorer


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 0 hop op I op

Proof

Step Hyp Ref Expression
1 0hmop 0 hop HrmOp
2 idhmop I op HrmOp
3 leop2 0 hop HrmOp I op HrmOp 0 hop op I op x 0 hop x ih x I op x ih x
4 1 2 3 mp2an 0 hop op I op x 0 hop x ih x I op x ih x
5 hiidge0 x 0 x ih x
6 ho0val x 0 hop x = 0
7 6 oveq1d x 0 hop x ih x = 0 ih x
8 hi01 x 0 ih x = 0
9 7 8 eqtrd x 0 hop x ih x = 0
10 hoival x I op x = x
11 10 oveq1d x I op x ih x = x ih x
12 5 9 11 3brtr4d x 0 hop x ih x I op x ih x
13 4 12 mprgbir 0 hop op I op