| Step |
Hyp |
Ref |
Expression |
| 1 |
|
mhphf.q |
|- Q = ( ( I evalSub S ) ` R ) |
| 2 |
|
mhphf.h |
|- H = ( I mHomP U ) |
| 3 |
|
mhphf.u |
|- U = ( S |`s R ) |
| 4 |
|
mhphf.k |
|- K = ( Base ` S ) |
| 5 |
|
mhphf.m |
|- .x. = ( .r ` S ) |
| 6 |
|
mhphf.e |
|- .^ = ( .g ` ( mulGrp ` S ) ) |
| 7 |
|
mhphf.s |
|- ( ph -> S e. CRing ) |
| 8 |
|
mhphf.r |
|- ( ph -> R e. ( SubRing ` S ) ) |
| 9 |
|
mhphf.l |
|- ( ph -> L e. R ) |
| 10 |
|
mhphf.x |
|- ( ph -> X e. ( H ` N ) ) |
| 11 |
|
mhphf.a |
|- ( ph -> A e. ( K ^m I ) ) |
| 12 |
|
elmapi |
|- ( A e. ( K ^m I ) -> A : I --> K ) |
| 13 |
11 12
|
syl |
|- ( ph -> A : I --> K ) |
| 14 |
13
|
ffnd |
|- ( ph -> A Fn I ) |
| 15 |
11 14
|
fndmexd |
|- ( ph -> I e. _V ) |
| 16 |
15
|
adantr |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> I e. _V ) |
| 17 |
9
|
adantr |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> L e. R ) |
| 18 |
14
|
adantr |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> A Fn I ) |
| 19 |
|
eqidd |
|- ( ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) /\ i e. I ) -> ( A ` i ) = ( A ` i ) ) |
| 20 |
16 17 18 19
|
ofc1 |
|- ( ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) /\ i e. I ) -> ( ( ( I X. { L } ) oF .x. A ) ` i ) = ( L .x. ( A ` i ) ) ) |
| 21 |
20
|
oveq2d |
|- ( ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) /\ i e. I ) -> ( ( b ` i ) .^ ( ( ( I X. { L } ) oF .x. A ) ` i ) ) = ( ( b ` i ) .^ ( L .x. ( A ` i ) ) ) ) |
| 22 |
|
eqid |
|- ( mulGrp ` S ) = ( mulGrp ` S ) |
| 23 |
22
|
crngmgp |
|- ( S e. CRing -> ( mulGrp ` S ) e. CMnd ) |
| 24 |
7 23
|
syl |
|- ( ph -> ( mulGrp ` S ) e. CMnd ) |
| 25 |
24
|
ad2antrr |
|- ( ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) /\ i e. I ) -> ( mulGrp ` S ) e. CMnd ) |
| 26 |
|
elrabi |
|- ( b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } -> b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) |
| 27 |
|
eqid |
|- { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |
| 28 |
27
|
psrbagf |
|- ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> b : I --> NN0 ) |
| 29 |
26 28
|
syl |
|- ( b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } -> b : I --> NN0 ) |
| 30 |
29
|
adantl |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> b : I --> NN0 ) |
| 31 |
30
|
ffvelcdmda |
|- ( ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) /\ i e. I ) -> ( b ` i ) e. NN0 ) |
| 32 |
4
|
subrgss |
|- ( R e. ( SubRing ` S ) -> R C_ K ) |
| 33 |
8 32
|
syl |
|- ( ph -> R C_ K ) |
| 34 |
33 9
|
sseldd |
|- ( ph -> L e. K ) |
| 35 |
34
|
ad2antrr |
|- ( ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) /\ i e. I ) -> L e. K ) |
| 36 |
13
|
adantr |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> A : I --> K ) |
| 37 |
36
|
ffvelcdmda |
|- ( ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) /\ i e. I ) -> ( A ` i ) e. K ) |
| 38 |
22 4
|
mgpbas |
|- K = ( Base ` ( mulGrp ` S ) ) |
| 39 |
22 5
|
mgpplusg |
|- .x. = ( +g ` ( mulGrp ` S ) ) |
| 40 |
38 6 39
|
mulgnn0di |
|- ( ( ( mulGrp ` S ) e. CMnd /\ ( ( b ` i ) e. NN0 /\ L e. K /\ ( A ` i ) e. K ) ) -> ( ( b ` i ) .^ ( L .x. ( A ` i ) ) ) = ( ( ( b ` i ) .^ L ) .x. ( ( b ` i ) .^ ( A ` i ) ) ) ) |
| 41 |
25 31 35 37 40
|
syl13anc |
|- ( ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) /\ i e. I ) -> ( ( b ` i ) .^ ( L .x. ( A ` i ) ) ) = ( ( ( b ` i ) .^ L ) .x. ( ( b ` i ) .^ ( A ` i ) ) ) ) |
| 42 |
21 41
|
eqtrd |
|- ( ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) /\ i e. I ) -> ( ( b ` i ) .^ ( ( ( I X. { L } ) oF .x. A ) ` i ) ) = ( ( ( b ` i ) .^ L ) .x. ( ( b ` i ) .^ ( A ` i ) ) ) ) |
| 43 |
42
|
mpteq2dva |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( i e. I |-> ( ( b ` i ) .^ ( ( ( I X. { L } ) oF .x. A ) ` i ) ) ) = ( i e. I |-> ( ( ( b ` i ) .^ L ) .x. ( ( b ` i ) .^ ( A ` i ) ) ) ) ) |
| 44 |
43
|
oveq2d |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( ( ( I X. { L } ) oF .x. A ) ` i ) ) ) ) = ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( ( b ` i ) .^ L ) .x. ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) |
| 45 |
|
eqid |
|- ( 1r ` S ) = ( 1r ` S ) |
| 46 |
22 45
|
ringidval |
|- ( 1r ` S ) = ( 0g ` ( mulGrp ` S ) ) |
| 47 |
7
|
adantr |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> S e. CRing ) |
| 48 |
47 23
|
syl |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( mulGrp ` S ) e. CMnd ) |
| 49 |
7
|
crngringd |
|- ( ph -> S e. Ring ) |
| 50 |
22
|
ringmgp |
|- ( S e. Ring -> ( mulGrp ` S ) e. Mnd ) |
| 51 |
49 50
|
syl |
|- ( ph -> ( mulGrp ` S ) e. Mnd ) |
| 52 |
51
|
ad2antrr |
|- ( ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) /\ i e. I ) -> ( mulGrp ` S ) e. Mnd ) |
| 53 |
38 6 52 31 35
|
mulgnn0cld |
|- ( ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) /\ i e. I ) -> ( ( b ` i ) .^ L ) e. K ) |
| 54 |
38 6 52 31 37
|
mulgnn0cld |
|- ( ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) /\ i e. I ) -> ( ( b ` i ) .^ ( A ` i ) ) e. K ) |
| 55 |
|
eqidd |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( i e. I |-> ( ( b ` i ) .^ L ) ) = ( i e. I |-> ( ( b ` i ) .^ L ) ) ) |
| 56 |
|
eqidd |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) = ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) |
| 57 |
15
|
mptexd |
|- ( ph -> ( i e. I |-> ( ( b ` i ) .^ L ) ) e. _V ) |
| 58 |
57
|
adantr |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( i e. I |-> ( ( b ` i ) .^ L ) ) e. _V ) |
| 59 |
|
fvexd |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( 1r ` S ) e. _V ) |
| 60 |
|
funmpt |
|- Fun ( i e. I |-> ( ( b ` i ) .^ L ) ) |
| 61 |
60
|
a1i |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> Fun ( i e. I |-> ( ( b ` i ) .^ L ) ) ) |
| 62 |
27
|
psrbagfsupp |
|- ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> b finSupp 0 ) |
| 63 |
26 62
|
syl |
|- ( b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } -> b finSupp 0 ) |
| 64 |
63
|
adantl |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> b finSupp 0 ) |
| 65 |
30
|
feqmptd |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> b = ( i e. I |-> ( b ` i ) ) ) |
| 66 |
65
|
oveq1d |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( b supp 0 ) = ( ( i e. I |-> ( b ` i ) ) supp 0 ) ) |
| 67 |
66
|
eqimsscd |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( ( i e. I |-> ( b ` i ) ) supp 0 ) C_ ( b supp 0 ) ) |
| 68 |
38 46 6
|
mulg0 |
|- ( k e. K -> ( 0 .^ k ) = ( 1r ` S ) ) |
| 69 |
68
|
adantl |
|- ( ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) /\ k e. K ) -> ( 0 .^ k ) = ( 1r ` S ) ) |
| 70 |
|
0zd |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> 0 e. ZZ ) |
| 71 |
67 69 31 35 70
|
suppssov1 |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( ( i e. I |-> ( ( b ` i ) .^ L ) ) supp ( 1r ` S ) ) C_ ( b supp 0 ) ) |
| 72 |
58 59 61 64 71
|
fsuppsssuppgd |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( i e. I |-> ( ( b ` i ) .^ L ) ) finSupp ( 1r ` S ) ) |
| 73 |
15
|
mptexd |
|- ( ph -> ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) e. _V ) |
| 74 |
73
|
adantr |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) e. _V ) |
| 75 |
|
funmpt |
|- Fun ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) |
| 76 |
75
|
a1i |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> Fun ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) |
| 77 |
67 69 31 37 70
|
suppssov1 |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) supp ( 1r ` S ) ) C_ ( b supp 0 ) ) |
| 78 |
74 59 76 64 77
|
fsuppsssuppgd |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) finSupp ( 1r ` S ) ) |
| 79 |
38 46 39 48 16 53 54 55 56 72 78
|
gsummptfsadd |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( ( b ` i ) .^ L ) .x. ( ( b ` i ) .^ ( A ` i ) ) ) ) ) = ( ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ L ) ) ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) |
| 80 |
|
eqid |
|- { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } = { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } |
| 81 |
2 10
|
mhprcl |
|- ( ph -> N e. NN0 ) |
| 82 |
27 80 38 6 15 51 34 81
|
mhphflem |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ L ) ) ) = ( N .^ L ) ) |
| 83 |
82
|
oveq1d |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ L ) ) ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) = ( ( N .^ L ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) |
| 84 |
44 79 83
|
3eqtrd |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( ( ( I X. { L } ) oF .x. A ) ` i ) ) ) ) = ( ( N .^ L ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) |
| 85 |
84
|
oveq2d |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( ( X ` b ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( ( ( I X. { L } ) oF .x. A ) ` i ) ) ) ) ) = ( ( X ` b ) .x. ( ( N .^ L ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) |
| 86 |
|
eqid |
|- ( I mPoly U ) = ( I mPoly U ) |
| 87 |
|
eqid |
|- ( Base ` U ) = ( Base ` U ) |
| 88 |
|
eqid |
|- ( Base ` ( I mPoly U ) ) = ( Base ` ( I mPoly U ) ) |
| 89 |
2 86 88 10
|
mhpmpl |
|- ( ph -> X e. ( Base ` ( I mPoly U ) ) ) |
| 90 |
86 87 88 27 89
|
mplelf |
|- ( ph -> X : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` U ) ) |
| 91 |
3
|
subrgbas |
|- ( R e. ( SubRing ` S ) -> R = ( Base ` U ) ) |
| 92 |
91 32
|
eqsstrrd |
|- ( R e. ( SubRing ` S ) -> ( Base ` U ) C_ K ) |
| 93 |
8 92
|
syl |
|- ( ph -> ( Base ` U ) C_ K ) |
| 94 |
90 93
|
fssd |
|- ( ph -> X : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> K ) |
| 95 |
94
|
ffvelcdmda |
|- ( ( ph /\ b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( X ` b ) e. K ) |
| 96 |
26 95
|
sylan2 |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( X ` b ) e. K ) |
| 97 |
38 6 51 81 34
|
mulgnn0cld |
|- ( ph -> ( N .^ L ) e. K ) |
| 98 |
97
|
adantr |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( N .^ L ) e. K ) |
| 99 |
15
|
adantr |
|- ( ( ph /\ b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> I e. _V ) |
| 100 |
7
|
adantr |
|- ( ( ph /\ b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> S e. CRing ) |
| 101 |
11
|
adantr |
|- ( ( ph /\ b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> A e. ( K ^m I ) ) |
| 102 |
|
simpr |
|- ( ( ph /\ b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) |
| 103 |
27 4 22 6 99 100 101 102
|
evlsvvvallem |
|- ( ( ph /\ b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) e. K ) |
| 104 |
26 103
|
sylan2 |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) e. K ) |
| 105 |
4 5 47 96 98 104
|
crng12d |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( ( X ` b ) .x. ( ( N .^ L ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) = ( ( N .^ L ) .x. ( ( X ` b ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) |
| 106 |
85 105
|
eqtrd |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( ( X ` b ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( ( ( I X. { L } ) oF .x. A ) ` i ) ) ) ) ) = ( ( N .^ L ) .x. ( ( X ` b ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) |
| 107 |
106
|
mpteq2dva |
|- ( ph -> ( b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } |-> ( ( X ` b ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( ( ( I X. { L } ) oF .x. A ) ` i ) ) ) ) ) ) = ( b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } |-> ( ( N .^ L ) .x. ( ( X ` b ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) ) |
| 108 |
107
|
oveq2d |
|- ( ph -> ( S gsum ( b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } |-> ( ( X ` b ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( ( ( I X. { L } ) oF .x. A ) ` i ) ) ) ) ) ) ) = ( S gsum ( b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } |-> ( ( N .^ L ) .x. ( ( X ` b ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) ) ) |
| 109 |
|
eqid |
|- ( 0g ` S ) = ( 0g ` S ) |
| 110 |
|
ovex |
|- ( NN0 ^m I ) e. _V |
| 111 |
110
|
rabex |
|- { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V |
| 112 |
111
|
rabex |
|- { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } e. _V |
| 113 |
112
|
a1i |
|- ( ph -> { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } e. _V ) |
| 114 |
49
|
adantr |
|- ( ( ph /\ b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> S e. Ring ) |
| 115 |
4 5 114 95 103
|
ringcld |
|- ( ( ph /\ b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( X ` b ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) e. K ) |
| 116 |
26 115
|
sylan2 |
|- ( ( ph /\ b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( ( X ` b ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) e. K ) |
| 117 |
|
ssrab2 |
|- { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } C_ { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |
| 118 |
|
mptss |
|- ( { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } C_ { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> ( b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } |-> ( ( X ` b ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) C_ ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( X ` b ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) |
| 119 |
117 118
|
mp1i |
|- ( ph -> ( b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } |-> ( ( X ` b ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) C_ ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( X ` b ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) |
| 120 |
27 86 3 88 4 22 6 5 15 7 8 89 11
|
evlsvvvallem2 |
|- ( ph -> ( b e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( X ` b ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) finSupp ( 0g ` S ) ) |
| 121 |
119 120
|
fsuppss |
|- ( ph -> ( b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } |-> ( ( X ` b ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) finSupp ( 0g ` S ) ) |
| 122 |
4 109 5 49 113 97 116 121
|
gsummulc2 |
|- ( ph -> ( S gsum ( b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } |-> ( ( N .^ L ) .x. ( ( X ` b ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) ) = ( ( N .^ L ) .x. ( S gsum ( b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } |-> ( ( X ` b ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) ) ) |
| 123 |
108 122
|
eqtrd |
|- ( ph -> ( S gsum ( b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } |-> ( ( X ` b ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( ( ( I X. { L } ) oF .x. A ) ` i ) ) ) ) ) ) ) = ( ( N .^ L ) .x. ( S gsum ( b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } |-> ( ( X ` b ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) ) ) |
| 124 |
4
|
fvexi |
|- K e. _V |
| 125 |
124
|
a1i |
|- ( ph -> K e. _V ) |
| 126 |
4 5
|
ringcl |
|- ( ( S e. Ring /\ j e. K /\ k e. K ) -> ( j .x. k ) e. K ) |
| 127 |
49 126
|
syl3an1 |
|- ( ( ph /\ j e. K /\ k e. K ) -> ( j .x. k ) e. K ) |
| 128 |
127
|
3expb |
|- ( ( ph /\ ( j e. K /\ k e. K ) ) -> ( j .x. k ) e. K ) |
| 129 |
|
fconst6g |
|- ( L e. K -> ( I X. { L } ) : I --> K ) |
| 130 |
34 129
|
syl |
|- ( ph -> ( I X. { L } ) : I --> K ) |
| 131 |
|
inidm |
|- ( I i^i I ) = I |
| 132 |
128 130 13 15 15 131
|
off |
|- ( ph -> ( ( I X. { L } ) oF .x. A ) : I --> K ) |
| 133 |
125 15 132
|
elmapdd |
|- ( ph -> ( ( I X. { L } ) oF .x. A ) e. ( K ^m I ) ) |
| 134 |
1 2 3 27 80 4 22 6 5 7 8 10 133
|
evlsmhpvvval |
|- ( ph -> ( ( Q ` X ) ` ( ( I X. { L } ) oF .x. A ) ) = ( S gsum ( b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } |-> ( ( X ` b ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( ( ( I X. { L } ) oF .x. A ) ` i ) ) ) ) ) ) ) ) |
| 135 |
1 2 3 27 80 4 22 6 5 7 8 10 11
|
evlsmhpvvval |
|- ( ph -> ( ( Q ` X ) ` A ) = ( S gsum ( b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } |-> ( ( X ` b ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) ) |
| 136 |
135
|
oveq2d |
|- ( ph -> ( ( N .^ L ) .x. ( ( Q ` X ) ` A ) ) = ( ( N .^ L ) .x. ( S gsum ( b e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } |-> ( ( X ` b ) .x. ( ( mulGrp ` S ) gsum ( i e. I |-> ( ( b ` i ) .^ ( A ` i ) ) ) ) ) ) ) ) ) |
| 137 |
123 134 136
|
3eqtr4d |
|- ( ph -> ( ( Q ` X ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` X ) ` A ) ) ) |