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