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)

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 eqid 
 |-  ( Base ` U ) = ( Base ` U )
15 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
16 eqid 
 |-  ( I mPoly U ) = ( I mPoly U )
17 eqid 
 |-  ( +g ` ( I mPoly U ) ) = ( +g ` ( I mPoly U ) )
18 eqid 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
19 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 }
20 3 subrgring 
 |-  ( R e. ( SubRing ` S ) -> U e. Ring )
21 9 20 syl 
 |-  ( ph -> U e. Ring )
22 21 ringgrpd 
 |-  ( ph -> U e. Grp )
23 16 7 21 mplsca 
 |-  ( ph -> U = ( Scalar ` ( I mPoly U ) ) )
24 23 fveq2d 
 |-  ( ph -> ( 0g ` U ) = ( 0g ` ( Scalar ` ( I mPoly U ) ) ) )
25 24 fveq2d 
 |-  ( ph -> ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) = ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` ( Scalar ` ( I mPoly U ) ) ) ) )
26 eqid 
 |-  ( algSc ` ( I mPoly U ) ) = ( algSc ` ( I mPoly U ) )
27 eqid 
 |-  ( Scalar ` ( I mPoly U ) ) = ( Scalar ` ( I mPoly U ) )
28 16 mpllmod 
 |-  ( ( I e. V /\ U e. Ring ) -> ( I mPoly U ) e. LMod )
29 7 21 28 syl2anc 
 |-  ( ph -> ( I mPoly U ) e. LMod )
30 16 mplring 
 |-  ( ( I e. V /\ U e. Ring ) -> ( I mPoly U ) e. Ring )
31 7 21 30 syl2anc 
 |-  ( ph -> ( I mPoly U ) e. Ring )
32 26 27 29 31 ascl0 
 |-  ( ph -> ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` ( Scalar ` ( I mPoly U ) ) ) ) = ( 0g ` ( I mPoly U ) ) )
33 eqid 
 |-  ( 0g ` ( I mPoly U ) ) = ( 0g ` ( I mPoly U ) )
34 16 18 15 33 7 22 mpl0 
 |-  ( ph -> ( 0g ` ( I mPoly U ) ) = ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( 0g ` U ) } ) )
35 25 32 34 3eqtrrd 
 |-  ( ph -> ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( 0g ` U ) } ) = ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) )
36 3 5 ressmulr 
 |-  ( R e. ( SubRing ` S ) -> .x. = ( .r ` U ) )
37 9 36 syl 
 |-  ( ph -> .x. = ( .r ` U ) )
38 37 oveqd 
 |-  ( ph -> ( ( N .^ L ) .x. ( 0g ` U ) ) = ( ( N .^ L ) ( .r ` U ) ( 0g ` U ) ) )
39 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
40 39 subrgsubm 
 |-  ( R e. ( SubRing ` S ) -> R e. ( SubMnd ` ( mulGrp ` S ) ) )
41 9 40 syl 
 |-  ( ph -> R e. ( SubMnd ` ( mulGrp ` S ) ) )
42 6 submmulgcl 
 |-  ( ( R e. ( SubMnd ` ( mulGrp ` S ) ) /\ N e. NN0 /\ L e. R ) -> ( N .^ L ) e. R )
43 41 11 10 42 syl3anc 
 |-  ( ph -> ( N .^ L ) e. R )
44 3 subrgbas 
 |-  ( R e. ( SubRing ` S ) -> R = ( Base ` U ) )
45 9 44 syl 
 |-  ( ph -> R = ( Base ` U ) )
46 43 45 eleqtrd 
 |-  ( ph -> ( N .^ L ) e. ( Base ` U ) )
47 eqid 
 |-  ( .r ` U ) = ( .r ` U )
48 14 47 15 ringrz 
 |-  ( ( U e. Ring /\ ( N .^ L ) e. ( Base ` U ) ) -> ( ( N .^ L ) ( .r ` U ) ( 0g ` U ) ) = ( 0g ` U ) )
49 21 46 48 syl2anc 
 |-  ( ph -> ( ( N .^ L ) ( .r ` U ) ( 0g ` U ) ) = ( 0g ` U ) )
50 38 49 eqtrd 
 |-  ( ph -> ( ( N .^ L ) .x. ( 0g ` U ) ) = ( 0g ` U ) )
51 eqid 
 |-  ( Base ` ( I mPoly U ) ) = ( Base ` ( I mPoly U ) )
52 14 15 ring0cl 
 |-  ( U e. Ring -> ( 0g ` U ) e. ( Base ` U ) )
53 21 52 syl 
 |-  ( ph -> ( 0g ` U ) e. ( Base ` U ) )
54 53 45 eleqtrrd 
 |-  ( ph -> ( 0g ` U ) e. R )
55 1 16 3 4 51 26 7 8 9 54 13 evlsscaval 
 |-  ( ph -> ( ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) e. ( Base ` ( I mPoly U ) ) /\ ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) ) ` A ) = ( 0g ` U ) ) )
56 55 simprd 
 |-  ( ph -> ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) ) ` A ) = ( 0g ` U ) )
57 56 oveq2d 
 |-  ( ph -> ( ( N .^ L ) .x. ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) ) ` A ) ) = ( ( N .^ L ) .x. ( 0g ` U ) ) )
58 4 fvexi 
 |-  K e. _V
59 58 a1i 
 |-  ( ph -> K e. _V )
60 8 crngringd 
 |-  ( ph -> S e. Ring )
61 4 5 ringcl 
 |-  ( ( S e. Ring /\ j e. K /\ k e. K ) -> ( j .x. k ) e. K )
62 60 61 syl3an1 
 |-  ( ( ph /\ j e. K /\ k e. K ) -> ( j .x. k ) e. K )
63 62 3expb 
 |-  ( ( ph /\ ( j e. K /\ k e. K ) ) -> ( j .x. k ) e. K )
64 4 subrgss 
 |-  ( R e. ( SubRing ` S ) -> R C_ K )
65 9 64 syl 
 |-  ( ph -> R C_ K )
66 65 10 sseldd 
 |-  ( ph -> L e. K )
67 fconst6g 
 |-  ( L e. K -> ( I X. { L } ) : I --> K )
68 66 67 syl 
 |-  ( ph -> ( I X. { L } ) : I --> K )
69 elmapi 
 |-  ( A e. ( K ^m I ) -> A : I --> K )
70 13 69 syl 
 |-  ( ph -> A : I --> K )
71 inidm 
 |-  ( I i^i I ) = I
72 63 68 70 7 7 71 off 
 |-  ( ph -> ( ( I X. { L } ) oF .x. A ) : I --> K )
73 59 7 72 elmapdd 
 |-  ( ph -> ( ( I X. { L } ) oF .x. A ) e. ( K ^m I ) )
74 1 16 3 4 51 26 7 8 9 54 73 evlsscaval 
 |-  ( ph -> ( ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) e. ( Base ` ( I mPoly U ) ) /\ ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) ) ` ( ( I X. { L } ) oF .x. A ) ) = ( 0g ` U ) ) )
75 74 simprd 
 |-  ( ph -> ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) ) ` ( ( I X. { L } ) oF .x. A ) ) = ( 0g ` U ) )
76 50 57 75 3eqtr4rd 
 |-  ( ph -> ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) ) ` A ) ) )
77 fvex 
 |-  ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) e. _V
78 fveq2 
 |-  ( f = ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) -> ( Q ` f ) = ( Q ` ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) ) )
79 78 fveq1d 
 |-  ( f = ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) -> ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) ) ` ( ( I X. { L } ) oF .x. A ) ) )
80 78 fveq1d 
 |-  ( f = ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) -> ( ( Q ` f ) ` A ) = ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) ) ` A ) )
81 80 oveq2d 
 |-  ( f = ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) -> ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) = ( ( N .^ L ) .x. ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) ) ` A ) ) )
82 79 81 eqeq12d 
 |-  ( f = ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) -> ( ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) <-> ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) ) ` A ) ) ) )
83 77 82 elab 
 |-  ( ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) e. { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } <-> ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) ) ` A ) ) )
84 76 83 sylibr 
 |-  ( ph -> ( ( algSc ` ( I mPoly U ) ) ` ( 0g ` U ) ) e. { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } )
85 35 84 eqeltrd 
 |-  ( ph -> ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( 0g ` U ) } ) e. { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } )
86 3 subrgcrng 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> U e. CRing )
87 8 9 86 syl2anc 
 |-  ( ph -> U e. CRing )
88 16 mplassa 
 |-  ( ( I e. V /\ U e. CRing ) -> ( I mPoly U ) e. AssAlg )
89 7 87 88 syl2anc 
 |-  ( ph -> ( I mPoly U ) e. AssAlg )
90 89 adantr 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( I mPoly U ) e. AssAlg )
91 23 fveq2d 
 |-  ( ph -> ( Base ` U ) = ( Base ` ( Scalar ` ( I mPoly U ) ) ) )
92 91 eleq2d 
 |-  ( ph -> ( b e. ( Base ` U ) <-> b e. ( Base ` ( Scalar ` ( I mPoly U ) ) ) ) )
93 92 biimpa 
 |-  ( ( ph /\ b e. ( Base ` U ) ) -> b e. ( Base ` ( Scalar ` ( I mPoly U ) ) ) )
94 93 adantrl 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> b e. ( Base ` ( Scalar ` ( I mPoly U ) ) ) )
95 fvexd 
 |-  ( ph -> ( Base ` U ) e. _V )
96 ovex 
 |-  ( NN0 ^m I ) e. _V
97 96 rabex 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V
98 97 a1i 
 |-  ( ph -> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V )
99 eqid 
 |-  ( 1r ` U ) = ( 1r ` U )
100 14 99 ringidcl 
 |-  ( U e. Ring -> ( 1r ` U ) e. ( Base ` U ) )
101 21 100 syl 
 |-  ( ph -> ( 1r ` U ) e. ( Base ` U ) )
102 101 53 ifcld 
 |-  ( ph -> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) e. ( Base ` U ) )
103 102 adantr 
 |-  ( ( ph /\ w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) e. ( Base ` U ) )
104 103 fmpttd 
 |-  ( ph -> ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` U ) )
105 95 98 104 elmapdd 
 |-  ( ph -> ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) e. ( ( Base ` U ) ^m { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) )
106 eqid 
 |-  ( I mPwSer U ) = ( I mPwSer U )
107 eqid 
 |-  ( Base ` ( I mPwSer U ) ) = ( Base ` ( I mPwSer U ) )
108 106 14 18 107 7 psrbas 
 |-  ( ph -> ( Base ` ( I mPwSer U ) ) = ( ( Base ` U ) ^m { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) )
109 105 108 eleqtrrd 
 |-  ( ph -> ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) e. ( Base ` ( I mPwSer U ) ) )
110 97 mptex 
 |-  ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) e. _V
111 110 a1i 
 |-  ( ph -> ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) e. _V )
112 fvexd 
 |-  ( ph -> ( 0g ` U ) e. _V )
113 funmpt 
 |-  Fun ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) )
114 113 a1i 
 |-  ( ph -> Fun ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) )
115 snfi 
 |-  { a } e. Fin
116 115 a1i 
 |-  ( ph -> { a } e. Fin )
117 eldifsnneq 
 |-  ( w e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ { a } ) -> -. w = a )
118 117 adantl 
 |-  ( ( ph /\ w e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ { a } ) ) -> -. w = a )
119 118 iffalsed 
 |-  ( ( ph /\ w e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ { a } ) ) -> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) = ( 0g ` U ) )
120 119 98 suppss2 
 |-  ( ph -> ( ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) supp ( 0g ` U ) ) C_ { a } )
121 116 120 ssfid 
 |-  ( ph -> ( ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) supp ( 0g ` U ) ) e. Fin )
122 111 112 114 121 isfsuppd 
 |-  ( ph -> ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) finSupp ( 0g ` U ) )
123 16 106 107 15 51 mplelbas 
 |-  ( ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) e. ( Base ` ( I mPoly U ) ) <-> ( ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) e. ( Base ` ( I mPwSer U ) ) /\ ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) finSupp ( 0g ` U ) ) )
124 109 122 123 sylanbrc 
 |-  ( ph -> ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) e. ( Base ` ( I mPoly U ) ) )
125 124 adantr 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) e. ( Base ` ( I mPoly U ) ) )
126 eqid 
 |-  ( Base ` ( Scalar ` ( I mPoly U ) ) ) = ( Base ` ( Scalar ` ( I mPoly U ) ) )
127 eqid 
 |-  ( .r ` ( I mPoly U ) ) = ( .r ` ( I mPoly U ) )
128 eqid 
 |-  ( .s ` ( I mPoly U ) ) = ( .s ` ( I mPoly U ) )
129 26 27 126 51 127 128 asclmul1 
 |-  ( ( ( I mPoly U ) e. AssAlg /\ b e. ( Base ` ( Scalar ` ( I mPoly U ) ) ) /\ ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) e. ( Base ` ( I mPoly U ) ) ) -> ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) = ( b ( .s ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) )
130 90 94 125 129 syl3anc 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) = ( b ( .s ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) )
131 simprr 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> b e. ( Base ` U ) )
132 16 128 14 51 47 18 131 125 mplvsca 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( b ( .s ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) = ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { b } ) oF ( .r ` U ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) )
133 130 132 eqtrd 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) = ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { b } ) oF ( .r ` U ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) )
134 vex 
 |-  b e. _V
135 fnconstg 
 |-  ( b e. _V -> ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { b } ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
136 134 135 mp1i 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { b } ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
137 fvex 
 |-  ( 1r ` U ) e. _V
138 fvex 
 |-  ( 0g ` U ) e. _V
139 137 138 ifex 
 |-  if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) e. _V
140 eqid 
 |-  ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) = ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) )
141 139 140 fnmpti 
 |-  ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
142 141 a1i 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) Fn { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
143 97 a1i 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V )
144 inidm 
 |-  ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } i^i { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
145 134 fvconst2 
 |-  ( s e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { b } ) ` s ) = b )
146 145 adantl 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ s e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { b } ) ` s ) = b )
147 equequ1 
 |-  ( w = s -> ( w = a <-> s = a ) )
148 147 ifbid 
 |-  ( w = s -> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) = if ( s = a , ( 1r ` U ) , ( 0g ` U ) ) )
149 137 138 ifex 
 |-  if ( s = a , ( 1r ` U ) , ( 0g ` U ) ) e. _V
150 148 140 149 fvmpt 
 |-  ( s e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> ( ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ` s ) = if ( s = a , ( 1r ` U ) , ( 0g ` U ) ) )
151 150 adantl 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ s e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ` s ) = if ( s = a , ( 1r ` U ) , ( 0g ` U ) ) )
152 136 142 143 143 144 146 151 offval 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { b } ) oF ( .r ` U ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) = ( s e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b ( .r ` U ) if ( s = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) )
153 ovif2 
 |-  ( b ( .r ` U ) if ( s = a , ( 1r ` U ) , ( 0g ` U ) ) ) = if ( s = a , ( b ( .r ` U ) ( 1r ` U ) ) , ( b ( .r ` U ) ( 0g ` U ) ) )
154 21 ad2antrr 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ s e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> U e. Ring )
155 simplrr 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ s e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> b e. ( Base ` U ) )
156 14 47 99 ringridm 
 |-  ( ( U e. Ring /\ b e. ( Base ` U ) ) -> ( b ( .r ` U ) ( 1r ` U ) ) = b )
157 154 155 156 syl2anc 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ s e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( b ( .r ` U ) ( 1r ` U ) ) = b )
158 14 47 15 ringrz 
 |-  ( ( U e. Ring /\ b e. ( Base ` U ) ) -> ( b ( .r ` U ) ( 0g ` U ) ) = ( 0g ` U ) )
159 154 155 158 syl2anc 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ s e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( b ( .r ` U ) ( 0g ` U ) ) = ( 0g ` U ) )
160 157 159 ifeq12d 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ s e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> if ( s = a , ( b ( .r ` U ) ( 1r ` U ) ) , ( b ( .r ` U ) ( 0g ` U ) ) ) = if ( s = a , b , ( 0g ` U ) ) )
161 153 160 syl5eq 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ s e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( b ( .r ` U ) if ( s = a , ( 1r ` U ) , ( 0g ` U ) ) ) = if ( s = a , b , ( 0g ` U ) ) )
162 161 mpteq2dva 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( s e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( b ( .r ` U ) if ( s = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) = ( s e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( s = a , b , ( 0g ` U ) ) ) )
163 133 152 162 3eqtrd 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) = ( s e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( s = a , b , ( 0g ` U ) ) ) )
164 7 adantr 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> I e. V )
165 8 adantr 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> S e. CRing )
166 9 adantr 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> R e. ( SubRing ` S ) )
167 73 adantr 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( I X. { L } ) oF .x. A ) e. ( K ^m I ) )
168 21 adantr 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> U e. Ring )
169 16 51 14 26 164 168 mplasclf 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( algSc ` ( I mPoly U ) ) : ( Base ` U ) --> ( Base ` ( I mPoly U ) ) )
170 169 131 ffvelrnd 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( algSc ` ( I mPoly U ) ) ` b ) e. ( Base ` ( I mPoly U ) ) )
171 eqidd 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` b ) ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` b ) ) ` ( ( I X. { L } ) oF .x. A ) ) )
172 170 171 jca 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( ( algSc ` ( I mPoly U ) ) ` b ) e. ( Base ` ( I mPoly U ) ) /\ ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` b ) ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` b ) ) ` ( ( I X. { L } ) oF .x. A ) ) ) )
173 elrabi 
 |-  ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } -> a e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
174 173 ad2antrl 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> a e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
175 1 16 3 51 4 39 6 15 99 18 140 164 165 166 167 174 evlsbagval 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) e. ( Base ` ( I mPoly U ) ) /\ ( ( Q ` ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( ( ( I X. { L } ) oF .x. A ) ` v ) ) ) ) ) )
176 1 16 3 4 51 164 165 166 167 172 175 127 5 evlsmulval 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) e. ( Base ` ( I mPoly U ) ) /\ ( ( Q ` ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` b ) ) ` ( ( I X. { L } ) oF .x. A ) ) .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( ( ( I X. { L } ) oF .x. A ) ` v ) ) ) ) ) ) )
177 176 simprd 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( Q ` ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` b ) ) ` ( ( I X. { L } ) oF .x. A ) ) .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( ( ( I X. { L } ) oF .x. A ) ` v ) ) ) ) ) )
178 39 ringmgp 
 |-  ( S e. Ring -> ( mulGrp ` S ) e. Mnd )
179 60 178 syl 
 |-  ( ph -> ( mulGrp ` S ) e. Mnd )
180 39 4 mgpbas 
 |-  K = ( Base ` ( mulGrp ` S ) )
181 180 6 mulgnn0cl 
 |-  ( ( ( mulGrp ` S ) e. Mnd /\ N e. NN0 /\ L e. K ) -> ( N .^ L ) e. K )
182 179 11 66 181 syl3anc 
 |-  ( ph -> ( N .^ L ) e. K )
183 182 adantr 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( N .^ L ) e. K )
184 45 65 eqsstrrd 
 |-  ( ph -> ( Base ` U ) C_ K )
185 184 sselda 
 |-  ( ( ph /\ b e. ( Base ` U ) ) -> b e. K )
186 185 adantrl 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> b e. K )
187 4 5 crngcom 
 |-  ( ( S e. CRing /\ ( N .^ L ) e. K /\ b e. K ) -> ( ( N .^ L ) .x. b ) = ( b .x. ( N .^ L ) ) )
188 165 183 186 187 syl3anc 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( N .^ L ) .x. b ) = ( b .x. ( N .^ L ) ) )
189 188 oveq1d 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( ( N .^ L ) .x. b ) .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) ) = ( ( b .x. ( N .^ L ) ) .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) ) )
190 165 crngringd 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> S e. Ring )
191 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
192 39 191 ringidval 
 |-  ( 1r ` S ) = ( 0g ` ( mulGrp ` S ) )
193 39 crngmgp 
 |-  ( S e. CRing -> ( mulGrp ` S ) e. CMnd )
194 8 193 syl 
 |-  ( ph -> ( mulGrp ` S ) e. CMnd )
195 194 adantr 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( mulGrp ` S ) e. CMnd )
196 179 ad2antrr 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ v e. I ) -> ( mulGrp ` S ) e. Mnd )
197 elrabi 
 |-  ( a e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> a e. ( NN0 ^m I ) )
198 elmapi 
 |-  ( a e. ( NN0 ^m I ) -> a : I --> NN0 )
199 173 197 198 3syl 
 |-  ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } -> a : I --> NN0 )
200 199 adantl 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> a : I --> NN0 )
201 200 adantrr 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> a : I --> NN0 )
202 201 ffvelrnda 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ v e. I ) -> ( a ` v ) e. NN0 )
203 70 ad2antrr 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ v e. I ) -> A : I --> K )
204 simpr 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ v e. I ) -> v e. I )
205 203 204 ffvelrnd 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ v e. I ) -> ( A ` v ) e. K )
206 180 6 mulgnn0cl 
 |-  ( ( ( mulGrp ` S ) e. Mnd /\ ( a ` v ) e. NN0 /\ ( A ` v ) e. K ) -> ( ( a ` v ) .^ ( A ` v ) ) e. K )
207 196 202 205 206 syl3anc 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ v e. I ) -> ( ( a ` v ) .^ ( A ` v ) ) e. K )
208 207 fmpttd 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) : I --> K )
209 18 psrbagfsupp 
 |-  ( a e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> a finSupp 0 )
210 209 adantl 
 |-  ( ( ph /\ a e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> a finSupp 0 )
211 210 fsuppimpd 
 |-  ( ( ph /\ a e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( a supp 0 ) e. Fin )
212 173 211 sylan2 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( a supp 0 ) e. Fin )
213 212 adantrr 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( a supp 0 ) e. Fin )
214 201 feqmptd 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> a = ( v e. I |-> ( a ` v ) ) )
215 214 oveq1d 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( a supp 0 ) = ( ( v e. I |-> ( a ` v ) ) supp 0 ) )
216 ssidd 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( a supp 0 ) C_ ( a supp 0 ) )
217 215 216 eqsstrrd 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( v e. I |-> ( a ` v ) ) supp 0 ) C_ ( a supp 0 ) )
218 180 192 6 mulg0 
 |-  ( k e. K -> ( 0 .^ k ) = ( 1r ` S ) )
219 218 adantl 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ k e. K ) -> ( 0 .^ k ) = ( 1r ` S ) )
220 c0ex 
 |-  0 e. _V
221 220 a1i 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> 0 e. _V )
222 217 219 202 205 221 suppssov1 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) supp ( 1r ` S ) ) C_ ( a supp 0 ) )
223 213 222 ssfid 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) supp ( 1r ` S ) ) e. Fin )
224 180 192 195 164 208 223 gsumcl2 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) e. K )
225 4 5 ringass 
 |-  ( ( S e. Ring /\ ( ( N .^ L ) e. K /\ b e. K /\ ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) e. K ) ) -> ( ( ( N .^ L ) .x. b ) .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) ) = ( ( N .^ L ) .x. ( b .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) ) ) )
226 190 183 186 224 225 syl13anc 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( ( N .^ L ) .x. b ) .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) ) = ( ( N .^ L ) .x. ( b .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) ) ) )
227 4 5 ringass 
 |-  ( ( S e. Ring /\ ( b e. K /\ ( N .^ L ) e. K /\ ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) e. K ) ) -> ( ( b .x. ( N .^ L ) ) .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) ) = ( b .x. ( ( N .^ L ) .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) ) ) )
228 190 186 183 224 227 syl13anc 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( b .x. ( N .^ L ) ) .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) ) = ( b .x. ( ( N .^ L ) .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) ) ) )
229 189 226 228 3eqtr3d 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( N .^ L ) .x. ( b .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) ) ) = ( b .x. ( ( N .^ L ) .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) ) ) )
230 13 adantr 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> A e. ( K ^m I ) )
231 45 eleq2d 
 |-  ( ph -> ( b e. R <-> b e. ( Base ` U ) ) )
232 231 biimpar 
 |-  ( ( ph /\ b e. ( Base ` U ) ) -> b e. R )
233 232 adantrl 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> b e. R )
234 1 16 3 4 51 26 164 165 166 233 230 evlsscaval 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( ( algSc ` ( I mPoly U ) ) ` b ) e. ( Base ` ( I mPoly U ) ) /\ ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` b ) ) ` A ) = b ) )
235 1 16 3 51 4 39 6 15 99 18 140 164 165 166 230 174 evlsbagval 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) e. ( Base ` ( I mPoly U ) ) /\ ( ( Q ` ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) ` A ) = ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) ) )
236 1 16 3 4 51 164 165 166 230 234 235 127 5 evlsmulval 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) e. ( Base ` ( I mPoly U ) ) /\ ( ( Q ` ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) ) ` A ) = ( b .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) ) ) )
237 236 simprd 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( Q ` ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) ) ` A ) = ( b .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) ) )
238 237 oveq2d 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( N .^ L ) .x. ( ( Q ` ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) ) ` A ) ) = ( ( N .^ L ) .x. ( b .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) ) ) )
239 1 16 3 4 51 26 164 165 166 233 167 evlsscaval 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( ( algSc ` ( I mPoly U ) ) ` b ) e. ( Base ` ( I mPoly U ) ) /\ ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` b ) ) ` ( ( I X. { L } ) oF .x. A ) ) = b ) )
240 239 simprd 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` b ) ) ` ( ( I X. { L } ) oF .x. A ) ) = b )
241 fconst6g 
 |-  ( L e. R -> ( I X. { L } ) : I --> R )
242 10 241 syl 
 |-  ( ph -> ( I X. { L } ) : I --> R )
243 242 ffnd 
 |-  ( ph -> ( I X. { L } ) Fn I )
244 243 adantr 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( I X. { L } ) Fn I )
245 70 ffnd 
 |-  ( ph -> A Fn I )
246 245 adantr 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> A Fn I )
247 10 ad2antrr 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ v e. I ) -> L e. R )
248 fvconst2g 
 |-  ( ( L e. R /\ v e. I ) -> ( ( I X. { L } ) ` v ) = L )
249 247 204 248 syl2anc 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ v e. I ) -> ( ( I X. { L } ) ` v ) = L )
250 eqidd 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ v e. I ) -> ( A ` v ) = ( A ` v ) )
251 244 246 164 164 71 249 250 ofval 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ v e. I ) -> ( ( ( I X. { L } ) oF .x. A ) ` v ) = ( L .x. ( A ` v ) ) )
252 251 oveq2d 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ v e. I ) -> ( ( a ` v ) .^ ( ( ( I X. { L } ) oF .x. A ) ` v ) ) = ( ( a ` v ) .^ ( L .x. ( A ` v ) ) ) )
253 194 ad2antrr 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ v e. I ) -> ( mulGrp ` S ) e. CMnd )
254 66 ad2antrr 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ v e. I ) -> L e. K )
255 39 5 mgpplusg 
 |-  .x. = ( +g ` ( mulGrp ` S ) )
256 180 6 255 mulgnn0di 
 |-  ( ( ( mulGrp ` S ) e. CMnd /\ ( ( a ` v ) e. NN0 /\ L e. K /\ ( A ` v ) e. K ) ) -> ( ( a ` v ) .^ ( L .x. ( A ` v ) ) ) = ( ( ( a ` v ) .^ L ) .x. ( ( a ` v ) .^ ( A ` v ) ) ) )
257 253 202 254 205 256 syl13anc 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ v e. I ) -> ( ( a ` v ) .^ ( L .x. ( A ` v ) ) ) = ( ( ( a ` v ) .^ L ) .x. ( ( a ` v ) .^ ( A ` v ) ) ) )
258 252 257 eqtrd 
 |-  ( ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) /\ v e. I ) -> ( ( a ` v ) .^ ( ( ( I X. { L } ) oF .x. A ) ` v ) ) = ( ( ( a ` v ) .^ L ) .x. ( ( a ` v ) .^ ( A ` v ) ) ) )
259 258 mpteq2dva 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( v e. I |-> ( ( a ` v ) .^ ( ( ( I X. { L } ) oF .x. A ) ` v ) ) ) = ( v e. I |-> ( ( ( a ` v ) .^ L ) .x. ( ( a ` v ) .^ ( A ` v ) ) ) ) )
260 259 oveq2d 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( ( ( I X. { L } ) oF .x. A ) ` v ) ) ) ) = ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( ( a ` v ) .^ L ) .x. ( ( a ` v ) .^ ( A ` v ) ) ) ) ) )
261 194 adantr 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( mulGrp ` S ) e. CMnd )
262 7 adantr 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> I e. V )
263 179 ad2antrr 
 |-  ( ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) /\ v e. I ) -> ( mulGrp ` S ) e. Mnd )
264 200 ffvelrnda 
 |-  ( ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) /\ v e. I ) -> ( a ` v ) e. NN0 )
265 66 ad2antrr 
 |-  ( ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) /\ v e. I ) -> L e. K )
266 180 6 mulgnn0cl 
 |-  ( ( ( mulGrp ` S ) e. Mnd /\ ( a ` v ) e. NN0 /\ L e. K ) -> ( ( a ` v ) .^ L ) e. K )
267 263 264 265 266 syl3anc 
 |-  ( ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) /\ v e. I ) -> ( ( a ` v ) .^ L ) e. K )
268 70 ffvelrnda 
 |-  ( ( ph /\ v e. I ) -> ( A ` v ) e. K )
269 268 adantlr 
 |-  ( ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) /\ v e. I ) -> ( A ` v ) e. K )
270 263 264 269 206 syl3anc 
 |-  ( ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) /\ v e. I ) -> ( ( a ` v ) .^ ( A ` v ) ) e. K )
271 eqidd 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( v e. I |-> ( ( a ` v ) .^ L ) ) = ( v e. I |-> ( ( a ` v ) .^ L ) ) )
272 eqidd 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) = ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) )
273 262 mptexd 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( v e. I |-> ( ( a ` v ) .^ L ) ) e. _V )
274 fvexd 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( 1r ` S ) e. _V )
275 funmpt 
 |-  Fun ( v e. I |-> ( ( a ` v ) .^ L ) )
276 275 a1i 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> Fun ( v e. I |-> ( ( a ` v ) .^ L ) ) )
277 200 feqmptd 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> a = ( v e. I |-> ( a ` v ) ) )
278 277 oveq1d 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( a supp 0 ) = ( ( v e. I |-> ( a ` v ) ) supp 0 ) )
279 ssidd 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( a supp 0 ) C_ ( a supp 0 ) )
280 278 279 eqsstrrd 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( ( v e. I |-> ( a ` v ) ) supp 0 ) C_ ( a supp 0 ) )
281 218 adantl 
 |-  ( ( ( ph /\ a 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 ) )
282 220 a1i 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> 0 e. _V )
283 280 281 264 265 282 suppssov1 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( ( v e. I |-> ( ( a ` v ) .^ L ) ) supp ( 1r ` S ) ) C_ ( a supp 0 ) )
284 212 283 ssfid 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( ( v e. I |-> ( ( a ` v ) .^ L ) ) supp ( 1r ` S ) ) e. Fin )
285 273 274 276 284 isfsuppd 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( v e. I |-> ( ( a ` v ) .^ L ) ) finSupp ( 1r ` S ) )
286 262 mptexd 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) e. _V )
287 funmpt 
 |-  Fun ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) )
288 287 a1i 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> Fun ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) )
289 280 281 264 269 282 suppssov1 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) supp ( 1r ` S ) ) C_ ( a supp 0 ) )
290 212 289 ssfid 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) supp ( 1r ` S ) ) e. Fin )
291 286 274 288 290 isfsuppd 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) finSupp ( 1r ` S ) )
292 180 192 255 261 262 267 270 271 272 285 291 gsummptfsadd 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( ( a ` v ) .^ L ) .x. ( ( a ` v ) .^ ( A ` v ) ) ) ) ) = ( ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ L ) ) ) .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) ) )
293 18 19 180 6 7 179 66 11 mhphflem 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ L ) ) ) = ( N .^ L ) )
294 293 oveq1d 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ L ) ) ) .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) ) = ( ( N .^ L ) .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) ) )
295 292 294 eqtrd 
 |-  ( ( ph /\ a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } ) -> ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( ( a ` v ) .^ L ) .x. ( ( a ` v ) .^ ( A ` v ) ) ) ) ) = ( ( N .^ L ) .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) ) )
296 295 adantrr 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( ( a ` v ) .^ L ) .x. ( ( a ` v ) .^ ( A ` v ) ) ) ) ) = ( ( N .^ L ) .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) ) )
297 260 296 eqtrd 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( ( ( I X. { L } ) oF .x. A ) ` v ) ) ) ) = ( ( N .^ L ) .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) ) )
298 240 297 oveq12d 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` b ) ) ` ( ( I X. { L } ) oF .x. A ) ) .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( ( ( I X. { L } ) oF .x. A ) ` v ) ) ) ) ) = ( b .x. ( ( N .^ L ) .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( A ` v ) ) ) ) ) ) )
299 229 238 298 3eqtr4rd 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( ( Q ` ( ( algSc ` ( I mPoly U ) ) ` b ) ) ` ( ( I X. { L } ) oF .x. A ) ) .x. ( ( mulGrp ` S ) gsum ( v e. I |-> ( ( a ` v ) .^ ( ( ( I X. { L } ) oF .x. A ) ` v ) ) ) ) ) = ( ( N .^ L ) .x. ( ( Q ` ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) ) ` A ) ) )
300 177 299 eqtrd 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( Q ` ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) ) ` A ) ) )
301 ovex 
 |-  ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) e. _V
302 fveq2 
 |-  ( f = ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) -> ( Q ` f ) = ( Q ` ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) ) )
303 302 fveq1d 
 |-  ( f = ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) -> ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( Q ` ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) ) ` ( ( I X. { L } ) oF .x. A ) ) )
304 302 fveq1d 
 |-  ( f = ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) -> ( ( Q ` f ) ` A ) = ( ( Q ` ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) ) ` A ) )
305 304 oveq2d 
 |-  ( f = ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) -> ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) = ( ( N .^ L ) .x. ( ( Q ` ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) ) ` A ) ) )
306 303 305 eqeq12d 
 |-  ( f = ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) -> ( ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) <-> ( ( Q ` ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) ) ` A ) ) ) )
307 301 306 elab 
 |-  ( ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) e. { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } <-> ( ( Q ` ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) ) ` A ) ) )
308 300 307 sylibr 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( ( ( algSc ` ( I mPoly U ) ) ` b ) ( .r ` ( I mPoly U ) ) ( w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( w = a , ( 1r ` U ) , ( 0g ` U ) ) ) ) e. { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } )
309 163 308 eqeltrrd 
 |-  ( ( ph /\ ( a e. { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } /\ b e. ( Base ` U ) ) ) -> ( s e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( s = a , b , ( 0g ` U ) ) ) e. { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } )
310 elin 
 |-  ( x e. ( ( H ` N ) i^i { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } ) <-> ( x e. ( H ` N ) /\ x e. { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } ) )
311 vex 
 |-  x e. _V
312 fveq2 
 |-  ( f = x -> ( Q ` f ) = ( Q ` x ) )
313 312 fveq1d 
 |-  ( f = x -> ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) )
314 312 fveq1d 
 |-  ( f = x -> ( ( Q ` f ) ` A ) = ( ( Q ` x ) ` A ) )
315 314 oveq2d 
 |-  ( f = x -> ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) )
316 313 315 eqeq12d 
 |-  ( f = x -> ( ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) <-> ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) )
317 311 316 elab 
 |-  ( x e. { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } <-> ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) )
318 317 anbi2i 
 |-  ( ( x e. ( H ` N ) /\ x e. { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } ) <-> ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) )
319 310 318 bitri 
 |-  ( x e. ( ( H ` N ) i^i { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } ) <-> ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) )
320 elin 
 |-  ( y e. ( ( H ` N ) i^i { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } ) <-> ( y e. ( H ` N ) /\ y e. { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } ) )
321 vex 
 |-  y e. _V
322 fveq2 
 |-  ( f = y -> ( Q ` f ) = ( Q ` y ) )
323 322 fveq1d 
 |-  ( f = y -> ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) )
324 322 fveq1d 
 |-  ( f = y -> ( ( Q ` f ) ` A ) = ( ( Q ` y ) ` A ) )
325 324 oveq2d 
 |-  ( f = y -> ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) )
326 323 325 eqeq12d 
 |-  ( f = y -> ( ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) <-> ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) )
327 321 326 elab 
 |-  ( y e. { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } <-> ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) )
328 327 anbi2i 
 |-  ( ( y e. ( H ` N ) /\ y e. { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } ) <-> ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) )
329 320 328 bitri 
 |-  ( y e. ( ( H ` N ) i^i { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } ) <-> ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) )
330 319 329 anbi12i 
 |-  ( ( x e. ( ( H ` N ) i^i { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } ) /\ y e. ( ( H ` N ) i^i { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } ) ) <-> ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) )
331 60 adantr 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> S e. Ring )
332 182 adantr 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( N .^ L ) e. K )
333 eqid 
 |-  ( S ^s ( Base ` ( S ^s I ) ) ) = ( S ^s ( Base ` ( S ^s I ) ) )
334 eqid 
 |-  ( Base ` ( S ^s ( Base ` ( S ^s I ) ) ) ) = ( Base ` ( S ^s ( Base ` ( S ^s I ) ) ) )
335 8 adantr 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> S e. CRing )
336 fvexd 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( Base ` ( S ^s I ) ) e. _V )
337 eqid 
 |-  ( S ^s ( K ^m I ) ) = ( S ^s ( K ^m I ) )
338 1 16 3 337 4 evlsrhm 
 |-  ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( ( I mPoly U ) RingHom ( S ^s ( K ^m I ) ) ) )
339 7 8 9 338 syl3anc 
 |-  ( ph -> Q e. ( ( I mPoly U ) RingHom ( S ^s ( K ^m I ) ) ) )
340 eqid 
 |-  ( Base ` ( S ^s ( K ^m I ) ) ) = ( Base ` ( S ^s ( K ^m I ) ) )
341 51 340 rhmf 
 |-  ( Q e. ( ( I mPoly U ) RingHom ( S ^s ( K ^m I ) ) ) -> Q : ( Base ` ( I mPoly U ) ) --> ( Base ` ( S ^s ( K ^m I ) ) ) )
342 339 341 syl 
 |-  ( ph -> Q : ( Base ` ( I mPoly U ) ) --> ( Base ` ( S ^s ( K ^m I ) ) ) )
343 342 adantr 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> Q : ( Base ` ( I mPoly U ) ) --> ( Base ` ( S ^s ( K ^m I ) ) ) )
344 7 adantr 
 |-  ( ( ph /\ x e. ( H ` N ) ) -> I e. V )
345 21 adantr 
 |-  ( ( ph /\ x e. ( H ` N ) ) -> U e. Ring )
346 11 adantr 
 |-  ( ( ph /\ x e. ( H ` N ) ) -> N e. NN0 )
347 simpr 
 |-  ( ( ph /\ x e. ( H ` N ) ) -> x e. ( H ` N ) )
348 2 16 51 344 345 346 347 mhpmpl 
 |-  ( ( ph /\ x e. ( H ` N ) ) -> x e. ( Base ` ( I mPoly U ) ) )
349 348 adantrr 
 |-  ( ( ph /\ ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) ) -> x e. ( Base ` ( I mPoly U ) ) )
350 349 adantrr 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> x e. ( Base ` ( I mPoly U ) ) )
351 343 350 ffvelrnd 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( Q ` x ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
352 eqid 
 |-  ( S ^s I ) = ( S ^s I )
353 352 4 pwsbas 
 |-  ( ( S e. CRing /\ I e. V ) -> ( K ^m I ) = ( Base ` ( S ^s I ) ) )
354 8 7 353 syl2anc 
 |-  ( ph -> ( K ^m I ) = ( Base ` ( S ^s I ) ) )
355 354 oveq2d 
 |-  ( ph -> ( S ^s ( K ^m I ) ) = ( S ^s ( Base ` ( S ^s I ) ) ) )
356 355 fveq2d 
 |-  ( ph -> ( Base ` ( S ^s ( K ^m I ) ) ) = ( Base ` ( S ^s ( Base ` ( S ^s I ) ) ) ) )
357 356 adantr 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( Base ` ( S ^s ( K ^m I ) ) ) = ( Base ` ( S ^s ( Base ` ( S ^s I ) ) ) ) )
358 351 357 eleqtrd 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( Q ` x ) e. ( Base ` ( S ^s ( Base ` ( S ^s I ) ) ) ) )
359 333 4 334 335 336 358 pwselbas 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( Q ` x ) : ( Base ` ( S ^s I ) ) --> K )
360 13 354 eleqtrd 
 |-  ( ph -> A e. ( Base ` ( S ^s I ) ) )
361 360 adantr 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> A e. ( Base ` ( S ^s I ) ) )
362 359 361 ffvelrnd 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( ( Q ` x ) ` A ) e. K )
363 7 adantr 
 |-  ( ( ph /\ y e. ( H ` N ) ) -> I e. V )
364 21 adantr 
 |-  ( ( ph /\ y e. ( H ` N ) ) -> U e. Ring )
365 11 adantr 
 |-  ( ( ph /\ y e. ( H ` N ) ) -> N e. NN0 )
366 simpr 
 |-  ( ( ph /\ y e. ( H ` N ) ) -> y e. ( H ` N ) )
367 2 16 51 363 364 365 366 mhpmpl 
 |-  ( ( ph /\ y e. ( H ` N ) ) -> y e. ( Base ` ( I mPoly U ) ) )
368 367 adantrr 
 |-  ( ( ph /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) -> y e. ( Base ` ( I mPoly U ) ) )
369 368 adantrl 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> y e. ( Base ` ( I mPoly U ) ) )
370 343 369 ffvelrnd 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( Q ` y ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
371 370 357 eleqtrd 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( Q ` y ) e. ( Base ` ( S ^s ( Base ` ( S ^s I ) ) ) ) )
372 333 4 334 335 336 371 pwselbas 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( Q ` y ) : ( Base ` ( S ^s I ) ) --> K )
373 372 361 ffvelrnd 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( ( Q ` y ) ` A ) e. K )
374 eqid 
 |-  ( +g ` S ) = ( +g ` S )
375 4 374 5 ringdi 
 |-  ( ( S e. Ring /\ ( ( N .^ L ) e. K /\ ( ( Q ` x ) ` A ) e. K /\ ( ( Q ` y ) ` A ) e. K ) ) -> ( ( N .^ L ) .x. ( ( ( Q ` x ) ` A ) ( +g ` S ) ( ( Q ` y ) ` A ) ) ) = ( ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ( +g ` S ) ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) )
376 331 332 362 373 375 syl13anc 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( ( N .^ L ) .x. ( ( ( Q ` x ) ` A ) ( +g ` S ) ( ( Q ` y ) ` A ) ) ) = ( ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ( +g ` S ) ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) )
377 7 adantr 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> I e. V )
378 9 adantr 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> R e. ( SubRing ` S ) )
379 13 adantr 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> A e. ( K ^m I ) )
380 eqidd 
 |-  ( ( ph /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) -> ( ( Q ` x ) ` A ) = ( ( Q ` x ) ` A ) )
381 348 380 anim12dan 
 |-  ( ( ph /\ ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) ) -> ( x e. ( Base ` ( I mPoly U ) ) /\ ( ( Q ` x ) ` A ) = ( ( Q ` x ) ` A ) ) )
382 381 adantrr 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( x e. ( Base ` ( I mPoly U ) ) /\ ( ( Q ` x ) ` A ) = ( ( Q ` x ) ` A ) ) )
383 eqidd 
 |-  ( ( ph /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) -> ( ( Q ` y ) ` A ) = ( ( Q ` y ) ` A ) )
384 367 383 anim12dan 
 |-  ( ( ph /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) -> ( y e. ( Base ` ( I mPoly U ) ) /\ ( ( Q ` y ) ` A ) = ( ( Q ` y ) ` A ) ) )
385 384 adantrl 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( y e. ( Base ` ( I mPoly U ) ) /\ ( ( Q ` y ) ` A ) = ( ( Q ` y ) ` A ) ) )
386 1 16 3 4 51 377 335 378 379 382 385 17 374 evlsaddval 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( ( x ( +g ` ( I mPoly U ) ) y ) e. ( Base ` ( I mPoly U ) ) /\ ( ( Q ` ( x ( +g ` ( I mPoly U ) ) y ) ) ` A ) = ( ( ( Q ` x ) ` A ) ( +g ` S ) ( ( Q ` y ) ` A ) ) ) )
387 386 simprd 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( ( Q ` ( x ( +g ` ( I mPoly U ) ) y ) ) ` A ) = ( ( ( Q ` x ) ` A ) ( +g ` S ) ( ( Q ` y ) ` A ) ) )
388 387 oveq2d 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( ( N .^ L ) .x. ( ( Q ` ( x ( +g ` ( I mPoly U ) ) y ) ) ` A ) ) = ( ( N .^ L ) .x. ( ( ( Q ` x ) ` A ) ( +g ` S ) ( ( Q ` y ) ` A ) ) ) )
389 58 a1i 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> K e. _V )
390 63 adantlr 
 |-  ( ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) /\ ( j e. K /\ k e. K ) ) -> ( j .x. k ) e. K )
391 68 adantr 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( I X. { L } ) : I --> K )
392 70 adantr 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> A : I --> K )
393 390 391 392 377 377 71 off 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( ( I X. { L } ) oF .x. A ) : I --> K )
394 389 377 393 elmapdd 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( ( I X. { L } ) oF .x. A ) e. ( K ^m I ) )
395 simpr 
 |-  ( ( ph /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) -> ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) )
396 348 395 anim12dan 
 |-  ( ( ph /\ ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) ) -> ( x e. ( Base ` ( I mPoly U ) ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) )
397 396 adantrr 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( x e. ( Base ` ( I mPoly U ) ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) )
398 simpr 
 |-  ( ( ph /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) -> ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) )
399 367 398 anim12dan 
 |-  ( ( ph /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) -> ( y e. ( Base ` ( I mPoly U ) ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) )
400 399 adantrl 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( y e. ( Base ` ( I mPoly U ) ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) )
401 1 16 3 4 51 377 335 378 394 397 400 17 374 evlsaddval 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( ( x ( +g ` ( I mPoly U ) ) y ) e. ( Base ` ( I mPoly U ) ) /\ ( ( Q ` ( x ( +g ` ( I mPoly U ) ) y ) ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ( +g ` S ) ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) )
402 401 simprd 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( ( Q ` ( x ( +g ` ( I mPoly U ) ) y ) ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ( +g ` S ) ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) )
403 376 388 402 3eqtr4rd 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( ( Q ` ( x ( +g ` ( I mPoly U ) ) y ) ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` ( x ( +g ` ( I mPoly U ) ) y ) ) ` A ) ) )
404 ovex 
 |-  ( x ( +g ` ( I mPoly U ) ) y ) e. _V
405 fveq2 
 |-  ( f = ( x ( +g ` ( I mPoly U ) ) y ) -> ( Q ` f ) = ( Q ` ( x ( +g ` ( I mPoly U ) ) y ) ) )
406 405 fveq1d 
 |-  ( f = ( x ( +g ` ( I mPoly U ) ) y ) -> ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( Q ` ( x ( +g ` ( I mPoly U ) ) y ) ) ` ( ( I X. { L } ) oF .x. A ) ) )
407 405 fveq1d 
 |-  ( f = ( x ( +g ` ( I mPoly U ) ) y ) -> ( ( Q ` f ) ` A ) = ( ( Q ` ( x ( +g ` ( I mPoly U ) ) y ) ) ` A ) )
408 407 oveq2d 
 |-  ( f = ( x ( +g ` ( I mPoly U ) ) y ) -> ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) = ( ( N .^ L ) .x. ( ( Q ` ( x ( +g ` ( I mPoly U ) ) y ) ) ` A ) ) )
409 406 408 eqeq12d 
 |-  ( f = ( x ( +g ` ( I mPoly U ) ) y ) -> ( ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) <-> ( ( Q ` ( x ( +g ` ( I mPoly U ) ) y ) ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` ( x ( +g ` ( I mPoly U ) ) y ) ) ` A ) ) ) )
410 404 409 elab 
 |-  ( ( x ( +g ` ( I mPoly U ) ) y ) e. { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } <-> ( ( Q ` ( x ( +g ` ( I mPoly U ) ) y ) ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` ( x ( +g ` ( I mPoly U ) ) y ) ) ` A ) ) )
411 403 410 sylibr 
 |-  ( ( ph /\ ( ( x e. ( H ` N ) /\ ( ( Q ` x ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` x ) ` A ) ) ) /\ ( y e. ( H ` N ) /\ ( ( Q ` y ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` y ) ` A ) ) ) ) ) -> ( x ( +g ` ( I mPoly U ) ) y ) e. { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } )
412 330 411 sylan2b 
 |-  ( ( ph /\ ( x e. ( ( H ` N ) i^i { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } ) /\ y e. ( ( H ` N ) i^i { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } ) ) ) -> ( x ( +g ` ( I mPoly U ) ) y ) e. { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } )
413 2 14 15 16 17 18 19 7 22 11 12 85 309 412 mhpind 
 |-  ( ph -> X e. { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } )
414 fveq2 
 |-  ( f = X -> ( Q ` f ) = ( Q ` X ) )
415 414 fveq1d 
 |-  ( f = X -> ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( Q ` X ) ` ( ( I X. { L } ) oF .x. A ) ) )
416 414 fveq1d 
 |-  ( f = X -> ( ( Q ` f ) ` A ) = ( ( Q ` X ) ` A ) )
417 416 oveq2d 
 |-  ( f = X -> ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) = ( ( N .^ L ) .x. ( ( Q ` X ) ` A ) ) )
418 415 417 eqeq12d 
 |-  ( f = X -> ( ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) <-> ( ( Q ` X ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` X ) ` A ) ) ) )
419 418 elabg 
 |-  ( X e. ( H ` N ) -> ( X e. { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } <-> ( ( Q ` X ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` X ) ` A ) ) ) )
420 12 419 syl 
 |-  ( ph -> ( X e. { f | ( ( Q ` f ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` f ) ` A ) ) } <-> ( ( Q ` X ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` X ) ` A ) ) ) )
421 413 420 mpbid 
 |-  ( ph -> ( ( Q ` X ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` X ) ` A ) ) )