issrg

Description: The predicate "is a semiring". (Contributed by Thierry Arnoux, 21-Mar-2018)

	Ref	Expression
Hypotheses	issrg.b	$⊢ B = {Base}_{R}$
	issrg.g	$⊢ G = {mulGrp}_{R}$
	issrg.p	$⊢ \underset{˙}{+} = +_{R}$
	issrg.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	issrg.0	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	issrg	$⊢ R \in SRing \leftrightarrow (R \in CMnd \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)) \land (\underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0} \land x \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0})))$

Proof

Step	Hyp	Ref	Expression
1		issrg.b	$⊢ B = {Base}_{R}$
2		issrg.g	$⊢ G = {mulGrp}_{R}$
3		issrg.p	$⊢ \underset{˙}{+} = +_{R}$
4		issrg.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		issrg.0	$⊢ \underset{˙}{0} = 0_{R}$
6	2	eleq1i	$⊢ G \in Mnd \leftrightarrow {mulGrp}_{R} \in Mnd$
7	6	bicomi	$⊢ {mulGrp}_{R} \in Mnd \leftrightarrow G \in Mnd$
8	1	fvexi	$⊢ B \in V$
9	3	fvexi	$⊢ \underset{˙}{+} \in V$
10	4	fvexi	$⊢ \underset{˙}{\cdot} \in V$
11	10	a1i	$⊢ (b = B \land p = \underset{˙}{+}) \to \underset{˙}{\cdot} \in V$
12	5	fvexi	$⊢ \underset{˙}{0} \in V$
13	12	a1i	$⊢ ((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to \underset{˙}{0} \in V$
14		simplll	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \to b = B$
15		simplr	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \to t = \underset{˙}{\cdot}$
16		eqidd	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \to x = x$
17		simpllr	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \to p = \underset{˙}{+}$
18	17	oveqd	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \to y p z = y \underset{˙}{+} z$
19	15 16 18	oveq123d	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \to x t (y p z) = x \underset{˙}{\cdot} (y \underset{˙}{+} z)$
20	15	oveqd	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \to x t y = x \underset{˙}{\cdot} y$
21	15	oveqd	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \to x t z = x \underset{˙}{\cdot} z$
22	17 20 21	oveq123d	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \to (x t y) p (x t z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z)$
23	19 22	eqeq12d	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \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))$
24	17	oveqd	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \to x p y = x \underset{˙}{+} y$
25		eqidd	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \to z = z$
26	15 24 25	oveq123d	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \to (x p y) t z = (x \underset{˙}{+} y) \underset{˙}{\cdot} z$
27	15	oveqd	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \to y t z = y \underset{˙}{\cdot} z$
28	17 21 27	oveq123d	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \to (x t z) p (y t z) = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)$
29	26 28	eqeq12d	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \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))$
30	23 29	anbi12d	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \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)))$
31	14 30	raleqbidv	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \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)))$
32	14 31	raleqbidv	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \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)))$
33		simpr	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \to n = \underset{˙}{0}$
34	15 33 16	oveq123d	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \to n t x = \underset{˙}{0} \underset{˙}{\cdot} x$
35	34 33	eqeq12d	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \to (n t x = n \leftrightarrow \underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0})$
36	15 16 33	oveq123d	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \to x t n = x \underset{˙}{\cdot} \underset{˙}{0}$
37	36 33	eqeq12d	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \to (x t n = n \leftrightarrow x \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0})$
38	35 37	anbi12d	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \to ((n t x = n \land x t n = n) \leftrightarrow (\underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0} \land x \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}))$
39	32 38	anbi12d	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \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)) \land (n t x = n \land x t n = n)) \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)) \land (\underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0} \land x \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0})))$
40	14 39	raleqbidv	$⊢ (((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \land n = \underset{˙}{0}) \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)) \land (n t x = n \land x t n = n)) \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)) \land (\underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0} \land x \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0})))$
41	13 40	sbcied	$⊢ ((b = B \land p = \underset{˙}{+}) \land t = \underset{˙}{\cdot}) \to (\underset{˙}{[} \underset{˙}{0} / n \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)) \land (n t x = n \land x t n = n)) \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)) \land (\underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0} \land x \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0})))$
42	11 41	sbcied	$⊢ (b = B \land p = \underset{˙}{+}) \to (\underset{˙}{[} \underset{˙}{\cdot} / t \underset{˙}{]} \underset{˙}{[} \underset{˙}{0} / n \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)) \land (n t x = n \land x t n = n)) \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)) \land (\underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0} \land x \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0})))$
43	8 9 42	sbc2ie	$⊢ \underset{˙}{[} B / b \underset{˙}{]} \underset{˙}{[} \underset{˙}{+} / p \underset{˙}{]} \underset{˙}{[} \underset{˙}{\cdot} / t \underset{˙}{]} \underset{˙}{[} \underset{˙}{0} / n \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)) \land (n t x = n \land x t n = n)) \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)) \land (\underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0} \land x \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}))$
44	7 43	anbi12i	$⊢ ({mulGrp}_{R} \in Mnd \land \underset{˙}{[} B / b \underset{˙}{]} \underset{˙}{[} \underset{˙}{+} / p \underset{˙}{]} \underset{˙}{[} \underset{˙}{\cdot} / t \underset{˙}{]} \underset{˙}{[} \underset{˙}{0} / n \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)) \land (n t x = n \land x t n = n))) \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)) \land (\underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0} \land x \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0})))$
45	44	anbi2i	$⊢ (R \in CMnd \land ({mulGrp}_{R} \in Mnd \land \underset{˙}{[} B / b \underset{˙}{]} \underset{˙}{[} \underset{˙}{+} / p \underset{˙}{]} \underset{˙}{[} \underset{˙}{\cdot} / t \underset{˙}{]} \underset{˙}{[} \underset{˙}{0} / n \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)) \land (n t x = n \land x t n = n)))) \leftrightarrow (R \in CMnd \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)) \land (\underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0} \land x \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}))))$
46		fveq2	$⊢ r = R \to {mulGrp}_{r} = {mulGrp}_{R}$
47	46	eleq1d	$⊢ r = R \to ({mulGrp}_{r} \in Mnd \leftrightarrow {mulGrp}_{R} \in Mnd)$
48		fveq2	$⊢ r = R \to {Base}_{r} = {Base}_{R}$
49	48 1	syl6eqr	$⊢ r = R \to {Base}_{r} = B$
50		fveq2	$⊢ r = R \to +_{r} = +_{R}$
51	50 3	syl6eqr	$⊢ r = R \to +_{r} = \underset{˙}{+}$
52		fveq2	$⊢ r = R \to \cdot_{r} = \cdot_{R}$
53	52 4	syl6eqr	$⊢ r = R \to \cdot_{r} = \underset{˙}{\cdot}$
54		fveq2	$⊢ r = R \to 0_{r} = 0_{R}$
55	54 5	syl6eqr	$⊢ r = R \to 0_{r} = \underset{˙}{0}$
56	55	sbceq1d	$⊢ r = R \to (\underset{˙}{[} 0_{r} / n \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)) \land (n t x = n \land x t n = n)) \leftrightarrow \underset{˙}{[} \underset{˙}{0} / n \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)) \land (n t x = n \land x t n = n)))$
57	53 56	sbceqbid	$⊢ r = R \to (\underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \underset{˙}{[} 0_{r} / n \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)) \land (n t x = n \land x t n = n)) \leftrightarrow \underset{˙}{[} \underset{˙}{\cdot} / t \underset{˙}{]} \underset{˙}{[} \underset{˙}{0} / n \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)) \land (n t x = n \land x t n = n)))$
58	51 57	sbceqbid	$⊢ r = R \to (\underset{˙}{[} +_{r} / p \underset{˙}{]} \underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \underset{˙}{[} 0_{r} / n \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)) \land (n t x = n \land x t n = n)) \leftrightarrow \underset{˙}{[} \underset{˙}{+} / p \underset{˙}{]} \underset{˙}{[} \underset{˙}{\cdot} / t \underset{˙}{]} \underset{˙}{[} \underset{˙}{0} / n \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)) \land (n t x = n \land x t n = n)))$
59	49 58	sbceqbid	$⊢ r = R \to (\underset{˙}{[} {Base}_{r} / b \underset{˙}{]} \underset{˙}{[} +_{r} / p \underset{˙}{]} \underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \underset{˙}{[} 0_{r} / n \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)) \land (n t x = n \land x t n = n)) \leftrightarrow \underset{˙}{[} B / b \underset{˙}{]} \underset{˙}{[} \underset{˙}{+} / p \underset{˙}{]} \underset{˙}{[} \underset{˙}{\cdot} / t \underset{˙}{]} \underset{˙}{[} \underset{˙}{0} / n \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)) \land (n t x = n \land x t n = n)))$
60	47 59	anbi12d	$⊢ r = R \to (({mulGrp}_{r} \in Mnd \land \underset{˙}{[} {Base}_{r} / b \underset{˙}{]} \underset{˙}{[} +_{r} / p \underset{˙}{]} \underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \underset{˙}{[} 0_{r} / n \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)) \land (n t x = n \land x t n = n))) \leftrightarrow ({mulGrp}_{R} \in Mnd \land \underset{˙}{[} B / b \underset{˙}{]} \underset{˙}{[} \underset{˙}{+} / p \underset{˙}{]} \underset{˙}{[} \underset{˙}{\cdot} / t \underset{˙}{]} \underset{˙}{[} \underset{˙}{0} / n \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)) \land (n t x = n \land x t n = n))))$
61		df-srg	$⊢ SRing = \{r \in CMnd \| ({mulGrp}_{r} \in Mnd \land \underset{˙}{[} {Base}_{r} / b \underset{˙}{]} \underset{˙}{[} +_{r} / p \underset{˙}{]} \underset{˙}{[} \cdot_{r} / t \underset{˙}{]} \underset{˙}{[} 0_{r} / n \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)) \land (n t x = n \land x t n = n)))\}$
62	60 61	elrab2	$⊢ R \in SRing \leftrightarrow (R \in CMnd \land ({mulGrp}_{R} \in Mnd \land \underset{˙}{[} B / b \underset{˙}{]} \underset{˙}{[} \underset{˙}{+} / p \underset{˙}{]} \underset{˙}{[} \underset{˙}{\cdot} / t \underset{˙}{]} \underset{˙}{[} \underset{˙}{0} / n \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)) \land (n t x = n \land x t n = n))))$
63		3anass	$⊢ (R \in CMnd \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)) \land (\underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0} \land x \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}))) \leftrightarrow (R \in CMnd \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)) \land (\underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0} \land x \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}))))$
64	45 62 63	3bitr4i	$⊢ R \in SRing \leftrightarrow (R \in CMnd \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)) \land (\underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0} \land x \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0})))$

Metamath Proof Explorer

Theorem issrg

Proof