Metamath Proof Explorer

Theorem ply1coe

Description: Decompose a univariate polynomial as a sum of powers. (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by AV, 7-Oct-2019)

Ref Expression
Hypotheses ply1coe.p 
|- P = ( Poly1 ` R )
ply1coe.x 
|- X = ( var1 ` R )
ply1coe.b 
|- B = ( Base ` P )
ply1coe.n 
|- .x. = ( .s ` P )
ply1coe.m 
|- M = ( mulGrp ` P )
ply1coe.e 
|- .^ = ( .g ` M )
ply1coe.a 
|- A = ( coe1 ` K )
Assertion ply1coe 
|- ( ( R e. Ring /\ K e. B ) -> K = ( P gsum ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ply1coe.p 
 |-  P = ( Poly1 ` R )
2 ply1coe.x 
 |-  X = ( var1 ` R )
3 ply1coe.b 
 |-  B = ( Base ` P )
4 ply1coe.n 
 |-  .x. = ( .s ` P )
5 ply1coe.m 
 |-  M = ( mulGrp ` P )
6 ply1coe.e 
 |-  .^ = ( .g ` M )
7 ply1coe.a 
 |-  A = ( coe1 ` K )
8 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
9 psr1baslem 
 |-  ( NN0 ^m 1o ) = { d e. ( NN0 ^m 1o ) | ( `' d " NN ) e. Fin }
10 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
11 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
12 1onn 
 |-  1o e. _om
13 12 a1i 
 |-  ( ( R e. Ring /\ K e. B ) -> 1o e. _om )
14 eqid 
 |-  ( PwSer1 ` R ) = ( PwSer1 ` R )
15 1 14 3 ply1bas 
 |-  B = ( Base ` ( 1o mPoly R ) )
16 1 8 4 ply1vsca 
 |-  .x. = ( .s ` ( 1o mPoly R ) )
17 simpl 
 |-  ( ( R e. Ring /\ K e. B ) -> R e. Ring )
18 simpr 
 |-  ( ( R e. Ring /\ K e. B ) -> K e. B )
19 8 9 10 11 13 15 16 17 18 mplcoe1 
 |-  ( ( R e. Ring /\ K e. B ) -> K = ( ( 1o mPoly R ) gsum ( a e. ( NN0 ^m 1o ) |-> ( ( K ` a ) .x. ( b e. ( NN0 ^m 1o ) |-> if ( b = a , ( 1r ` R ) , ( 0g ` R ) ) ) ) ) ) )
20 7 fvcoe1 
 |-  ( ( K e. B /\ a e. ( NN0 ^m 1o ) ) -> ( K ` a ) = ( A ` ( a ` (/) ) ) )
21 20 adantll 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ a e. ( NN0 ^m 1o ) ) -> ( K ` a ) = ( A ` ( a ` (/) ) ) )
22 12 a1i 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ a e. ( NN0 ^m 1o ) ) -> 1o e. _om )
23 eqid 
 |-  ( mulGrp ` ( 1o mPoly R ) ) = ( mulGrp ` ( 1o mPoly R ) )
24 eqid 
 |-  ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) = ( .g ` ( mulGrp ` ( 1o mPoly R ) ) )
25 eqid 
 |-  ( 1o mVar R ) = ( 1o mVar R )
26 simpll 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ a e. ( NN0 ^m 1o ) ) -> R e. Ring )
27 simpr 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ a e. ( NN0 ^m 1o ) ) -> a e. ( NN0 ^m 1o ) )
28 eqidd 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ a e. ( NN0 ^m 1o ) ) -> ( ( ( 1o mVar R ) ` (/) ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` (/) ) ) = ( ( ( 1o mVar R ) ` (/) ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` (/) ) ) )
29 0ex 
 |-  (/) e. _V
30 fveq2 
 |-  ( b = (/) -> ( ( 1o mVar R ) ` b ) = ( ( 1o mVar R ) ` (/) ) )
31 30 oveq1d 
 |-  ( b = (/) -> ( ( ( 1o mVar R ) ` b ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` (/) ) ) = ( ( ( 1o mVar R ) ` (/) ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` (/) ) ) )
32 30 oveq2d 
 |-  ( b = (/) -> ( ( ( 1o mVar R ) ` (/) ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` b ) ) = ( ( ( 1o mVar R ) ` (/) ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` (/) ) ) )
33 31 32 eqeq12d 
 |-  ( b = (/) -> ( ( ( ( 1o mVar R ) ` b ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` (/) ) ) = ( ( ( 1o mVar R ) ` (/) ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` b ) ) <-> ( ( ( 1o mVar R ) ` (/) ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` (/) ) ) = ( ( ( 1o mVar R ) ` (/) ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` (/) ) ) ) )
34 29 33 ralsn 
 |-  ( A. b e. { (/) } ( ( ( 1o mVar R ) ` b ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` (/) ) ) = ( ( ( 1o mVar R ) ` (/) ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` b ) ) <-> ( ( ( 1o mVar R ) ` (/) ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` (/) ) ) = ( ( ( 1o mVar R ) ` (/) ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` (/) ) ) )
35 28 34 sylibr 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ a e. ( NN0 ^m 1o ) ) -> A. b e. { (/) } ( ( ( 1o mVar R ) ` b ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` (/) ) ) = ( ( ( 1o mVar R ) ` (/) ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` b ) ) )
36 fveq2 
 |-  ( x = (/) -> ( ( 1o mVar R ) ` x ) = ( ( 1o mVar R ) ` (/) ) )
37 36 oveq2d 
 |-  ( x = (/) -> ( ( ( 1o mVar R ) ` b ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` x ) ) = ( ( ( 1o mVar R ) ` b ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` (/) ) ) )
38 36 oveq1d 
 |-  ( x = (/) -> ( ( ( 1o mVar R ) ` x ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` b ) ) = ( ( ( 1o mVar R ) ` (/) ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` b ) ) )
39 37 38 eqeq12d 
 |-  ( x = (/) -> ( ( ( ( 1o mVar R ) ` b ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` x ) ) = ( ( ( 1o mVar R ) ` x ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` b ) ) <-> ( ( ( 1o mVar R ) ` b ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` (/) ) ) = ( ( ( 1o mVar R ) ` (/) ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` b ) ) ) )
40 39 ralbidv 
 |-  ( x = (/) -> ( A. b e. { (/) } ( ( ( 1o mVar R ) ` b ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` x ) ) = ( ( ( 1o mVar R ) ` x ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` b ) ) <-> A. b e. { (/) } ( ( ( 1o mVar R ) ` b ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` (/) ) ) = ( ( ( 1o mVar R ) ` (/) ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` b ) ) ) )
41 29 40 ralsn 
 |-  ( A. x e. { (/) } A. b e. { (/) } ( ( ( 1o mVar R ) ` b ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` x ) ) = ( ( ( 1o mVar R ) ` x ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` b ) ) <-> A. b e. { (/) } ( ( ( 1o mVar R ) ` b ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` (/) ) ) = ( ( ( 1o mVar R ) ` (/) ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` b ) ) )
42 35 41 sylibr 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ a e. ( NN0 ^m 1o ) ) -> A. x e. { (/) } A. b e. { (/) } ( ( ( 1o mVar R ) ` b ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` x ) ) = ( ( ( 1o mVar R ) ` x ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` b ) ) )
43 df1o2 
 |-  1o = { (/) }
44 43 raleqi 
 |-  ( A. b e. 1o ( ( ( 1o mVar R ) ` b ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` x ) ) = ( ( ( 1o mVar R ) ` x ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` b ) ) <-> A. b e. { (/) } ( ( ( 1o mVar R ) ` b ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` x ) ) = ( ( ( 1o mVar R ) ` x ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` b ) ) )
45 43 44 raleqbii 
 |-  ( A. x e. 1o A. b e. 1o ( ( ( 1o mVar R ) ` b ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` x ) ) = ( ( ( 1o mVar R ) ` x ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` b ) ) <-> A. x e. { (/) } A. b e. { (/) } ( ( ( 1o mVar R ) ` b ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` x ) ) = ( ( ( 1o mVar R ) ` x ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` b ) ) )
46 42 45 sylibr 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ a e. ( NN0 ^m 1o ) ) -> A. x e. 1o A. b e. 1o ( ( ( 1o mVar R ) ` b ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` x ) ) = ( ( ( 1o mVar R ) ` x ) ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` b ) ) )
47 8 9 10 11 22 23 24 25 26 27 46 mplcoe5 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ a e. ( NN0 ^m 1o ) ) -> ( b e. ( NN0 ^m 1o ) |-> if ( b = a , ( 1r ` R ) , ( 0g ` R ) ) ) = ( ( mulGrp ` ( 1o mPoly R ) ) gsum ( c e. 1o |-> ( ( a ` c ) ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` c ) ) ) ) )
48 43 mpteq1i 
 |-  ( c e. 1o |-> ( ( a ` c ) ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` c ) ) ) = ( c e. { (/) } |-> ( ( a ` c ) ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` c ) ) )
49 48 oveq2i 
 |-  ( ( mulGrp ` ( 1o mPoly R ) ) gsum ( c e. 1o |-> ( ( a ` c ) ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` c ) ) ) ) = ( ( mulGrp ` ( 1o mPoly R ) ) gsum ( c e. { (/) } |-> ( ( a ` c ) ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` c ) ) ) )
50 8 mplring 
 |-  ( ( 1o e. _om /\ R e. Ring ) -> ( 1o mPoly R ) e. Ring )
51 12 50 mpan 
 |-  ( R e. Ring -> ( 1o mPoly R ) e. Ring )
52 23 ringmgp 
 |-  ( ( 1o mPoly R ) e. Ring -> ( mulGrp ` ( 1o mPoly R ) ) e. Mnd )
53 51 52 syl 
 |-  ( R e. Ring -> ( mulGrp ` ( 1o mPoly R ) ) e. Mnd )
54 53 ad2antrr 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ a e. ( NN0 ^m 1o ) ) -> ( mulGrp ` ( 1o mPoly R ) ) e. Mnd )
55 29 a1i 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ a e. ( NN0 ^m 1o ) ) -> (/) e. _V )
56 23 15 mgpbas 
 |-  B = ( Base ` ( mulGrp ` ( 1o mPoly R ) ) )
57 56 a1i 
 |-  ( ( R e. Ring /\ K e. B ) -> B = ( Base ` ( mulGrp ` ( 1o mPoly R ) ) ) )
58 5 3 mgpbas 
 |-  B = ( Base ` M )
59 58 a1i 
 |-  ( ( R e. Ring /\ K e. B ) -> B = ( Base ` M ) )
60 ssv 
 |-  B C_ _V
61 60 a1i 
 |-  ( ( R e. Ring /\ K e. B ) -> B C_ _V )
62 ovexd 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ ( a e. _V /\ b e. _V ) ) -> ( a ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) b ) e. _V )
63 eqid 
 |-  ( .r ` P ) = ( .r ` P )
64 1 8 63 ply1mulr 
 |-  ( .r ` P ) = ( .r ` ( 1o mPoly R ) )
65 23 64 mgpplusg 
 |-  ( .r ` P ) = ( +g ` ( mulGrp ` ( 1o mPoly R ) ) )
66 5 63 mgpplusg 
 |-  ( .r ` P ) = ( +g ` M )
67 65 66 eqtr3i 
 |-  ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) = ( +g ` M )
68 67 oveqi 
 |-  ( a ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) b ) = ( a ( +g ` M ) b )
69 68 a1i 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ ( a e. _V /\ b e. _V ) ) -> ( a ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) b ) = ( a ( +g ` M ) b ) )
70 24 6 57 59 61 62 69 mulgpropd 
 |-  ( ( R e. Ring /\ K e. B ) -> ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) = .^ )
71 70 oveqd 
 |-  ( ( R e. Ring /\ K e. B ) -> ( ( a ` (/) ) ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) X ) = ( ( a ` (/) ) .^ X ) )
72 71 adantr 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ a e. ( NN0 ^m 1o ) ) -> ( ( a ` (/) ) ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) X ) = ( ( a ` (/) ) .^ X ) )
73 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
74 5 ringmgp 
 |-  ( P e. Ring -> M e. Mnd )
75 73 74 syl 
 |-  ( R e. Ring -> M e. Mnd )
76 75 ad2antrr 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ a e. ( NN0 ^m 1o ) ) -> M e. Mnd )
77 elmapi 
 |-  ( a e. ( NN0 ^m 1o ) -> a : 1o --> NN0 )
78 0lt1o 
 |-  (/) e. 1o
79 ffvelrn 
 |-  ( ( a : 1o --> NN0 /\ (/) e. 1o ) -> ( a ` (/) ) e. NN0 )
80 77 78 79 sylancl 
 |-  ( a e. ( NN0 ^m 1o ) -> ( a ` (/) ) e. NN0 )
81 80 adantl 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ a e. ( NN0 ^m 1o ) ) -> ( a ` (/) ) e. NN0 )
82 2 1 3 vr1cl 
 |-  ( R e. Ring -> X e. B )
83 82 ad2antrr 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ a e. ( NN0 ^m 1o ) ) -> X e. B )
84 58 6 mulgnn0cl 
 |-  ( ( M e. Mnd /\ ( a ` (/) ) e. NN0 /\ X e. B ) -> ( ( a ` (/) ) .^ X ) e. B )
85 76 81 83 84 syl3anc 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ a e. ( NN0 ^m 1o ) ) -> ( ( a ` (/) ) .^ X ) e. B )
86 72 85 eqeltrd 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ a e. ( NN0 ^m 1o ) ) -> ( ( a ` (/) ) ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) X ) e. B )
87 fveq2 
 |-  ( c = (/) -> ( a ` c ) = ( a ` (/) ) )
88 fveq2 
 |-  ( c = (/) -> ( ( 1o mVar R ) ` c ) = ( ( 1o mVar R ) ` (/) ) )
89 2 vr1val 
 |-  X = ( ( 1o mVar R ) ` (/) )
90 88 89 eqtr4di 
 |-  ( c = (/) -> ( ( 1o mVar R ) ` c ) = X )
91 87 90 oveq12d 
 |-  ( c = (/) -> ( ( a ` c ) ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` c ) ) = ( ( a ` (/) ) ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) X ) )
92 56 91 gsumsn 
 |-  ( ( ( mulGrp ` ( 1o mPoly R ) ) e. Mnd /\ (/) e. _V /\ ( ( a ` (/) ) ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) X ) e. B ) -> ( ( mulGrp ` ( 1o mPoly R ) ) gsum ( c e. { (/) } |-> ( ( a ` c ) ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` c ) ) ) ) = ( ( a ` (/) ) ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) X ) )
93 54 55 86 92 syl3anc 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ a e. ( NN0 ^m 1o ) ) -> ( ( mulGrp ` ( 1o mPoly R ) ) gsum ( c e. { (/) } |-> ( ( a ` c ) ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` c ) ) ) ) = ( ( a ` (/) ) ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) X ) )
94 49 93 syl5eq 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ a e. ( NN0 ^m 1o ) ) -> ( ( mulGrp ` ( 1o mPoly R ) ) gsum ( c e. 1o |-> ( ( a ` c ) ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` c ) ) ) ) = ( ( a ` (/) ) ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) X ) )
95 47 94 72 3eqtrd 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ a e. ( NN0 ^m 1o ) ) -> ( b e. ( NN0 ^m 1o ) |-> if ( b = a , ( 1r ` R ) , ( 0g ` R ) ) ) = ( ( a ` (/) ) .^ X ) )
96 21 95 oveq12d 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ a e. ( NN0 ^m 1o ) ) -> ( ( K ` a ) .x. ( b e. ( NN0 ^m 1o ) |-> if ( b = a , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( ( A ` ( a ` (/) ) ) .x. ( ( a ` (/) ) .^ X ) ) )
97 96 mpteq2dva 
 |-  ( ( R e. Ring /\ K e. B ) -> ( a e. ( NN0 ^m 1o ) |-> ( ( K ` a ) .x. ( b e. ( NN0 ^m 1o ) |-> if ( b = a , ( 1r ` R ) , ( 0g ` R ) ) ) ) ) = ( a e. ( NN0 ^m 1o ) |-> ( ( A ` ( a ` (/) ) ) .x. ( ( a ` (/) ) .^ X ) ) ) )
98 97 oveq2d 
 |-  ( ( R e. Ring /\ K e. B ) -> ( ( 1o mPoly R ) gsum ( a e. ( NN0 ^m 1o ) |-> ( ( K ` a ) .x. ( b e. ( NN0 ^m 1o ) |-> if ( b = a , ( 1r ` R ) , ( 0g ` R ) ) ) ) ) ) = ( ( 1o mPoly R ) gsum ( a e. ( NN0 ^m 1o ) |-> ( ( A ` ( a ` (/) ) ) .x. ( ( a ` (/) ) .^ X ) ) ) ) )
99 nn0ex 
 |-  NN0 e. _V
100 99 mptex 
 |-  ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) e. _V
101 100 a1i 
 |-  ( ( R e. Ring /\ K e. B ) -> ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) e. _V )
102 1 fvexi 
 |-  P e. _V
103 102 a1i 
 |-  ( ( R e. Ring /\ K e. B ) -> P e. _V )
104 ovexd 
 |-  ( ( R e. Ring /\ K e. B ) -> ( 1o mPoly R ) e. _V )
105 3 15 eqtr3i 
 |-  ( Base ` P ) = ( Base ` ( 1o mPoly R ) )
106 105 a1i 
 |-  ( ( R e. Ring /\ K e. B ) -> ( Base ` P ) = ( Base ` ( 1o mPoly R ) ) )
107 eqid 
 |-  ( +g ` P ) = ( +g ` P )
108 1 8 107 ply1plusg 
 |-  ( +g ` P ) = ( +g ` ( 1o mPoly R ) )
109 108 a1i 
 |-  ( ( R e. Ring /\ K e. B ) -> ( +g ` P ) = ( +g ` ( 1o mPoly R ) ) )
110 101 103 104 106 109 gsumpropd 
 |-  ( ( R e. Ring /\ K e. B ) -> ( P gsum ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) ) = ( ( 1o mPoly R ) gsum ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) ) )
111 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
112 8 1 111 ply1mpl0 
 |-  ( 0g ` P ) = ( 0g ` ( 1o mPoly R ) )
113 8 mpllmod 
 |-  ( ( 1o e. _om /\ R e. Ring ) -> ( 1o mPoly R ) e. LMod )
114 12 17 113 sylancr 
 |-  ( ( R e. Ring /\ K e. B ) -> ( 1o mPoly R ) e. LMod )
115 lmodcmn 
 |-  ( ( 1o mPoly R ) e. LMod -> ( 1o mPoly R ) e. CMnd )
116 114 115 syl 
 |-  ( ( R e. Ring /\ K e. B ) -> ( 1o mPoly R ) e. CMnd )
117 99 a1i 
 |-  ( ( R e. Ring /\ K e. B ) -> NN0 e. _V )
118 1 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
119 118 ad2antrr 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> P e. LMod )
120 eqid 
 |-  ( Base ` R ) = ( Base ` R )
121 7 3 1 120 coe1f 
 |-  ( K e. B -> A : NN0 --> ( Base ` R ) )
122 121 adantl 
 |-  ( ( R e. Ring /\ K e. B ) -> A : NN0 --> ( Base ` R ) )
123 122 ffvelrnda 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> ( A ` k ) e. ( Base ` R ) )
124 1 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
125 124 eqcomd 
 |-  ( R e. Ring -> ( Scalar ` P ) = R )
126 125 ad2antrr 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> ( Scalar ` P ) = R )
127 126 fveq2d 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> ( Base ` ( Scalar ` P ) ) = ( Base ` R ) )
128 123 127 eleqtrrd 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> ( A ` k ) e. ( Base ` ( Scalar ` P ) ) )
129 75 ad2antrr 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> M e. Mnd )
130 simpr 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> k e. NN0 )
131 82 ad2antrr 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> X e. B )
132 58 6 mulgnn0cl 
 |-  ( ( M e. Mnd /\ k e. NN0 /\ X e. B ) -> ( k .^ X ) e. B )
133 129 130 131 132 syl3anc 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> ( k .^ X ) e. B )
134 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
135 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
136 3 134 4 135 lmodvscl 
 |-  ( ( P e. LMod /\ ( A ` k ) e. ( Base ` ( Scalar ` P ) ) /\ ( k .^ X ) e. B ) -> ( ( A ` k ) .x. ( k .^ X ) ) e. B )
137 119 128 133 136 syl3anc 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> ( ( A ` k ) .x. ( k .^ X ) ) e. B )
138 137 fmpttd 
 |-  ( ( R e. Ring /\ K e. B ) -> ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) : NN0 --> B )
139 1 2 3 4 5 6 7 ply1coefsupp 
 |-  ( ( R e. Ring /\ K e. B ) -> ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) finSupp ( 0g ` P ) )
140 eqid 
 |-  ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) = ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) )
141 43 99 29 140 mapsnf1o2 
 |-  ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) : ( NN0 ^m 1o ) -1-1-onto-> NN0
142 141 a1i 
 |-  ( ( R e. Ring /\ K e. B ) -> ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) : ( NN0 ^m 1o ) -1-1-onto-> NN0 )
143 15 112 116 117 138 139 142 gsumf1o 
 |-  ( ( R e. Ring /\ K e. B ) -> ( ( 1o mPoly R ) gsum ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) ) = ( ( 1o mPoly R ) gsum ( ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) o. ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ) ) )
144 eqidd 
 |-  ( ( R e. Ring /\ K e. B ) -> ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) = ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) )
145 eqidd 
 |-  ( ( R e. Ring /\ K e. B ) -> ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) = ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) )
146 fveq2 
 |-  ( k = ( a ` (/) ) -> ( A ` k ) = ( A ` ( a ` (/) ) ) )
147 oveq1 
 |-  ( k = ( a ` (/) ) -> ( k .^ X ) = ( ( a ` (/) ) .^ X ) )
148 146 147 oveq12d 
 |-  ( k = ( a ` (/) ) -> ( ( A ` k ) .x. ( k .^ X ) ) = ( ( A ` ( a ` (/) ) ) .x. ( ( a ` (/) ) .^ X ) ) )
149 81 144 145 148 fmptco 
 |-  ( ( R e. Ring /\ K e. B ) -> ( ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) o. ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ) = ( a e. ( NN0 ^m 1o ) |-> ( ( A ` ( a ` (/) ) ) .x. ( ( a ` (/) ) .^ X ) ) ) )
150 149 oveq2d 
 |-  ( ( R e. Ring /\ K e. B ) -> ( ( 1o mPoly R ) gsum ( ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) o. ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ) ) = ( ( 1o mPoly R ) gsum ( a e. ( NN0 ^m 1o ) |-> ( ( A ` ( a ` (/) ) ) .x. ( ( a ` (/) ) .^ X ) ) ) ) )
151 110 143 150 3eqtrrd 
 |-  ( ( R e. Ring /\ K e. B ) -> ( ( 1o mPoly R ) gsum ( a e. ( NN0 ^m 1o ) |-> ( ( A ` ( a ` (/) ) ) .x. ( ( a ` (/) ) .^ X ) ) ) ) = ( P gsum ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) ) )
152 19 98 151 3eqtrd 
 |-  ( ( R e. Ring /\ K e. B ) -> K = ( P gsum ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) ) )