This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )