Metamath Proof Explorer


Theorem coe1tmmul2

Description: Coefficient vector of a polynomial multiplied on the right by a term. (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 )
Assertion coe1tmmul2 ( 𝜑 → ( coe1 ‘ ( 𝐴 ( 𝐶 · ( 𝐷 𝑋 ) ) ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷𝑥 , ( ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) × 𝐶 ) , 0 ) ) )

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 2 3 4 5 6 7 8 ply1tmcl ( ( 𝑅 ∈ Ring ∧ 𝐶𝐾𝐷 ∈ ℕ0 ) → ( 𝐶 · ( 𝐷 𝑋 ) ) ∈ 𝐵 )
16 12 13 14 15 syl3anc ( 𝜑 → ( 𝐶 · ( 𝐷 𝑋 ) ) ∈ 𝐵 )
17 3 9 10 8 coe1mul ( ( 𝑅 ∈ Ring ∧ 𝐴𝐵 ∧ ( 𝐶 · ( 𝐷 𝑋 ) ) ∈ 𝐵 ) → ( coe1 ‘ ( 𝐴 ( 𝐶 · ( 𝐷 𝑋 ) ) ) ) = ( 𝑥 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) ) ) ) )
18 12 11 16 17 syl3anc ( 𝜑 → ( coe1 ‘ ( 𝐴 ( 𝐶 · ( 𝐷 𝑋 ) ) ) ) = ( 𝑥 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) ) ) ) )
19 eqeq2 ( ( ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) × 𝐶 ) = if ( 𝐷𝑥 , ( ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) × 𝐶 ) , 0 ) → ( ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) ) ) = ( ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) × 𝐶 ) ↔ ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) ) ) = if ( 𝐷𝑥 , ( ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) × 𝐶 ) , 0 ) ) )
20 eqeq2 ( 0 = if ( 𝐷𝑥 , ( ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) × 𝐶 ) , 0 ) → ( ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) ) ) = 0 ↔ ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) ) ) = if ( 𝐷𝑥 , ( ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) × 𝐶 ) , 0 ) ) )
21 12 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → 𝑅 ∈ Ring )
22 ringmnd ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
23 21 22 syl ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → 𝑅 ∈ Mnd )
24 ovex ( 0 ... 𝑥 ) ∈ V
25 24 a1i ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → ( 0 ... 𝑥 ) ∈ V )
26 simprr ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → 𝐷𝑥 )
27 14 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → 𝐷 ∈ ℕ0 )
28 simprl ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → 𝑥 ∈ ℕ0 )
29 nn0sub ( ( 𝐷 ∈ ℕ0𝑥 ∈ ℕ0 ) → ( 𝐷𝑥 ↔ ( 𝑥𝐷 ) ∈ ℕ0 ) )
30 27 28 29 syl2anc ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → ( 𝐷𝑥 ↔ ( 𝑥𝐷 ) ∈ ℕ0 ) )
31 26 30 mpbid ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → ( 𝑥𝐷 ) ∈ ℕ0 )
32 27 nn0ge0d ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → 0 ≤ 𝐷 )
33 nn0re ( 𝑥 ∈ ℕ0𝑥 ∈ ℝ )
34 33 ad2antrl ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → 𝑥 ∈ ℝ )
35 14 nn0red ( 𝜑𝐷 ∈ ℝ )
36 35 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → 𝐷 ∈ ℝ )
37 34 36 subge02d ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → ( 0 ≤ 𝐷 ↔ ( 𝑥𝐷 ) ≤ 𝑥 ) )
38 32 37 mpbid ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → ( 𝑥𝐷 ) ≤ 𝑥 )
39 fznn0 ( 𝑥 ∈ ℕ0 → ( ( 𝑥𝐷 ) ∈ ( 0 ... 𝑥 ) ↔ ( ( 𝑥𝐷 ) ∈ ℕ0 ∧ ( 𝑥𝐷 ) ≤ 𝑥 ) ) )
40 39 ad2antrl ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → ( ( 𝑥𝐷 ) ∈ ( 0 ... 𝑥 ) ↔ ( ( 𝑥𝐷 ) ∈ ℕ0 ∧ ( 𝑥𝐷 ) ≤ 𝑥 ) ) )
41 31 38 40 mpbir2and ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → ( 𝑥𝐷 ) ∈ ( 0 ... 𝑥 ) )
42 12 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝑅 ∈ Ring )
43 eqid ( coe1𝐴 ) = ( coe1𝐴 )
44 43 8 3 2 coe1f ( 𝐴𝐵 → ( coe1𝐴 ) : ℕ0𝐾 )
45 11 44 syl ( 𝜑 → ( coe1𝐴 ) : ℕ0𝐾 )
46 45 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( coe1𝐴 ) : ℕ0𝐾 )
47 elfznn0 ( 𝑦 ∈ ( 0 ... 𝑥 ) → 𝑦 ∈ ℕ0 )
48 47 adantl ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝑦 ∈ ℕ0 )
49 46 48 ffvelrnd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ( coe1𝐴 ) ‘ 𝑦 ) ∈ 𝐾 )
50 eqid ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) = ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) )
51 50 8 3 2 coe1f ( ( 𝐶 · ( 𝐷 𝑋 ) ) ∈ 𝐵 → ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) : ℕ0𝐾 )
52 16 51 syl ( 𝜑 → ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) : ℕ0𝐾 )
53 52 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) : ℕ0𝐾 )
54 fznn0sub ( 𝑦 ∈ ( 0 ... 𝑥 ) → ( 𝑥𝑦 ) ∈ ℕ0 )
55 54 adantl ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( 𝑥𝑦 ) ∈ ℕ0 )
56 53 55 ffvelrnd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ∈ 𝐾 )
57 2 10 ringcl ( ( 𝑅 ∈ Ring ∧ ( ( coe1𝐴 ) ‘ 𝑦 ) ∈ 𝐾 ∧ ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ∈ 𝐾 ) → ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) ∈ 𝐾 )
58 42 49 56 57 syl3anc ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) ∈ 𝐾 )
59 58 fmpttd ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) ) : ( 0 ... 𝑥 ) ⟶ 𝐾 )
60 12 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥𝐷 ) } ) ) → 𝑅 ∈ Ring )
61 13 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥𝐷 ) } ) ) → 𝐶𝐾 )
62 14 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥𝐷 ) } ) ) → 𝐷 ∈ ℕ0 )
63 eldifi ( 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥𝐷 ) } ) → 𝑦 ∈ ( 0 ... 𝑥 ) )
64 63 54 syl ( 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥𝐷 ) } ) → ( 𝑥𝑦 ) ∈ ℕ0 )
65 64 adantl ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥𝐷 ) } ) ) → ( 𝑥𝑦 ) ∈ ℕ0 )
66 eldifsn ( 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥𝐷 ) } ) ↔ ( 𝑦 ∈ ( 0 ... 𝑥 ) ∧ 𝑦 ≠ ( 𝑥𝐷 ) ) )
67 simplrl ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝑥 ∈ ℕ0 )
68 67 nn0cnd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝑥 ∈ ℂ )
69 47 nn0cnd ( 𝑦 ∈ ( 0 ... 𝑥 ) → 𝑦 ∈ ℂ )
70 69 adantl ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝑦 ∈ ℂ )
71 68 70 nncand ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( 𝑥 − ( 𝑥𝑦 ) ) = 𝑦 )
72 71 eqcomd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝑦 = ( 𝑥 − ( 𝑥𝑦 ) ) )
73 oveq2 ( 𝐷 = ( 𝑥𝑦 ) → ( 𝑥𝐷 ) = ( 𝑥 − ( 𝑥𝑦 ) ) )
74 73 eqeq2d ( 𝐷 = ( 𝑥𝑦 ) → ( 𝑦 = ( 𝑥𝐷 ) ↔ 𝑦 = ( 𝑥 − ( 𝑥𝑦 ) ) ) )
75 72 74 syl5ibrcom ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( 𝐷 = ( 𝑥𝑦 ) → 𝑦 = ( 𝑥𝐷 ) ) )
76 75 necon3d ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( 𝑦 ≠ ( 𝑥𝐷 ) → 𝐷 ≠ ( 𝑥𝑦 ) ) )
77 76 impr ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ ( 𝑦 ∈ ( 0 ... 𝑥 ) ∧ 𝑦 ≠ ( 𝑥𝐷 ) ) ) → 𝐷 ≠ ( 𝑥𝑦 ) )
78 66 77 sylan2b ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥𝐷 ) } ) ) → 𝐷 ≠ ( 𝑥𝑦 ) )
79 1 2 3 4 5 6 7 60 61 62 65 78 coe1tmfv2 ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥𝐷 ) } ) ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) = 0 )
80 79 oveq2d ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥𝐷 ) } ) ) → ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) = ( ( ( coe1𝐴 ) ‘ 𝑦 ) × 0 ) )
81 2 10 1 ringrz ( ( 𝑅 ∈ Ring ∧ ( ( coe1𝐴 ) ‘ 𝑦 ) ∈ 𝐾 ) → ( ( ( coe1𝐴 ) ‘ 𝑦 ) × 0 ) = 0 )
82 42 49 81 syl2anc ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ( ( coe1𝐴 ) ‘ 𝑦 ) × 0 ) = 0 )
83 63 82 sylan2 ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥𝐷 ) } ) ) → ( ( ( coe1𝐴 ) ‘ 𝑦 ) × 0 ) = 0 )
84 80 83 eqtrd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { ( 𝑥𝐷 ) } ) ) → ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) = 0 )
85 84 25 suppss2 ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → ( ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) ) supp 0 ) ⊆ { ( 𝑥𝐷 ) } )
86 2 1 23 25 41 59 85 gsumpt ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) ) ) = ( ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) ) ‘ ( 𝑥𝐷 ) ) )
87 fveq2 ( 𝑦 = ( 𝑥𝐷 ) → ( ( coe1𝐴 ) ‘ 𝑦 ) = ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) )
88 oveq2 ( 𝑦 = ( 𝑥𝐷 ) → ( 𝑥𝑦 ) = ( 𝑥 − ( 𝑥𝐷 ) ) )
89 88 fveq2d ( 𝑦 = ( 𝑥𝐷 ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) = ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥 − ( 𝑥𝐷 ) ) ) )
90 87 89 oveq12d ( 𝑦 = ( 𝑥𝐷 ) → ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) = ( ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥 − ( 𝑥𝐷 ) ) ) ) )
91 eqid ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) ) = ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) )
92 ovex ( ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥 − ( 𝑥𝐷 ) ) ) ) ∈ V
93 90 91 92 fvmpt ( ( 𝑥𝐷 ) ∈ ( 0 ... 𝑥 ) → ( ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) ) ‘ ( 𝑥𝐷 ) ) = ( ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥 − ( 𝑥𝐷 ) ) ) ) )
94 41 93 syl ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → ( ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) ) ‘ ( 𝑥𝐷 ) ) = ( ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥 − ( 𝑥𝐷 ) ) ) ) )
95 28 nn0cnd ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → 𝑥 ∈ ℂ )
96 27 nn0cnd ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → 𝐷 ∈ ℂ )
97 95 96 nncand ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → ( 𝑥 − ( 𝑥𝐷 ) ) = 𝐷 )
98 97 fveq2d ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥 − ( 𝑥𝐷 ) ) ) = ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝐷 ) )
99 13 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → 𝐶𝐾 )
100 1 2 3 4 5 6 7 coe1tmfv1 ( ( 𝑅 ∈ Ring ∧ 𝐶𝐾𝐷 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝐷 ) = 𝐶 )
101 21 99 27 100 syl3anc ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝐷 ) = 𝐶 )
102 98 101 eqtrd ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥 − ( 𝑥𝐷 ) ) ) = 𝐶 )
103 102 oveq2d ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → ( ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥 − ( 𝑥𝐷 ) ) ) ) = ( ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) × 𝐶 ) )
104 86 94 103 3eqtrd ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ0𝐷𝑥 ) ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) ) ) = ( ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) × 𝐶 ) )
105 104 anassrs ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) ) ) = ( ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) × 𝐶 ) )
106 12 ad2antrr ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷𝑥𝑦 ∈ ( 0 ... 𝑥 ) ) ) → 𝑅 ∈ Ring )
107 13 ad2antrr ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷𝑥𝑦 ∈ ( 0 ... 𝑥 ) ) ) → 𝐶𝐾 )
108 14 ad2antrr ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷𝑥𝑦 ∈ ( 0 ... 𝑥 ) ) ) → 𝐷 ∈ ℕ0 )
109 54 ad2antll ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷𝑥𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( 𝑥𝑦 ) ∈ ℕ0 )
110 54 nn0red ( 𝑦 ∈ ( 0 ... 𝑥 ) → ( 𝑥𝑦 ) ∈ ℝ )
111 110 ad2antll ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷𝑥𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( 𝑥𝑦 ) ∈ ℝ )
112 33 ad2antlr ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷𝑥𝑦 ∈ ( 0 ... 𝑥 ) ) ) → 𝑥 ∈ ℝ )
113 35 ad2antrr ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷𝑥𝑦 ∈ ( 0 ... 𝑥 ) ) ) → 𝐷 ∈ ℝ )
114 47 ad2antll ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷𝑥𝑦 ∈ ( 0 ... 𝑥 ) ) ) → 𝑦 ∈ ℕ0 )
115 114 nn0ge0d ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷𝑥𝑦 ∈ ( 0 ... 𝑥 ) ) ) → 0 ≤ 𝑦 )
116 47 nn0red ( 𝑦 ∈ ( 0 ... 𝑥 ) → 𝑦 ∈ ℝ )
117 116 ad2antll ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷𝑥𝑦 ∈ ( 0 ... 𝑥 ) ) ) → 𝑦 ∈ ℝ )
118 112 117 subge02d ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷𝑥𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( 0 ≤ 𝑦 ↔ ( 𝑥𝑦 ) ≤ 𝑥 ) )
119 115 118 mpbid ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷𝑥𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( 𝑥𝑦 ) ≤ 𝑥 )
120 simprl ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷𝑥𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ¬ 𝐷𝑥 )
121 112 113 ltnled ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷𝑥𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( 𝑥 < 𝐷 ↔ ¬ 𝐷𝑥 ) )
122 120 121 mpbird ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷𝑥𝑦 ∈ ( 0 ... 𝑥 ) ) ) → 𝑥 < 𝐷 )
123 111 112 113 119 122 lelttrd ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷𝑥𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( 𝑥𝑦 ) < 𝐷 )
124 111 123 gtned ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷𝑥𝑦 ∈ ( 0 ... 𝑥 ) ) ) → 𝐷 ≠ ( 𝑥𝑦 ) )
125 1 2 3 4 5 6 7 106 107 108 109 124 coe1tmfv2 ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷𝑥𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) = 0 )
126 125 oveq2d ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷𝑥𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) = ( ( ( coe1𝐴 ) ‘ 𝑦 ) × 0 ) )
127 45 ad2antrr ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷𝑥𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( coe1𝐴 ) : ℕ0𝐾 )
128 127 114 ffvelrnd ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷𝑥𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( ( coe1𝐴 ) ‘ 𝑦 ) ∈ 𝐾 )
129 106 128 81 syl2anc ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷𝑥𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( ( ( coe1𝐴 ) ‘ 𝑦 ) × 0 ) = 0 )
130 126 129 eqtrd ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ( ¬ 𝐷𝑥𝑦 ∈ ( 0 ... 𝑥 ) ) ) → ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) = 0 )
131 130 anassrs ( ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷𝑥 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) = 0 )
132 131 mpteq2dva ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷𝑥 ) → ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) ) = ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ 0 ) )
133 132 oveq2d ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷𝑥 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) ) ) = ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ 0 ) ) )
134 12 22 syl ( 𝜑𝑅 ∈ Mnd )
135 1 gsumz ( ( 𝑅 ∈ Mnd ∧ ( 0 ... 𝑥 ) ∈ V ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ 0 ) ) = 0 )
136 134 24 135 sylancl ( 𝜑 → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ 0 ) ) = 0 )
137 136 ad2antrr ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷𝑥 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ 0 ) ) = 0 )
138 133 137 eqtrd ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷𝑥 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) ) ) = 0 )
139 19 20 105 138 ifbothda ( ( 𝜑𝑥 ∈ ℕ0 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) ) ) = if ( 𝐷𝑥 , ( ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) × 𝐶 ) , 0 ) )
140 139 mpteq2dva ( 𝜑 → ( 𝑥 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐴 ) ‘ 𝑦 ) × ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ ( 𝑥𝑦 ) ) ) ) ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷𝑥 , ( ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) × 𝐶 ) , 0 ) ) )
141 18 140 eqtrd ( 𝜑 → ( coe1 ‘ ( 𝐴 ( 𝐶 · ( 𝐷 𝑋 ) ) ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷𝑥 , ( ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) × 𝐶 ) , 0 ) ) )