Metamath Proof Explorer


Theorem coe1mul3

Description: The coefficient vector of multiplication in the univariate polynomial ring, at indices high enough that at most one component can be active in the sum. (Contributed by Stefan O'Rear, 25-Mar-2015)

Ref Expression
Hypotheses coe1mul3.s 𝑌 = ( Poly1𝑅 )
coe1mul3.t = ( .r𝑌 )
coe1mul3.u · = ( .r𝑅 )
coe1mul3.b 𝐵 = ( Base ‘ 𝑌 )
coe1mul3.d 𝐷 = ( deg1𝑅 )
coe1mul3.r ( 𝜑𝑅 ∈ Ring )
coe1mul3.f1 ( 𝜑𝐹𝐵 )
coe1mul3.f2 ( 𝜑𝐼 ∈ ℕ0 )
coe1mul3.f3 ( 𝜑 → ( 𝐷𝐹 ) ≤ 𝐼 )
coe1mul3.g1 ( 𝜑𝐺𝐵 )
coe1mul3.g2 ( 𝜑𝐽 ∈ ℕ0 )
coe1mul3.g3 ( 𝜑 → ( 𝐷𝐺 ) ≤ 𝐽 )
Assertion coe1mul3 ( 𝜑 → ( ( coe1 ‘ ( 𝐹 𝐺 ) ) ‘ ( 𝐼 + 𝐽 ) ) = ( ( ( coe1𝐹 ) ‘ 𝐼 ) · ( ( coe1𝐺 ) ‘ 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 coe1mul3.s 𝑌 = ( Poly1𝑅 )
2 coe1mul3.t = ( .r𝑌 )
3 coe1mul3.u · = ( .r𝑅 )
4 coe1mul3.b 𝐵 = ( Base ‘ 𝑌 )
5 coe1mul3.d 𝐷 = ( deg1𝑅 )
6 coe1mul3.r ( 𝜑𝑅 ∈ Ring )
7 coe1mul3.f1 ( 𝜑𝐹𝐵 )
8 coe1mul3.f2 ( 𝜑𝐼 ∈ ℕ0 )
9 coe1mul3.f3 ( 𝜑 → ( 𝐷𝐹 ) ≤ 𝐼 )
10 coe1mul3.g1 ( 𝜑𝐺𝐵 )
11 coe1mul3.g2 ( 𝜑𝐽 ∈ ℕ0 )
12 coe1mul3.g3 ( 𝜑 → ( 𝐷𝐺 ) ≤ 𝐽 )
13 1 2 3 4 coe1mul ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) → ( coe1 ‘ ( 𝐹 𝐺 ) ) = ( 𝑥 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( 𝑥𝑦 ) ) ) ) ) ) )
14 6 7 10 13 syl3anc ( 𝜑 → ( coe1 ‘ ( 𝐹 𝐺 ) ) = ( 𝑥 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( 𝑥𝑦 ) ) ) ) ) ) )
15 14 fveq1d ( 𝜑 → ( ( coe1 ‘ ( 𝐹 𝐺 ) ) ‘ ( 𝐼 + 𝐽 ) ) = ( ( 𝑥 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( 𝑥𝑦 ) ) ) ) ) ) ‘ ( 𝐼 + 𝐽 ) ) )
16 8 11 nn0addcld ( 𝜑 → ( 𝐼 + 𝐽 ) ∈ ℕ0 )
17 oveq2 ( 𝑥 = ( 𝐼 + 𝐽 ) → ( 0 ... 𝑥 ) = ( 0 ... ( 𝐼 + 𝐽 ) ) )
18 fvoveq1 ( 𝑥 = ( 𝐼 + 𝐽 ) → ( ( coe1𝐺 ) ‘ ( 𝑥𝑦 ) ) = ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) )
19 18 oveq2d ( 𝑥 = ( 𝐼 + 𝐽 ) → ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( 𝑥𝑦 ) ) ) = ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) )
20 17 19 mpteq12dv ( 𝑥 = ( 𝐼 + 𝐽 ) → ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( 𝑥𝑦 ) ) ) ) = ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) )
21 20 oveq2d ( 𝑥 = ( 𝐼 + 𝐽 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( 𝑥𝑦 ) ) ) ) ) = ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) ) )
22 eqid ( 𝑥 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( 𝑥𝑦 ) ) ) ) ) ) = ( 𝑥 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( 𝑥𝑦 ) ) ) ) ) )
23 ovex ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) ) ∈ V
24 21 22 23 fvmpt ( ( 𝐼 + 𝐽 ) ∈ ℕ0 → ( ( 𝑥 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( 𝑥𝑦 ) ) ) ) ) ) ‘ ( 𝐼 + 𝐽 ) ) = ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) ) )
25 16 24 syl ( 𝜑 → ( ( 𝑥 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( 𝑥𝑦 ) ) ) ) ) ) ‘ ( 𝐼 + 𝐽 ) ) = ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) ) )
26 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
27 eqid ( 0g𝑅 ) = ( 0g𝑅 )
28 ringmnd ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
29 6 28 syl ( 𝜑𝑅 ∈ Mnd )
30 ovexd ( 𝜑 → ( 0 ... ( 𝐼 + 𝐽 ) ) ∈ V )
31 8 nn0red ( 𝜑𝐼 ∈ ℝ )
32 nn0addge1 ( ( 𝐼 ∈ ℝ ∧ 𝐽 ∈ ℕ0 ) → 𝐼 ≤ ( 𝐼 + 𝐽 ) )
33 31 11 32 syl2anc ( 𝜑𝐼 ≤ ( 𝐼 + 𝐽 ) )
34 fznn0 ( ( 𝐼 + 𝐽 ) ∈ ℕ0 → ( 𝐼 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↔ ( 𝐼 ∈ ℕ0𝐼 ≤ ( 𝐼 + 𝐽 ) ) ) )
35 16 34 syl ( 𝜑 → ( 𝐼 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↔ ( 𝐼 ∈ ℕ0𝐼 ≤ ( 𝐼 + 𝐽 ) ) ) )
36 8 33 35 mpbir2and ( 𝜑𝐼 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) )
37 6 adantr ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → 𝑅 ∈ Ring )
38 eqid ( coe1𝐹 ) = ( coe1𝐹 )
39 38 4 1 26 coe1f ( 𝐹𝐵 → ( coe1𝐹 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
40 7 39 syl ( 𝜑 → ( coe1𝐹 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
41 elfznn0 ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) → 𝑦 ∈ ℕ0 )
42 ffvelrn ( ( ( coe1𝐹 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ℕ0 ) → ( ( coe1𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
43 40 41 42 syl2an ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( ( coe1𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
44 eqid ( coe1𝐺 ) = ( coe1𝐺 )
45 44 4 1 26 coe1f ( 𝐺𝐵 → ( coe1𝐺 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
46 10 45 syl ( 𝜑 → ( coe1𝐺 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
47 fznn0sub ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) → ( ( 𝐼 + 𝐽 ) − 𝑦 ) ∈ ℕ0 )
48 ffvelrn ( ( ( coe1𝐺 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) ∧ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ∈ ℕ0 ) → ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) )
49 46 47 48 syl2an ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) )
50 26 3 ringcl ( ( 𝑅 ∈ Ring ∧ ( ( coe1𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ∈ ( Base ‘ 𝑅 ) )
51 37 43 49 50 syl3anc ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ∈ ( Base ‘ 𝑅 ) )
52 51 fmpttd ( 𝜑 → ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) : ( 0 ... ( 𝐼 + 𝐽 ) ) ⟶ ( Base ‘ 𝑅 ) )
53 eldifsn ( 𝑦 ∈ ( ( 0 ... ( 𝐼 + 𝐽 ) ) ∖ { 𝐼 } ) ↔ ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ∧ 𝑦𝐼 ) )
54 41 adantl ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → 𝑦 ∈ ℕ0 )
55 54 nn0red ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → 𝑦 ∈ ℝ )
56 31 adantr ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → 𝐼 ∈ ℝ )
57 55 56 lttri2d ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( 𝑦𝐼 ↔ ( 𝑦 < 𝐼𝐼 < 𝑦 ) ) )
58 10 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝑦 < 𝐼 ) → 𝐺𝐵 )
59 47 adantl ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( ( 𝐼 + 𝐽 ) − 𝑦 ) ∈ ℕ0 )
60 59 adantr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝑦 < 𝐼 ) → ( ( 𝐼 + 𝐽 ) − 𝑦 ) ∈ ℕ0 )
61 5 1 4 deg1xrcl ( 𝐺𝐵 → ( 𝐷𝐺 ) ∈ ℝ* )
62 10 61 syl ( 𝜑 → ( 𝐷𝐺 ) ∈ ℝ* )
63 62 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝑦 < 𝐼 ) → ( 𝐷𝐺 ) ∈ ℝ* )
64 11 nn0red ( 𝜑𝐽 ∈ ℝ )
65 64 rexrd ( 𝜑𝐽 ∈ ℝ* )
66 65 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝑦 < 𝐼 ) → 𝐽 ∈ ℝ* )
67 16 nn0red ( 𝜑 → ( 𝐼 + 𝐽 ) ∈ ℝ )
68 67 adantr ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( 𝐼 + 𝐽 ) ∈ ℝ )
69 68 55 resubcld ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( ( 𝐼 + 𝐽 ) − 𝑦 ) ∈ ℝ )
70 69 rexrd ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( ( 𝐼 + 𝐽 ) − 𝑦 ) ∈ ℝ* )
71 70 adantr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝑦 < 𝐼 ) → ( ( 𝐼 + 𝐽 ) − 𝑦 ) ∈ ℝ* )
72 12 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝑦 < 𝐼 ) → ( 𝐷𝐺 ) ≤ 𝐽 )
73 64 adantr ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → 𝐽 ∈ ℝ )
74 55 56 73 ltadd1d ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( 𝑦 < 𝐼 ↔ ( 𝑦 + 𝐽 ) < ( 𝐼 + 𝐽 ) ) )
75 55 73 68 ltaddsub2d ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( ( 𝑦 + 𝐽 ) < ( 𝐼 + 𝐽 ) ↔ 𝐽 < ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) )
76 74 75 bitrd ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( 𝑦 < 𝐼𝐽 < ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) )
77 76 biimpa ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝑦 < 𝐼 ) → 𝐽 < ( ( 𝐼 + 𝐽 ) − 𝑦 ) )
78 63 66 71 72 77 xrlelttrd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝑦 < 𝐼 ) → ( 𝐷𝐺 ) < ( ( 𝐼 + 𝐽 ) − 𝑦 ) )
79 5 1 4 27 44 deg1lt ( ( 𝐺𝐵 ∧ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ∈ ℕ0 ∧ ( 𝐷𝐺 ) < ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) → ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) = ( 0g𝑅 ) )
80 58 60 78 79 syl3anc ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝑦 < 𝐼 ) → ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) = ( 0g𝑅 ) )
81 80 oveq2d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝑦 < 𝐼 ) → ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( 0g𝑅 ) ) )
82 26 3 27 ringrz ( ( 𝑅 ∈ Ring ∧ ( ( coe1𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( 0g𝑅 ) ) = ( 0g𝑅 ) )
83 37 43 82 syl2anc ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( 0g𝑅 ) ) = ( 0g𝑅 ) )
84 83 adantr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝑦 < 𝐼 ) → ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( 0g𝑅 ) ) = ( 0g𝑅 ) )
85 81 84 eqtrd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝑦 < 𝐼 ) → ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( 0g𝑅 ) )
86 7 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝐼 < 𝑦 ) → 𝐹𝐵 )
87 54 adantr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝐼 < 𝑦 ) → 𝑦 ∈ ℕ0 )
88 5 1 4 deg1xrcl ( 𝐹𝐵 → ( 𝐷𝐹 ) ∈ ℝ* )
89 7 88 syl ( 𝜑 → ( 𝐷𝐹 ) ∈ ℝ* )
90 89 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝐼 < 𝑦 ) → ( 𝐷𝐹 ) ∈ ℝ* )
91 31 rexrd ( 𝜑𝐼 ∈ ℝ* )
92 91 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝐼 < 𝑦 ) → 𝐼 ∈ ℝ* )
93 55 rexrd ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → 𝑦 ∈ ℝ* )
94 93 adantr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝐼 < 𝑦 ) → 𝑦 ∈ ℝ* )
95 9 ad2antrr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝐼 < 𝑦 ) → ( 𝐷𝐹 ) ≤ 𝐼 )
96 simpr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝐼 < 𝑦 ) → 𝐼 < 𝑦 )
97 90 92 94 95 96 xrlelttrd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝐼 < 𝑦 ) → ( 𝐷𝐹 ) < 𝑦 )
98 5 1 4 27 38 deg1lt ( ( 𝐹𝐵𝑦 ∈ ℕ0 ∧ ( 𝐷𝐹 ) < 𝑦 ) → ( ( coe1𝐹 ) ‘ 𝑦 ) = ( 0g𝑅 ) )
99 86 87 97 98 syl3anc ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝐼 < 𝑦 ) → ( ( coe1𝐹 ) ‘ 𝑦 ) = ( 0g𝑅 ) )
100 99 oveq1d ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝐼 < 𝑦 ) → ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( ( 0g𝑅 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) )
101 26 3 27 ringlz ( ( 𝑅 ∈ Ring ∧ ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 0g𝑅 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( 0g𝑅 ) )
102 37 49 101 syl2anc ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( ( 0g𝑅 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( 0g𝑅 ) )
103 102 adantr ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝐼 < 𝑦 ) → ( ( 0g𝑅 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( 0g𝑅 ) )
104 100 103 eqtrd ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝐼 < 𝑦 ) → ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( 0g𝑅 ) )
105 85 104 jaodan ( ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ ( 𝑦 < 𝐼𝐼 < 𝑦 ) ) → ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( 0g𝑅 ) )
106 105 ex ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( ( 𝑦 < 𝐼𝐼 < 𝑦 ) → ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( 0g𝑅 ) ) )
107 57 106 sylbid ( ( 𝜑𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( 𝑦𝐼 → ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( 0g𝑅 ) ) )
108 107 impr ( ( 𝜑 ∧ ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ∧ 𝑦𝐼 ) ) → ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( 0g𝑅 ) )
109 53 108 sylan2b ( ( 𝜑𝑦 ∈ ( ( 0 ... ( 𝐼 + 𝐽 ) ) ∖ { 𝐼 } ) ) → ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( 0g𝑅 ) )
110 109 30 suppss2 ( 𝜑 → ( ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) supp ( 0g𝑅 ) ) ⊆ { 𝐼 } )
111 26 27 29 30 36 52 110 gsumpt ( 𝜑 → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) ) = ( ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) ‘ 𝐼 ) )
112 fveq2 ( 𝑦 = 𝐼 → ( ( coe1𝐹 ) ‘ 𝑦 ) = ( ( coe1𝐹 ) ‘ 𝐼 ) )
113 oveq2 ( 𝑦 = 𝐼 → ( ( 𝐼 + 𝐽 ) − 𝑦 ) = ( ( 𝐼 + 𝐽 ) − 𝐼 ) )
114 113 fveq2d ( 𝑦 = 𝐼 → ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) = ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝐼 ) ) )
115 112 114 oveq12d ( 𝑦 = 𝐼 → ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( ( ( coe1𝐹 ) ‘ 𝐼 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝐼 ) ) ) )
116 eqid ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) = ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) )
117 ovex ( ( ( coe1𝐹 ) ‘ 𝐼 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝐼 ) ) ) ∈ V
118 115 116 117 fvmpt ( 𝐼 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) → ( ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) ‘ 𝐼 ) = ( ( ( coe1𝐹 ) ‘ 𝐼 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝐼 ) ) ) )
119 36 118 syl ( 𝜑 → ( ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) ‘ 𝐼 ) = ( ( ( coe1𝐹 ) ‘ 𝐼 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝐼 ) ) ) )
120 8 nn0cnd ( 𝜑𝐼 ∈ ℂ )
121 11 nn0cnd ( 𝜑𝐽 ∈ ℂ )
122 120 121 pncan2d ( 𝜑 → ( ( 𝐼 + 𝐽 ) − 𝐼 ) = 𝐽 )
123 122 fveq2d ( 𝜑 → ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝐼 ) ) = ( ( coe1𝐺 ) ‘ 𝐽 ) )
124 123 oveq2d ( 𝜑 → ( ( ( coe1𝐹 ) ‘ 𝐼 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝐼 ) ) ) = ( ( ( coe1𝐹 ) ‘ 𝐼 ) · ( ( coe1𝐺 ) ‘ 𝐽 ) ) )
125 111 119 124 3eqtrd ( 𝜑 → ( 𝑅 Σg ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑦 ) · ( ( coe1𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) ) = ( ( ( coe1𝐹 ) ‘ 𝐼 ) · ( ( coe1𝐺 ) ‘ 𝐽 ) ) )
126 15 25 125 3eqtrd ( 𝜑 → ( ( coe1 ‘ ( 𝐹 𝐺 ) ) ‘ ( 𝐼 + 𝐽 ) ) = ( ( ( coe1𝐹 ) ‘ 𝐼 ) · ( ( coe1𝐺 ) ‘ 𝐽 ) ) )