Step |
Hyp |
Ref |
Expression |
1 |
|
prds1.y |
|- Y = ( S Xs_ R ) |
2 |
|
prds1.i |
|- ( ph -> I e. W ) |
3 |
|
prds1.s |
|- ( ph -> S e. V ) |
4 |
|
prds1.r |
|- ( ph -> R : I --> Ring ) |
5 |
|
eqid |
|- ( S Xs_ ( mulGrp o. R ) ) = ( S Xs_ ( mulGrp o. R ) ) |
6 |
|
mgpf |
|- ( mulGrp |` Ring ) : Ring --> Mnd |
7 |
|
fco2 |
|- ( ( ( mulGrp |` Ring ) : Ring --> Mnd /\ R : I --> Ring ) -> ( mulGrp o. R ) : I --> Mnd ) |
8 |
6 4 7
|
sylancr |
|- ( ph -> ( mulGrp o. R ) : I --> Mnd ) |
9 |
5 2 3 8
|
prds0g |
|- ( ph -> ( 0g o. ( mulGrp o. R ) ) = ( 0g ` ( S Xs_ ( mulGrp o. R ) ) ) ) |
10 |
|
eqidd |
|- ( ph -> ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( mulGrp ` Y ) ) ) |
11 |
|
eqid |
|- ( mulGrp ` Y ) = ( mulGrp ` Y ) |
12 |
4
|
ffnd |
|- ( ph -> R Fn I ) |
13 |
1 11 5 2 3 12
|
prdsmgp |
|- ( ph -> ( ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( S Xs_ ( mulGrp o. R ) ) ) /\ ( +g ` ( mulGrp ` Y ) ) = ( +g ` ( S Xs_ ( mulGrp o. R ) ) ) ) ) |
14 |
13
|
simpld |
|- ( ph -> ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( S Xs_ ( mulGrp o. R ) ) ) ) |
15 |
13
|
simprd |
|- ( ph -> ( +g ` ( mulGrp ` Y ) ) = ( +g ` ( S Xs_ ( mulGrp o. R ) ) ) ) |
16 |
15
|
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 ) ) |
17 |
10 14 16
|
grpidpropd |
|- ( ph -> ( 0g ` ( mulGrp ` Y ) ) = ( 0g ` ( S Xs_ ( mulGrp o. R ) ) ) ) |
18 |
9 17
|
eqtr4d |
|- ( ph -> ( 0g o. ( mulGrp o. R ) ) = ( 0g ` ( mulGrp ` Y ) ) ) |
19 |
|
df-ur |
|- 1r = ( 0g o. mulGrp ) |
20 |
19
|
coeq1i |
|- ( 1r o. R ) = ( ( 0g o. mulGrp ) o. R ) |
21 |
|
coass |
|- ( ( 0g o. mulGrp ) o. R ) = ( 0g o. ( mulGrp o. R ) ) |
22 |
20 21
|
eqtri |
|- ( 1r o. R ) = ( 0g o. ( mulGrp o. R ) ) |
23 |
|
eqid |
|- ( 1r ` Y ) = ( 1r ` Y ) |
24 |
11 23
|
ringidval |
|- ( 1r ` Y ) = ( 0g ` ( mulGrp ` Y ) ) |
25 |
18 22 24
|
3eqtr4g |
|- ( ph -> ( 1r o. R ) = ( 1r ` Y ) ) |