Theorem 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	⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
	prdscrngd.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	prdscrngd.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	prdscrngd.r	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ CRing )
Assertion	prdscrngd	⊢ ( 𝜑 → 𝑌 ∈ CRing )

Proof

Step	Hyp	Ref	Expression
1		prdscrngd.y	⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2		prdscrngd.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
3		prdscrngd.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4		prdscrngd.r	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ CRing )
5		crngring	⊢ ( 𝑥 ∈ CRing → 𝑥 ∈ Ring )
6	5	ssriv	⊢ CRing ⊆ Ring
7		fss	⊢ ( ( 𝑅 : 𝐼 ⟶ CRing ∧ CRing ⊆ Ring ) → 𝑅 : 𝐼 ⟶ Ring )
8	4 6 7	sylancl	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Ring )
9	1 2 3 8	prdsringd	⊢ ( 𝜑 → 𝑌 ∈ Ring )
10		eqid	⊢ ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) = ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) )
11		fnmgp	⊢ mulGrp Fn V
12		ssv	⊢ CRing ⊆ V
13		fnssres	⊢ ( ( mulGrp Fn V ∧ CRing ⊆ V ) → ( mulGrp ↾ CRing ) Fn CRing )
14	11 12 13	mp2an	⊢ ( mulGrp ↾ CRing ) Fn CRing
15		fvres	⊢ ( 𝑥 ∈ CRing → ( ( mulGrp ↾ CRing ) ‘ 𝑥 ) = ( mulGrp ‘ 𝑥 ) )
16		eqid	⊢ ( mulGrp ‘ 𝑥 ) = ( mulGrp ‘ 𝑥 )
17	16	crngmgp	⊢ ( 𝑥 ∈ CRing → ( mulGrp ‘ 𝑥 ) ∈ CMnd )
18	15 17	eqeltrd	⊢ ( 𝑥 ∈ CRing → ( ( mulGrp ↾ CRing ) ‘ 𝑥 ) ∈ CMnd )
19	18	rgen	⊢ ∀ 𝑥 ∈ CRing ( ( mulGrp ↾ CRing ) ‘ 𝑥 ) ∈ CMnd
20		ffnfv	⊢ ( ( mulGrp ↾ CRing ) : CRing ⟶ CMnd ↔ ( ( mulGrp ↾ CRing ) Fn CRing ∧ ∀ 𝑥 ∈ CRing ( ( mulGrp ↾ CRing ) ‘ 𝑥 ) ∈ CMnd ) )
21	14 19 20	mpbir2an	⊢ ( mulGrp ↾ CRing ) : CRing ⟶ CMnd
22		fco2	⊢ ( ( ( mulGrp ↾ CRing ) : CRing ⟶ CMnd ∧ 𝑅 : 𝐼 ⟶ CRing ) → ( mulGrp ∘ 𝑅 ) : 𝐼 ⟶ CMnd )
23	21 4 22	sylancr	⊢ ( 𝜑 → ( mulGrp ∘ 𝑅 ) : 𝐼 ⟶ CMnd )
24	10 2 3 23	prdscmnd	⊢ ( 𝜑 → ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) ∈ CMnd )
25		eqidd	⊢ ( 𝜑 → ( Base ‘ ( mulGrp ‘ 𝑌 ) ) = ( Base ‘ ( mulGrp ‘ 𝑌 ) ) )
26		eqid	⊢ ( mulGrp ‘ 𝑌 ) = ( mulGrp ‘ 𝑌 )
27	4	ffnd	⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
28	1 26 10 2 3 27	prdsmgp	⊢ ( 𝜑 → ( ( Base ‘ ( mulGrp ‘ 𝑌 ) ) = ( Base ‘ ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) ) ∧ ( +g ‘ ( mulGrp ‘ 𝑌 ) ) = ( +g ‘ ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) ) ) )
29	28	simpld	⊢ ( 𝜑 → ( Base ‘ ( mulGrp ‘ 𝑌 ) ) = ( Base ‘ ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) ) )
30	28	simprd	⊢ ( 𝜑 → ( +g ‘ ( mulGrp ‘ 𝑌 ) ) = ( +g ‘ ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) ) )
31	30	oveqdr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( mulGrp ‘ 𝑌 ) ) ∧ 𝑦 ∈ ( Base ‘ ( mulGrp ‘ 𝑌 ) ) ) ) → ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝑌 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) ) 𝑦 ) )
32	25 29 31	cmnpropd	⊢ ( 𝜑 → ( ( mulGrp ‘ 𝑌 ) ∈ CMnd ↔ ( 𝑆 Xs ( mulGrp ∘ 𝑅 ) ) ∈ CMnd ) )
33	24 32	mpbird	⊢ ( 𝜑 → ( mulGrp ‘ 𝑌 ) ∈ CMnd )
34	26	iscrng	⊢ ( 𝑌 ∈ CRing ↔ ( 𝑌 ∈ Ring ∧ ( mulGrp ‘ 𝑌 ) ∈ CMnd ) )
35	9 33 34	sylanbrc	⊢ ( 𝜑 → 𝑌 ∈ CRing )