Metamath Proof Explorer

Theorem mhphf

Description: A homogeneous polynomial defines a homogeneous function. Equivalently, an algebraic form is a homogeneous function. (An algebraic form is the function corresponding to a homogeneous polynomial, which in this case is the ( QX ) which corresponds to X ). (Contributed by SN, 28-Jul-2024) (Proof shortened by SN, 8-Mar-2025)

Ref Expression
Hypotheses mhphf.q 
|- Q = ( ( I evalSub S ) ` R )
mhphf.h 
|- H = ( I mHomP U )
mhphf.u 
|- U = ( S |`s R )
mhphf.k 
|- K = ( Base ` S )
mhphf.m 
|- .x. = ( .r ` S )
mhphf.e 
|- .^ = ( .g ` ( mulGrp ` S ) )
mhphf.i 
|- ( ph -> I e. V )
mhphf.s 
|- ( ph -> S e. CRing )
mhphf.r 
|- ( ph -> R e. ( SubRing ` S ) )
mhphf.l 
|- ( ph -> L e. R )
mhphf.n 
|- ( ph -> N e. NN0 )
mhphf.x 
|- ( ph -> X e. ( H ` N ) )
mhphf.a 
|- ( ph -> A e. ( K ^m I ) )
Assertion mhphf 
|- ( ph -> ( ( Q ` X ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` X ) ` A ) ) )

Proof

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