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 29927
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 3829 . . 3 (𝑅 ∈ (Ring ∩ oGrp) ↔ (𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp))
21anbi1i 731 . 2 ((𝑅 ∈ (Ring ∩ oGrp) ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))) ↔ ((𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp) ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
3 fvexd 6241 . . . . 5 (𝑟 = 𝑅 → (.r𝑟) ∈ V)
4 simpr 476 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → 𝑡 = (.r𝑟))
5 simpl 472 . . . . . . . . . . . . 13 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → 𝑟 = 𝑅)
65fveq2d 6233 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → (.r𝑟) = (.r𝑅))
7 isorng.2 . . . . . . . . . . . 12 · = (.r𝑅)
86, 7syl6eqr 2703 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → (.r𝑟) = · )
94, 8eqtrd 2685 . . . . . . . . . 10 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → 𝑡 = · )
109oveqd 6707 . . . . . . . . 9 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → (𝑎𝑡𝑏) = (𝑎 · 𝑏))
1110breq2d 4697 . . . . . . . 8 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → ( 0 𝑙(𝑎𝑡𝑏) ↔ 0 𝑙(𝑎 · 𝑏)))
1211imbi2d 329 . . . . . . 7 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → ((( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏))))
13122ralbidv 3018 . . . . . 6 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → (∀𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏))))
1413sbcbidv 3523 . . . . 5 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → ([(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏))))
153, 14sbcied 3505 . . . 4 (𝑟 = 𝑅 → ([(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏))))
16 fvexd 6241 . . . . . 6 (𝑟 = 𝑅 → (Base‘𝑟) ∈ V)
17 simpr 476 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → 𝑣 = (Base‘𝑟))
18 fveq2 6229 . . . . . . . . . . . . 13 (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
19 isorng.0 . . . . . . . . . . . . 13 𝐵 = (Base‘𝑅)
2018, 19syl6eqr 2703 . . . . . . . . . . . 12 (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵)
2120adantr 480 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → (Base‘𝑟) = 𝐵)
2217, 21eqtrd 2685 . . . . . . . . . 10 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → 𝑣 = 𝐵)
23 raleq 3168 . . . . . . . . . . 11 (𝑣 = 𝐵 → (∀𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2423raleqbi1dv 3176 . . . . . . . . . 10 (𝑣 = 𝐵 → (∀𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2522, 24syl 17 . . . . . . . . 9 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → (∀𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2625sbcbidv 3523 . . . . . . . 8 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → ([(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2726sbcbidv 3523 . . . . . . 7 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → ([(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2827sbcbidv 3523 . . . . . 6 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → ([(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2916, 28sbcied 3505 . . . . 5 (𝑟 = 𝑅 → ([(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
30 fvexd 6241 . . . . . 6 (𝑟 = 𝑅 → (0g𝑟) ∈ V)
31 simpr 476 . . . . . . . . . . . . 13 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → 𝑧 = (0g𝑟))
32 fveq2 6229 . . . . . . . . . . . . . . 15 (𝑟 = 𝑅 → (0g𝑟) = (0g𝑅))
33 isorng.1 . . . . . . . . . . . . . . 15 0 = (0g𝑅)
3432, 33syl6eqr 2703 . . . . . . . . . . . . . 14 (𝑟 = 𝑅 → (0g𝑟) = 0 )
3534adantr 480 . . . . . . . . . . . . 13 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (0g𝑟) = 0 )
3631, 35eqtrd 2685 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → 𝑧 = 0 )
3736breq1d 4695 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (𝑧𝑙𝑎0 𝑙𝑎))
3836breq1d 4695 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (𝑧𝑙𝑏0 𝑙𝑏))
3937, 38anbi12d 747 . . . . . . . . . 10 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → ((𝑧𝑙𝑎𝑧𝑙𝑏) ↔ ( 0 𝑙𝑎0 𝑙𝑏)))
4036breq1d 4695 . . . . . . . . . 10 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (𝑧𝑙(𝑎𝑡𝑏) ↔ 0 𝑙(𝑎𝑡𝑏)))
4139, 40imbi12d 333 . . . . . . . . 9 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
42412ralbidv 3018 . . . . . . . 8 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (∀𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
4342sbcbidv 3523 . . . . . . 7 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → ([(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
4443sbcbidv 3523 . . . . . 6 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → ([(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
4530, 44sbcied 3505 . . . . 5 (𝑟 = 𝑅 → ([(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
4629, 45bitr2d 269 . . . 4 (𝑟 = 𝑅 → ([(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ [(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
47 fvexd 6241 . . . . 5 (𝑟 = 𝑅 → (le‘𝑟) ∈ V)
48 simpr 476 . . . . . . . . . 10 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → 𝑙 = (le‘𝑟))
49 simpl 472 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → 𝑟 = 𝑅)
5049fveq2d 6233 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → (le‘𝑟) = (le‘𝑅))
51 isorng.3 . . . . . . . . . . 11 = (le‘𝑅)
5250, 51syl6eqr 2703 . . . . . . . . . 10 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → (le‘𝑟) = )
5348, 52eqtrd 2685 . . . . . . . . 9 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → 𝑙 = )
5453breqd 4696 . . . . . . . 8 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → ( 0 𝑙𝑎0 𝑎))
5553breqd 4696 . . . . . . . 8 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → ( 0 𝑙𝑏0 𝑏))
5654, 55anbi12d 747 . . . . . . 7 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → (( 0 𝑙𝑎0 𝑙𝑏) ↔ ( 0 𝑎0 𝑏)))
5753breqd 4696 . . . . . . 7 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → ( 0 𝑙(𝑎 · 𝑏) ↔ 0 (𝑎 · 𝑏)))
5856, 57imbi12d 333 . . . . . 6 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → ((( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏)) ↔ (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
59582ralbidv 3018 . . . . 5 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → (∀𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
6047, 59sbcied 3505 . . . 4 (𝑟 = 𝑅 → ([(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
6115, 46, 603bitr3d 298 . . 3 (𝑟 = 𝑅 → ([(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
62 df-orng 29925 . . 3 oRing = {𝑟 ∈ (Ring ∩ oGrp) ∣ [(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))}
6361, 62elrab2 3399 . 2 (𝑅 ∈ oRing ↔ (𝑅 ∈ (Ring ∩ oGrp) ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
64 df-3an 1056 . 2 ((𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))) ↔ ((𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp) ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
652, 63, 643bitr4i 292 1 (𝑅 ∈ oRing ↔ (𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wral 2941  Vcvv 3231  [wsbc 3468  cin 3606   class class class wbr 4685  cfv 5926  (class class class)co 6690  Basecbs 15904  .rcmulr 15989  lecple 15995  0gc0g 16147  Ringcrg 18593  oGrpcogrp 29826  oRingcorng 29923
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-nul 4822
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-orng 29925
This theorem is referenced by:  orngring  29928  orngogrp  29929  orngmul  29931  suborng  29943  reofld  29968
  Copyright terms: Public domain W3C validator