ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  isring GIF version

Theorem isring 13006
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 5511 . . . . . 6 (𝑟 = 𝑅 → (mulGrp‘𝑟) = (mulGrp‘𝑅))
2 isring.g . . . . . 6 𝐺 = (mulGrp‘𝑅)
31, 2eqtr4di 2228 . . . . 5 (𝑟 = 𝑅 → (mulGrp‘𝑟) = 𝐺)
43eleq1d 2246 . . . 4 (𝑟 = 𝑅 → ((mulGrp‘𝑟) ∈ Mnd ↔ 𝐺 ∈ Mnd))
5 basfn 12499 . . . . . . 7 Base Fn V
6 vex 2740 . . . . . . 7 𝑟 ∈ V
7 funfvex 5528 . . . . . . . 8 ((Fun Base ∧ 𝑟 ∈ dom Base) → (Base‘𝑟) ∈ V)
87funfni 5312 . . . . . . 7 ((Base Fn V ∧ 𝑟 ∈ V) → (Base‘𝑟) ∈ V)
95, 6, 8mp2an 426 . . . . . 6 (Base‘𝑟) ∈ V
109a1i 9 . . . . 5 (𝑟 = 𝑅 → (Base‘𝑟) ∈ V)
11 fveq2 5511 . . . . . 6 (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
12 isring.b . . . . . 6 𝐵 = (Base‘𝑅)
1311, 12eqtr4di 2228 . . . . 5 (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵)
14 plusgslid 12548 . . . . . . . . 9 (+g = Slot (+g‘ndx) ∧ (+g‘ndx) ∈ ℕ)
1514slotex 12469 . . . . . . . 8 (𝑟 ∈ V → (+g𝑟) ∈ V)
1615elv 2741 . . . . . . 7 (+g𝑟) ∈ V
1716a1i 9 . . . . . 6 ((𝑟 = 𝑅𝑏 = 𝐵) → (+g𝑟) ∈ V)
18 simpl 109 . . . . . . . 8 ((𝑟 = 𝑅𝑏 = 𝐵) → 𝑟 = 𝑅)
1918fveq2d 5515 . . . . . . 7 ((𝑟 = 𝑅𝑏 = 𝐵) → (+g𝑟) = (+g𝑅))
20 isring.p . . . . . . 7 + = (+g𝑅)
2119, 20eqtr4di 2228 . . . . . 6 ((𝑟 = 𝑅𝑏 = 𝐵) → (+g𝑟) = + )
22 mulrslid 12566 . . . . . . . . . 10 (.r = Slot (.r‘ndx) ∧ (.r‘ndx) ∈ ℕ)
2322slotex 12469 . . . . . . . . 9 (𝑟 ∈ V → (.r𝑟) ∈ V)
2423elv 2741 . . . . . . . 8 (.r𝑟) ∈ V
2524a1i 9 . . . . . . 7 (((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) → (.r𝑟) ∈ V)
26 simpll 527 . . . . . . . . 9 (((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) → 𝑟 = 𝑅)
2726fveq2d 5515 . . . . . . . 8 (((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) → (.r𝑟) = (.r𝑅))
28 isring.t . . . . . . . 8 · = (.r𝑅)
2927, 28eqtr4di 2228 . . . . . . 7 (((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) → (.r𝑟) = · )
30 simpllr 534 . . . . . . . 8 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑏 = 𝐵)
31 simpr 110 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑡 = · )
32 eqidd 2178 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑥 = 𝑥)
33 simplr 528 . . . . . . . . . . . . . 14 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑝 = + )
3433oveqd 5886 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑦𝑝𝑧) = (𝑦 + 𝑧))
3531, 32, 34oveq123d 5890 . . . . . . . . . . . 12 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑥𝑡(𝑦𝑝𝑧)) = (𝑥 · (𝑦 + 𝑧)))
3631oveqd 5886 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑥𝑡𝑦) = (𝑥 · 𝑦))
3731oveqd 5886 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑥𝑡𝑧) = (𝑥 · 𝑧))
3833, 36, 37oveq123d 5890 . . . . . . . . . . . 12 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)))
3935, 38eqeq12d 2192 . . . . . . . . . . 11 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ↔ (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))))
4033oveqd 5886 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑥𝑝𝑦) = (𝑥 + 𝑦))
41 eqidd 2178 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑧 = 𝑧)
4231, 40, 41oveq123d 5890 . . . . . . . . . . . 12 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥 + 𝑦) · 𝑧))
4331oveqd 5886 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (𝑦𝑡𝑧) = (𝑦 · 𝑧))
4433, 37, 43oveq123d 5890 . . . . . . . . . . . 12 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))
4542, 44eqeq12d 2192 . . . . . . . . . . 11 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)) ↔ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))
4639, 45anbi12d 473 . . . . . . . . . 10 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
4730, 46raleqbidv 2684 . . . . . . . . 9 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (∀𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
4830, 47raleqbidv 2684 . . . . . . . 8 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (∀𝑦𝑏𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑦𝐵𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
4930, 48raleqbidv 2684 . . . . . . 7 ((((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → (∀𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
5025, 29, 49sbcied2 3000 . . . . . 6 (((𝑟 = 𝑅𝑏 = 𝐵) ∧ 𝑝 = + ) → ([(.r𝑟) / 𝑡]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
5117, 21, 50sbcied2 3000 . . . . 5 ((𝑟 = 𝑅𝑏 = 𝐵) → ([(+g𝑟) / 𝑝][(.r𝑟) / 𝑡]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
5210, 13, 51sbcied2 3000 . . . 4 (𝑟 = 𝑅 → ([(Base‘𝑟) / 𝑏][(+g𝑟) / 𝑝][(.r𝑟) / 𝑡]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ↔ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
534, 52anbi12d 473 . . 3 (𝑟 = 𝑅 → (((mulGrp‘𝑟) ∈ Mnd ∧ [(Base‘𝑟) / 𝑏][(+g𝑟) / 𝑝][(.r𝑟) / 𝑡]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))) ↔ (𝐺 ∈ Mnd ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))))
54 df-ring 13004 . . 3 Ring = {𝑟 ∈ Grp ∣ ((mulGrp‘𝑟) ∈ Mnd ∧ [(Base‘𝑟) / 𝑏][(+g𝑟) / 𝑝][(.r𝑟) / 𝑡]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))}
5553, 54elrab2 2896 . 2 (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ (𝐺 ∈ Mnd ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))))
56 3anass 982 . 2 ((𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))) ↔ (𝑅 ∈ Grp ∧ (𝐺 ∈ Mnd ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))))
5755, 56bitr4i 187 1 (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥𝐵𝑦𝐵𝑧𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))))
Colors of variables: wff set class
Syntax hints:  wa 104  wb 105  w3a 978   = wceq 1353  wcel 2148  wral 2455  Vcvv 2737  [wsbc 2962   Fn wfn 5207  cfv 5212  (class class class)co 5869  Basecbs 12442  +gcplusg 12515  .rcmulr 12516  Mndcmnd 12706  Grpcgrp 12764  mulGrpcmgp 12954  Ringcrg 13002
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-cnex 7890  ax-resscn 7891  ax-1re 7893  ax-addrcl 7896
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-sbc 2963  df-un 3133  df-in 3135  df-ss 3142  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-br 4001  df-opab 4062  df-mpt 4063  df-id 4290  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-iota 5174  df-fun 5214  df-fn 5215  df-fv 5220  df-ov 5872  df-inn 8906  df-2 8964  df-3 8965  df-ndx 12445  df-slot 12446  df-base 12448  df-plusg 12528  df-mulr 12529  df-ring 13004
This theorem is referenced by:  ringgrp  13007  ringmgp  13008  ringdilem  13018  ringpropd  13040  isringd  13043  ringsrg  13047  ring1  13059
  Copyright terms: Public domain W3C validator