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 ‘ 𝑅 )
	coe1tm.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	coe1tm.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	coe1tm.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	coe1tm.m	⊢ · = ( ·𝑠 ‘ 𝑃 )
	coe1tm.n	⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
	coe1tm.e	⊢ ↑ = ( .g ‘ 𝑁 )
	coe1tmmul.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	coe1tmmul.t	⊢ ∙ = ( .r ‘ 𝑃 )
	coe1tmmul.u	⊢ × = ( .r ‘ 𝑅 )
	coe1tmmul.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	coe1tmmul.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	coe1tmmul.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
	coe1tmmul.d	⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
	coe1tmmul2fv.y	⊢ ( 𝜑 → 𝑌 ∈ ℕ0 )
Assertion	coe1tmmul2fv	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝐴 ∙ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ) ‘ ( 𝐷 + 𝑌 ) ) = ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑌 ) × 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		coe1tm.z	⊢ 0 = ( 0g ‘ 𝑅 )
2		coe1tm.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
3		coe1tm.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4		coe1tm.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
5		coe1tm.m	⊢ · = ( ·𝑠 ‘ 𝑃 )
6		coe1tm.n	⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
7		coe1tm.e	⊢ ↑ = ( .g ‘ 𝑁 )
8		coe1tmmul.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
9		coe1tmmul.t	⊢ ∙ = ( .r ‘ 𝑃 )
10		coe1tmmul.u	⊢ × = ( .r ‘ 𝑅 )
11		coe1tmmul.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
12		coe1tmmul.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
13		coe1tmmul.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
14		coe1tmmul.d	⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
15		coe1tmmul2fv.y	⊢ ( 𝜑 → 𝑌 ∈ ℕ0 )
16	1 2 3 4 5 6 7 8 9 10 11 12 13 14	coe1tmmul2	⊢ ( 𝜑 → ( coe1 ‘ ( 𝐴 ∙ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷 ≤ 𝑥 , ( ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) × 𝐶 ) , 0 ) ) )
17	16	fveq1d	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝐴 ∙ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ) ‘ ( 𝐷 + 𝑌 ) ) = ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷 ≤ 𝑥 , ( ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) × 𝐶 ) , 0 ) ) ‘ ( 𝐷 + 𝑌 ) ) )
18	14 15	nn0addcld	⊢ ( 𝜑 → ( 𝐷 + 𝑌 ) ∈ ℕ0 )
19		breq2	⊢ ( 𝑥 = ( 𝐷 + 𝑌 ) → ( 𝐷 ≤ 𝑥 ↔ 𝐷 ≤ ( 𝐷 + 𝑌 ) ) )
20		fvoveq1	⊢ ( 𝑥 = ( 𝐷 + 𝑌 ) → ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) = ( ( coe1 ‘ 𝐴 ) ‘ ( ( 𝐷 + 𝑌 ) − 𝐷 ) ) )
21	20	oveq1d	⊢ ( 𝑥 = ( 𝐷 + 𝑌 ) → ( ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) × 𝐶 ) = ( ( ( coe1 ‘ 𝐴 ) ‘ ( ( 𝐷 + 𝑌 ) − 𝐷 ) ) × 𝐶 ) )
22	19 21	ifbieq1d	⊢ ( 𝑥 = ( 𝐷 + 𝑌 ) → if ( 𝐷 ≤ 𝑥 , ( ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) × 𝐶 ) , 0 ) = if ( 𝐷 ≤ ( 𝐷 + 𝑌 ) , ( ( ( coe1 ‘ 𝐴 ) ‘ ( ( 𝐷 + 𝑌 ) − 𝐷 ) ) × 𝐶 ) , 0 ) )
23		eqid	⊢ ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷 ≤ 𝑥 , ( ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) × 𝐶 ) , 0 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷 ≤ 𝑥 , ( ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) × 𝐶 ) , 0 ) )
24		ovex	⊢ ( ( ( coe1 ‘ 𝐴 ) ‘ ( ( 𝐷 + 𝑌 ) − 𝐷 ) ) × 𝐶 ) ∈ V
25	1	fvexi	⊢ 0 ∈ V
26	24 25	ifex	⊢ if ( 𝐷 ≤ ( 𝐷 + 𝑌 ) , ( ( ( coe1 ‘ 𝐴 ) ‘ ( ( 𝐷 + 𝑌 ) − 𝐷 ) ) × 𝐶 ) , 0 ) ∈ V
27	22 23 26	fvmpt	⊢ ( ( 𝐷 + 𝑌 ) ∈ ℕ0 → ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷 ≤ 𝑥 , ( ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) × 𝐶 ) , 0 ) ) ‘ ( 𝐷 + 𝑌 ) ) = if ( 𝐷 ≤ ( 𝐷 + 𝑌 ) , ( ( ( coe1 ‘ 𝐴 ) ‘ ( ( 𝐷 + 𝑌 ) − 𝐷 ) ) × 𝐶 ) , 0 ) )
28	18 27	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷 ≤ 𝑥 , ( ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) × 𝐶 ) , 0 ) ) ‘ ( 𝐷 + 𝑌 ) ) = if ( 𝐷 ≤ ( 𝐷 + 𝑌 ) , ( ( ( coe1 ‘ 𝐴 ) ‘ ( ( 𝐷 + 𝑌 ) − 𝐷 ) ) × 𝐶 ) , 0 ) )
29	14	nn0red	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
30		nn0addge1	⊢ ( ( 𝐷 ∈ ℝ ∧ 𝑌 ∈ ℕ0 ) → 𝐷 ≤ ( 𝐷 + 𝑌 ) )
31	29 15 30	syl2anc	⊢ ( 𝜑 → 𝐷 ≤ ( 𝐷 + 𝑌 ) )
32	31	iftrued	⊢ ( 𝜑 → if ( 𝐷 ≤ ( 𝐷 + 𝑌 ) , ( ( ( coe1 ‘ 𝐴 ) ‘ ( ( 𝐷 + 𝑌 ) − 𝐷 ) ) × 𝐶 ) , 0 ) = ( ( ( coe1 ‘ 𝐴 ) ‘ ( ( 𝐷 + 𝑌 ) − 𝐷 ) ) × 𝐶 ) )
33	14	nn0cnd	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
34	15	nn0cnd	⊢ ( 𝜑 → 𝑌 ∈ ℂ )
35	33 34	pncan2d	⊢ ( 𝜑 → ( ( 𝐷 + 𝑌 ) − 𝐷 ) = 𝑌 )
36	35	fveq2d	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐴 ) ‘ ( ( 𝐷 + 𝑌 ) − 𝐷 ) ) = ( ( coe1 ‘ 𝐴 ) ‘ 𝑌 ) )
37	36	oveq1d	⊢ ( 𝜑 → ( ( ( coe1 ‘ 𝐴 ) ‘ ( ( 𝐷 + 𝑌 ) − 𝐷 ) ) × 𝐶 ) = ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑌 ) × 𝐶 ) )
38	28 32 37	3eqtrd	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷 ≤ 𝑥 , ( ( ( coe1 ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) × 𝐶 ) , 0 ) ) ‘ ( 𝐷 + 𝑌 ) ) = ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑌 ) × 𝐶 ) )
39	17 38	eqtrd	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝐴 ∙ ( 𝐶 · ( 𝐷 ↑ 𝑋 ) ) ) ) ‘ ( 𝐷 + 𝑌 ) ) = ( ( ( coe1 ‘ 𝐴 ) ‘ 𝑌 ) × 𝐶 ) )