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≤opT

Proof

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