Metamath Proof Explorer


Theorem coe1tm

Description: Coefficient vector of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015)

Ref Expression
Hypotheses coe1tm.z
|- .0. = ( 0g ` R )
coe1tm.k
|- K = ( Base ` R )
coe1tm.p
|- P = ( Poly1 ` R )
coe1tm.x
|- X = ( var1 ` R )
coe1tm.m
|- .x. = ( .s ` P )
coe1tm.n
|- N = ( mulGrp ` P )
coe1tm.e
|- .^ = ( .g ` N )
Assertion coe1tm
|- ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( coe1 ` ( C .x. ( D .^ X ) ) ) = ( x e. NN0 |-> if ( x = D , C , .0. ) ) )

Proof

Step Hyp Ref Expression
1 coe1tm.z
 |-  .0. = ( 0g ` R )
2 coe1tm.k
 |-  K = ( Base ` R )
3 coe1tm.p
 |-  P = ( Poly1 ` R )
4 coe1tm.x
 |-  X = ( var1 ` R )
5 coe1tm.m
 |-  .x. = ( .s ` P )
6 coe1tm.n
 |-  N = ( mulGrp ` P )
7 coe1tm.e
 |-  .^ = ( .g ` N )
8 eqid
 |-  ( Base ` P ) = ( Base ` P )
9 2 3 4 5 6 7 8 ply1tmcl
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( C .x. ( D .^ X ) ) e. ( Base ` P ) )
10 eqid
 |-  ( coe1 ` ( C .x. ( D .^ X ) ) ) = ( coe1 ` ( C .x. ( D .^ X ) ) )
11 eqid
 |-  ( x e. NN0 |-> ( 1o X. { x } ) ) = ( x e. NN0 |-> ( 1o X. { x } ) )
12 10 8 3 11 coe1fval2
 |-  ( ( C .x. ( D .^ X ) ) e. ( Base ` P ) -> ( coe1 ` ( C .x. ( D .^ X ) ) ) = ( ( C .x. ( D .^ X ) ) o. ( x e. NN0 |-> ( 1o X. { x } ) ) ) )
13 9 12 syl
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( coe1 ` ( C .x. ( D .^ X ) ) ) = ( ( C .x. ( D .^ X ) ) o. ( x e. NN0 |-> ( 1o X. { x } ) ) ) )
14 fconst6g
 |-  ( x e. NN0 -> ( 1o X. { x } ) : 1o --> NN0 )
15 nn0ex
 |-  NN0 e. _V
16 1oex
 |-  1o e. _V
17 15 16 elmap
 |-  ( ( 1o X. { x } ) e. ( NN0 ^m 1o ) <-> ( 1o X. { x } ) : 1o --> NN0 )
18 14 17 sylibr
 |-  ( x e. NN0 -> ( 1o X. { x } ) e. ( NN0 ^m 1o ) )
19 18 adantl
 |-  ( ( ( R e. Ring /\ C e. K /\ D e. NN0 ) /\ x e. NN0 ) -> ( 1o X. { x } ) e. ( NN0 ^m 1o ) )
20 eqidd
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( x e. NN0 |-> ( 1o X. { x } ) ) = ( x e. NN0 |-> ( 1o X. { x } ) ) )
21 eqid
 |-  ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) = ( .g ` ( mulGrp ` ( 1o mPoly R ) ) )
22 6 8 mgpbas
 |-  ( Base ` P ) = ( Base ` N )
23 22 a1i
 |-  ( R e. Ring -> ( Base ` P ) = ( Base ` N ) )
24 eqid
 |-  ( mulGrp ` ( 1o mPoly R ) ) = ( mulGrp ` ( 1o mPoly R ) )
25 3 8 ply1bas
 |-  ( Base ` P ) = ( Base ` ( 1o mPoly R ) )
26 24 25 mgpbas
 |-  ( Base ` P ) = ( Base ` ( mulGrp ` ( 1o mPoly R ) ) )
27 26 a1i
 |-  ( R e. Ring -> ( Base ` P ) = ( Base ` ( mulGrp ` ( 1o mPoly R ) ) ) )
28 ssv
 |-  ( Base ` P ) C_ _V
29 28 a1i
 |-  ( R e. Ring -> ( Base ` P ) C_ _V )
30 ovexd
 |-  ( ( R e. Ring /\ ( x e. _V /\ y e. _V ) ) -> ( x ( +g ` N ) y ) e. _V )
31 eqid
 |-  ( .r ` P ) = ( .r ` P )
32 6 31 mgpplusg
 |-  ( .r ` P ) = ( +g ` N )
33 eqid
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
34 3 33 31 ply1mulr
 |-  ( .r ` P ) = ( .r ` ( 1o mPoly R ) )
35 24 34 mgpplusg
 |-  ( .r ` P ) = ( +g ` ( mulGrp ` ( 1o mPoly R ) ) )
36 32 35 eqtr3i
 |-  ( +g ` N ) = ( +g ` ( mulGrp ` ( 1o mPoly R ) ) )
37 36 a1i
 |-  ( R e. Ring -> ( +g ` N ) = ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) )
38 37 oveqdr
 |-  ( ( R e. Ring /\ ( x e. _V /\ y e. _V ) ) -> ( x ( +g ` N ) y ) = ( x ( +g ` ( mulGrp ` ( 1o mPoly R ) ) ) y ) )
39 7 21 23 27 29 30 38 mulgpropd
 |-  ( R e. Ring -> .^ = ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) )
40 39 3ad2ant1
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> .^ = ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) )
41 eqidd
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> D = D )
42 4 vr1val
 |-  X = ( ( 1o mVar R ) ` (/) )
43 42 a1i
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> X = ( ( 1o mVar R ) ` (/) ) )
44 40 41 43 oveq123d
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( D .^ X ) = ( D ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` (/) ) ) )
45 44 oveq2d
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( C .x. ( D .^ X ) ) = ( C .x. ( D ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` (/) ) ) ) )
46 psr1baslem
 |-  ( NN0 ^m 1o ) = { a e. ( NN0 ^m 1o ) | ( `' a " NN ) e. Fin }
47 eqid
 |-  ( 1r ` R ) = ( 1r ` R )
48 1on
 |-  1o e. On
49 48 a1i
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> 1o e. On )
50 eqid
 |-  ( 1o mVar R ) = ( 1o mVar R )
51 simp1
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> R e. Ring )
52 0lt1o
 |-  (/) e. 1o
53 52 a1i
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> (/) e. 1o )
54 simp3
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> D e. NN0 )
55 33 46 1 47 49 24 21 50 51 53 54 mplcoe3
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( y e. ( NN0 ^m 1o ) |-> if ( y = ( b e. 1o |-> if ( b = (/) , D , 0 ) ) , ( 1r ` R ) , .0. ) ) = ( D ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` (/) ) ) )
56 55 oveq2d
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( C .x. ( y e. ( NN0 ^m 1o ) |-> if ( y = ( b e. 1o |-> if ( b = (/) , D , 0 ) ) , ( 1r ` R ) , .0. ) ) ) = ( C .x. ( D ( .g ` ( mulGrp ` ( 1o mPoly R ) ) ) ( ( 1o mVar R ) ` (/) ) ) ) )
57 3 33 5 ply1vsca
 |-  .x. = ( .s ` ( 1o mPoly R ) )
58 elsni
 |-  ( b e. { (/) } -> b = (/) )
59 df1o2
 |-  1o = { (/) }
60 58 59 eleq2s
 |-  ( b e. 1o -> b = (/) )
61 60 iftrued
 |-  ( b e. 1o -> if ( b = (/) , D , 0 ) = D )
62 61 adantl
 |-  ( ( ( R e. Ring /\ C e. K /\ D e. NN0 ) /\ b e. 1o ) -> if ( b = (/) , D , 0 ) = D )
63 62 mpteq2dva
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( b e. 1o |-> if ( b = (/) , D , 0 ) ) = ( b e. 1o |-> D ) )
64 fconstmpt
 |-  ( 1o X. { D } ) = ( b e. 1o |-> D )
65 63 64 eqtr4di
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( b e. 1o |-> if ( b = (/) , D , 0 ) ) = ( 1o X. { D } ) )
66 fconst6g
 |-  ( D e. NN0 -> ( 1o X. { D } ) : 1o --> NN0 )
67 15 16 elmap
 |-  ( ( 1o X. { D } ) e. ( NN0 ^m 1o ) <-> ( 1o X. { D } ) : 1o --> NN0 )
68 66 67 sylibr
 |-  ( D e. NN0 -> ( 1o X. { D } ) e. ( NN0 ^m 1o ) )
69 68 3ad2ant3
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( 1o X. { D } ) e. ( NN0 ^m 1o ) )
70 65 69 eqeltrd
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( b e. 1o |-> if ( b = (/) , D , 0 ) ) e. ( NN0 ^m 1o ) )
71 simp2
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> C e. K )
72 33 57 46 47 1 2 49 51 70 71 mplmon2
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( C .x. ( y e. ( NN0 ^m 1o ) |-> if ( y = ( b e. 1o |-> if ( b = (/) , D , 0 ) ) , ( 1r ` R ) , .0. ) ) ) = ( y e. ( NN0 ^m 1o ) |-> if ( y = ( b e. 1o |-> if ( b = (/) , D , 0 ) ) , C , .0. ) ) )
73 45 56 72 3eqtr2d
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( C .x. ( D .^ X ) ) = ( y e. ( NN0 ^m 1o ) |-> if ( y = ( b e. 1o |-> if ( b = (/) , D , 0 ) ) , C , .0. ) ) )
74 eqeq1
 |-  ( y = ( 1o X. { x } ) -> ( y = ( b e. 1o |-> if ( b = (/) , D , 0 ) ) <-> ( 1o X. { x } ) = ( b e. 1o |-> if ( b = (/) , D , 0 ) ) ) )
75 74 ifbid
 |-  ( y = ( 1o X. { x } ) -> if ( y = ( b e. 1o |-> if ( b = (/) , D , 0 ) ) , C , .0. ) = if ( ( 1o X. { x } ) = ( b e. 1o |-> if ( b = (/) , D , 0 ) ) , C , .0. ) )
76 19 20 73 75 fmptco
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( ( C .x. ( D .^ X ) ) o. ( x e. NN0 |-> ( 1o X. { x } ) ) ) = ( x e. NN0 |-> if ( ( 1o X. { x } ) = ( b e. 1o |-> if ( b = (/) , D , 0 ) ) , C , .0. ) ) )
77 65 adantr
 |-  ( ( ( R e. Ring /\ C e. K /\ D e. NN0 ) /\ x e. NN0 ) -> ( b e. 1o |-> if ( b = (/) , D , 0 ) ) = ( 1o X. { D } ) )
78 77 eqeq2d
 |-  ( ( ( R e. Ring /\ C e. K /\ D e. NN0 ) /\ x e. NN0 ) -> ( ( 1o X. { x } ) = ( b e. 1o |-> if ( b = (/) , D , 0 ) ) <-> ( 1o X. { x } ) = ( 1o X. { D } ) ) )
79 fveq1
 |-  ( ( 1o X. { x } ) = ( 1o X. { D } ) -> ( ( 1o X. { x } ) ` (/) ) = ( ( 1o X. { D } ) ` (/) ) )
80 vex
 |-  x e. _V
81 80 fvconst2
 |-  ( (/) e. 1o -> ( ( 1o X. { x } ) ` (/) ) = x )
82 52 81 mp1i
 |-  ( ( ( R e. Ring /\ C e. K /\ D e. NN0 ) /\ x e. NN0 ) -> ( ( 1o X. { x } ) ` (/) ) = x )
83 simpl3
 |-  ( ( ( R e. Ring /\ C e. K /\ D e. NN0 ) /\ x e. NN0 ) -> D e. NN0 )
84 fvconst2g
 |-  ( ( D e. NN0 /\ (/) e. 1o ) -> ( ( 1o X. { D } ) ` (/) ) = D )
85 83 52 84 sylancl
 |-  ( ( ( R e. Ring /\ C e. K /\ D e. NN0 ) /\ x e. NN0 ) -> ( ( 1o X. { D } ) ` (/) ) = D )
86 82 85 eqeq12d
 |-  ( ( ( R e. Ring /\ C e. K /\ D e. NN0 ) /\ x e. NN0 ) -> ( ( ( 1o X. { x } ) ` (/) ) = ( ( 1o X. { D } ) ` (/) ) <-> x = D ) )
87 79 86 imbitrid
 |-  ( ( ( R e. Ring /\ C e. K /\ D e. NN0 ) /\ x e. NN0 ) -> ( ( 1o X. { x } ) = ( 1o X. { D } ) -> x = D ) )
88 sneq
 |-  ( x = D -> { x } = { D } )
89 88 xpeq2d
 |-  ( x = D -> ( 1o X. { x } ) = ( 1o X. { D } ) )
90 87 89 impbid1
 |-  ( ( ( R e. Ring /\ C e. K /\ D e. NN0 ) /\ x e. NN0 ) -> ( ( 1o X. { x } ) = ( 1o X. { D } ) <-> x = D ) )
91 78 90 bitrd
 |-  ( ( ( R e. Ring /\ C e. K /\ D e. NN0 ) /\ x e. NN0 ) -> ( ( 1o X. { x } ) = ( b e. 1o |-> if ( b = (/) , D , 0 ) ) <-> x = D ) )
92 91 ifbid
 |-  ( ( ( R e. Ring /\ C e. K /\ D e. NN0 ) /\ x e. NN0 ) -> if ( ( 1o X. { x } ) = ( b e. 1o |-> if ( b = (/) , D , 0 ) ) , C , .0. ) = if ( x = D , C , .0. ) )
93 92 mpteq2dva
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( x e. NN0 |-> if ( ( 1o X. { x } ) = ( b e. 1o |-> if ( b = (/) , D , 0 ) ) , C , .0. ) ) = ( x e. NN0 |-> if ( x = D , C , .0. ) ) )
94 13 76 93 3eqtrd
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( coe1 ` ( C .x. ( D .^ X ) ) ) = ( x e. NN0 |-> if ( x = D , C , .0. ) ) )