isring

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)

	Ref	Expression
Hypotheses	isring.b	$⊢ B = {Base}_{R}$
	isring.g	$⊢ G = {mulGrp}_{R}$
	isring.p	$⊢ \underset{˙}{+} = +_{R}$
	isring.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	isring	$⊢ R \in Ring \leftrightarrow (R \in Grp \land G \in Mnd \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)))$

Proof

Step	Hyp	Ref	Expression
1		isring.b	$⊢ B = {Base}_{R}$
2		isring.g	$⊢ G = {mulGrp}_{R}$
3		isring.p	$⊢ \underset{˙}{+} = +_{R}$
4		isring.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		fveq2	$⊢ r = R \to {mulGrp}_{r} = {mulGrp}_{R}$
6	5 2	eqtr4di	$⊢ r = R \to {mulGrp}_{r} = G$
7	6	eleq1d	$⊢ r = R \to ({mulGrp}_{r} \in Mnd \leftrightarrow G \in Mnd)$
8		fvexd	$⊢ r = R \to {Base}_{r} \in V$
9		fveq2	$⊢ r = R \to {Base}_{r} = {Base}_{R}$
10	9 1	eqtr4di	$⊢ r = R \to {Base}_{r} = B$
11		fvexd	$⊢ (r = R \land b = B) \to +_{r} \in V$
12		simpl	$⊢ (r = R \land b = B) \to r = R$
13	12	fveq2d	$⊢ (r = R \land b = B) \to +_{r} = +_{R}$
14	13 3	eqtr4di	$⊢ (r = R \land b = B) \to +_{r} = \underset{˙}{+}$
15		fvexd	$⊢ ((r = R \land b = B) \land p = \underset{˙}{+}) \to \cdot_{r} \in V$
16		simpll	$⊢ ((r = R \land b = B) \land p = \underset{˙}{+}) \to r = R$
17	16	fveq2d	$⊢ ((r = R \land b = B) \land p = \underset{˙}{+}) \to \cdot_{r} = \cdot_{R}$
18	17 4	eqtr4di	$⊢ ((r = R \land b = B) \land p = \underset{˙}{+}) \to \cdot_{r} = \underset{˙}{\cdot}$
19		simpllr	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to b = B$
20		simpr	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to t = \underset{˙}{\cdot}$
21		eqidd	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to x = x$
22		simplr	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to p = \underset{˙}{+}$
23	22	oveqd	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to y p z = y \underset{˙}{+} z$
24	20 21 23	oveq123d	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to x t (y p z) = x \underset{˙}{\cdot} (y \underset{˙}{+} z)$
25	20	oveqd	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to x t y = x \underset{˙}{\cdot} y$
26	20	oveqd	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to x t z = x \underset{˙}{\cdot} z$
27	22 25 26	oveq123d	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to (x t y) p (x t z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z)$
28	24 27	eqeq12d	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to (x t (y p z) = (x t y) p (x t z) \leftrightarrow x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z))$
29	22	oveqd	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to x p y = x \underset{˙}{+} y$
30		eqidd	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to z = z$
31	20 29 30	oveq123d	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to (x p y) t z = (x \underset{˙}{+} y) \underset{˙}{\cdot} z$
32	20	oveqd	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to y t z = y \underset{˙}{\cdot} z$
33	22 26 32	oveq123d	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to (x t z) p (y t z) = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)$
34	31 33	eqeq12d	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to ((x p y) t z = (x t z) p (y t z) \leftrightarrow (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))$
35	28 34	anbi12d	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to ((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)) \leftrightarrow (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)))$
36	19 35	raleqbidv	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to (\forall z \in b (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)) \leftrightarrow \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)))$
37	19 36	raleqbidv	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to (\forall y \in b \forall z \in b (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)) \leftrightarrow \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)))$
38	19 37	raleqbidv	$⊢ (((r = R \land b = B) \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to (\forall x \in b \forall y \in b \forall z \in b (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)) \leftrightarrow \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)))$
39	15 18 38	sbcied2	$⊢ ((r = R \land b = B) \land p = \underset{˙}{+}) \to (\underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \forall x \in b \forall y \in b \forall z \in b (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)) \leftrightarrow \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)))$
40	11 14 39	sbcied2	$⊢ (r = R \land b = B) \to (\underset{˙}{[} +_{r} / p \underset{˙}{]} \underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \forall x \in b \forall y \in b \forall z \in b (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)) \leftrightarrow \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)))$
41	8 10 40	sbcied2	$⊢ r = R \to (\underset{˙}{[} {Base}_{r} / b \underset{˙}{]} \underset{˙}{[} +_{r} / p \underset{˙}{]} \underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \forall x \in b \forall y \in b \forall z \in b (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)) \leftrightarrow \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)))$
42	7 41	anbi12d	$⊢ r = R \to (({mulGrp}_{r} \in Mnd \land \underset{˙}{[} {Base}_{r} / b \underset{˙}{]} \underset{˙}{[} +_{r} / p \underset{˙}{]} \underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \forall x \in b \forall y \in b \forall z \in b (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))) \leftrightarrow (G \in Mnd \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))))$
43		df-ring	$⊢ Ring = \{r \in Grp \| ({mulGrp}_{r} \in Mnd \land \underset{˙}{[} {Base}_{r} / b \underset{˙}{]} \underset{˙}{[} +_{r} / p \underset{˙}{]} \underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \forall x \in b \forall y \in b \forall z \in b (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	42 43	elrab2	$⊢ R \in Ring \leftrightarrow (R \in Grp \land (G \in Mnd \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))))$
45		3anass	$⊢ (R \in Grp \land G \in Mnd \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))) \leftrightarrow (R \in Grp \land (G \in Mnd \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))))$
46	44 45	bitr4i	$⊢ R \in Ring \leftrightarrow (R \in Grp \land G \in Mnd \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)))$

Metamath Proof Explorer

Theorem isring

Proof