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.s 
|- ( ph -> S e. CRing )
mhphf.r 
|- ( ph -> R e. ( SubRing ` S ) )
mhphf.l 
|- ( ph -> L e. R )
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.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 ) ) )