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 ≤ op T

Proof

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