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 ‘ 𝑅 )
	coe1pwmul.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	coe1pwmul.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	coe1pwmul.n	⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
	coe1pwmul.e	⊢ ↑ = ( .g ‘ 𝑁 )
	coe1pwmul.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	coe1pwmul.t	⊢ · = ( .r ‘ 𝑃 )
	coe1pwmul.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	coe1pwmul.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	coe1pwmul.d	⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
	coe1pwmulfv.y	⊢ ( 𝜑 → 𝑌 ∈ ℕ0 )
Assertion	coe1pwmulfv	⊢ ( 𝜑 → ( ( coe1 ‘ ( ( 𝐷 ↑ 𝑋 ) · 𝐴 ) ) ‘ ( 𝐷 + 𝑌 ) ) = ( ( coe1 ‘ 𝐴 ) ‘ 𝑌 ) )

Proof

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