This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem orngmullt

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

Ref Expression
Hypotheses orngmullt.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
orngmullt.t ⊢ · = ( .r ‘ 𝑅 )
orngmullt.0 ⊢ 0 = ( 0g ‘ 𝑅 )
orngmullt.l ⊢ < = ( lt ‘ 𝑅 )
orngmullt.1 ⊢ ( 𝜑 → 𝑅 ∈ oRing )
orngmullt.4 ⊢ ( 𝜑 → 𝑅 ∈ DivRing )
orngmullt.2 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
orngmullt.3 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
orngmullt.x ⊢ ( 𝜑 → 0 < 𝑋 )
orngmullt.y ⊢ ( 𝜑 → 0 < 𝑌 )
Assertion orngmullt ( 𝜑 → 0 < ( 𝑋 · 𝑌 ) )

Proof

Step Hyp Ref Expression
1 orngmullt.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 orngmullt.t ⊢ · = ( .r ‘ 𝑅 )
3 orngmullt.0 ⊢ 0 = ( 0g ‘ 𝑅 )
4 orngmullt.l ⊢ < = ( lt ‘ 𝑅 )
5 orngmullt.1 ⊢ ( 𝜑 → 𝑅 ∈ oRing )
6 orngmullt.4 ⊢ ( 𝜑 → 𝑅 ∈ DivRing )
7 orngmullt.2 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8 orngmullt.3 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9 orngmullt.x ⊢ ( 𝜑 → 0 < 𝑋 )
10 orngmullt.y ⊢ ( 𝜑 → 0 < 𝑌 )
11 orngring ⊢ ( 𝑅 ∈ oRing → 𝑅 ∈ Ring )
12 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
13 1 3 grpidcl ⊢ ( 𝑅 ∈ Grp → 0 ∈ 𝐵 )
14 5 11 12 13 4syl ⊢ ( 𝜑 → 0 ∈ 𝐵 )
15 eqid ⊢ ( le ‘ 𝑅 ) = ( le ‘ 𝑅 )
16 15 4 pltval ⊢ ( ( 𝑅 ∈ oRing ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 0 < 𝑋 ↔ ( 0 ( le ‘ 𝑅 ) 𝑋 ∧ 0 ≠ 𝑋 ) ) )
17 5 14 7 16 syl3anc ⊢ ( 𝜑 → ( 0 < 𝑋 ↔ ( 0 ( le ‘ 𝑅 ) 𝑋 ∧ 0 ≠ 𝑋 ) ) )
18 9 17 mpbid ⊢ ( 𝜑 → ( 0 ( le ‘ 𝑅 ) 𝑋 ∧ 0 ≠ 𝑋 ) )
19 18 simpld ⊢ ( 𝜑 → 0 ( le ‘ 𝑅 ) 𝑋 )
20 15 4 pltval ⊢ ( ( 𝑅 ∈ oRing ∧ 0 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 0 < 𝑌 ↔ ( 0 ( le ‘ 𝑅 ) 𝑌 ∧ 0 ≠ 𝑌 ) ) )
21 5 14 8 20 syl3anc ⊢ ( 𝜑 → ( 0 < 𝑌 ↔ ( 0 ( le ‘ 𝑅 ) 𝑌 ∧ 0 ≠ 𝑌 ) ) )
22 10 21 mpbid ⊢ ( 𝜑 → ( 0 ( le ‘ 𝑅 ) 𝑌 ∧ 0 ≠ 𝑌 ) )
23 22 simpld ⊢ ( 𝜑 → 0 ( le ‘ 𝑅 ) 𝑌 )
24 1 15 3 2 orngmul ⊢ ( ( 𝑅 ∈ oRing ∧ ( 𝑋 ∈ 𝐵 ∧ 0 ( le ‘ 𝑅 ) 𝑋 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 0 ( le ‘ 𝑅 ) 𝑌 ) ) → 0 ( le ‘ 𝑅 ) ( 𝑋 · 𝑌 ) )
25 5 7 19 8 23 24 syl122anc ⊢ ( 𝜑 → 0 ( le ‘ 𝑅 ) ( 𝑋 · 𝑌 ) )
26 18 simprd ⊢ ( 𝜑 → 0 ≠ 𝑋 )
27 26 necomd ⊢ ( 𝜑 → 𝑋 ≠ 0 )
28 22 simprd ⊢ ( 𝜑 → 0 ≠ 𝑌 )
29 28 necomd ⊢ ( 𝜑 → 𝑌 ≠ 0 )
30 1 3 2 6 7 8 drngmulne0 ⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) ≠ 0 ↔ ( 𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ) ) )
31 27 29 30 mpbir2and ⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ≠ 0 )
32 31 necomd ⊢ ( 𝜑 → 0 ≠ ( 𝑋 · 𝑌 ) )
33 5 11 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
34 1 2 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
35 33 7 8 34 syl3anc ⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
36 15 4 pltval ⊢ ( ( 𝑅 ∈ oRing ∧ 0 ∈ 𝐵 ∧ ( 𝑋 · 𝑌 ) ∈ 𝐵 ) → ( 0 < ( 𝑋 · 𝑌 ) ↔ ( 0 ( le ‘ 𝑅 ) ( 𝑋 · 𝑌 ) ∧ 0 ≠ ( 𝑋 · 𝑌 ) ) ) )
37 5 14 35 36 syl3anc ⊢ ( 𝜑 → ( 0 < ( 𝑋 · 𝑌 ) ↔ ( 0 ( le ‘ 𝑅 ) ( 𝑋 · 𝑌 ) ∧ 0 ≠ ( 𝑋 · 𝑌 ) ) ) )
38 25 32 37 mpbir2and ⊢ ( 𝜑 → 0 < ( 𝑋 · 𝑌 ) )