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