prdscrngd

Description: A product of commutative rings is a commutative ring. Since the resulting ring will have zero divisors in all nontrivial cases, this cannot be strengthened much further. (Contributed by Mario Carneiro, 11-Mar-2015)

	Ref	Expression
Hypotheses	prdscrngd.y	$⊢ Y = S ⨉_{𝑠} R$
	prdscrngd.i	$⊢ φ \to I \in W$
	prdscrngd.s	$⊢ φ \to S \in V$
	prdscrngd.r	$⊢ φ \to R : I ⟶ CRing$
Assertion	prdscrngd	$⊢ φ \to Y \in CRing$

Proof

Step	Hyp	Ref	Expression
1		prdscrngd.y	$⊢ Y = S ⨉_{𝑠} R$
2		prdscrngd.i	$⊢ φ \to I \in W$
3		prdscrngd.s	$⊢ φ \to S \in V$
4		prdscrngd.r	$⊢ φ \to R : I ⟶ CRing$
5		crngring	$⊢ x \in CRing \to x \in Ring$
6	5	ssriv	$⊢ CRing \subseteq Ring$
7		fss	$⊢ (R : I ⟶ CRing \land CRing \subseteq Ring) \to R : I ⟶ Ring$
8	4 6 7	sylancl	$⊢ φ \to R : I ⟶ Ring$
9	1 2 3 8	prdsringd	$⊢ φ \to Y \in Ring$
10		eqid	$⊢ S ⨉_{𝑠} (mulGrp \circ R) = S ⨉_{𝑠} (mulGrp \circ R)$
11		fnmgp	$⊢ mulGrp Fn V$
12		ssv	$⊢ CRing \subseteq V$
13		fnssres	$⊢ (mulGrp Fn V \land CRing \subseteq V) \to ({mulGrp ↾}_{CRing}) Fn CRing$
14	11 12 13	mp2an	$⊢ ({mulGrp ↾}_{CRing}) Fn CRing$
15		fvres	$⊢ x \in CRing \to ({mulGrp ↾}_{CRing}) (x) = {mulGrp}_{x}$
16		eqid	$⊢ {mulGrp}_{x} = {mulGrp}_{x}$
17	16	crngmgp	$⊢ x \in CRing \to {mulGrp}_{x} \in CMnd$
18	15 17	eqeltrd	$⊢ x \in CRing \to ({mulGrp ↾}_{CRing}) (x) \in CMnd$
19	18	rgen	$⊢ \forall x \in CRing ({mulGrp ↾}_{CRing}) (x) \in CMnd$
20		ffnfv	$⊢ ({mulGrp ↾}_{CRing}) : CRing ⟶ CMnd \leftrightarrow (({mulGrp ↾}_{CRing}) Fn CRing \land \forall x \in CRing ({mulGrp ↾}_{CRing}) (x) \in CMnd)$
21	14 19 20	mpbir2an	$⊢ ({mulGrp ↾}_{CRing}) : CRing ⟶ CMnd$
22		fco2	$⊢ (({mulGrp ↾}_{CRing}) : CRing ⟶ CMnd \land R : I ⟶ CRing) \to (mulGrp \circ R) : I ⟶ CMnd$
23	21 4 22	sylancr	$⊢ φ \to (mulGrp \circ R) : I ⟶ CMnd$
24	10 2 3 23	prdscmnd	$⊢ φ \to S ⨉_{𝑠} (mulGrp \circ R) \in CMnd$
25		eqidd	$⊢ φ \to {Base}_{{mulGrp}_{Y}} = {Base}_{{mulGrp}_{Y}}$
26		eqid	$⊢ {mulGrp}_{Y} = {mulGrp}_{Y}$
27	4	ffnd	$⊢ φ \to R Fn I$
28	1 26 10 2 3 27	prdsmgp	$⊢ φ \to ({Base}_{{mulGrp}_{Y}} = {Base}_{(S ⨉_{𝑠} (mulGrp \circ R))} \land +_{{mulGrp}_{Y}} = +_{(S ⨉_{𝑠} (mulGrp \circ R))})$
29	28	simpld	$⊢ φ \to {Base}_{{mulGrp}_{Y}} = {Base}_{(S ⨉_{𝑠} (mulGrp \circ R))}$
30	28	simprd	$⊢ φ \to +_{{mulGrp}_{Y}} = +_{(S ⨉_{𝑠} (mulGrp \circ R))}$
31	30	oveqdr	$⊢ (φ \land (x \in {Base}_{{mulGrp}_{Y}} \land y \in {Base}_{{mulGrp}_{Y}})) \to x +_{{mulGrp}_{Y}} y = x +_{(S ⨉_{𝑠} (mulGrp \circ R))} y$
32	25 29 31	cmnpropd	$⊢ φ \to ({mulGrp}_{Y} \in CMnd \leftrightarrow S ⨉_{𝑠} (mulGrp \circ R) \in CMnd)$
33	24 32	mpbird	$⊢ φ \to {mulGrp}_{Y} \in CMnd$
34	26	iscrng	$⊢ Y \in CRing \leftrightarrow (Y \in Ring \land {mulGrp}_{Y} \in CMnd)$
35	9 33 34	sylanbrc	$⊢ φ \to Y \in CRing$

Metamath Proof Explorer

Theorem prdscrngd

Proof