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 ∈ HrmOp
2		idhmop	⊢ Iop ∈ HrmOp
3		leop2	⊢ ( ( 0hop ∈ HrmOp ∧ Iop ∈ HrmOp ) → ( 0hop ≤op Iop ↔ ∀ 𝑥 ∈ ℋ ( ( 0hop ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( Iop ‘ 𝑥 ) ·ih 𝑥 ) ) )
4	1 2 3	mp2an	⊢ ( 0hop ≤op 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	⊢ 0hop ≤op Iop