Metamath Proof Explorer

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 ≤ ( 𝑋 · 𝑌 ) )