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 |