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