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 ) ) ) ) )