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

Metamath Proof Explorer

Theorem coe1tmmul2fv

Proof