Metamath Proof Explorer

Theorem coe1sclmul2

Description: Coefficient vector of a polynomial multiplied on the right by a scalar. (Contributed by Stefan O'Rear, 29-Mar-2015)

Ref Expression
Hypotheses coe1sclmul.p 
|- P = ( Poly1 ` R )
coe1sclmul.b 
|- B = ( Base ` P )
coe1sclmul.k 
|- K = ( Base ` R )
coe1sclmul.a 
|- A = ( algSc ` P )
coe1sclmul.t 
|- .xb = ( .r ` P )
coe1sclmul.u 
|- .x. = ( .r ` R )
Assertion coe1sclmul2 
|- ( ( R e. Ring /\ X e. K /\ Y e. B ) -> ( coe1 ` ( Y .xb ( A ` X ) ) ) = ( ( coe1 ` Y ) oF .x. ( NN0 X. { X } ) ) )

Proof

Step Hyp Ref Expression
1 coe1sclmul.p 
 |-  P = ( Poly1 ` R )
2 coe1sclmul.b 
 |-  B = ( Base ` P )
3 coe1sclmul.k 
 |-  K = ( Base ` R )
4 coe1sclmul.a 
 |-  A = ( algSc ` P )
5 coe1sclmul.t 
 |-  .xb = ( .r ` P )
6 coe1sclmul.u 
 |-  .x. = ( .r ` R )
7 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
8 eqid 
 |-  ( var1 ` R ) = ( var1 ` R )
9 eqid 
 |-  ( .s ` P ) = ( .s ` P )
10 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
11 eqid 
 |-  ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
12 simp3 
 |-  ( ( R e. Ring /\ X e. K /\ Y e. B ) -> Y e. B )
13 simp1 
 |-  ( ( R e. Ring /\ X e. K /\ Y e. B ) -> R e. Ring )
14 simp2 
 |-  ( ( R e. Ring /\ X e. K /\ Y e. B ) -> X e. K )
15 0nn0 
 |-  0 e. NN0
16 15 a1i 
 |-  ( ( R e. Ring /\ X e. K /\ Y e. B ) -> 0 e. NN0 )
17 7 3 1 8 9 10 11 2 5 6 12 13 14 16 coe1tmmul2 
 |-  ( ( R e. Ring /\ X e. K /\ Y e. B ) -> ( coe1 ` ( Y .xb ( X ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) = ( x e. NN0 |-> if ( 0 <_ x , ( ( ( coe1 ` Y ) ` ( x - 0 ) ) .x. X ) , ( 0g ` R ) ) ) )
18 3 1 8 9 10 11 4 ply1scltm 
 |-  ( ( R e. Ring /\ X e. K ) -> ( A ` X ) = ( X ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
19 18 3adant3 
 |-  ( ( R e. Ring /\ X e. K /\ Y e. B ) -> ( A ` X ) = ( X ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
20 19 oveq2d 
 |-  ( ( R e. Ring /\ X e. K /\ Y e. B ) -> ( Y .xb ( A ` X ) ) = ( Y .xb ( X ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) )
21 20 fveq2d 
 |-  ( ( R e. Ring /\ X e. K /\ Y e. B ) -> ( coe1 ` ( Y .xb ( A ` X ) ) ) = ( coe1 ` ( Y .xb ( X ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) )
22 nn0ex 
 |-  NN0 e. _V
23 22 a1i 
 |-  ( ( R e. Ring /\ X e. K /\ Y e. B ) -> NN0 e. _V )
24 fvexd 
 |-  ( ( ( R e. Ring /\ X e. K /\ Y e. B ) /\ x e. NN0 ) -> ( ( coe1 ` Y ) ` x ) e. _V )
25 simpl2 
 |-  ( ( ( R e. Ring /\ X e. K /\ Y e. B ) /\ x e. NN0 ) -> X e. K )
26 eqid 
 |-  ( coe1 ` Y ) = ( coe1 ` Y )
27 26 2 1 3 coe1f 
 |-  ( Y e. B -> ( coe1 ` Y ) : NN0 --> K )
28 27 feqmptd 
 |-  ( Y e. B -> ( coe1 ` Y ) = ( x e. NN0 |-> ( ( coe1 ` Y ) ` x ) ) )
29 28 3ad2ant3 
 |-  ( ( R e. Ring /\ X e. K /\ Y e. B ) -> ( coe1 ` Y ) = ( x e. NN0 |-> ( ( coe1 ` Y ) ` x ) ) )
30 fconstmpt 
 |-  ( NN0 X. { X } ) = ( x e. NN0 |-> X )
31 30 a1i 
 |-  ( ( R e. Ring /\ X e. K /\ Y e. B ) -> ( NN0 X. { X } ) = ( x e. NN0 |-> X ) )
32 23 24 25 29 31 offval2 
 |-  ( ( R e. Ring /\ X e. K /\ Y e. B ) -> ( ( coe1 ` Y ) oF .x. ( NN0 X. { X } ) ) = ( x e. NN0 |-> ( ( ( coe1 ` Y ) ` x ) .x. X ) ) )
33 nn0ge0 
 |-  ( x e. NN0 -> 0 <_ x )
34 33 iftrued 
 |-  ( x e. NN0 -> if ( 0 <_ x , ( ( ( coe1 ` Y ) ` ( x - 0 ) ) .x. X ) , ( 0g ` R ) ) = ( ( ( coe1 ` Y ) ` ( x - 0 ) ) .x. X ) )
35 nn0cn 
 |-  ( x e. NN0 -> x e. CC )
36 35 subid1d 
 |-  ( x e. NN0 -> ( x - 0 ) = x )
37 36 fveq2d 
 |-  ( x e. NN0 -> ( ( coe1 ` Y ) ` ( x - 0 ) ) = ( ( coe1 ` Y ) ` x ) )
38 37 oveq1d 
 |-  ( x e. NN0 -> ( ( ( coe1 ` Y ) ` ( x - 0 ) ) .x. X ) = ( ( ( coe1 ` Y ) ` x ) .x. X ) )
39 34 38 eqtrd 
 |-  ( x e. NN0 -> if ( 0 <_ x , ( ( ( coe1 ` Y ) ` ( x - 0 ) ) .x. X ) , ( 0g ` R ) ) = ( ( ( coe1 ` Y ) ` x ) .x. X ) )
40 39 mpteq2ia 
 |-  ( x e. NN0 |-> if ( 0 <_ x , ( ( ( coe1 ` Y ) ` ( x - 0 ) ) .x. X ) , ( 0g ` R ) ) ) = ( x e. NN0 |-> ( ( ( coe1 ` Y ) ` x ) .x. X ) )
41 32 40 eqtr4di 
 |-  ( ( R e. Ring /\ X e. K /\ Y e. B ) -> ( ( coe1 ` Y ) oF .x. ( NN0 X. { X } ) ) = ( x e. NN0 |-> if ( 0 <_ x , ( ( ( coe1 ` Y ) ` ( x - 0 ) ) .x. X ) , ( 0g ` R ) ) ) )
42 17 21 41 3eqtr4d 
 |-  ( ( R e. Ring /\ X e. K /\ Y e. B ) -> ( coe1 ` ( Y .xb ( A ` X ) ) ) = ( ( coe1 ` Y ) oF .x. ( NN0 X. { X } ) ) )