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
|- Y = ( S Xs_ R )
prdscrngd.i
|- ( ph -> I e. W )
prdscrngd.s
|- ( ph -> S e. V )
prdscrngd.r
|- ( ph -> R : I --> CRing )
Assertion prdscrngd
|- ( ph -> Y e. CRing )

Proof

Step Hyp Ref Expression
1 prdscrngd.y
 |-  Y = ( S Xs_ R )
2 prdscrngd.i
 |-  ( ph -> I e. W )
3 prdscrngd.s
 |-  ( ph -> S e. V )
4 prdscrngd.r
 |-  ( ph -> R : I --> CRing )
5 crngring
 |-  ( x e. CRing -> x e. Ring )
6 5 ssriv
 |-  CRing C_ Ring
7 fss
 |-  ( ( R : I --> CRing /\ CRing C_ Ring ) -> R : I --> Ring )
8 4 6 7 sylancl
 |-  ( ph -> R : I --> Ring )
9 1 2 3 8 prdsringd
 |-  ( ph -> Y e. Ring )
10 eqid
 |-  ( S Xs_ ( mulGrp o. R ) ) = ( S Xs_ ( mulGrp o. R ) )
11 fnmgp
 |-  mulGrp Fn _V
12 ssv
 |-  CRing C_ _V
13 fnssres
 |-  ( ( mulGrp Fn _V /\ CRing C_ _V ) -> ( mulGrp |` CRing ) Fn CRing )
14 11 12 13 mp2an
 |-  ( mulGrp |` CRing ) Fn CRing
15 fvres
 |-  ( x e. CRing -> ( ( mulGrp |` CRing ) ` x ) = ( mulGrp ` x ) )
16 eqid
 |-  ( mulGrp ` x ) = ( mulGrp ` x )
17 16 crngmgp
 |-  ( x e. CRing -> ( mulGrp ` x ) e. CMnd )
18 15 17 eqeltrd
 |-  ( x e. CRing -> ( ( mulGrp |` CRing ) ` x ) e. CMnd )
19 18 rgen
 |-  A. x e. CRing ( ( mulGrp |` CRing ) ` x ) e. CMnd
20 ffnfv
 |-  ( ( mulGrp |` CRing ) : CRing --> CMnd <-> ( ( mulGrp |` CRing ) Fn CRing /\ A. x e. CRing ( ( mulGrp |` CRing ) ` x ) e. CMnd ) )
21 14 19 20 mpbir2an
 |-  ( mulGrp |` CRing ) : CRing --> CMnd
22 fco2
 |-  ( ( ( mulGrp |` CRing ) : CRing --> CMnd /\ R : I --> CRing ) -> ( mulGrp o. R ) : I --> CMnd )
23 21 4 22 sylancr
 |-  ( ph -> ( mulGrp o. R ) : I --> CMnd )
24 10 2 3 23 prdscmnd
 |-  ( ph -> ( S Xs_ ( mulGrp o. R ) ) e. CMnd )
25 eqidd
 |-  ( ph -> ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( mulGrp ` Y ) ) )
26 eqid
 |-  ( mulGrp ` Y ) = ( mulGrp ` Y )
27 4 ffnd
 |-  ( ph -> R Fn I )
28 1 26 10 2 3 27 prdsmgp
 |-  ( ph -> ( ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( S Xs_ ( mulGrp o. R ) ) ) /\ ( +g ` ( mulGrp ` Y ) ) = ( +g ` ( S Xs_ ( mulGrp o. R ) ) ) ) )
29 28 simpld
 |-  ( ph -> ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( S Xs_ ( mulGrp o. R ) ) ) )
30 28 simprd
 |-  ( ph -> ( +g ` ( mulGrp ` Y ) ) = ( +g ` ( S Xs_ ( mulGrp o. R ) ) ) )
31 30 oveqdr
 |-  ( ( ph /\ ( x e. ( Base ` ( mulGrp ` Y ) ) /\ y e. ( Base ` ( mulGrp ` Y ) ) ) ) -> ( x ( +g ` ( mulGrp ` Y ) ) y ) = ( x ( +g ` ( S Xs_ ( mulGrp o. R ) ) ) y ) )
32 25 29 31 cmnpropd
 |-  ( ph -> ( ( mulGrp ` Y ) e. CMnd <-> ( S Xs_ ( mulGrp o. R ) ) e. CMnd ) )
33 24 32 mpbird
 |-  ( ph -> ( mulGrp ` Y ) e. CMnd )
34 26 iscrng
 |-  ( Y e. CRing <-> ( Y e. Ring /\ ( mulGrp ` Y ) e. CMnd ) )
35 9 33 34 sylanbrc
 |-  ( ph -> Y e. CRing )