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 0hopop Iop

Proof

Step Hyp Ref Expression
1 0hmop 0hop ∈ HrmOp
2 idhmop Iop ∈ HrmOp
3 leop2 ( ( 0hop ∈ HrmOp ∧ Iop ∈ HrmOp ) → ( 0hopop Iop ↔ ∀ 𝑥 ∈ ℋ ( ( 0hop𝑥 ) ·ih 𝑥 ) ≤ ( ( Iop𝑥 ) ·ih 𝑥 ) ) )
4 1 2 3 mp2an ( 0hopop Iop ↔ ∀ 𝑥 ∈ ℋ ( ( 0hop𝑥 ) ·ih 𝑥 ) ≤ ( ( Iop𝑥 ) ·ih 𝑥 ) )
5 hiidge0 ( 𝑥 ∈ ℋ → 0 ≤ ( 𝑥 ·ih 𝑥 ) )
6 ho0val ( 𝑥 ∈ ℋ → ( 0hop𝑥 ) = 0 )
7 6 oveq1d ( 𝑥 ∈ ℋ → ( ( 0hop𝑥 ) ·ih 𝑥 ) = ( 0 ·ih 𝑥 ) )
8 hi01 ( 𝑥 ∈ ℋ → ( 0 ·ih 𝑥 ) = 0 )
9 7 8 eqtrd ( 𝑥 ∈ ℋ → ( ( 0hop𝑥 ) ·ih 𝑥 ) = 0 )
10 hoival ( 𝑥 ∈ ℋ → ( Iop𝑥 ) = 𝑥 )
11 10 oveq1d ( 𝑥 ∈ ℋ → ( ( Iop𝑥 ) ·ih 𝑥 ) = ( 𝑥 ·ih 𝑥 ) )
12 5 9 11 3brtr4d ( 𝑥 ∈ ℋ → ( ( 0hop𝑥 ) ·ih 𝑥 ) ≤ ( ( Iop𝑥 ) ·ih 𝑥 ) )
13 4 12 mprgbir 0hopop Iop