Metamath Proof Explorer

Theorem prdsringd

Description: A product of rings is a ring. (Contributed by Mario Carneiro, 11-Mar-2015)

Ref Expression
Hypotheses prdsringd.y 
|- Y = ( S Xs_ R )
prdsringd.i 
|- ( ph -> I e. W )
prdsringd.s 
|- ( ph -> S e. V )
prdsringd.r 
|- ( ph -> R : I --> Ring )
Assertion prdsringd 
|- ( ph -> Y e. Ring )

Proof

Step Hyp Ref Expression
1 prdsringd.y 
 |-  Y = ( S Xs_ R )
2 prdsringd.i 
 |-  ( ph -> I e. W )
3 prdsringd.s 
 |-  ( ph -> S e. V )
4 prdsringd.r 
 |-  ( ph -> R : I --> Ring )
5 ringgrp 
 |-  ( x e. Ring -> x e. Grp )
6 5 ssriv 
 |-  Ring C_ Grp
7 fss 
 |-  ( ( R : I --> Ring /\ Ring C_ Grp ) -> R : I --> Grp )
8 4 6 7 sylancl 
 |-  ( ph -> R : I --> Grp )
9 1 2 3 8 prdsgrpd 
 |-  ( ph -> Y e. Grp )
10 eqid 
 |-  ( S Xs_ ( mulGrp o. R ) ) = ( S Xs_ ( mulGrp o. R ) )
11 mgpf 
 |-  ( mulGrp |` Ring ) : Ring --> Mnd
12 fco2 
 |-  ( ( ( mulGrp |` Ring ) : Ring --> Mnd /\ R : I --> Ring ) -> ( mulGrp o. R ) : I --> Mnd )
13 11 4 12 sylancr 
 |-  ( ph -> ( mulGrp o. R ) : I --> Mnd )
14 10 2 3 13 prdsmndd 
 |-  ( ph -> ( S Xs_ ( mulGrp o. R ) ) e. Mnd )
15 eqidd 
 |-  ( ph -> ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( mulGrp ` Y ) ) )
16 eqid 
 |-  ( mulGrp ` Y ) = ( mulGrp ` Y )
17 4 ffnd 
 |-  ( ph -> R Fn I )
18 1 16 10 2 3 17 prdsmgp 
 |-  ( ph -> ( ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( S Xs_ ( mulGrp o. R ) ) ) /\ ( +g ` ( mulGrp ` Y ) ) = ( +g ` ( S Xs_ ( mulGrp o. R ) ) ) ) )
19 18 simpld 
 |-  ( ph -> ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( S Xs_ ( mulGrp o. R ) ) ) )
20 18 simprd 
 |-  ( ph -> ( +g ` ( mulGrp ` Y ) ) = ( +g ` ( S Xs_ ( mulGrp o. R ) ) ) )
21 20 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 ) )
22 15 19 21 mndpropd 
 |-  ( ph -> ( ( mulGrp ` Y ) e. Mnd <-> ( S Xs_ ( mulGrp o. R ) ) e. Mnd ) )
23 14 22 mpbird 
 |-  ( ph -> ( mulGrp ` Y ) e. Mnd )
24 4 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> R : I --> Ring )
25 24 ffvelcdmda 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( R ` w ) e. Ring )
26 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
27 3 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> S e. V )
28 27 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> S e. V )
29 2 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> I e. W )
30 29 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> I e. W )
31 17 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> R Fn I )
32 31 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> R Fn I )
33 simplr1 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> x e. ( Base ` Y ) )
34 simpr 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> w e. I )
35 1 26 28 30 32 33 34 prdsbasprj 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( x ` w ) e. ( Base ` ( R ` w ) ) )
36 simpr2 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> y e. ( Base ` Y ) )
37 36 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> y e. ( Base ` Y ) )
38 1 26 28 30 32 37 34 prdsbasprj 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( y ` w ) e. ( Base ` ( R ` w ) ) )
39 simpr3 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> z e. ( Base ` Y ) )
40 39 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> z e. ( Base ` Y ) )
41 1 26 28 30 32 40 34 prdsbasprj 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( z ` w ) e. ( Base ` ( R ` w ) ) )
42 eqid 
 |-  ( Base ` ( R ` w ) ) = ( Base ` ( R ` w ) )
43 eqid 
 |-  ( +g ` ( R ` w ) ) = ( +g ` ( R ` w ) )
44 eqid 
 |-  ( .r ` ( R ` w ) ) = ( .r ` ( R ` w ) )
45 42 43 44 ringdi 
 |-  ( ( ( R ` w ) e. Ring /\ ( ( x ` w ) e. ( Base ` ( R ` w ) ) /\ ( y ` w ) e. ( Base ` ( R ` w ) ) /\ ( z ` w ) e. ( Base ` ( R ` w ) ) ) ) -> ( ( x ` w ) ( .r ` ( R ` w ) ) ( ( y ` w ) ( +g ` ( R ` w ) ) ( z ` w ) ) ) = ( ( ( x ` w ) ( .r ` ( R ` w ) ) ( y ` w ) ) ( +g ` ( R ` w ) ) ( ( x ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) ) )
46 25 35 38 41 45 syl13anc 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( x ` w ) ( .r ` ( R ` w ) ) ( ( y ` w ) ( +g ` ( R ` w ) ) ( z ` w ) ) ) = ( ( ( x ` w ) ( .r ` ( R ` w ) ) ( y ` w ) ) ( +g ` ( R ` w ) ) ( ( x ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) ) )
47 eqid 
 |-  ( +g ` Y ) = ( +g ` Y )
48 1 26 28 30 32 37 40 47 34 prdsplusgfval 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( y ( +g ` Y ) z ) ` w ) = ( ( y ` w ) ( +g ` ( R ` w ) ) ( z ` w ) ) )
49 48 oveq2d 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( x ` w ) ( .r ` ( R ` w ) ) ( ( y ( +g ` Y ) z ) ` w ) ) = ( ( x ` w ) ( .r ` ( R ` w ) ) ( ( y ` w ) ( +g ` ( R ` w ) ) ( z ` w ) ) ) )
50 eqid 
 |-  ( .r ` Y ) = ( .r ` Y )
51 1 26 28 30 32 33 37 50 34 prdsmulrfval 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( x ( .r ` Y ) y ) ` w ) = ( ( x ` w ) ( .r ` ( R ` w ) ) ( y ` w ) ) )
52 1 26 28 30 32 33 40 50 34 prdsmulrfval 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( x ( .r ` Y ) z ) ` w ) = ( ( x ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) )
53 51 52 oveq12d 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( ( x ( .r ` Y ) y ) ` w ) ( +g ` ( R ` w ) ) ( ( x ( .r ` Y ) z ) ` w ) ) = ( ( ( x ` w ) ( .r ` ( R ` w ) ) ( y ` w ) ) ( +g ` ( R ` w ) ) ( ( x ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) ) )
54 46 49 53 3eqtr4d 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( x ` w ) ( .r ` ( R ` w ) ) ( ( y ( +g ` Y ) z ) ` w ) ) = ( ( ( x ( .r ` Y ) y ) ` w ) ( +g ` ( R ` w ) ) ( ( x ( .r ` Y ) z ) ` w ) ) )
55 54 mpteq2dva 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( w e. I |-> ( ( x ` w ) ( .r ` ( R ` w ) ) ( ( y ( +g ` Y ) z ) ` w ) ) ) = ( w e. I |-> ( ( ( x ( .r ` Y ) y ) ` w ) ( +g ` ( R ` w ) ) ( ( x ( .r ` Y ) z ) ` w ) ) ) )
56 simpr1 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> x e. ( Base ` Y ) )
57 ringmnd 
 |-  ( x e. Ring -> x e. Mnd )
58 57 ssriv 
 |-  Ring C_ Mnd
59 fss 
 |-  ( ( R : I --> Ring /\ Ring C_ Mnd ) -> R : I --> Mnd )
60 4 58 59 sylancl 
 |-  ( ph -> R : I --> Mnd )
61 60 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> R : I --> Mnd )
62 1 26 47 27 29 61 36 39 prdsplusgcl 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( y ( +g ` Y ) z ) e. ( Base ` Y ) )
63 1 26 27 29 31 56 62 50 prdsmulrval 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( x ( .r ` Y ) ( y ( +g ` Y ) z ) ) = ( w e. I |-> ( ( x ` w ) ( .r ` ( R ` w ) ) ( ( y ( +g ` Y ) z ) ` w ) ) ) )
64 1 26 50 27 29 24 56 36 prdsmulrcl 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( x ( .r ` Y ) y ) e. ( Base ` Y ) )
65 1 26 50 27 29 24 56 39 prdsmulrcl 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( x ( .r ` Y ) z ) e. ( Base ` Y ) )
66 1 26 27 29 31 64 65 47 prdsplusgval 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( ( x ( .r ` Y ) y ) ( +g ` Y ) ( x ( .r ` Y ) z ) ) = ( w e. I |-> ( ( ( x ( .r ` Y ) y ) ` w ) ( +g ` ( R ` w ) ) ( ( x ( .r ` Y ) z ) ` w ) ) ) )
67 55 63 66 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( x ( .r ` Y ) ( y ( +g ` Y ) z ) ) = ( ( x ( .r ` Y ) y ) ( +g ` Y ) ( x ( .r ` Y ) z ) ) )
68 42 43 44 ringdir 
 |-  ( ( ( R ` w ) e. Ring /\ ( ( x ` w ) e. ( Base ` ( R ` w ) ) /\ ( y ` w ) e. ( Base ` ( R ` w ) ) /\ ( z ` w ) e. ( Base ` ( R ` w ) ) ) ) -> ( ( ( x ` w ) ( +g ` ( R ` w ) ) ( y ` w ) ) ( .r ` ( R ` w ) ) ( z ` w ) ) = ( ( ( x ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) ( +g ` ( R ` w ) ) ( ( y ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) ) )
69 25 35 38 41 68 syl13anc 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( ( x ` w ) ( +g ` ( R ` w ) ) ( y ` w ) ) ( .r ` ( R ` w ) ) ( z ` w ) ) = ( ( ( x ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) ( +g ` ( R ` w ) ) ( ( y ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) ) )
70 1 26 28 30 32 33 37 47 34 prdsplusgfval 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( x ( +g ` Y ) y ) ` w ) = ( ( x ` w ) ( +g ` ( R ` w ) ) ( y ` w ) ) )
71 70 oveq1d 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( ( x ( +g ` Y ) y ) ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) = ( ( ( x ` w ) ( +g ` ( R ` w ) ) ( y ` w ) ) ( .r ` ( R ` w ) ) ( z ` w ) ) )
72 1 26 28 30 32 37 40 50 34 prdsmulrfval 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( y ( .r ` Y ) z ) ` w ) = ( ( y ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) )
73 52 72 oveq12d 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( ( x ( .r ` Y ) z ) ` w ) ( +g ` ( R ` w ) ) ( ( y ( .r ` Y ) z ) ` w ) ) = ( ( ( x ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) ( +g ` ( R ` w ) ) ( ( y ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) ) )
74 69 71 73 3eqtr4d 
 |-  ( ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) /\ w e. I ) -> ( ( ( x ( +g ` Y ) y ) ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) = ( ( ( x ( .r ` Y ) z ) ` w ) ( +g ` ( R ` w ) ) ( ( y ( .r ` Y ) z ) ` w ) ) )
75 74 mpteq2dva 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( w e. I |-> ( ( ( x ( +g ` Y ) y ) ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) ) = ( w e. I |-> ( ( ( x ( .r ` Y ) z ) ` w ) ( +g ` ( R ` w ) ) ( ( y ( .r ` Y ) z ) ` w ) ) ) )
76 1 26 47 27 29 61 56 36 prdsplusgcl 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( x ( +g ` Y ) y ) e. ( Base ` Y ) )
77 1 26 27 29 31 76 39 50 prdsmulrval 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( ( x ( +g ` Y ) y ) ( .r ` Y ) z ) = ( w e. I |-> ( ( ( x ( +g ` Y ) y ) ` w ) ( .r ` ( R ` w ) ) ( z ` w ) ) ) )
78 1 26 50 27 29 24 36 39 prdsmulrcl 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( y ( .r ` Y ) z ) e. ( Base ` Y ) )
79 1 26 27 29 31 65 78 47 prdsplusgval 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( ( x ( .r ` Y ) z ) ( +g ` Y ) ( y ( .r ` Y ) z ) ) = ( w e. I |-> ( ( ( x ( .r ` Y ) z ) ` w ) ( +g ` ( R ` w ) ) ( ( y ( .r ` Y ) z ) ` w ) ) ) )
80 75 77 79 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( ( x ( +g ` Y ) y ) ( .r ` Y ) z ) = ( ( x ( .r ` Y ) z ) ( +g ` Y ) ( y ( .r ` Y ) z ) ) )
81 67 80 jca 
 |-  ( ( ph /\ ( x e. ( Base ` Y ) /\ y e. ( Base ` Y ) /\ z e. ( Base ` Y ) ) ) -> ( ( x ( .r ` Y ) ( y ( +g ` Y ) z ) ) = ( ( x ( .r ` Y ) y ) ( +g ` Y ) ( x ( .r ` Y ) z ) ) /\ ( ( x ( +g ` Y ) y ) ( .r ` Y ) z ) = ( ( x ( .r ` Y ) z ) ( +g ` Y ) ( y ( .r ` Y ) z ) ) ) )
82 81 ralrimivvva 
 |-  ( ph -> A. x e. ( Base ` Y ) A. y e. ( Base ` Y ) A. z e. ( Base ` Y ) ( ( x ( .r ` Y ) ( y ( +g ` Y ) z ) ) = ( ( x ( .r ` Y ) y ) ( +g ` Y ) ( x ( .r ` Y ) z ) ) /\ ( ( x ( +g ` Y ) y ) ( .r ` Y ) z ) = ( ( x ( .r ` Y ) z ) ( +g ` Y ) ( y ( .r ` Y ) z ) ) ) )
83 26 16 47 50 isring 
 |-  ( Y e. Ring <-> ( Y e. Grp /\ ( mulGrp ` Y ) e. Mnd /\ A. x e. ( Base ` Y ) A. y e. ( Base ` Y ) A. z e. ( Base ` Y ) ( ( x ( .r ` Y ) ( y ( +g ` Y ) z ) ) = ( ( x ( .r ` Y ) y ) ( +g ` Y ) ( x ( .r ` Y ) z ) ) /\ ( ( x ( +g ` Y ) y ) ( .r ` Y ) z ) = ( ( x ( .r ` Y ) z ) ( +g ` Y ) ( y ( .r ` Y ) z ) ) ) ) )
84 9 23 82 83 syl3anbrc 
 |-  ( ph -> Y e. Ring )