Theorem orngmul

Description: In an ordered ring, the ordering is compatible with the ring multiplication operation. (Contributed by Thierry Arnoux, 20-Jan-2018)

	Ref	Expression
Hypotheses	orngmul.0	⊢ 𝐵 = ( Base ‘ 𝑅 )
	orngmul.1	⊢ ≤ = ( le ‘ 𝑅 )
	orngmul.2	⊢ 0 = ( 0g ‘ 𝑅 )
	orngmul.3	⊢ · = ( .r ‘ 𝑅 )
Assertion	orngmul	⊢ ( ( 𝑅 ∈ oRing ∧ ( 𝑋 ∈ 𝐵 ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 0 ≤ 𝑌 ) ) → 0 ≤ ( 𝑋 · 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		orngmul.0	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		orngmul.1	⊢ ≤ = ( le ‘ 𝑅 )
3		orngmul.2	⊢ 0 = ( 0g ‘ 𝑅 )
4		orngmul.3	⊢ · = ( .r ‘ 𝑅 )
5		simp2r	⊢ ( ( 𝑅 ∈ oRing ∧ ( 𝑋 ∈ 𝐵 ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 0 ≤ 𝑌 ) ) → 0 ≤ 𝑋 )
6		simp3r	⊢ ( ( 𝑅 ∈ oRing ∧ ( 𝑋 ∈ 𝐵 ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 0 ≤ 𝑌 ) ) → 0 ≤ 𝑌 )
7		simp2l	⊢ ( ( 𝑅 ∈ oRing ∧ ( 𝑋 ∈ 𝐵 ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 0 ≤ 𝑌 ) ) → 𝑋 ∈ 𝐵 )
8		simp3l	⊢ ( ( 𝑅 ∈ oRing ∧ ( 𝑋 ∈ 𝐵 ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 0 ≤ 𝑌 ) ) → 𝑌 ∈ 𝐵 )
9	1 3 4 2	isorng	⊢ ( 𝑅 ∈ oRing ↔ ( 𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏 ) → 0 ≤ ( 𝑎 · 𝑏 ) ) ) )
10	9	simp3bi	⊢ ( 𝑅 ∈ oRing → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏 ) → 0 ≤ ( 𝑎 · 𝑏 ) ) )
11	10	3ad2ant1	⊢ ( ( 𝑅 ∈ oRing ∧ ( 𝑋 ∈ 𝐵 ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 0 ≤ 𝑌 ) ) → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏 ) → 0 ≤ ( 𝑎 · 𝑏 ) ) )
12		breq2	⊢ ( 𝑎 = 𝑋 → ( 0 ≤ 𝑎 ↔ 0 ≤ 𝑋 ) )
13	12	anbi1d	⊢ ( 𝑎 = 𝑋 → ( ( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏 ) ↔ ( 0 ≤ 𝑋 ∧ 0 ≤ 𝑏 ) ) )
14		oveq1	⊢ ( 𝑎 = 𝑋 → ( 𝑎 · 𝑏 ) = ( 𝑋 · 𝑏 ) )
15	14	breq2d	⊢ ( 𝑎 = 𝑋 → ( 0 ≤ ( 𝑎 · 𝑏 ) ↔ 0 ≤ ( 𝑋 · 𝑏 ) ) )
16	13 15	imbi12d	⊢ ( 𝑎 = 𝑋 → ( ( ( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏 ) → 0 ≤ ( 𝑎 · 𝑏 ) ) ↔ ( ( 0 ≤ 𝑋 ∧ 0 ≤ 𝑏 ) → 0 ≤ ( 𝑋 · 𝑏 ) ) ) )
17		breq2	⊢ ( 𝑏 = 𝑌 → ( 0 ≤ 𝑏 ↔ 0 ≤ 𝑌 ) )
18	17	anbi2d	⊢ ( 𝑏 = 𝑌 → ( ( 0 ≤ 𝑋 ∧ 0 ≤ 𝑏 ) ↔ ( 0 ≤ 𝑋 ∧ 0 ≤ 𝑌 ) ) )
19		oveq2	⊢ ( 𝑏 = 𝑌 → ( 𝑋 · 𝑏 ) = ( 𝑋 · 𝑌 ) )
20	19	breq2d	⊢ ( 𝑏 = 𝑌 → ( 0 ≤ ( 𝑋 · 𝑏 ) ↔ 0 ≤ ( 𝑋 · 𝑌 ) ) )
21	18 20	imbi12d	⊢ ( 𝑏 = 𝑌 → ( ( ( 0 ≤ 𝑋 ∧ 0 ≤ 𝑏 ) → 0 ≤ ( 𝑋 · 𝑏 ) ) ↔ ( ( 0 ≤ 𝑋 ∧ 0 ≤ 𝑌 ) → 0 ≤ ( 𝑋 · 𝑌 ) ) ) )
22	16 21	rspc2va	⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏 ) → 0 ≤ ( 𝑎 · 𝑏 ) ) ) → ( ( 0 ≤ 𝑋 ∧ 0 ≤ 𝑌 ) → 0 ≤ ( 𝑋 · 𝑌 ) ) )
23	7 8 11 22	syl21anc	⊢ ( ( 𝑅 ∈ oRing ∧ ( 𝑋 ∈ 𝐵 ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 0 ≤ 𝑌 ) ) → ( ( 0 ≤ 𝑋 ∧ 0 ≤ 𝑌 ) → 0 ≤ ( 𝑋 · 𝑌 ) ) )
24	5 6 23	mp2and	⊢ ( ( 𝑅 ∈ oRing ∧ ( 𝑋 ∈ 𝐵 ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 0 ≤ 𝑌 ) ) → 0 ≤ ( 𝑋 · 𝑌 ) )