iscrngd

Description: Properties that determine a commutative ring. (Contributed by Mario Carneiro, 7-Jan-2015)

	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$
	iscrngd.c	$⊢ (φ \land x \in B \land y \in B) \to x \underset{˙}{\cdot} y = y \underset{˙}{\cdot} x$
Assertion	iscrngd	$⊢ φ \to R \in CRing$

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		iscrngd.c	$⊢ (φ \land x \in B \land y \in B) \to x \underset{˙}{\cdot} y = y \underset{˙}{\cdot} x$
13	1 2 3 4 5 6 7 8 9 10 11	isringd	$⊢ φ \to R \in Ring$
14		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
15		eqid	$⊢ {Base}_{R} = {Base}_{R}$
16	14 15	mgpbas	$⊢ {Base}_{R} = {Base}_{{mulGrp}_{R}}$
17	1 16	eqtrdi	$⊢ φ \to B = {Base}_{{mulGrp}_{R}}$
18		eqid	$⊢ \cdot_{R} = \cdot_{R}$
19	14 18	mgpplusg	$⊢ \cdot_{R} = +_{{mulGrp}_{R}}$
20	3 19	eqtrdi	$⊢ φ \to \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
21	17 20 5 6 9 10 11	ismndd	$⊢ φ \to {mulGrp}_{R} \in Mnd$
22	17 20 21 12	iscmnd	$⊢ φ \to {mulGrp}_{R} \in CMnd$
23	14	iscrng	$⊢ R \in CRing \leftrightarrow (R \in Ring \land {mulGrp}_{R} \in CMnd)$
24	13 22 23	sylanbrc	$⊢ φ \to R \in CRing$

Metamath Proof Explorer

Theorem iscrngd

Proof