Step |
Hyp |
Ref |
Expression |
1 |
|
mplsubg.s |
|- S = ( I mPwSer R ) |
2 |
|
mplsubg.p |
|- P = ( I mPoly R ) |
3 |
|
mplsubg.u |
|- U = ( Base ` P ) |
4 |
|
mplsubg.i |
|- ( ph -> I e. W ) |
5 |
|
mpllss.r |
|- ( ph -> R e. Ring ) |
6 |
|
ringgrp |
|- ( R e. Ring -> R e. Grp ) |
7 |
5 6
|
syl |
|- ( ph -> R e. Grp ) |
8 |
1 2 3 4 7
|
mplsubg |
|- ( ph -> U e. ( SubGrp ` S ) ) |
9 |
1 4 5
|
psrring |
|- ( ph -> S e. Ring ) |
10 |
|
eqid |
|- ( Base ` S ) = ( Base ` S ) |
11 |
|
eqid |
|- ( 1r ` S ) = ( 1r ` S ) |
12 |
10 11
|
ringidcl |
|- ( S e. Ring -> ( 1r ` S ) e. ( Base ` S ) ) |
13 |
9 12
|
syl |
|- ( ph -> ( 1r ` S ) e. ( Base ` S ) ) |
14 |
|
eqid |
|- { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |
15 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
16 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
17 |
1 4 5 14 15 16 11
|
psr1 |
|- ( ph -> ( 1r ` S ) = ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) |
18 |
|
ovex |
|- ( NN0 ^m I ) e. _V |
19 |
18
|
mptrabex |
|- ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) e. _V |
20 |
|
funmpt |
|- Fun ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) |
21 |
|
fvex |
|- ( 0g ` R ) e. _V |
22 |
19 20 21
|
3pm3.2i |
|- ( ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) e. _V /\ Fun ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) /\ ( 0g ` R ) e. _V ) |
23 |
22
|
a1i |
|- ( ph -> ( ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) e. _V /\ Fun ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) /\ ( 0g ` R ) e. _V ) ) |
24 |
|
snfi |
|- { ( I X. { 0 } ) } e. Fin |
25 |
24
|
a1i |
|- ( ph -> { ( I X. { 0 } ) } e. Fin ) |
26 |
|
eldifsni |
|- ( k e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ { ( I X. { 0 } ) } ) -> k =/= ( I X. { 0 } ) ) |
27 |
26
|
adantl |
|- ( ( ph /\ k e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ { ( I X. { 0 } ) } ) ) -> k =/= ( I X. { 0 } ) ) |
28 |
|
ifnefalse |
|- ( k =/= ( I X. { 0 } ) -> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) = ( 0g ` R ) ) |
29 |
27 28
|
syl |
|- ( ( ph /\ k e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ { ( I X. { 0 } ) } ) ) -> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) = ( 0g ` R ) ) |
30 |
18
|
rabex |
|- { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V |
31 |
30
|
a1i |
|- ( ph -> { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V ) |
32 |
29 31
|
suppss2 |
|- ( ph -> ( ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) supp ( 0g ` R ) ) C_ { ( I X. { 0 } ) } ) |
33 |
|
suppssfifsupp |
|- ( ( ( ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) e. _V /\ Fun ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) /\ ( 0g ` R ) e. _V ) /\ ( { ( I X. { 0 } ) } e. Fin /\ ( ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) supp ( 0g ` R ) ) C_ { ( I X. { 0 } ) } ) ) -> ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) finSupp ( 0g ` R ) ) |
34 |
23 25 32 33
|
syl12anc |
|- ( ph -> ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) finSupp ( 0g ` R ) ) |
35 |
17 34
|
eqbrtrd |
|- ( ph -> ( 1r ` S ) finSupp ( 0g ` R ) ) |
36 |
2 1 10 15 3
|
mplelbas |
|- ( ( 1r ` S ) e. U <-> ( ( 1r ` S ) e. ( Base ` S ) /\ ( 1r ` S ) finSupp ( 0g ` R ) ) ) |
37 |
13 35 36
|
sylanbrc |
|- ( ph -> ( 1r ` S ) e. U ) |
38 |
4
|
adantr |
|- ( ( ph /\ ( x e. U /\ y e. U ) ) -> I e. W ) |
39 |
5
|
adantr |
|- ( ( ph /\ ( x e. U /\ y e. U ) ) -> R e. Ring ) |
40 |
|
eqid |
|- ( oF + " ( ( x supp ( 0g ` R ) ) X. ( y supp ( 0g ` R ) ) ) ) = ( oF + " ( ( x supp ( 0g ` R ) ) X. ( y supp ( 0g ` R ) ) ) ) |
41 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
42 |
|
simprl |
|- ( ( ph /\ ( x e. U /\ y e. U ) ) -> x e. U ) |
43 |
|
simprr |
|- ( ( ph /\ ( x e. U /\ y e. U ) ) -> y e. U ) |
44 |
1 2 3 38 39 14 15 40 41 42 43
|
mplsubrglem |
|- ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( x ( .r ` S ) y ) e. U ) |
45 |
44
|
ralrimivva |
|- ( ph -> A. x e. U A. y e. U ( x ( .r ` S ) y ) e. U ) |
46 |
|
eqid |
|- ( .r ` S ) = ( .r ` S ) |
47 |
10 11 46
|
issubrg2 |
|- ( S e. Ring -> ( U e. ( SubRing ` S ) <-> ( U e. ( SubGrp ` S ) /\ ( 1r ` S ) e. U /\ A. x e. U A. y e. U ( x ( .r ` S ) y ) e. U ) ) ) |
48 |
9 47
|
syl |
|- ( ph -> ( U e. ( SubRing ` S ) <-> ( U e. ( SubGrp ` S ) /\ ( 1r ` S ) e. U /\ A. x e. U A. y e. U ( x ( .r ` S ) y ) e. U ) ) ) |
49 |
8 37 45 48
|
mpbir3and |
|- ( ph -> U e. ( SubRing ` S ) ) |