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	⊢ 𝑌 = ( Poly₁ ‘ 𝑅 )
	coe1mul3.t	⊢ ∙ = ( ._r ‘ 𝑌 )
	coe1mul3.u	⊢ · = ( ._r ‘ 𝑅 )
	coe1mul3.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	coe1mul3.d	⊢ 𝐷 = ( deg₁ ‘ 𝑅 )
	coe1mul3.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	coe1mul3.f1	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	coe1mul3.f2	⊢ ( 𝜑 → 𝐼 ∈ ℕ₀ )
	coe1mul3.f3	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ 𝐼 )
	coe1mul3.g1	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
	coe1mul3.g2	⊢ ( 𝜑 → 𝐽 ∈ ℕ₀ )
	coe1mul3.g3	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ≤ 𝐽 )
Assertion	coe1mul3	⊢ ( 𝜑 → ( ( coe₁ ‘ ( 𝐹 ∙ 𝐺 ) ) ‘ ( 𝐼 + 𝐽 ) ) = ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝐼 ) · ( ( coe₁ ‘ 𝐺 ) ‘ 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		coe1mul3.s	⊢ 𝑌 = ( Poly₁ ‘ 𝑅 )
2		coe1mul3.t	⊢ ∙ = ( ._r ‘ 𝑌 )
3		coe1mul3.u	⊢ · = ( ._r ‘ 𝑅 )
4		coe1mul3.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
5		coe1mul3.d	⊢ 𝐷 = ( deg₁ ‘ 𝑅 )
6		coe1mul3.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
7		coe1mul3.f1	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
8		coe1mul3.f2	⊢ ( 𝜑 → 𝐼 ∈ ℕ₀ )
9		coe1mul3.f3	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ 𝐼 )
10		coe1mul3.g1	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
11		coe1mul3.g2	⊢ ( 𝜑 → 𝐽 ∈ ℕ₀ )
12		coe1mul3.g3	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ≤ 𝐽 )
13	1 2 3 4	coe1mul	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe₁ ‘ ( 𝐹 ∙ 𝐺 ) ) = ( 𝑥 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) ) )
14	6 7 10 13	syl3anc	⊢ ( 𝜑 → ( coe₁ ‘ ( 𝐹 ∙ 𝐺 ) ) = ( 𝑥 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) ) )
15	14	fveq1d	⊢ ( 𝜑 → ( ( coe₁ ‘ ( 𝐹 ∙ 𝐺 ) ) ‘ ( 𝐼 + 𝐽 ) ) = ( ( 𝑥 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) ) ‘ ( 𝐼 + 𝐽 ) ) )
16	8 11	nn0addcld	⊢ ( 𝜑 → ( 𝐼 + 𝐽 ) ∈ ℕ₀ )
17		oveq2	⊢ ( 𝑥 = ( 𝐼 + 𝐽 ) → ( 0 ... 𝑥 ) = ( 0 ... ( 𝐼 + 𝐽 ) ) )
18		fvoveq1	⊢ ( 𝑥 = ( 𝐼 + 𝐽 ) → ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑥 − 𝑦 ) ) = ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) )
19	18	oveq2d	⊢ ( 𝑥 = ( 𝐼 + 𝐽 ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑥 − 𝑦 ) ) ) = ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) )
20	17 19	mpteq12dv	⊢ ( 𝑥 = ( 𝐼 + 𝐽 ) → ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) = ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) )
21	20	oveq2d	⊢ ( 𝑥 = ( 𝐼 + 𝐽 ) → ( 𝑅 Σ_g ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) = ( 𝑅 Σ_g ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) ) )
22		eqid	⊢ ( 𝑥 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) ) = ( 𝑥 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) )
23		ovex	⊢ ( 𝑅 Σ_g ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) ) ∈ V
24	21 22 23	fvmpt	⊢ ( ( 𝐼 + 𝐽 ) ∈ ℕ₀ → ( ( 𝑥 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) ) ‘ ( 𝐼 + 𝐽 ) ) = ( 𝑅 Σ_g ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) ) )
25	16 24	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑦 ∈ ( 0 ... 𝑥 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑥 − 𝑦 ) ) ) ) ) ) ‘ ( 𝐼 + 𝐽 ) ) = ( 𝑅 Σ_g ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) ) )
26		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
27		eqid	⊢ ( 0_g ‘ 𝑅 ) = ( 0_g ‘ 𝑅 )
28		ringmnd	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
29	6 28	syl	⊢ ( 𝜑 → 𝑅 ∈ Mnd )
30		ovexd	⊢ ( 𝜑 → ( 0 ... ( 𝐼 + 𝐽 ) ) ∈ V )
31	8	nn0red	⊢ ( 𝜑 → 𝐼 ∈ ℝ )
32		nn0addge1	⊢ ( ( 𝐼 ∈ ℝ ∧ 𝐽 ∈ ℕ₀ ) → 𝐼 ≤ ( 𝐼 + 𝐽 ) )
33	31 11 32	syl2anc	⊢ ( 𝜑 → 𝐼 ≤ ( 𝐼 + 𝐽 ) )
34		fznn0	⊢ ( ( 𝐼 + 𝐽 ) ∈ ℕ₀ → ( 𝐼 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↔ ( 𝐼 ∈ ℕ₀ ∧ 𝐼 ≤ ( 𝐼 + 𝐽 ) ) ) )
35	16 34	syl	⊢ ( 𝜑 → ( 𝐼 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↔ ( 𝐼 ∈ ℕ₀ ∧ 𝐼 ≤ ( 𝐼 + 𝐽 ) ) ) )
36	8 33 35	mpbir2and	⊢ ( 𝜑 → 𝐼 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) )
37	6	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → 𝑅 ∈ Ring )
38		eqid	⊢ ( coe₁ ‘ 𝐹 ) = ( coe₁ ‘ 𝐹 )
39	38 4 1 26	coe1f	⊢ ( 𝐹 ∈ 𝐵 → ( coe₁ ‘ 𝐹 ) : ℕ₀ ⟶ ( Base ‘ 𝑅 ) )
40	7 39	syl	⊢ ( 𝜑 → ( coe₁ ‘ 𝐹 ) : ℕ₀ ⟶ ( Base ‘ 𝑅 ) )
41		elfznn0	⊢ ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) → 𝑦 ∈ ℕ₀ )
42		ffvelcdm	⊢ ( ( ( coe₁ ‘ 𝐹 ) : ℕ₀ ⟶ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ℕ₀ ) → ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
43	40 41 42	syl2an	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
44		eqid	⊢ ( coe₁ ‘ 𝐺 ) = ( coe₁ ‘ 𝐺 )
45	44 4 1 26	coe1f	⊢ ( 𝐺 ∈ 𝐵 → ( coe₁ ‘ 𝐺 ) : ℕ₀ ⟶ ( Base ‘ 𝑅 ) )
46	10 45	syl	⊢ ( 𝜑 → ( coe₁ ‘ 𝐺 ) : ℕ₀ ⟶ ( Base ‘ 𝑅 ) )
47		fznn0sub	⊢ ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) → ( ( 𝐼 + 𝐽 ) − 𝑦 ) ∈ ℕ₀ )
48		ffvelcdm	⊢ ( ( ( coe₁ ‘ 𝐺 ) : ℕ₀ ⟶ ( Base ‘ 𝑅 ) ∧ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ∈ ℕ₀ ) → ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) )
49	46 47 48	syl2an	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) )
50	26 3	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ∈ ( Base ‘ 𝑅 ) )
51	37 43 49 50	syl3anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ∈ ( Base ‘ 𝑅 ) )
52	51	fmpttd	⊢ ( 𝜑 → ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) : ( 0 ... ( 𝐼 + 𝐽 ) ) ⟶ ( Base ‘ 𝑅 ) )
53		eldifsn	⊢ ( 𝑦 ∈ ( ( 0 ... ( 𝐼 + 𝐽 ) ) ∖ { 𝐼 } ) ↔ ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ∧ 𝑦 ≠ 𝐼 ) )
54	41	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → 𝑦 ∈ ℕ₀ )
55	54	nn0red	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → 𝑦 ∈ ℝ )
56	31	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → 𝐼 ∈ ℝ )
57	55 56	lttri2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( 𝑦 ≠ 𝐼 ↔ ( 𝑦 < 𝐼 ∨ 𝐼 < 𝑦 ) ) )
58	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝑦 < 𝐼 ) → 𝐺 ∈ 𝐵 )
59	47	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( ( 𝐼 + 𝐽 ) − 𝑦 ) ∈ ℕ₀ )
60	59	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 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	⊢ ( ( 𝐺 ∈ 𝐵 ∧ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ∈ ℕ₀ ∧ ( 𝐷 ‘ 𝐺 ) < ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) → ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) = ( 0_g ‘ 𝑅 ) )
80	58 60 78 79	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝑦 < 𝐼 ) → ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) = ( 0_g ‘ 𝑅 ) )
81	80	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝑦 < 𝐼 ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( 0_g ‘ 𝑅 ) ) )
82	26 3 27	ringrz	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( 0_g ‘ 𝑅 ) ) = ( 0_g ‘ 𝑅 ) )
83	37 43 82	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( 0_g ‘ 𝑅 ) ) = ( 0_g ‘ 𝑅 ) )
84	83	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝑦 < 𝐼 ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( 0_g ‘ 𝑅 ) ) = ( 0_g ‘ 𝑅 ) )
85	81 84	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝑦 < 𝐼 ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( 0_g ‘ 𝑅 ) )
86	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝐼 < 𝑦 ) → 𝐹 ∈ 𝐵 )
87	54	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 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	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝑦 ∈ ℕ₀ ∧ ( 𝐷 ‘ 𝐹 ) < 𝑦 ) → ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) = ( 0_g ‘ 𝑅 ) )
99	86 87 97 98	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝐼 < 𝑦 ) → ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) = ( 0_g ‘ 𝑅 ) )
100	99	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝐼 < 𝑦 ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( ( 0_g ‘ 𝑅 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) )
101	26 3 27	ringlz	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 0_g ‘ 𝑅 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( 0_g ‘ 𝑅 ) )
102	37 49 101	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( ( 0_g ‘ 𝑅 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( 0_g ‘ 𝑅 ) )
103	102	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝐼 < 𝑦 ) → ( ( 0_g ‘ 𝑅 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( 0_g ‘ 𝑅 ) )
104	100 103	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ 𝐼 < 𝑦 ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( 0_g ‘ 𝑅 ) )
105	85 104	jaodan	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) ∧ ( 𝑦 < 𝐼 ∨ 𝐼 < 𝑦 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( 0_g ‘ 𝑅 ) )
106	105	ex	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( ( 𝑦 < 𝐼 ∨ 𝐼 < 𝑦 ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( 0_g ‘ 𝑅 ) ) )
107	57 106	sylbid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ) → ( 𝑦 ≠ 𝐼 → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( 0_g ‘ 𝑅 ) ) )
108	107	impr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ∧ 𝑦 ≠ 𝐼 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( 0_g ‘ 𝑅 ) )
109	53 108	sylan2b	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 0 ... ( 𝐼 + 𝐽 ) ) ∖ { 𝐼 } ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( 0_g ‘ 𝑅 ) )
110	109 30	suppss2	⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) supp ( 0_g ‘ 𝑅 ) ) ⊆ { 𝐼 } )
111	26 27 29 30 36 52 110	gsumpt	⊢ ( 𝜑 → ( 𝑅 Σ_g ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) ) = ( ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) ‘ 𝐼 ) )
112		fveq2	⊢ ( 𝑦 = 𝐼 → ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) = ( ( coe₁ ‘ 𝐹 ) ‘ 𝐼 ) )
113		oveq2	⊢ ( 𝑦 = 𝐼 → ( ( 𝐼 + 𝐽 ) − 𝑦 ) = ( ( 𝐼 + 𝐽 ) − 𝐼 ) )
114	113	fveq2d	⊢ ( 𝑦 = 𝐼 → ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) = ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝐼 ) ) )
115	112 114	oveq12d	⊢ ( 𝑦 = 𝐼 → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) = ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝐼 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝐼 ) ) ) )
116		eqid	⊢ ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) = ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) )
117		ovex	⊢ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝐼 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝐼 ) ) ) ∈ V
118	115 116 117	fvmpt	⊢ ( 𝐼 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) → ( ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) ‘ 𝐼 ) = ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝐼 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝐼 ) ) ) )
119	36 118	syl	⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) ‘ 𝐼 ) = ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝐼 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝐼 ) ) ) )
120	8	nn0cnd	⊢ ( 𝜑 → 𝐼 ∈ ℂ )
121	11	nn0cnd	⊢ ( 𝜑 → 𝐽 ∈ ℂ )
122	120 121	pncan2d	⊢ ( 𝜑 → ( ( 𝐼 + 𝐽 ) − 𝐼 ) = 𝐽 )
123	122	fveq2d	⊢ ( 𝜑 → ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝐼 ) ) = ( ( coe₁ ‘ 𝐺 ) ‘ 𝐽 ) )
124	123	oveq2d	⊢ ( 𝜑 → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝐼 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝐼 ) ) ) = ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝐼 ) · ( ( coe₁ ‘ 𝐺 ) ‘ 𝐽 ) ) )
125	111 119 124	3eqtrd	⊢ ( 𝜑 → ( 𝑅 Σ_g ( 𝑦 ∈ ( 0 ... ( 𝐼 + 𝐽 ) ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑦 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( ( 𝐼 + 𝐽 ) − 𝑦 ) ) ) ) ) = ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝐼 ) · ( ( coe₁ ‘ 𝐺 ) ‘ 𝐽 ) ) )
126	15 25 125	3eqtrd	⊢ ( 𝜑 → ( ( coe₁ ‘ ( 𝐹 ∙ 𝐺 ) ) ‘ ( 𝐼 + 𝐽 ) ) = ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝐼 ) · ( ( coe₁ ‘ 𝐺 ) ‘ 𝐽 ) ) )

Metamath Proof Explorer

Theorem coe1mul3

Proof