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