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 ffvelcdm ⊢ ( ( ( 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 ffvelcdm ⊢ ( ( ( 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 ‘ 𝐺 ) ‘ 𝐽 ) ) )