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 30029
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 3904 . . 3 (𝑅 ∈ (Ring ∩ oGrp) ↔ (𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp))
21anbi1i 733 . 2 ((𝑅 ∈ (Ring ∩ oGrp) ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))) ↔ ((𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp) ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
3 fvexd 6316 . . . . 5 (𝑟 = 𝑅 → (.r𝑟) ∈ V)
4 simpr 479 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → 𝑡 = (.r𝑟))
5 simpl 474 . . . . . . . . . . . . 13 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → 𝑟 = 𝑅)
65fveq2d 6308 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → (.r𝑟) = (.r𝑅))
7 isorng.2 . . . . . . . . . . . 12 · = (.r𝑅)
86, 7syl6eqr 2776 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → (.r𝑟) = · )
94, 8eqtrd 2758 . . . . . . . . . 10 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → 𝑡 = · )
109oveqd 6782 . . . . . . . . 9 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → (𝑎𝑡𝑏) = (𝑎 · 𝑏))
1110breq2d 4772 . . . . . . . 8 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → ( 0 𝑙(𝑎𝑡𝑏) ↔ 0 𝑙(𝑎 · 𝑏)))
1211imbi2d 329 . . . . . . 7 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → ((( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏))))
13122ralbidv 3091 . . . . . 6 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → (∀𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏))))
1413sbcbidv 3596 . . . . 5 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → ([(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏))))
153, 14sbcied 3578 . . . 4 (𝑟 = 𝑅 → ([(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏))))
16 fvexd 6316 . . . . . 6 (𝑟 = 𝑅 → (Base‘𝑟) ∈ V)
17 simpr 479 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → 𝑣 = (Base‘𝑟))
18 fveq2 6304 . . . . . . . . . . . . 13 (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
19 isorng.0 . . . . . . . . . . . . 13 𝐵 = (Base‘𝑅)
2018, 19syl6eqr 2776 . . . . . . . . . . . 12 (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵)
2120adantr 472 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → (Base‘𝑟) = 𝐵)
2217, 21eqtrd 2758 . . . . . . . . . 10 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → 𝑣 = 𝐵)
23 raleq 3241 . . . . . . . . . . 11 (𝑣 = 𝐵 → (∀𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2423raleqbi1dv 3249 . . . . . . . . . 10 (𝑣 = 𝐵 → (∀𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2522, 24syl 17 . . . . . . . . 9 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → (∀𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2625sbcbidv 3596 . . . . . . . 8 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → ([(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2726sbcbidv 3596 . . . . . . 7 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → ([(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2827sbcbidv 3596 . . . . . 6 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → ([(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2916, 28sbcied 3578 . . . . 5 (𝑟 = 𝑅 → ([(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
30 fvexd 6316 . . . . . 6 (𝑟 = 𝑅 → (0g𝑟) ∈ V)
31 simpr 479 . . . . . . . . . . . . 13 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → 𝑧 = (0g𝑟))
32 fveq2 6304 . . . . . . . . . . . . . . 15 (𝑟 = 𝑅 → (0g𝑟) = (0g𝑅))
33 isorng.1 . . . . . . . . . . . . . . 15 0 = (0g𝑅)
3432, 33syl6eqr 2776 . . . . . . . . . . . . . 14 (𝑟 = 𝑅 → (0g𝑟) = 0 )
3534adantr 472 . . . . . . . . . . . . 13 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (0g𝑟) = 0 )
3631, 35eqtrd 2758 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → 𝑧 = 0 )
3736breq1d 4770 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (𝑧𝑙𝑎0 𝑙𝑎))
3836breq1d 4770 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (𝑧𝑙𝑏0 𝑙𝑏))
3937, 38anbi12d 749 . . . . . . . . . 10 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → ((𝑧𝑙𝑎𝑧𝑙𝑏) ↔ ( 0 𝑙𝑎0 𝑙𝑏)))
4036breq1d 4770 . . . . . . . . . 10 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (𝑧𝑙(𝑎𝑡𝑏) ↔ 0 𝑙(𝑎𝑡𝑏)))
4139, 40imbi12d 333 . . . . . . . . 9 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
42412ralbidv 3091 . . . . . . . 8 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (∀𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
4342sbcbidv 3596 . . . . . . 7 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → ([(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
4443sbcbidv 3596 . . . . . 6 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → ([(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
4530, 44sbcied 3578 . . . . 5 (𝑟 = 𝑅 → ([(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
4629, 45bitr2d 269 . . . 4 (𝑟 = 𝑅 → ([(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ [(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
47 fvexd 6316 . . . . 5 (𝑟 = 𝑅 → (le‘𝑟) ∈ V)
48 simpr 479 . . . . . . . . . 10 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → 𝑙 = (le‘𝑟))
49 simpl 474 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → 𝑟 = 𝑅)
5049fveq2d 6308 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → (le‘𝑟) = (le‘𝑅))
51 isorng.3 . . . . . . . . . . 11 = (le‘𝑅)
5250, 51syl6eqr 2776 . . . . . . . . . 10 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → (le‘𝑟) = )
5348, 52eqtrd 2758 . . . . . . . . 9 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → 𝑙 = )
5453breqd 4771 . . . . . . . 8 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → ( 0 𝑙𝑎0 𝑎))
5553breqd 4771 . . . . . . . 8 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → ( 0 𝑙𝑏0 𝑏))
5654, 55anbi12d 749 . . . . . . 7 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → (( 0 𝑙𝑎0 𝑙𝑏) ↔ ( 0 𝑎0 𝑏)))
5753breqd 4771 . . . . . . 7 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → ( 0 𝑙(𝑎 · 𝑏) ↔ 0 (𝑎 · 𝑏)))
5856, 57imbi12d 333 . . . . . 6 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → ((( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏)) ↔ (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
59582ralbidv 3091 . . . . 5 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → (∀𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
6047, 59sbcied 3578 . . . 4 (𝑟 = 𝑅 → ([(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
6115, 46, 603bitr3d 298 . . 3 (𝑟 = 𝑅 → ([(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
62 df-orng 30027 . . 3 oRing = {𝑟 ∈ (Ring ∩ oGrp) ∣ [(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))}
6361, 62elrab2 3472 . 2 (𝑅 ∈ oRing ↔ (𝑅 ∈ (Ring ∩ oGrp) ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
64 df-3an 1074 . 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 1072   = wceq 1596  wcel 2103  wral 3014  Vcvv 3304  [wsbc 3541  cin 3679   class class class wbr 4760  cfv 6001  (class class class)co 6765  Basecbs 15980  .rcmulr 16065  lecple 16071  0gc0g 16223  Ringcrg 18668  oGrpcogrp 29928  oRingcorng 30025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-nul 4897
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ral 3019  df-rex 3020  df-rab 3023  df-v 3306  df-sbc 3542  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-br 4761  df-iota 5964  df-fv 6009  df-ov 6768  df-orng 30027
This theorem is referenced by:  orngring  30030  orngogrp  30031  orngmul  30033  suborng  30045  reofld  30070
  Copyright terms: Public domain W3C validator