Metamath Proof Explorer

Theorem leoprf

Description: The ordering relation for operators is reflexive. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion leoprf ⊢T∈HrmOp→T≤opT

Proof

Step Hyp Ref Expression
1 0le0 ⊢0≤0
2 hmopf ⊢T∈HrmOp→T:ℋ⟶ℋ
3 hodid ⊢T:ℋ⟶ℋ→T-opT=0hop
4 2 3 syl ⊢T∈HrmOp→T-opT=0hop
5 4 adantr ⊢T∈HrmOp∧x∈ℋ→T-opT=0hop
6 5 fveq1d ⊢T∈HrmOp∧x∈ℋ→T-opT⁡x=0hop⁡x
7 ho0val ⊢x∈ℋ→0hop⁡x=0ℎ
8 7 adantl ⊢T∈HrmOp∧x∈ℋ→0hop⁡x=0ℎ
9 6 8 eqtrd ⊢T∈HrmOp∧x∈ℋ→T-opT⁡x=0ℎ
10 9 oveq1d ⊢T∈HrmOp∧x∈ℋ→T-opT⁡x⋅ihx=0ℎ⋅ihx
11 hi01 ⊢x∈ℋ→0ℎ⋅ihx=0
12 11 adantl ⊢T∈HrmOp∧x∈ℋ→0ℎ⋅ihx=0
13 10 12 eqtr2d ⊢T∈HrmOp∧x∈ℋ→0=T-opT⁡x⋅ihx
14 1 13 breqtrid ⊢T∈HrmOp∧x∈ℋ→0≤T-opT⁡x⋅ihx
15 14 ralrimiva ⊢T∈HrmOp→∀x∈ℋ0≤T-opT⁡x⋅ihx
16 leop ⊢T∈HrmOp∧T∈HrmOp→T≤opT↔∀x∈ℋ0≤T-opT⁡x⋅ihx
17 16 anidms ⊢T∈HrmOp→T≤opT↔∀x∈ℋ0≤T-opT⁡x⋅ihx
18 15 17 mpbird ⊢T∈HrmOp→T≤opT