Theorem leoprf2

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

	Ref	Expression
Assertion	leoprf2	⊢ ( 𝑇 : ℋ ⟶ ℋ → 𝑇 ≤op 𝑇 )

Proof

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