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

Definition df-ring 19564
Description: Define class of all (unital) rings. A unital ring is a set equipped with two everywhere-defined internal operations, whose first one is an additive group structure and the second one is a multiplicative monoid structure, and where the addition is left- and right-distributive for the multiplication. Definition 1 in [BourbakiAlg1] p. 92 or definition of a ring with identity in part Preliminaries of [Roman] p. 19. So that the additive structure must be abelian (see ringcom 19597), care must be taken that in the case of a non-unital ring, the commutativity of addition must be postulated and cannot be proved from the other conditions. (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 27-Dec-2014.)
Assertion
Ref Expression
df-ring Ring = {𝑓 ∈ Grp ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡]𝑥𝑟𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))}
Distinct variable group:   𝑓,𝑝,𝑟,𝑡,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-ring
StepHypRef Expression
1 crg 19562 . 2 class Ring
2 vf . . . . . . 7 setvar 𝑓
32cv 1542 . . . . . 6 class 𝑓
4 cmgp 19504 . . . . . 6 class mulGrp
53, 4cfv 6380 . . . . 5 class (mulGrp‘𝑓)
6 cmnd 18173 . . . . 5 class Mnd
75, 6wcel 2110 . . . 4 wff (mulGrp‘𝑓) ∈ Mnd
8 vx . . . . . . . . . . . . . 14 setvar 𝑥
98cv 1542 . . . . . . . . . . . . 13 class 𝑥
10 vy . . . . . . . . . . . . . . 15 setvar 𝑦
1110cv 1542 . . . . . . . . . . . . . 14 class 𝑦
12 vz . . . . . . . . . . . . . . 15 setvar 𝑧
1312cv 1542 . . . . . . . . . . . . . 14 class 𝑧
14 vp . . . . . . . . . . . . . . 15 setvar 𝑝
1514cv 1542 . . . . . . . . . . . . . 14 class 𝑝
1611, 13, 15co 7213 . . . . . . . . . . . . 13 class (𝑦𝑝𝑧)
17 vt . . . . . . . . . . . . . 14 setvar 𝑡
1817cv 1542 . . . . . . . . . . . . 13 class 𝑡
199, 16, 18co 7213 . . . . . . . . . . . 12 class (𝑥𝑡(𝑦𝑝𝑧))
209, 11, 18co 7213 . . . . . . . . . . . . 13 class (𝑥𝑡𝑦)
219, 13, 18co 7213 . . . . . . . . . . . . 13 class (𝑥𝑡𝑧)
2220, 21, 15co 7213 . . . . . . . . . . . 12 class ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
2319, 22wceq 1543 . . . . . . . . . . 11 wff (𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
249, 11, 15co 7213 . . . . . . . . . . . . 13 class (𝑥𝑝𝑦)
2524, 13, 18co 7213 . . . . . . . . . . . 12 class ((𝑥𝑝𝑦)𝑡𝑧)
2611, 13, 18co 7213 . . . . . . . . . . . . 13 class (𝑦𝑡𝑧)
2721, 26, 15co 7213 . . . . . . . . . . . 12 class ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))
2825, 27wceq 1543 . . . . . . . . . . 11 wff ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))
2923, 28wa 399 . . . . . . . . . 10 wff ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
30 vr . . . . . . . . . . 11 setvar 𝑟
3130cv 1542 . . . . . . . . . 10 class 𝑟
3229, 12, 31wral 3061 . . . . . . . . 9 wff 𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
3332, 10, 31wral 3061 . . . . . . . 8 wff 𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
3433, 8, 31wral 3061 . . . . . . 7 wff 𝑥𝑟𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
35 cmulr 16803 . . . . . . . 8 class .r
363, 35cfv 6380 . . . . . . 7 class (.r𝑓)
3734, 17, 36wsbc 3694 . . . . . 6 wff [(.r𝑓) / 𝑡]𝑥𝑟𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
38 cplusg 16802 . . . . . . 7 class +g
393, 38cfv 6380 . . . . . 6 class (+g𝑓)
4037, 14, 39wsbc 3694 . . . . 5 wff [(+g𝑓) / 𝑝][(.r𝑓) / 𝑡]𝑥𝑟𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
41 cbs 16760 . . . . . 6 class Base
423, 41cfv 6380 . . . . 5 class (Base‘𝑓)
4340, 30, 42wsbc 3694 . . . 4 wff [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡]𝑥𝑟𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
447, 43wa 399 . . 3 wff ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡]𝑥𝑟𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))
45 cgrp 18365 . . 3 class Grp
4644, 2, 45crab 3065 . 2 class {𝑓 ∈ Grp ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡]𝑥𝑟𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))}
471, 46wceq 1543 1 wff Ring = {𝑓 ∈ Grp ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡]𝑥𝑟𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))}
Colors of variables: wff setvar class
This definition is referenced by:  isring  19566
  Copyright terms: Public domain W3C validator