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 ffvelcdm 
 |-  ( ( 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 76 81 83 mulgnn0cld 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ a e. ( NN0 ^m 1o ) ) -> ( ( a ` (/) ) .^ X ) e. B )
85 72 84 eqeltrd 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ a e. ( NN0 ^m 1o ) ) -> ( ( a ` (/) ) ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) X ) e. B )
86 fveq2 
 |-  ( c = (/) -> ( a ` c ) = ( a ` (/) ) )
87 fveq2 
 |-  ( c = (/) -> ( ( 1o mVar R ) ` c ) = ( ( 1o mVar R ) ` (/) ) )
88 2 vr1val 
 |-  X = ( ( 1o mVar R ) ` (/) )
89 87 88 eqtr4di 
 |-  ( c = (/) -> ( ( 1o mVar R ) ` c ) = X )
90 86 89 oveq12d 
 |-  ( c = (/) -> ( ( a ` c ) ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` c ) ) = ( ( a ` (/) ) ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) X ) )
91 56 90 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 ) )
92 54 55 85 91 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 ) )
93 49 92 eqtrid 
 |-  ( ( ( 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 ) )
94 47 93 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 ) )
95 21 94 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 ) ) )
96 95 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 ) ) ) )
97 96 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 ) ) ) ) )
98 nn0ex 
 |-  NN0 e. _V
99 98 mptex 
 |-  ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) e. _V
100 99 a1i 
 |-  ( ( R e. Ring /\ K e. B ) -> ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) e. _V )
101 1 fvexi 
 |-  P e. _V
102 101 a1i 
 |-  ( ( R e. Ring /\ K e. B ) -> P e. _V )
103 ovexd 
 |-  ( ( R e. Ring /\ K e. B ) -> ( 1o mPoly R ) e. _V )
104 3 15 eqtr3i 
 |-  ( Base ` P ) = ( Base ` ( 1o mPoly R ) )
105 104 a1i 
 |-  ( ( R e. Ring /\ K e. B ) -> ( Base ` P ) = ( Base ` ( 1o mPoly R ) ) )
106 eqid 
 |-  ( +g ` P ) = ( +g ` P )
107 1 8 106 ply1plusg 
 |-  ( +g ` P ) = ( +g ` ( 1o mPoly R ) )
108 107 a1i 
 |-  ( ( R e. Ring /\ K e. B ) -> ( +g ` P ) = ( +g ` ( 1o mPoly R ) ) )
109 100 102 103 105 108 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 ) ) ) ) )
110 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
111 8 1 110 ply1mpl0 
 |-  ( 0g ` P ) = ( 0g ` ( 1o mPoly R ) )
112 8 mpllmod 
 |-  ( ( 1o e. _om /\ R e. Ring ) -> ( 1o mPoly R ) e. LMod )
113 12 17 112 sylancr 
 |-  ( ( R e. Ring /\ K e. B ) -> ( 1o mPoly R ) e. LMod )
114 lmodcmn 
 |-  ( ( 1o mPoly R ) e. LMod -> ( 1o mPoly R ) e. CMnd )
115 113 114 syl 
 |-  ( ( R e. Ring /\ K e. B ) -> ( 1o mPoly R ) e. CMnd )
116 98 a1i 
 |-  ( ( R e. Ring /\ K e. B ) -> NN0 e. _V )
117 1 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
118 117 ad2antrr 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> P e. LMod )
119 eqid 
 |-  ( Base ` R ) = ( Base ` R )
120 7 3 1 119 coe1f 
 |-  ( K e. B -> A : NN0 --> ( Base ` R ) )
121 120 adantl 
 |-  ( ( R e. Ring /\ K e. B ) -> A : NN0 --> ( Base ` R ) )
122 121 ffvelcdmda 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> ( A ` k ) e. ( Base ` R ) )
123 1 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
124 123 eqcomd 
 |-  ( R e. Ring -> ( Scalar ` P ) = R )
125 124 ad2antrr 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> ( Scalar ` P ) = R )
126 125 fveq2d 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> ( Base ` ( Scalar ` P ) ) = ( Base ` R ) )
127 122 126 eleqtrrd 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> ( A ` k ) e. ( Base ` ( Scalar ` P ) ) )
128 75 ad2antrr 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> M e. Mnd )
129 simpr 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> k e. NN0 )
130 82 ad2antrr 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> X e. B )
131 58 6 128 129 130 mulgnn0cld 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> ( k .^ X ) e. B )
132 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
133 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
134 3 132 4 133 lmodvscl 
 |-  ( ( P e. LMod /\ ( A ` k ) e. ( Base ` ( Scalar ` P ) ) /\ ( k .^ X ) e. B ) -> ( ( A ` k ) .x. ( k .^ X ) ) e. B )
135 118 127 131 134 syl3anc 
 |-  ( ( ( R e. Ring /\ K e. B ) /\ k e. NN0 ) -> ( ( A ` k ) .x. ( k .^ X ) ) e. B )
136 135 fmpttd 
 |-  ( ( R e. Ring /\ K e. B ) -> ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) : NN0 --> B )
137 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 ) )
138 eqid 
 |-  ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) = ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) )
139 43 98 29 138 mapsnf1o2 
 |-  ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) : ( NN0 ^m 1o ) -1-1-onto-> NN0
140 139 a1i 
 |-  ( ( R e. Ring /\ K e. B ) -> ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) : ( NN0 ^m 1o ) -1-1-onto-> NN0 )
141 15 111 115 116 136 137 140 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 ` (/) ) ) ) ) )
142 eqidd 
 |-  ( ( R e. Ring /\ K e. B ) -> ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) = ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) )
143 eqidd 
 |-  ( ( R e. Ring /\ K e. B ) -> ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) = ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) )
144 fveq2 
 |-  ( k = ( a ` (/) ) -> ( A ` k ) = ( A ` ( a ` (/) ) ) )
145 oveq1 
 |-  ( k = ( a ` (/) ) -> ( k .^ X ) = ( ( a ` (/) ) .^ X ) )
146 144 145 oveq12d 
 |-  ( k = ( a ` (/) ) -> ( ( A ` k ) .x. ( k .^ X ) ) = ( ( A ` ( a ` (/) ) ) .x. ( ( a ` (/) ) .^ X ) ) )
147 81 142 143 146 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 ) ) ) )
148 147 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 ) ) ) ) )
149 109 141 148 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 ) ) ) ) )
150 19 97 149 3eqtrd 
 |-  ( ( R e. Ring /\ K e. B ) -> K = ( P gsum ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) ) )