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 29576
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 3779 . . 3 (𝑅 ∈ (Ring ∩ oGrp) ↔ (𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp))
21anbi1i 730 . 2 ((𝑅 ∈ (Ring ∩ oGrp) ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))) ↔ ((𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp) ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
3 fvex 6160 . . . . . 6 (.r𝑟) ∈ V
43a1i 11 . . . . 5 (𝑟 = 𝑅 → (.r𝑟) ∈ V)
5 simpr 477 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → 𝑡 = (.r𝑟))
6 simpl 473 . . . . . . . . . . . . 13 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → 𝑟 = 𝑅)
76fveq2d 6154 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → (.r𝑟) = (.r𝑅))
8 isorng.2 . . . . . . . . . . . 12 · = (.r𝑅)
97, 8syl6eqr 2678 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → (.r𝑟) = · )
105, 9eqtrd 2660 . . . . . . . . . 10 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → 𝑡 = · )
1110oveqd 6622 . . . . . . . . 9 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → (𝑎𝑡𝑏) = (𝑎 · 𝑏))
1211breq2d 4630 . . . . . . . 8 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → ( 0 𝑙(𝑎𝑡𝑏) ↔ 0 𝑙(𝑎 · 𝑏)))
1312imbi2d 330 . . . . . . 7 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → ((( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏))))
14132ralbidv 2988 . . . . . 6 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → (∀𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏))))
1514sbcbidv 3477 . . . . 5 ((𝑟 = 𝑅𝑡 = (.r𝑟)) → ([(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏))))
164, 15sbcied 3459 . . . 4 (𝑟 = 𝑅 → ([(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏))))
17 fvex 6160 . . . . . . 7 (Base‘𝑟) ∈ V
1817a1i 11 . . . . . 6 (𝑟 = 𝑅 → (Base‘𝑟) ∈ V)
19 simpr 477 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → 𝑣 = (Base‘𝑟))
20 fveq2 6150 . . . . . . . . . . . . 13 (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
21 isorng.0 . . . . . . . . . . . . 13 𝐵 = (Base‘𝑅)
2220, 21syl6eqr 2678 . . . . . . . . . . . 12 (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵)
2322adantr 481 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → (Base‘𝑟) = 𝐵)
2419, 23eqtrd 2660 . . . . . . . . . 10 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → 𝑣 = 𝐵)
25 raleq 3132 . . . . . . . . . . 11 (𝑣 = 𝐵 → (∀𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2625raleqbi1dv 3140 . . . . . . . . . 10 (𝑣 = 𝐵 → (∀𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2724, 26syl 17 . . . . . . . . 9 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → (∀𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2827sbcbidv 3477 . . . . . . . 8 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → ([(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
2928sbcbidv 3477 . . . . . . 7 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → ([(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
3029sbcbidv 3477 . . . . . 6 ((𝑟 = 𝑅𝑣 = (Base‘𝑟)) → ([(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
3118, 30sbcied 3459 . . . . 5 (𝑟 = 𝑅 → ([(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
32 fvex 6160 . . . . . . 7 (0g𝑟) ∈ V
3332a1i 11 . . . . . 6 (𝑟 = 𝑅 → (0g𝑟) ∈ V)
34 simpr 477 . . . . . . . . . . . . 13 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → 𝑧 = (0g𝑟))
35 fveq2 6150 . . . . . . . . . . . . . . 15 (𝑟 = 𝑅 → (0g𝑟) = (0g𝑅))
36 isorng.1 . . . . . . . . . . . . . . 15 0 = (0g𝑅)
3735, 36syl6eqr 2678 . . . . . . . . . . . . . 14 (𝑟 = 𝑅 → (0g𝑟) = 0 )
3837adantr 481 . . . . . . . . . . . . 13 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (0g𝑟) = 0 )
3934, 38eqtrd 2660 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → 𝑧 = 0 )
4039breq1d 4628 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (𝑧𝑙𝑎0 𝑙𝑎))
4139breq1d 4628 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (𝑧𝑙𝑏0 𝑙𝑏))
4240, 41anbi12d 746 . . . . . . . . . 10 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → ((𝑧𝑙𝑎𝑧𝑙𝑏) ↔ ( 0 𝑙𝑎0 𝑙𝑏)))
4339breq1d 4628 . . . . . . . . . 10 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (𝑧𝑙(𝑎𝑡𝑏) ↔ 0 𝑙(𝑎𝑡𝑏)))
4442, 43imbi12d 334 . . . . . . . . 9 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
45442ralbidv 2988 . . . . . . . 8 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → (∀𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
4645sbcbidv 3477 . . . . . . 7 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → ([(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
4746sbcbidv 3477 . . . . . 6 ((𝑟 = 𝑅𝑧 = (0g𝑟)) → ([(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
4833, 47sbcied 3459 . . . . 5 (𝑟 = 𝑅 → ([(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ [(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏))))
4931, 48bitr2d 269 . . . 4 (𝑟 = 𝑅 → ([(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎𝑡𝑏)) ↔ [(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))))
50 fvex 6160 . . . . . 6 (le‘𝑟) ∈ V
5150a1i 11 . . . . 5 (𝑟 = 𝑅 → (le‘𝑟) ∈ V)
52 simpr 477 . . . . . . . . . 10 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → 𝑙 = (le‘𝑟))
53 simpl 473 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → 𝑟 = 𝑅)
5453fveq2d 6154 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → (le‘𝑟) = (le‘𝑅))
55 isorng.3 . . . . . . . . . . 11 = (le‘𝑅)
5654, 55syl6eqr 2678 . . . . . . . . . 10 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → (le‘𝑟) = )
5752, 56eqtrd 2660 . . . . . . . . 9 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → 𝑙 = )
5857breqd 4629 . . . . . . . 8 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → ( 0 𝑙𝑎0 𝑎))
5957breqd 4629 . . . . . . . 8 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → ( 0 𝑙𝑏0 𝑏))
6058, 59anbi12d 746 . . . . . . 7 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → (( 0 𝑙𝑎0 𝑙𝑏) ↔ ( 0 𝑎0 𝑏)))
6157breqd 4629 . . . . . . 7 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → ( 0 𝑙(𝑎 · 𝑏) ↔ 0 (𝑎 · 𝑏)))
6260, 61imbi12d 334 . . . . . 6 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → ((( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏)) ↔ (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
63622ralbidv 2988 . . . . 5 ((𝑟 = 𝑅𝑙 = (le‘𝑟)) → (∀𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
6451, 63sbcied 3459 . . . 4 (𝑟 = 𝑅 → ([(le‘𝑟) / 𝑙]𝑎𝐵𝑏𝐵 (( 0 𝑙𝑎0 𝑙𝑏) → 0 𝑙(𝑎 · 𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
6516, 49, 643bitr3d 298 . . 3 (𝑟 = 𝑅 → ([(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏)) ↔ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
66 df-orng 29574 . . 3 oRing = {𝑟 ∈ (Ring ∩ oGrp) ∣ [(Base‘𝑟) / 𝑣][(0g𝑟) / 𝑧][(.r𝑟) / 𝑡][(le‘𝑟) / 𝑙]𝑎𝑣𝑏𝑣 ((𝑧𝑙𝑎𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))}
6765, 66elrab2 3353 . 2 (𝑅 ∈ oRing ↔ (𝑅 ∈ (Ring ∩ oGrp) ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
68 df-3an 1038 . 2 ((𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))) ↔ ((𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp) ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
692, 67, 683bitr4i 292 1 (𝑅 ∈ oRing ↔ (𝑅 ∈ Ring ∧ 𝑅 ∈ oGrp ∧ ∀𝑎𝐵𝑏𝐵 (( 0 𝑎0 𝑏) → 0 (𝑎 · 𝑏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1992  wral 2912  Vcvv 3191  [wsbc 3422  cin 3559   class class class wbr 4618  cfv 5850  (class class class)co 6605  Basecbs 15776  .rcmulr 15858  lecple 15864  0gc0g 16016  Ringcrg 18463  oGrpcogrp 29475  oRingcorng 29572
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-nul 4754
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-iota 5813  df-fv 5858  df-ov 6608  df-orng 29574
This theorem is referenced by:  orngring  29577  orngogrp  29578  orngmul  29580  suborng  29592  reofld  29617
  Copyright terms: Public domain W3C validator