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𝑅 )
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𝐴 ) ‘ 𝑌 ) × 𝐶 ) )