Step |
Hyp |
Ref |
Expression |
1 |
|
psrcnrg.s |
|- S = ( I mPwSer R ) |
2 |
|
psrcnrg.i |
|- ( ph -> I e. V ) |
3 |
|
psrcnrg.r |
|- ( ph -> R e. CRing ) |
4 |
|
crngring |
|- ( R e. CRing -> R e. Ring ) |
5 |
3 4
|
syl |
|- ( ph -> R e. Ring ) |
6 |
1 2 5
|
psrring |
|- ( ph -> S e. Ring ) |
7 |
|
eqid |
|- ( mulGrp ` S ) = ( mulGrp ` S ) |
8 |
|
eqid |
|- ( Base ` S ) = ( Base ` S ) |
9 |
7 8
|
mgpbas |
|- ( Base ` S ) = ( Base ` ( mulGrp ` S ) ) |
10 |
9
|
a1i |
|- ( ph -> ( Base ` S ) = ( Base ` ( mulGrp ` S ) ) ) |
11 |
|
eqid |
|- ( .r ` S ) = ( .r ` S ) |
12 |
7 11
|
mgpplusg |
|- ( .r ` S ) = ( +g ` ( mulGrp ` S ) ) |
13 |
12
|
a1i |
|- ( ph -> ( .r ` S ) = ( +g ` ( mulGrp ` S ) ) ) |
14 |
7
|
ringmgp |
|- ( S e. Ring -> ( mulGrp ` S ) e. Mnd ) |
15 |
6 14
|
syl |
|- ( ph -> ( mulGrp ` S ) e. Mnd ) |
16 |
2
|
3ad2ant1 |
|- ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> I e. V ) |
17 |
5
|
3ad2ant1 |
|- ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> R e. Ring ) |
18 |
|
eqid |
|- { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |
19 |
|
simp2 |
|- ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> x e. ( Base ` S ) ) |
20 |
|
simp3 |
|- ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> y e. ( Base ` S ) ) |
21 |
3
|
3ad2ant1 |
|- ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> R e. CRing ) |
22 |
1 16 17 18 11 8 19 20 21
|
psrcom |
|- ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x ( .r ` S ) y ) = ( y ( .r ` S ) x ) ) |
23 |
10 13 15 22
|
iscmnd |
|- ( ph -> ( mulGrp ` S ) e. CMnd ) |
24 |
7
|
iscrng |
|- ( S e. CRing <-> ( S e. Ring /\ ( mulGrp ` S ) e. CMnd ) ) |
25 |
6 23 24
|
sylanbrc |
|- ( ph -> S e. CRing ) |