Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  orngmullt Structured version   Visualization version   GIF version

Theorem orngmullt 31808
Description: In an ordered ring, the strict ordering is compatible with the ring multiplication operation. (Contributed by Thierry Arnoux, 9-Sep-2018.)
Hypotheses
Ref Expression
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
Ref Expression
orngmullt (𝜑0 < (𝑋 · 𝑌))

Proof of Theorem orngmullt
StepHypRef Expression
1 orngmullt.1 . . 3 (𝜑𝑅 ∈ oRing)
2 orngmullt.2 . . 3 (𝜑𝑋𝐵)
3 orngmullt.x . . . . 5 (𝜑0 < 𝑋)
4 orngring 31799 . . . . . . 7 (𝑅 ∈ oRing → 𝑅 ∈ Ring)
5 ringgrp 19884 . . . . . . 7 (𝑅 ∈ Ring → 𝑅 ∈ Grp)
6 orngmullt.b . . . . . . . 8 𝐵 = (Base‘𝑅)
7 orngmullt.0 . . . . . . . 8 0 = (0g𝑅)
86, 7grpidcl 18704 . . . . . . 7 (𝑅 ∈ Grp → 0𝐵)
91, 4, 5, 84syl 19 . . . . . 6 (𝜑0𝐵)
10 eqid 2736 . . . . . . 7 (le‘𝑅) = (le‘𝑅)
11 orngmullt.l . . . . . . 7 < = (lt‘𝑅)
1210, 11pltval 18148 . . . . . 6 ((𝑅 ∈ oRing ∧ 0𝐵𝑋𝐵) → ( 0 < 𝑋 ↔ ( 0 (le‘𝑅)𝑋0𝑋)))
131, 9, 2, 12syl3anc 1370 . . . . 5 (𝜑 → ( 0 < 𝑋 ↔ ( 0 (le‘𝑅)𝑋0𝑋)))
143, 13mpbid 231 . . . 4 (𝜑 → ( 0 (le‘𝑅)𝑋0𝑋))
1514simpld 495 . . 3 (𝜑0 (le‘𝑅)𝑋)
16 orngmullt.3 . . 3 (𝜑𝑌𝐵)
17 orngmullt.y . . . . 5 (𝜑0 < 𝑌)
1810, 11pltval 18148 . . . . . 6 ((𝑅 ∈ oRing ∧ 0𝐵𝑌𝐵) → ( 0 < 𝑌 ↔ ( 0 (le‘𝑅)𝑌0𝑌)))
191, 9, 16, 18syl3anc 1370 . . . . 5 (𝜑 → ( 0 < 𝑌 ↔ ( 0 (le‘𝑅)𝑌0𝑌)))
2017, 19mpbid 231 . . . 4 (𝜑 → ( 0 (le‘𝑅)𝑌0𝑌))
2120simpld 495 . . 3 (𝜑0 (le‘𝑅)𝑌)
22 orngmullt.t . . . 4 · = (.r𝑅)
236, 10, 7, 22orngmul 31802 . . 3 ((𝑅 ∈ oRing ∧ (𝑋𝐵0 (le‘𝑅)𝑋) ∧ (𝑌𝐵0 (le‘𝑅)𝑌)) → 0 (le‘𝑅)(𝑋 · 𝑌))
241, 2, 15, 16, 21, 23syl122anc 1378 . 2 (𝜑0 (le‘𝑅)(𝑋 · 𝑌))
2514simprd 496 . . . . 5 (𝜑0𝑋)
2625necomd 2996 . . . 4 (𝜑𝑋0 )
2720simprd 496 . . . . 5 (𝜑0𝑌)
2827necomd 2996 . . . 4 (𝜑𝑌0 )
29 orngmullt.4 . . . . 5 (𝜑𝑅 ∈ DivRing)
306, 7, 22, 29, 2, 16drngmulne0 20119 . . . 4 (𝜑 → ((𝑋 · 𝑌) ≠ 0 ↔ (𝑋0𝑌0 )))
3126, 28, 30mpbir2and 710 . . 3 (𝜑 → (𝑋 · 𝑌) ≠ 0 )
3231necomd 2996 . 2 (𝜑0 ≠ (𝑋 · 𝑌))
331, 4syl 17 . . . 4 (𝜑𝑅 ∈ Ring)
346, 22ringcl 19896 . . . 4 ((𝑅 ∈ Ring ∧ 𝑋𝐵𝑌𝐵) → (𝑋 · 𝑌) ∈ 𝐵)
3533, 2, 16, 34syl3anc 1370 . . 3 (𝜑 → (𝑋 · 𝑌) ∈ 𝐵)
3610, 11pltval 18148 . . 3 ((𝑅 ∈ oRing ∧ 0𝐵 ∧ (𝑋 · 𝑌) ∈ 𝐵) → ( 0 < (𝑋 · 𝑌) ↔ ( 0 (le‘𝑅)(𝑋 · 𝑌) ∧ 0 ≠ (𝑋 · 𝑌))))
371, 9, 35, 36syl3anc 1370 . 2 (𝜑 → ( 0 < (𝑋 · 𝑌) ↔ ( 0 (le‘𝑅)(𝑋 · 𝑌) ∧ 0 ≠ (𝑋 · 𝑌))))
3824, 32, 37mpbir2and 710 1 (𝜑0 < (𝑋 · 𝑌))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1540  wcel 2105  wne 2940   class class class wbr 5093  cfv 6480  (class class class)co 7338  Basecbs 17010  .rcmulr 17061  lecple 17067  0gc0g 17248  ltcplt 18124  Grpcgrp 18674  Ringcrg 19879  DivRingcdr 20094  oRingcorng 31794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5230  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651  ax-cnex 11029  ax-resscn 11030  ax-1cn 11031  ax-icn 11032  ax-addcl 11033  ax-addrcl 11034  ax-mulcl 11035  ax-mulrcl 11036  ax-mulcom 11037  ax-addass 11038  ax-mulass 11039  ax-distr 11040  ax-i2m1 11041  ax-1ne0 11042  ax-1rid 11043  ax-rnegex 11044  ax-rrecex 11045  ax-cnre 11046  ax-pre-lttri 11047  ax-pre-lttrn 11048  ax-pre-ltadd 11049  ax-pre-mulgt0 11050
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4854  df-iun 4944  df-br 5094  df-opab 5156  df-mpt 5177  df-tr 5211  df-id 5519  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5576  df-we 5578  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6239  df-ord 6306  df-on 6307  df-lim 6308  df-suc 6309  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-riota 7294  df-ov 7341  df-oprab 7342  df-mpo 7343  df-om 7782  df-2nd 7901  df-tpos 8113  df-frecs 8168  df-wrecs 8199  df-recs 8273  df-rdg 8312  df-er 8570  df-en 8806  df-dom 8807  df-sdom 8808  df-pnf 11113  df-mnf 11114  df-xr 11115  df-ltxr 11116  df-le 11117  df-sub 11309  df-neg 11310  df-nn 12076  df-2 12138  df-3 12139  df-sets 16963  df-slot 16981  df-ndx 16993  df-base 17011  df-ress 17040  df-plusg 17073  df-mulr 17074  df-0g 17250  df-plt 18146  df-mgm 18424  df-sgrp 18473  df-mnd 18484  df-grp 18677  df-minusg 18678  df-mgp 19817  df-ur 19834  df-ring 19881  df-oppr 19958  df-dvdsr 19979  df-unit 19980  df-invr 20010  df-drng 20096  df-orng 31796
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator