This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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