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 ) |