Metamath Proof Explorer

Theorem coe1pwmulfv

Description: Function value of a right-multiplication by a variable power in the shifted domain. (Contributed by Stefan O'Rear, 1-Apr-2015)

Ref Expression
Hypotheses coe1pwmul.z 
|- .0. = ( 0g ` R )
coe1pwmul.p 
|- P = ( Poly1 ` R )
coe1pwmul.x 
|- X = ( var1 ` R )
coe1pwmul.n 
|- N = ( mulGrp ` P )
coe1pwmul.e 
|- .^ = ( .g ` N )
coe1pwmul.b 
|- B = ( Base ` P )
coe1pwmul.t 
|- .x. = ( .r ` P )
coe1pwmul.r 
|- ( ph -> R e. Ring )
coe1pwmul.a 
|- ( ph -> A e. B )
coe1pwmul.d 
|- ( ph -> D e. NN0 )
coe1pwmulfv.y 
|- ( ph -> Y e. NN0 )
Assertion coe1pwmulfv 
|- ( ph -> ( ( coe1 ` ( ( D .^ X ) .x. A ) ) ` ( D + Y ) ) = ( ( coe1 ` A ) ` Y ) )

Proof

Step Hyp Ref Expression
1 coe1pwmul.z 
 |-  .0. = ( 0g ` R )
2 coe1pwmul.p 
 |-  P = ( Poly1 ` R )
3 coe1pwmul.x 
 |-  X = ( var1 ` R )
4 coe1pwmul.n 
 |-  N = ( mulGrp ` P )
5 coe1pwmul.e 
 |-  .^ = ( .g ` N )
6 coe1pwmul.b 
 |-  B = ( Base ` P )
7 coe1pwmul.t 
 |-  .x. = ( .r ` P )
8 coe1pwmul.r 
 |-  ( ph -> R e. Ring )
9 coe1pwmul.a 
 |-  ( ph -> A e. B )
10 coe1pwmul.d 
 |-  ( ph -> D e. NN0 )
11 coe1pwmulfv.y 
 |-  ( ph -> Y e. NN0 )
12 1 2 3 4 5 6 7 8 9 10 coe1pwmul 
 |-  ( ph -> ( coe1 ` ( ( D .^ X ) .x. A ) ) = ( x e. NN0 |-> if ( D <_ x , ( ( coe1 ` A ) ` ( x - D ) ) , .0. ) ) )
13 12 fveq1d 
 |-  ( ph -> ( ( coe1 ` ( ( D .^ X ) .x. A ) ) ` ( D + Y ) ) = ( ( x e. NN0 |-> if ( D <_ x , ( ( coe1 ` A ) ` ( x - D ) ) , .0. ) ) ` ( D + Y ) ) )
14 10 11 nn0addcld 
 |-  ( ph -> ( D + Y ) e. NN0 )
15 breq2 
 |-  ( x = ( D + Y ) -> ( D <_ x <-> D <_ ( D + Y ) ) )
16 fvoveq1 
 |-  ( x = ( D + Y ) -> ( ( coe1 ` A ) ` ( x - D ) ) = ( ( coe1 ` A ) ` ( ( D + Y ) - D ) ) )
17 15 16 ifbieq1d 
 |-  ( x = ( D + Y ) -> if ( D <_ x , ( ( coe1 ` A ) ` ( x - D ) ) , .0. ) = if ( D <_ ( D + Y ) , ( ( coe1 ` A ) ` ( ( D + Y ) - D ) ) , .0. ) )
18 eqid 
 |-  ( x e. NN0 |-> if ( D <_ x , ( ( coe1 ` A ) ` ( x - D ) ) , .0. ) ) = ( x e. NN0 |-> if ( D <_ x , ( ( coe1 ` A ) ` ( x - D ) ) , .0. ) )
19 fvex 
 |-  ( ( coe1 ` A ) ` ( ( D + Y ) - D ) ) e. _V
20 1 fvexi 
 |-  .0. e. _V
21 19 20 ifex 
 |-  if ( D <_ ( D + Y ) , ( ( coe1 ` A ) ` ( ( D + Y ) - D ) ) , .0. ) e. _V
22 17 18 21 fvmpt 
 |-  ( ( D + Y ) e. NN0 -> ( ( x e. NN0 |-> if ( D <_ x , ( ( coe1 ` A ) ` ( x - D ) ) , .0. ) ) ` ( D + Y ) ) = if ( D <_ ( D + Y ) , ( ( coe1 ` A ) ` ( ( D + Y ) - D ) ) , .0. ) )
23 14 22 syl 
 |-  ( ph -> ( ( x e. NN0 |-> if ( D <_ x , ( ( coe1 ` A ) ` ( x - D ) ) , .0. ) ) ` ( D + Y ) ) = if ( D <_ ( D + Y ) , ( ( coe1 ` A ) ` ( ( D + Y ) - D ) ) , .0. ) )
24 10 nn0red 
 |-  ( ph -> D e. RR )
25 nn0addge1 
 |-  ( ( D e. RR /\ Y e. NN0 ) -> D <_ ( D + Y ) )
26 24 11 25 syl2anc 
 |-  ( ph -> D <_ ( D + Y ) )
27 26 iftrued 
 |-  ( ph -> if ( D <_ ( D + Y ) , ( ( coe1 ` A ) ` ( ( D + Y ) - D ) ) , .0. ) = ( ( coe1 ` A ) ` ( ( D + Y ) - D ) ) )
28 10 nn0cnd 
 |-  ( ph -> D e. CC )
29 11 nn0cnd 
 |-  ( ph -> Y e. CC )
30 28 29 pncan2d 
 |-  ( ph -> ( ( D + Y ) - D ) = Y )
31 30 fveq2d 
 |-  ( ph -> ( ( coe1 ` A ) ` ( ( D + Y ) - D ) ) = ( ( coe1 ` A ) ` Y ) )
32 23 27 31 3eqtrd 
 |-  ( ph -> ( ( x e. NN0 |-> if ( D <_ x , ( ( coe1 ` A ) ` ( x - D ) ) , .0. ) ) ` ( D + Y ) ) = ( ( coe1 ` A ) ` Y ) )
33 13 32 eqtrd 
 |-  ( ph -> ( ( coe1 ` ( ( D .^ X ) .x. A ) ) ` ( D + Y ) ) = ( ( coe1 ` A ) ` Y ) )