Metamath Proof Explorer


Theorem coe1tmmul

Description: Coefficient vector of a polynomial multiplied on the left by a term. (Contributed by Stefan O'Rear, 29-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 coe1tmmul ( 𝜑 → ( 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 16 11 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 ad2antrr ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → 𝑅 ∈ Ring )
22 ringmnd ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
23 21 22 syl ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → 𝑅 ∈ Mnd )
24 ovexd ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → ( 0 ... 𝑥 ) ∈ V )
25 14 ad2antrr ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → 𝐷 ∈ ℕ0 )
26 simpr ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → 𝐷𝑥 )
27 fznn0 ( 𝑥 ∈ ℕ0 → ( 𝐷 ∈ ( 0 ... 𝑥 ) ↔ ( 𝐷 ∈ ℕ0𝐷𝑥 ) ) )
28 27 ad2antlr ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → ( 𝐷 ∈ ( 0 ... 𝑥 ) ↔ ( 𝐷 ∈ ℕ0𝐷𝑥 ) ) )
29 25 26 28 mpbir2and ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → 𝐷 ∈ ( 0 ... 𝑥 ) )
30 12 ad2antrr ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝑅 ∈ Ring )
31 eqid ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) = ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) )
32 31 8 3 2 coe1f ( ( 𝐶 · ( 𝐷 𝑋 ) ) ∈ 𝐵 → ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) : ℕ0𝐾 )
33 16 32 syl ( 𝜑 → ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) : ℕ0𝐾 )
34 33 adantr ( ( 𝜑𝑥 ∈ ℕ0 ) → ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) : ℕ0𝐾 )
35 elfznn0 ( 𝑦 ∈ ( 0 ... 𝑥 ) → 𝑦 ∈ ℕ0 )
36 ffvelrn ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) : ℕ0𝐾𝑦 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) ∈ 𝐾 )
37 34 35 36 syl2an ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) ∈ 𝐾 )
38 eqid ( coe1𝐴 ) = ( coe1𝐴 )
39 38 8 3 2 coe1f ( 𝐴𝐵 → ( coe1𝐴 ) : ℕ0𝐾 )
40 11 39 syl ( 𝜑 → ( coe1𝐴 ) : ℕ0𝐾 )
41 40 adantr ( ( 𝜑𝑥 ∈ ℕ0 ) → ( coe1𝐴 ) : ℕ0𝐾 )
42 fznn0sub ( 𝑦 ∈ ( 0 ... 𝑥 ) → ( 𝑥𝑦 ) ∈ ℕ0 )
43 ffvelrn ( ( ( coe1𝐴 ) : ℕ0𝐾 ∧ ( 𝑥𝑦 ) ∈ ℕ0 ) → ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ∈ 𝐾 )
44 41 42 43 syl2an ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ∈ 𝐾 )
45 2 10 ringcl ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) ∈ 𝐾 ∧ ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ∈ 𝐾 ) → ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) ∈ 𝐾 )
46 30 37 44 45 syl3anc ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) ∈ 𝐾 )
47 46 fmpttd ( ( 𝜑𝑥 ∈ ℕ0 ) → ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) ) : ( 0 ... 𝑥 ) ⟶ 𝐾 )
48 47 adantr ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) ) : ( 0 ... 𝑥 ) ⟶ 𝐾 )
49 12 ad3antrrr ( ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) ) → 𝑅 ∈ Ring )
50 13 ad3antrrr ( ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) ) → 𝐶𝐾 )
51 14 ad3antrrr ( ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) ) → 𝐷 ∈ ℕ0 )
52 eldifi ( 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) → 𝑦 ∈ ( 0 ... 𝑥 ) )
53 52 35 syl ( 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) → 𝑦 ∈ ℕ0 )
54 53 adantl ( ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) ) → 𝑦 ∈ ℕ0 )
55 eldifsni ( 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) → 𝑦𝐷 )
56 55 necomd ( 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) → 𝐷𝑦 )
57 56 adantl ( ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) ) → 𝐷𝑦 )
58 1 2 3 4 5 6 7 49 50 51 54 57 coe1tmfv2 ( ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) = 0 )
59 58 oveq1d ( ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) ) → ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) = ( 0 × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) )
60 2 10 1 ringlz ( ( 𝑅 ∈ Ring ∧ ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ∈ 𝐾 ) → ( 0 × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) = 0 )
61 30 44 60 syl2anc ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( 0 × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) = 0 )
62 52 61 sylan2 ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) ) → ( 0 × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) = 0 )
63 62 adantlr ( ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) ) → ( 0 × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) = 0 )
64 59 63 eqtrd ( ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) ∧ 𝑦 ∈ ( ( 0 ... 𝑥 ) ∖ { 𝐷 } ) ) → ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) = 0 )
65 64 24 suppss2 ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → ( ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) ) supp 0 ) ⊆ { 𝐷 } )
66 2 1 23 24 29 48 65 gsumpt ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) ) ) = ( ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) ) ‘ 𝐷 ) )
67 fveq2 ( 𝑦 = 𝐷 → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) = ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝐷 ) )
68 oveq2 ( 𝑦 = 𝐷 → ( 𝑥𝑦 ) = ( 𝑥𝐷 ) )
69 68 fveq2d ( 𝑦 = 𝐷 → ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) = ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) )
70 67 69 oveq12d ( 𝑦 = 𝐷 → ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) = ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝐷 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) ) )
71 eqid ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) ) = ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) )
72 ovex ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝐷 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) ) ∈ V
73 70 71 72 fvmpt ( 𝐷 ∈ ( 0 ... 𝑥 ) → ( ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) ) ‘ 𝐷 ) = ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝐷 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) ) )
74 29 73 syl ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → ( ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) ) ‘ 𝐷 ) = ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝐷 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) ) )
75 1 2 3 4 5 6 7 coe1tmfv1 ( ( 𝑅 ∈ Ring ∧ 𝐶𝐾𝐷 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝐷 ) = 𝐶 )
76 12 13 14 75 syl3anc ( 𝜑 → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝐷 ) = 𝐶 )
77 76 ad2antrr ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝐷 ) = 𝐶 )
78 77 oveq1d ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝐷 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) ) = ( 𝐶 × ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) ) )
79 74 78 eqtrd ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → ( ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) ) ‘ 𝐷 ) = ( 𝐶 × ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) ) )
80 66 79 eqtrd ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝐷𝑥 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) ) ) = ( 𝐶 × ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) ) )
81 12 ad3antrrr ( ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷𝑥 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝑅 ∈ Ring )
82 13 ad3antrrr ( ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷𝑥 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝐶𝐾 )
83 14 ad3antrrr ( ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷𝑥 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝐷 ∈ ℕ0 )
84 35 adantl ( ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷𝑥 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝑦 ∈ ℕ0 )
85 elfzle2 ( 𝑦 ∈ ( 0 ... 𝑥 ) → 𝑦𝑥 )
86 85 adantl ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝑦𝑥 )
87 breq1 ( 𝐷 = 𝑦 → ( 𝐷𝑥𝑦𝑥 ) )
88 86 87 syl5ibrcom ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( 𝐷 = 𝑦𝐷𝑥 ) )
89 88 necon3bd ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ¬ 𝐷𝑥𝐷𝑦 ) )
90 89 imp ( ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) ∧ ¬ 𝐷𝑥 ) → 𝐷𝑦 )
91 90 an32s ( ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷𝑥 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → 𝐷𝑦 )
92 1 2 3 4 5 6 7 81 82 83 84 91 coe1tmfv2 ( ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷𝑥 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) = 0 )
93 92 oveq1d ( ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷𝑥 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) = ( 0 × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) )
94 61 adantlr ( ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷𝑥 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( 0 × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) = 0 )
95 93 94 eqtrd ( ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷𝑥 ) ∧ 𝑦 ∈ ( 0 ... 𝑥 ) ) → ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) = 0 )
96 95 mpteq2dva ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷𝑥 ) → ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) ) = ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ 0 ) )
97 96 oveq2d ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷𝑥 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) ) ) = ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ 0 ) ) )
98 12 22 syl ( 𝜑𝑅 ∈ Mnd )
99 98 ad2antrr ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷𝑥 ) → 𝑅 ∈ Mnd )
100 ovexd ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷𝑥 ) → ( 0 ... 𝑥 ) ∈ V )
101 1 gsumz ( ( 𝑅 ∈ Mnd ∧ ( 0 ... 𝑥 ) ∈ V ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ 0 ) ) = 0 )
102 99 100 101 syl2anc ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷𝑥 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ 0 ) ) = 0 )
103 97 102 eqtrd ( ( ( 𝜑𝑥 ∈ ℕ0 ) ∧ ¬ 𝐷𝑥 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) ) ) = 0 )
104 19 20 80 103 ifbothda ( ( 𝜑𝑥 ∈ ℕ0 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) ) ) = if ( 𝐷𝑥 , ( 𝐶 × ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) ) , 0 ) )
105 104 mpteq2dva ( 𝜑 → ( 𝑥 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1 ‘ ( 𝐶 · ( 𝐷 𝑋 ) ) ) ‘ 𝑦 ) × ( ( coe1𝐴 ) ‘ ( 𝑥𝑦 ) ) ) ) ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷𝑥 , ( 𝐶 × ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) ) , 0 ) ) )
106 18 105 eqtrd ( 𝜑 → ( coe1 ‘ ( ( 𝐶 · ( 𝐷 𝑋 ) ) 𝐴 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝐷𝑥 , ( 𝐶 × ( ( coe1𝐴 ) ‘ ( 𝑥𝐷 ) ) ) , 0 ) ) )