Step |
Hyp |
Ref |
Expression |
1 |
|
0hmop |
⊢ 0hop ∈ HrmOp |
2 |
|
leop |
⊢ ( ( 0hop ∈ HrmOp ∧ 𝑇 ∈ HrmOp ) → ( 0hop ≤op 𝑇 ↔ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑇 −op 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) ) ) |
3 |
1 2
|
mpan |
⊢ ( 𝑇 ∈ HrmOp → ( 0hop ≤op 𝑇 ↔ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑇 −op 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) ) ) |
4 |
|
hmopf |
⊢ ( 𝑇 ∈ HrmOp → 𝑇 : ℋ ⟶ ℋ ) |
5 |
|
hosubid1 |
⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇 −op 0hop ) = 𝑇 ) |
6 |
4 5
|
syl |
⊢ ( 𝑇 ∈ HrmOp → ( 𝑇 −op 0hop ) = 𝑇 ) |
7 |
6
|
fveq1d |
⊢ ( 𝑇 ∈ HrmOp → ( ( 𝑇 −op 0hop ) ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) ) |
8 |
7
|
oveq1d |
⊢ ( 𝑇 ∈ HrmOp → ( ( ( 𝑇 −op 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ) |
9 |
8
|
breq2d |
⊢ ( 𝑇 ∈ HrmOp → ( 0 ≤ ( ( ( 𝑇 −op 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ 0 ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ) ) |
10 |
9
|
ralbidv |
⊢ ( 𝑇 ∈ HrmOp → ( ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑇 −op 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ) ) |
11 |
3 10
|
bitrd |
⊢ ( 𝑇 ∈ HrmOp → ( 0hop ≤op 𝑇 ↔ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ) ) |