Metamath Proof Explorer

Theorem leoprf2

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

Ref Expression
Assertion leoprf2 ⊢ T : ℋ ⟶ ℋ → T ≤ op T

Proof

Step Hyp Ref Expression
1 hodid ⊢ T : ℋ ⟶ ℋ → T - op T = 0 hop
2 0hmop ⊢ 0 hop ∈ HrmOp
3 1 2 eqeltrdi ⊢ T : ℋ ⟶ ℋ → T - op T ∈ HrmOp
4 0le0 ⊢ 0 ≤ 0
5 1 adantr ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → T - op T = 0 hop
6 5 fveq1d ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → T - op T ⁡ x = 0 hop ⁡ x
7 ho0val ⊢ x ∈ ℋ → 0 hop ⁡ x = 0 ℎ
8 7 adantl ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → 0 hop ⁡ x = 0 ℎ
9 6 8 eqtrd ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → T - op T ⁡ x = 0 ℎ
10 9 oveq1d ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → T - op T ⁡ x ⋅ ih x = 0 ℎ ⋅ ih x
11 hi01 ⊢ x ∈ ℋ → 0 ℎ ⋅ ih x = 0
12 11 adantl ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → 0 ℎ ⋅ ih x = 0
13 10 12 eqtr2d ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → 0 = T - op T ⁡ x ⋅ ih x
14 4 13 breqtrid ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → 0 ≤ T - op T ⁡ x ⋅ ih x
15 14 ralrimiva ⊢ T : ℋ ⟶ ℋ → ∀ x ∈ ℋ 0 ≤ T - op T ⁡ x ⋅ ih x
16 ax-hilex ⊢ ℋ ∈ V
17 fex ⊢ T : ℋ ⟶ ℋ ∧ ℋ ∈ V → T ∈ V
18 16 17 mpan2 ⊢ T : ℋ ⟶ ℋ → T ∈ V
19 leopg ⊢ T ∈ V ∧ T ∈ V → T ≤ op T ↔ T - op T ∈ HrmOp ∧ ∀ x ∈ ℋ 0 ≤ T - op T ⁡ x ⋅ ih x
20 18 18 19 syl2anc ⊢ T : ℋ ⟶ ℋ → T ≤ op T ↔ T - op T ∈ HrmOp ∧ ∀ x ∈ ℋ 0 ≤ T - op T ⁡ x ⋅ ih x
21 3 15 20 mpbir2and ⊢ T : ℋ ⟶ ℋ → T ≤ op T