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 30181
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 3958 . . 3 (𝑅 ∈ (Ring ∩ oGrp) ↔ (𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp))
21anbi1i 617 . 2 ((𝑅 ∈ (Ring ∩ oGrp) ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))) ↔ ((𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp) ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
3 fvexd 6390 . . . . 5 (𝑟 = 𝑅 → (.r𝑟) ∈ V)
4 simpr 477 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → 𝑡 = (.r𝑟))
5 simpl 474 . . . . . . . . . . . . 13 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → 𝑟 = 𝑅)
65fveq2d 6379 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → (.r𝑟) = (.r𝑅))
7 isorng.2 . . . . . . . . . . . 12 · = (.r𝑅)
86, 7syl6eqr 2817 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → (.r𝑟) = · )
94, 8eqtrd 2799 . . . . . . . . . 10 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → 𝑡 = · )
109oveqd 6859 . . . . . . . . 9 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → (𝑎𝑡𝑏) = (𝑎 · 𝑏))
1110breq2d 4821 . . . . . . . 8 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → ( 0 𝑙(𝑎𝑡𝑏) ↔ 0 𝑙(𝑎 · 𝑏)))
1211imbi2d 331 . . . . . . 7 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → ((( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏))))
13122ralbidv 3136 . . . . . 6 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → (∀𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏))))
1413sbcbidv 3651 . . . . 5 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → ([(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏))))
153, 14sbcied 3633 . . . 4 (𝑟 = 𝑅 → ([(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏))))
16 fvexd 6390 . . . . . 6 (𝑟 = 𝑅 → (Base‘𝑟) ∈ V)
17 simpr 477 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → 𝑣 = (Base‘𝑟))
18 fveq2 6375 . . . . . . . . . . . . 13 (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
19 isorng.0 . . . . . . . . . . . . 13 𝐵 = (Base‘𝑅)
2018, 19syl6eqr 2817 . . . . . . . . . . . 12 (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵)
2120adantr 472 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → (Base‘𝑟) = 𝐵)
2217, 21eqtrd 2799 . . . . . . . . . 10 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → 𝑣 = 𝐵)
23 raleq 3286 . . . . . . . . . . 11 (𝑣 = 𝐵 → (∀𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2423raleqbi1dv 3294 . . . . . . . . . 10 (𝑣 = 𝐵 → (∀𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2522, 24syl 17 . . . . . . . . 9 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → (∀𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2625sbcbidv 3651 . . . . . . . 8 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → ([(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2726sbcbidv 3651 . . . . . . 7 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → ([(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2827sbcbidv 3651 . . . . . 6 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → ([(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2916, 28sbcied 3633 . . . . 5 (𝑟 = 𝑅 → ([(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
30 fvexd 6390 . . . . . 6 (𝑟 = 𝑅 → (0g𝑟) ∈ V)
31 simpr 477 . . . . . . . . . . . . 13 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → 𝑧 = (0g𝑟))
32 fveq2 6375 . . . . . . . . . . . . . . 15 (𝑟 = 𝑅 → (0g𝑟) = (0g𝑅))
33 isorng.1 . . . . . . . . . . . . . . 15 0 = (0g𝑅)
3432, 33syl6eqr 2817 . . . . . . . . . . . . . 14 (𝑟 = 𝑅 → (0g𝑟) = 0 )
3534adantr 472 . . . . . . . . . . . . 13 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (0g𝑟) = 0 )
3631, 35eqtrd 2799 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → 𝑧 = 0 )
3736breq1d 4819 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (𝑧𝑙𝑎0 𝑙𝑎))
3836breq1d 4819 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (𝑧𝑙𝑏0 𝑙𝑏))
3937, 38anbi12d 624 . . . . . . . . . 10 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → ((𝑧𝑙𝑎𝑧𝑙𝑏) ↔ ( 0 𝑙𝑎0 𝑙𝑏)))
4036breq1d 4819 . . . . . . . . . 10 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (𝑧𝑙(𝑎𝑡𝑏) ↔ 0 𝑙(𝑎𝑡𝑏)))
4139, 40imbi12d 335 . . . . . . . . 9 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
42412ralbidv 3136 . . . . . . . 8 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (∀𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
4342sbcbidv 3651 . . . . . . 7 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → ([(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
4443sbcbidv 3651 . . . . . 6 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → ([(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
4530, 44sbcied 3633 . . . . 5 (𝑟 = 𝑅 → ([(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
4629, 45bitr2d 271 . . . 4 (𝑟 = 𝑅 → ([(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ [(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
47 fvexd 6390 . . . . 5 (𝑟 = 𝑅 → (le‘𝑟) ∈ V)
48 simpr 477 . . . . . . . . . 10 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → 𝑙 = (le‘𝑟))
49 simpl 474 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → 𝑟 = 𝑅)
5049fveq2d 6379 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → (le‘𝑟) = (le‘𝑅))
51 isorng.3 . . . . . . . . . . 11 = (le‘𝑅)
5250, 51syl6eqr 2817 . . . . . . . . . 10 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → (le‘𝑟) = )
5348, 52eqtrd 2799 . . . . . . . . 9 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → 𝑙 = )
5453breqd 4820 . . . . . . . 8 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → ( 0 𝑙𝑎0 𝑎))
5553breqd 4820 . . . . . . . 8 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → ( 0 𝑙𝑏0 𝑏))
5654, 55anbi12d 624 . . . . . . 7 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → (( 0 𝑙𝑎0 𝑙𝑏) ↔ ( 0 𝑎0 𝑏)))
5753breqd 4820 . . . . . . 7 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → ( 0 𝑙(𝑎 · 𝑏) ↔ 0 (𝑎 · 𝑏)))
5856, 57imbi12d 335 . . . . . 6 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → ((( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏)) ↔ (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
59582ralbidv 3136 . . . . 5 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → (∀𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
6047, 59sbcied 3633 . . . 4 (𝑟 = 𝑅 → ([(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
6115, 46, 603bitr3d 300 . . 3 (𝑟 = 𝑅 → ([(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
62 df-orng 30179 . . 3 oRing = {𝑟 ∈ (Ring ∩ oGrp) ∣ [(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))}
6361, 62elrab2 3523 . 2 (𝑅 ∈ oRing ↔ (𝑅 ∈ (Ring ∩ oGrp) ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
64 df-3an 1109 . 2 ((𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))) ↔ ((𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp) ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
652, 63, 643bitr4i 294 1 (𝑅 ∈ oRing ↔ (𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wral 3055  Vcvv 3350  [wsbc 3596  cin 3731   class class class wbr 4809  cfv 6068  (class class class)co 6842  Basecbs 16132  .rcmulr 16217  lecple 16223  0gc0g 16368  Ringcrg 18814  oGrpcogrp 30080  oRingcorng 30177
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-nul 4949
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3597  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-iota 6031  df-fv 6076  df-ov 6845  df-orng 30179
This theorem is referenced by:  orngring  30182  orngogrp  30183  orngmul  30185  suborng  30197  reofld  30222
  Copyright terms: Public domain W3C validator