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 )