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

Theorem isorng 32094
Description: An ordered ring is a ring with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 18-Jan-2018.)
Hypotheses
Ref Expression
isorng.0 𝐵 = (Base‘𝑅)
isorng.1 0 = (0g𝑅)
isorng.2 · = (.r𝑅)
isorng.3 = (le‘𝑅)
Assertion
Ref Expression
isorng (𝑅 ∈ oRing ↔ (𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
Distinct variable groups:   𝑎,𝑏,𝐵   𝑅,𝑎,𝑏
Allowed substitution hints:   · (𝑎,𝑏)   (𝑎,𝑏)   0 (𝑎,𝑏)

Proof of Theorem isorng
Dummy variables 𝑙 𝑟 𝑡 𝑣 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elin 3926 . . 3 (𝑅 ∈ (Ring ∩ oGrp) ↔ (𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp))
21anbi1i 624 . 2 ((𝑅 ∈ (Ring ∩ oGrp) ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))) ↔ ((𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp) ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
3 fvexd 6857 . . . . 5 (𝑟 = 𝑅 → (.r𝑟) ∈ V)
4 simpr 485 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → 𝑡 = (.r𝑟))
5 simpl 483 . . . . . . . . . . . . 13 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → 𝑟 = 𝑅)
65fveq2d 6846 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → (.r𝑟) = (.r𝑅))
7 isorng.2 . . . . . . . . . . . 12 · = (.r𝑅)
86, 7eqtr4di 2794 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → (.r𝑟) = · )
94, 8eqtrd 2776 . . . . . . . . . 10 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → 𝑡 = · )
109oveqd 7374 . . . . . . . . 9 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → (𝑎𝑡𝑏) = (𝑎 · 𝑏))
1110breq2d 5117 . . . . . . . 8 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → ( 0 𝑙(𝑎𝑡𝑏) ↔ 0 𝑙(𝑎 · 𝑏)))
1211imbi2d 340 . . . . . . 7 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → ((( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏))))
13122ralbidv 3212 . . . . . 6 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → (∀𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏))))
1413sbcbidv 3798 . . . . 5 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → ([(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏))))
153, 14sbcied 3784 . . . 4 (𝑟 = 𝑅 → ([(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏))))
16 fvexd 6857 . . . . . 6 (𝑟 = 𝑅 → (Base‘𝑟) ∈ V)
17 simpr 485 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → 𝑣 = (Base‘𝑟))
18 fveq2 6842 . . . . . . . . . . . . 13 (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
19 isorng.0 . . . . . . . . . . . . 13 𝐵 = (Base‘𝑅)
2018, 19eqtr4di 2794 . . . . . . . . . . . 12 (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵)
2120adantr 481 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → (Base‘𝑟) = 𝐵)
2217, 21eqtrd 2776 . . . . . . . . . 10 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → 𝑣 = 𝐵)
23 raleq 3309 . . . . . . . . . . 11 (𝑣 = 𝐵 → (∀𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2423raleqbi1dv 3307 . . . . . . . . . 10 (𝑣 = 𝐵 → (∀𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2522, 24syl 17 . . . . . . . . 9 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → (∀𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2625sbcbidv 3798 . . . . . . . 8 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → ([(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2726sbcbidv 3798 . . . . . . 7 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → ([(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2827sbcbidv 3798 . . . . . 6 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → ([(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2916, 28sbcied 3784 . . . . 5 (𝑟 = 𝑅 → ([(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
30 fvexd 6857 . . . . . 6 (𝑟 = 𝑅 → (0g𝑟) ∈ V)
31 simpr 485 . . . . . . . . . . . . 13 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → 𝑧 = (0g𝑟))
32 fveq2 6842 . . . . . . . . . . . . . . 15 (𝑟 = 𝑅 → (0g𝑟) = (0g𝑅))
33 isorng.1 . . . . . . . . . . . . . . 15 0 = (0g𝑅)
3432, 33eqtr4di 2794 . . . . . . . . . . . . . 14 (𝑟 = 𝑅 → (0g𝑟) = 0 )
3534adantr 481 . . . . . . . . . . . . 13 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (0g𝑟) = 0 )
3631, 35eqtrd 2776 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → 𝑧 = 0 )
3736breq1d 5115 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (𝑧𝑙𝑎0 𝑙𝑎))
3836breq1d 5115 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (𝑧𝑙𝑏0 𝑙𝑏))
3937, 38anbi12d 631 . . . . . . . . . 10 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → ((𝑧𝑙𝑎𝑧𝑙𝑏) ↔ ( 0 𝑙𝑎0 𝑙𝑏)))
4036breq1d 5115 . . . . . . . . . 10 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (𝑧𝑙(𝑎𝑡𝑏) ↔ 0 𝑙(𝑎𝑡𝑏)))
4139, 40imbi12d 344 . . . . . . . . 9 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
42412ralbidv 3212 . . . . . . . 8 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (∀𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
4342sbcbidv 3798 . . . . . . 7 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → ([(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
4443sbcbidv 3798 . . . . . 6 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → ([(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
4530, 44sbcied 3784 . . . . 5 (𝑟 = 𝑅 → ([(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
4629, 45bitr2d 279 . . . 4 (𝑟 = 𝑅 → ([(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ [(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
47 fvexd 6857 . . . . 5 (𝑟 = 𝑅 → (le‘𝑟) ∈ V)
48 simpr 485 . . . . . . . . . 10 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → 𝑙 = (le‘𝑟))
49 simpl 483 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → 𝑟 = 𝑅)
5049fveq2d 6846 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → (le‘𝑟) = (le‘𝑅))
51 isorng.3 . . . . . . . . . . 11 = (le‘𝑅)
5250, 51eqtr4di 2794 . . . . . . . . . 10 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → (le‘𝑟) = )
5348, 52eqtrd 2776 . . . . . . . . 9 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → 𝑙 = )
5453breqd 5116 . . . . . . . 8 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → ( 0 𝑙𝑎0 𝑎))
5553breqd 5116 . . . . . . . 8 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → ( 0 𝑙𝑏0 𝑏))
5654, 55anbi12d 631 . . . . . . 7 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → (( 0 𝑙𝑎0 𝑙𝑏) ↔ ( 0 𝑎0 𝑏)))
5753breqd 5116 . . . . . . 7 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → ( 0 𝑙(𝑎 · 𝑏) ↔ 0 (𝑎 · 𝑏)))
5856, 57imbi12d 344 . . . . . 6 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → ((( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏)) ↔ (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
59582ralbidv 3212 . . . . 5 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → (∀𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
6047, 59sbcied 3784 . . . 4 (𝑟 = 𝑅 → ([(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
6115, 46, 603bitr3d 308 . . 3 (𝑟 = 𝑅 → ([(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
62 df-orng 32092 . . 3 oRing = {𝑟 ∈ (Ring ∩ oGrp) ∣ [(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))}
6361, 62elrab2 3648 . 2 (𝑅 ∈ oRing ↔ (𝑅 ∈ (Ring ∩ oGrp) ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
64 df-3an 1089 . 2 ((𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))) ↔ ((𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp) ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
652, 63, 643bitr4i 302 1 (𝑅 ∈ oRing ↔ (𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3064  Vcvv 3445  [wsbc 3739  cin 3909   class class class wbr 5105  cfv 6496  (class class class)co 7357  Basecbs 17083  .rcmulr 17134  lecple 17140  0gc0g 17321  Ringcrg 19964  oGrpcogrp 31906  oRingcorng 32090
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-nul 5263
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rab 3408  df-v 3447  df-sbc 3740  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-iota 6448  df-fv 6504  df-ov 7360  df-orng 32092
This theorem is referenced by:  orngring  32095  orngogrp  32096  orngmul  32098  suborng  32110  reofld  32136
  Copyright terms: Public domain W3C validator