Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  isring Structured version   Visualization version   GIF version

Theorem isring 19293
 Description: The predicate "is a (unital) ring." Definition of ring with unit in [Schechter] p. 187. (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.)
Hypotheses
Ref Expression
isring.b 𝐵 = (Base‘𝑅)
isring.g 𝐺 = (mulGrp‘𝑅)
isring.p + = (+g𝑅)
isring.t · = (.r𝑅)
Assertion
Ref Expression
isring (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
Distinct variable groups:   𝑥,𝑦,𝑧,𝐵   𝑥, + ,𝑦,𝑧   𝑥,𝑅,𝑦,𝑧   𝑥, · ,𝑦,𝑧
Allowed substitution hints:   𝐺(𝑥,𝑦,𝑧)

Proof of Theorem isring
Dummy variables 𝑝 𝑏 𝑟 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6663 . . . . . 6 (𝑟 = 𝑅 → (mulGrp‘𝑟) = (mulGrp‘𝑅))
2 isring.g . . . . . 6 𝐺 = (mulGrp‘𝑅)
31, 2syl6eqr 2872 . . . . 5 (𝑟 = 𝑅 → (mulGrp‘𝑟) = 𝐺)
43eleq1d 2895 . . . 4 (𝑟 = 𝑅 → ((mulGrp‘𝑟) ∈ Mnd ↔ 𝐺 ∈ Mnd))
5 fvexd 6678 . . . . 5 (𝑟 = 𝑅 → (Base‘𝑟) ∈ V)
6 fveq2 6663 . . . . . 6 (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
7 isring.b . . . . . 6 𝐵 = (Base‘𝑅)
86, 7syl6eqr 2872 . . . . 5 (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵)
9 fvexd 6678 . . . . . 6 ((𝑟 = 𝑅𝑏 = 𝐵) → (+g𝑟) ∈ V)
10 simpl 485 . . . . . . . 8 ((𝑟 = 𝑅𝑏 = 𝐵) → 𝑟 = 𝑅)
1110fveq2d 6667 . . . . . . 7 ((𝑟 = 𝑅𝑏 = 𝐵) → (+g𝑟) = (+g𝑅))
12 isring.p . . . . . . 7 + = (+g𝑅)
1311, 12syl6eqr 2872 . . . . . 6 ((𝑟 = 𝑅𝑏 = 𝐵) → (+g𝑟) = + )
14 fvexd 6678 . . . . . . 7 (((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) → (.r𝑟) ∈ V)
15 simpll 765 . . . . . . . . 9 (((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) → 𝑟 = 𝑅)
1615fveq2d 6667 . . . . . . . 8 (((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) → (.r𝑟) = (.r𝑅))
17 isring.t . . . . . . . 8 · = (.r𝑅)
1816, 17syl6eqr 2872 . . . . . . 7 (((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) → (.r𝑟) = · )
19 simpllr 774 . . . . . . . 8 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑏 = 𝐵)
20 simpr 487 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑡 = · )
21 eqidd 2820 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑥 = 𝑥)
22 simplr 767 . . . . . . . . . . . . . 14 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑝 = + )
2322oveqd 7165 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑦𝑝𝑧) = (𝑦 + 𝑧))
2420, 21, 23oveq123d 7169 . . . . . . . . . . . 12 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑥𝑡(𝑦𝑝𝑧)) = (𝑥 · (𝑦 + 𝑧)))
2520oveqd 7165 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑥𝑡𝑦) = (𝑥 · 𝑦))
2620oveqd 7165 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑥𝑡𝑧) = (𝑥 · 𝑧))
2722, 25, 26oveq123d 7169 . . . . . . . . . . . 12 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))
2824, 27eqeq12d 2835 . . . . . . . . . . 11 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ↔ (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))))
2922oveqd 7165 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑥𝑝𝑦) = (𝑥 + 𝑦))
30 eqidd 2820 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑧 = 𝑧)
3120, 29, 30oveq123d 7169 . . . . . . . . . . . 12 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥 + 𝑦) · 𝑧))
3220oveqd 7165 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑦𝑡𝑧) = (𝑦 · 𝑧))
3322, 26, 32oveq123d 7169 . . . . . . . . . . . 12 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
3431, 33eqeq12d 2835 . . . . . . . . . . 11 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)) ↔ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))
3528, 34anbi12d 632 . . . . . . . . . 10 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
3619, 35raleqbidv 3400 . . . . . . . . 9 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (∀𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
3719, 36raleqbidv 3400 . . . . . . . 8 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (∀𝑦𝑏𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑦𝐵𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
3819, 37raleqbidv 3400 . . . . . . 7 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (∀𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
3914, 18, 38sbcied2 3813 . . . . . 6 (((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) → ([(.r𝑟) / 𝑡]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
409, 13, 39sbcied2 3813 . . . . 5 ((𝑟 = 𝑅𝑏 = 𝐵) → ([(+g𝑟) / 𝑝][(.r𝑟) / 𝑡]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
415, 8, 40sbcied2 3813 . . . 4 (𝑟 = 𝑅 → ([(Base‘𝑟) / 𝑏][(+g𝑟) / 𝑝][(.r𝑟) / 𝑡]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
424, 41anbi12d 632 . . 3 (𝑟 = 𝑅 → (((mulGrp‘𝑟) ∈ Mnd ∧ [(Base‘𝑟) / 𝑏][(+g𝑟) / 𝑝][(.r𝑟) / 𝑡]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))) ↔ (𝐺 ∈ Mnd ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))))
43 df-ring 19291 . . 3 Ring = {𝑟 ∈ Grp ∣ ((mulGrp‘𝑟) ∈ Mnd ∧ [(Base‘𝑟) / 𝑏][(+g𝑟) / 𝑝][(.r𝑟) / 𝑡]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))}
4442, 43elrab2 3681 . 2 (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ (𝐺 ∈ Mnd ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))))
45 3anass 1089 . 2 ((𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))) ↔ (𝑅 ∈ Grp ∧ (𝐺 ∈ Mnd ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))))
4644, 45bitr4i 280 1 (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 208   ∧ wa 398   ∧ w3a 1081   = wceq 1530   ∈ wcel 2107  ∀wral 3136  Vcvv 3493  [wsbc 3770  ‘cfv 6348  (class class class)co 7148  Basecbs 16475  +gcplusg 16557  .rcmulr 16558  Mndcmnd 17903  Grpcgrp 18095  mulGrpcmgp 19231  Ringcrg 19289 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-nul 5201 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7151  df-ring 19291 This theorem is referenced by:  ringgrp  19294  ringmgp  19295  ringi  19302  ringpropd  19324  isringd  19327  ringsrg  19331  ring1  19344  prdsringd  19354  ringrng  44140  isringrng  44142  2zrngnring  44213  cznnring  44217
 Copyright terms: Public domain W3C validator