df-ring

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 ), 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)

		Ref	Expression
	Assertion	df-ring	$⊢ Ring = \{f \in Grp \| ({mulGrp}_{f} \in Mnd \land \underset{˙}{[} {Base}_{f} / r \underset{˙}{]} \underset{˙}{[} +_{f} / p \underset{˙}{]} \underset{˙}{[} \cdot_{f} / t \underset{˙}{]} \forall x \in r \forall y \in r \forall z \in r (x t (y p z) = (x t y) p (x t z) \land (x p y) t z = (x t z) p (y t z)))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crg	$class Ring$
1		vf	$setvar f$
2		cgrp	$class Grp$
3		cmgp	$class mulGrp$
4	1	cv	$setvar f$
5	4 3	cfv	$class {mulGrp}_{f}$
6		cmnd	$class Mnd$
7	5 6	wcel	$wff {mulGrp}_{f} \in Mnd$
8		cbs	$class Base$
9	4 8	cfv	$class {Base}_{f}$
10		vr	$setvar r$
11		cplusg	$class +_{𝑔}$
12	4 11	cfv	$class +_{f}$
13		vp	$setvar p$
14		cmulr	$class \cdot_{𝑟}$
15	4 14	cfv	$class \cdot_{f}$
16		vt	$setvar t$
17		vx	$setvar x$
18	10	cv	$setvar r$
19		vy	$setvar y$
20		vz	$setvar z$
21	17	cv	$setvar x$
22	16	cv	$setvar t$
23	19	cv	$setvar y$
24	13	cv	$setvar p$
25	20	cv	$setvar z$
26	23 25 24	co	$class (y p z)$
27	21 26 22	co	$class (x t (y p z))$
28	21 23 22	co	$class (x t y)$
29	21 25 22	co	$class (x t z)$
30	28 29 24	co	$class ((x t y) p (x t z))$
31	27 30	wceq	$wff x t (y p z) = (x t y) p (x t z)$
32	21 23 24	co	$class (x p y)$
33	32 25 22	co	$class ((x p y) t z)$
34	23 25 22	co	$class (y t z)$
35	29 34 24	co	$class ((x t z) p (y t z))$
36	33 35	wceq	$wff (x p y) t z = (x t z) p (y t z)$
37	31 36	wa	$wff (x t (y p z) = (x t y) p (x t z) \land (x p y) t z = (x t z) p (y t z))$
38	37 20 18	wral	$wff \forall z \in r (x t (y p z) = (x t y) p (x t z) \land (x p y) t z = (x t z) p (y t z))$
39	38 19 18	wral	$wff \forall y \in r \forall z \in r (x t (y p z) = (x t y) p (x t z) \land (x p y) t z = (x t z) p (y t z))$
40	39 17 18	wral	$wff \forall x \in r \forall y \in r \forall z \in r (x t (y p z) = (x t y) p (x t z) \land (x p y) t z = (x t z) p (y t z))$
41	40 16 15	wsbc	$wff \underset{˙}{[} \cdot_{f} / t \underset{˙}{]} \forall x \in r \forall y \in r \forall z \in r (x t (y p z) = (x t y) p (x t z) \land (x p y) t z = (x t z) p (y t z))$
42	41 13 12	wsbc	$wff \underset{˙}{[} +_{f} / p \underset{˙}{]} \underset{˙}{[} \cdot_{f} / t \underset{˙}{]} \forall x \in r \forall y \in r \forall z \in r (x t (y p z) = (x t y) p (x t z) \land (x p y) t z = (x t z) p (y t z))$
43	42 10 9	wsbc	$wff \underset{˙}{[} {Base}_{f} / r \underset{˙}{]} \underset{˙}{[} +_{f} / p \underset{˙}{]} \underset{˙}{[} \cdot_{f} / t \underset{˙}{]} \forall x \in r \forall y \in r \forall z \in r (x t (y p z) = (x t y) p (x t z) \land (x p y) t z = (x t z) p (y t z))$
44	7 43	wa	$wff ({mulGrp}_{f} \in Mnd \land \underset{˙}{[} {Base}_{f} / r \underset{˙}{]} \underset{˙}{[} +_{f} / p \underset{˙}{]} \underset{˙}{[} \cdot_{f} / t \underset{˙}{]} \forall x \in r \forall y \in r \forall z \in r (x t (y p z) = (x t y) p (x t z) \land (x p y) t z = (x t z) p (y t z)))$
45	44 1 2	crab	$class \{f \in Grp \| ({mulGrp}_{f} \in Mnd \land \underset{˙}{[} {Base}_{f} / r \underset{˙}{]} \underset{˙}{[} +_{f} / p \underset{˙}{]} \underset{˙}{[} \cdot_{f} / t \underset{˙}{]} \forall x \in r \forall y \in r \forall z \in r (x t (y p z) = (x t y) p (x t z) \land (x p y) t z = (x t z) p (y t z)))\}$
46	0 45	wceq	$wff Ring = \{f \in Grp \| ({mulGrp}_{f} \in Mnd \land \underset{˙}{[} {Base}_{f} / r \underset{˙}{]} \underset{˙}{[} +_{f} / p \underset{˙}{]} \underset{˙}{[} \cdot_{f} / t \underset{˙}{]} \forall x \in r \forall y \in r \forall z \in r (x t (y p z) = (x t y) p (x t z) \land (x p y) t z = (x t z) p (y t z)))\}$

Metamath Proof Explorer

Definition df-ring

Detailed syntax breakdown