isringd

Description: Properties that determine a ring. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by NM, 2-Aug-2013)

	Ref	Expression
Hypotheses	isringd.b	$⊢ φ \to B = {Base}_{R}$
	isringd.p	$⊢ φ \to \underset{˙}{+} = +_{R}$
	isringd.t	$⊢ φ \to \underset{˙}{\cdot} = \cdot_{R}$
	isringd.g	$⊢ φ \to R \in Grp$
	isringd.c	$⊢ (φ \land x \in B \land y \in B) \to x \underset{˙}{\cdot} y \in B$
	isringd.a	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z)$
	isringd.d	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z)$
	isringd.e	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)$
	isringd.u	$⊢ φ \to \underset{˙}{1} \in B$
	isringd.i	$⊢ (φ \land x \in B) \to \underset{˙}{1} \underset{˙}{\cdot} x = x$
	isringd.h	$⊢ (φ \land x \in B) \to x \underset{˙}{\cdot} \underset{˙}{1} = x$
Assertion	isringd	$⊢ φ \to R \in Ring$

Proof

Step	Hyp	Ref	Expression
1		isringd.b	$⊢ φ \to B = {Base}_{R}$
2		isringd.p	$⊢ φ \to \underset{˙}{+} = +_{R}$
3		isringd.t	$⊢ φ \to \underset{˙}{\cdot} = \cdot_{R}$
4		isringd.g	$⊢ φ \to R \in Grp$
5		isringd.c	$⊢ (φ \land x \in B \land y \in B) \to x \underset{˙}{\cdot} y \in B$
6		isringd.a	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z)$
7		isringd.d	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z)$
8		isringd.e	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)$
9		isringd.u	$⊢ φ \to \underset{˙}{1} \in B$
10		isringd.i	$⊢ (φ \land x \in B) \to \underset{˙}{1} \underset{˙}{\cdot} x = x$
11		isringd.h	$⊢ (φ \land x \in B) \to x \underset{˙}{\cdot} \underset{˙}{1} = x$
12		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
13		eqid	$⊢ {Base}_{R} = {Base}_{R}$
14	12 13	mgpbas	$⊢ {Base}_{R} = {Base}_{{mulGrp}_{R}}$
15	1 14	eqtrdi	$⊢ φ \to B = {Base}_{{mulGrp}_{R}}$
16		eqid	$⊢ \cdot_{R} = \cdot_{R}$
17	12 16	mgpplusg	$⊢ \cdot_{R} = +_{{mulGrp}_{R}}$
18	3 17	eqtrdi	$⊢ φ \to \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
19	15 18 5 6 9 10 11	ismndd	$⊢ φ \to {mulGrp}_{R} \in Mnd$
20	1	eleq2d	$⊢ φ \to (x \in B \leftrightarrow x \in {Base}_{R})$
21	1	eleq2d	$⊢ φ \to (y \in B \leftrightarrow y \in {Base}_{R})$
22	1	eleq2d	$⊢ φ \to (z \in B \leftrightarrow z \in {Base}_{R})$
23	20 21 22	3anbi123d	$⊢ φ \to ((x \in B \land y \in B \land z \in B) \leftrightarrow (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R}))$
24	23	biimpar	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to (x \in B \land y \in B \land z \in B)$
25	3	adantr	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to \underset{˙}{\cdot} = \cdot_{R}$
26		eqidd	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to x = x$
27	2	oveqdr	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to y \underset{˙}{+} z = y +_{R} z$
28	25 26 27	oveq123d	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to x \underset{˙}{\cdot} (y \underset{˙}{+} z) = x \cdot_{R} (y +_{R} z)$
29	2	adantr	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to \underset{˙}{+} = +_{R}$
30	3	oveqdr	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to x \underset{˙}{\cdot} y = x \cdot_{R} y$
31	3	oveqdr	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to x \underset{˙}{\cdot} z = x \cdot_{R} z$
32	29 30 31	oveq123d	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) = (x \cdot_{R} y) +_{R} (x \cdot_{R} z)$
33	7 28 32	3eqtr3d	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to x \cdot_{R} (y +_{R} z) = (x \cdot_{R} y) +_{R} (x \cdot_{R} z)$
34	2	oveqdr	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to x \underset{˙}{+} y = x +_{R} y$
35		eqidd	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to z = z$
36	25 34 35	oveq123d	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x +_{R} y) \cdot_{R} z$
37	3	oveqdr	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to y \underset{˙}{\cdot} z = y \cdot_{R} z$
38	29 31 37	oveq123d	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z) = (x \cdot_{R} z) +_{R} (y \cdot_{R} z)$
39	8 36 38	3eqtr3d	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x +_{R} y) \cdot_{R} z = (x \cdot_{R} z) +_{R} (y \cdot_{R} z)$
40	33 39	jca	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \cdot_{R} (y +_{R} z) = (x \cdot_{R} y) +_{R} (x \cdot_{R} z) \land (x +_{R} y) \cdot_{R} z = (x \cdot_{R} z) +_{R} (y \cdot_{R} z))$
41	24 40	syldan	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to (x \cdot_{R} (y +_{R} z) = (x \cdot_{R} y) +_{R} (x \cdot_{R} z) \land (x +_{R} y) \cdot_{R} z = (x \cdot_{R} z) +_{R} (y \cdot_{R} z))$
42	41	ralrimivvva	$⊢ φ \to \forall x \in {Base}_{R} \forall y \in {Base}_{R} \forall z \in {Base}_{R} (x \cdot_{R} (y +_{R} z) = (x \cdot_{R} y) +_{R} (x \cdot_{R} z) \land (x +_{R} y) \cdot_{R} z = (x \cdot_{R} z) +_{R} (y \cdot_{R} z))$
43		eqid	$⊢ +_{R} = +_{R}$
44	13 12 43 16	isring	$⊢ R \in Ring \leftrightarrow (R \in Grp \land {mulGrp}_{R} \in Mnd \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} \forall z \in {Base}_{R} (x \cdot_{R} (y +_{R} z) = (x \cdot_{R} y) +_{R} (x \cdot_{R} z) \land (x +_{R} y) \cdot_{R} z = (x \cdot_{R} z) +_{R} (y \cdot_{R} z)))$
45	4 19 42 44	syl3anbrc	$⊢ φ \to R \in Ring$

Metamath Proof Explorer

Theorem isringd

Proof