Metamath Proof Explorer

Theorem coe1tmmul2fv

Description: Function value of a right-multiplication by a term in the shifted domain. (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 )
coe1tmmul.b 
|- B = ( Base ` P )
coe1tmmul.t 
|- .xb = ( .r ` P )
coe1tmmul.u 
|- .X. = ( .r ` R )
coe1tmmul.a 
|- ( ph -> A e. B )
coe1tmmul.r 
|- ( ph -> R e. Ring )
coe1tmmul.c 
|- ( ph -> C e. K )
coe1tmmul.d 
|- ( ph -> D e. NN0 )
coe1tmmul2fv.y 
|- ( ph -> Y e. NN0 )
Assertion coe1tmmul2fv 
|- ( ph -> ( ( coe1 ` ( A .xb ( C .x. ( D .^ X ) ) ) ) ` ( D + Y ) ) = ( ( ( coe1 ` A ) ` Y ) .X. C ) )

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 coe1tmmul.b 
 |-  B = ( Base ` P )
9 coe1tmmul.t 
 |-  .xb = ( .r ` P )
10 coe1tmmul.u 
 |-  .X. = ( .r ` R )
11 coe1tmmul.a 
 |-  ( ph -> A e. B )
12 coe1tmmul.r 
 |-  ( ph -> R e. Ring )
13 coe1tmmul.c 
 |-  ( ph -> C e. K )
14 coe1tmmul.d 
 |-  ( ph -> D e. NN0 )
15 coe1tmmul2fv.y 
 |-  ( ph -> Y e. NN0 )
16 1 2 3 4 5 6 7 8 9 10 11 12 13 14 coe1tmmul2 
 |-  ( ph -> ( coe1 ` ( A .xb ( C .x. ( D .^ X ) ) ) ) = ( x e. NN0 |-> if ( D <_ x , ( ( ( coe1 ` A ) ` ( x - D ) ) .X. C ) , .0. ) ) )
17 16 fveq1d 
 |-  ( ph -> ( ( coe1 ` ( A .xb ( C .x. ( D .^ X ) ) ) ) ` ( D + Y ) ) = ( ( x e. NN0 |-> if ( D <_ x , ( ( ( coe1 ` A ) ` ( x - D ) ) .X. C ) , .0. ) ) ` ( D + Y ) ) )
18 14 15 nn0addcld 
 |-  ( ph -> ( D + Y ) e. NN0 )
19 breq2 
 |-  ( x = ( D + Y ) -> ( D <_ x <-> D <_ ( D + Y ) ) )
20 fvoveq1 
 |-  ( x = ( D + Y ) -> ( ( coe1 ` A ) ` ( x - D ) ) = ( ( coe1 ` A ) ` ( ( D + Y ) - D ) ) )
21 20 oveq1d 
 |-  ( x = ( D + Y ) -> ( ( ( coe1 ` A ) ` ( x - D ) ) .X. C ) = ( ( ( coe1 ` A ) ` ( ( D + Y ) - D ) ) .X. C ) )
22 19 21 ifbieq1d 
 |-  ( x = ( D + Y ) -> if ( D <_ x , ( ( ( coe1 ` A ) ` ( x - D ) ) .X. C ) , .0. ) = if ( D <_ ( D + Y ) , ( ( ( coe1 ` A ) ` ( ( D + Y ) - D ) ) .X. C ) , .0. ) )
23 eqid 
 |-  ( x e. NN0 |-> if ( D <_ x , ( ( ( coe1 ` A ) ` ( x - D ) ) .X. C ) , .0. ) ) = ( x e. NN0 |-> if ( D <_ x , ( ( ( coe1 ` A ) ` ( x - D ) ) .X. C ) , .0. ) )
24 ovex 
 |-  ( ( ( coe1 ` A ) ` ( ( D + Y ) - D ) ) .X. C ) e. _V
25 1 fvexi 
 |-  .0. e. _V
26 24 25 ifex 
 |-  if ( D <_ ( D + Y ) , ( ( ( coe1 ` A ) ` ( ( D + Y ) - D ) ) .X. C ) , .0. ) e. _V
27 22 23 26 fvmpt 
 |-  ( ( D + Y ) e. NN0 -> ( ( x e. NN0 |-> if ( D <_ x , ( ( ( coe1 ` A ) ` ( x - D ) ) .X. C ) , .0. ) ) ` ( D + Y ) ) = if ( D <_ ( D + Y ) , ( ( ( coe1 ` A ) ` ( ( D + Y ) - D ) ) .X. C ) , .0. ) )
28 18 27 syl 
 |-  ( ph -> ( ( x e. NN0 |-> if ( D <_ x , ( ( ( coe1 ` A ) ` ( x - D ) ) .X. C ) , .0. ) ) ` ( D + Y ) ) = if ( D <_ ( D + Y ) , ( ( ( coe1 ` A ) ` ( ( D + Y ) - D ) ) .X. C ) , .0. ) )
29 14 nn0red 
 |-  ( ph -> D e. RR )
30 nn0addge1 
 |-  ( ( D e. RR /\ Y e. NN0 ) -> D <_ ( D + Y ) )
31 29 15 30 syl2anc 
 |-  ( ph -> D <_ ( D + Y ) )
32 31 iftrued 
 |-  ( ph -> if ( D <_ ( D + Y ) , ( ( ( coe1 ` A ) ` ( ( D + Y ) - D ) ) .X. C ) , .0. ) = ( ( ( coe1 ` A ) ` ( ( D + Y ) - D ) ) .X. C ) )
33 14 nn0cnd 
 |-  ( ph -> D e. CC )
34 15 nn0cnd 
 |-  ( ph -> Y e. CC )
35 33 34 pncan2d 
 |-  ( ph -> ( ( D + Y ) - D ) = Y )
36 35 fveq2d 
 |-  ( ph -> ( ( coe1 ` A ) ` ( ( D + Y ) - D ) ) = ( ( coe1 ` A ) ` Y ) )
37 36 oveq1d 
 |-  ( ph -> ( ( ( coe1 ` A ) ` ( ( D + Y ) - D ) ) .X. C ) = ( ( ( coe1 ` A ) ` Y ) .X. C ) )
38 28 32 37 3eqtrd 
 |-  ( ph -> ( ( x e. NN0 |-> if ( D <_ x , ( ( ( coe1 ` A ) ` ( x - D ) ) .X. C ) , .0. ) ) ` ( D + Y ) ) = ( ( ( coe1 ` A ) ` Y ) .X. C ) )
39 17 38 eqtrd 
 |-  ( ph -> ( ( coe1 ` ( A .xb ( C .x. ( D .^ X ) ) ) ) ` ( D + Y ) ) = ( ( ( coe1 ` A ) ` Y ) .X. C ) )