ply1mulgsum

Description: The product of two polynomials expressed as group sum of scaled monomials. (Contributed by AV, 20-Oct-2019)

	Ref	Expression
Hypotheses	ply1mulgsum.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
	ply1mulgsum.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	ply1mulgsum.a	⊢ 𝐴 = ( coe₁ ‘ 𝐾 )
	ply1mulgsum.c	⊢ 𝐶 = ( coe₁ ‘ 𝐿 )
	ply1mulgsum.x	⊢ 𝑋 = ( var₁ ‘ 𝑅 )
	ply1mulgsum.pm	⊢ × = ( ._r ‘ 𝑃 )
	ply1mulgsum.sm	⊢ · = ( ·_𝑠 ‘ 𝑃 )
	ply1mulgsum.rm	⊢ ∗ = ( ._r ‘ 𝑅 )
	ply1mulgsum.m	⊢ 𝑀 = ( mulGrp ‘ 𝑃 )
	ply1mulgsum.e	⊢ ↑ = ( ._g ‘ 𝑀 )
Assertion	ply1mulgsum	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( 𝐾 × 𝐿 ) = ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ply1mulgsum.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
2		ply1mulgsum.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		ply1mulgsum.a	⊢ 𝐴 = ( coe₁ ‘ 𝐾 )
4		ply1mulgsum.c	⊢ 𝐶 = ( coe₁ ‘ 𝐿 )
5		ply1mulgsum.x	⊢ 𝑋 = ( var₁ ‘ 𝑅 )
6		ply1mulgsum.pm	⊢ × = ( ._r ‘ 𝑃 )
7		ply1mulgsum.sm	⊢ · = ( ·_𝑠 ‘ 𝑃 )
8		ply1mulgsum.rm	⊢ ∗ = ( ._r ‘ 𝑅 )
9		ply1mulgsum.m	⊢ 𝑀 = ( mulGrp ‘ 𝑃 )
10		ply1mulgsum.e	⊢ ↑ = ( ._g ‘ 𝑀 )
11	1 6 8 2	coe1mul	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( coe₁ ‘ ( 𝐾 × 𝐿 ) ) = ( 𝑚 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑖 ∈ ( 0 ... 𝑚 ) ↦ ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑖 ) ∗ ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑚 − 𝑖 ) ) ) ) ) ) )
12	11	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) → ( coe₁ ‘ ( 𝐾 × 𝐿 ) ) = ( 𝑚 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑖 ∈ ( 0 ... 𝑚 ) ↦ ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑖 ) ∗ ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑚 − 𝑖 ) ) ) ) ) ) )
13	12	fveq1d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) → ( ( coe₁ ‘ ( 𝐾 × 𝐿 ) ) ‘ 𝑛 ) = ( ( 𝑚 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑖 ∈ ( 0 ... 𝑚 ) ↦ ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑖 ) ∗ ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑚 − 𝑖 ) ) ) ) ) ) ‘ 𝑛 ) )
14		eqidd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) → ( 𝑚 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑖 ∈ ( 0 ... 𝑚 ) ↦ ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑖 ) ∗ ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑚 − 𝑖 ) ) ) ) ) ) = ( 𝑚 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑖 ∈ ( 0 ... 𝑚 ) ↦ ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑖 ) ∗ ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑚 − 𝑖 ) ) ) ) ) ) )
15		oveq2	⊢ ( 𝑚 = 𝑛 → ( 0 ... 𝑚 ) = ( 0 ... 𝑛 ) )
16		fvoveq1	⊢ ( 𝑚 = 𝑛 → ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑚 − 𝑖 ) ) = ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑛 − 𝑖 ) ) )
17	16	oveq2d	⊢ ( 𝑚 = 𝑛 → ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑖 ) ∗ ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑚 − 𝑖 ) ) ) = ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑖 ) ∗ ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑛 − 𝑖 ) ) ) )
18	15 17	mpteq12dv	⊢ ( 𝑚 = 𝑛 → ( 𝑖 ∈ ( 0 ... 𝑚 ) ↦ ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑖 ) ∗ ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑚 − 𝑖 ) ) ) ) = ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑖 ) ∗ ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑛 − 𝑖 ) ) ) ) )
19	18	oveq2d	⊢ ( 𝑚 = 𝑛 → ( 𝑅 Σ_g ( 𝑖 ∈ ( 0 ... 𝑚 ) ↦ ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑖 ) ∗ ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑚 − 𝑖 ) ) ) ) ) = ( 𝑅 Σ_g ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑖 ) ∗ ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑛 − 𝑖 ) ) ) ) ) )
20	19	adantl	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) ∧ 𝑚 = 𝑛 ) → ( 𝑅 Σ_g ( 𝑖 ∈ ( 0 ... 𝑚 ) ↦ ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑖 ) ∗ ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑚 − 𝑖 ) ) ) ) ) = ( 𝑅 Σ_g ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑖 ) ∗ ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑛 − 𝑖 ) ) ) ) ) )
21		simpr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) → 𝑛 ∈ ℕ₀ )
22		ovexd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) → ( 𝑅 Σ_g ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑖 ) ∗ ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑛 − 𝑖 ) ) ) ) ) ∈ V )
23	14 20 21 22	fvmptd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) → ( ( 𝑚 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑖 ∈ ( 0 ... 𝑚 ) ↦ ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑖 ) ∗ ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑚 − 𝑖 ) ) ) ) ) ) ‘ 𝑛 ) = ( 𝑅 Σ_g ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑖 ) ∗ ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑛 − 𝑖 ) ) ) ) ) )
24	9	fveq2i	⊢ ( ._g ‘ 𝑀 ) = ( ._g ‘ ( mulGrp ‘ 𝑃 ) )
25	10 24	eqtri	⊢ ↑ = ( ._g ‘ ( mulGrp ‘ 𝑃 ) )
26		simp1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → 𝑅 ∈ Ring )
27	26	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) → 𝑅 ∈ Ring )
28		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
29		eqid	⊢ ( 0_g ‘ 𝑅 ) = ( 0_g ‘ 𝑅 )
30		ringcmn	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
31	30	3ad2ant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → 𝑅 ∈ CMnd )
32	31	ad2antrr	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) → 𝑅 ∈ CMnd )
33		fzfid	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) → ( 0 ... 𝑘 ) ∈ Fin )
34		simpll1	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) → 𝑅 ∈ Ring )
35	34	adantr	⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → 𝑅 ∈ Ring )
36		simp2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → 𝐾 ∈ 𝐵 )
37	36	ad2antrr	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) → 𝐾 ∈ 𝐵 )
38		elfznn0	⊢ ( 𝑙 ∈ ( 0 ... 𝑘 ) → 𝑙 ∈ ℕ₀ )
39	3 2 1 28	coe1fvalcl	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑙 ∈ ℕ₀ ) → ( 𝐴 ‘ 𝑙 ) ∈ ( Base ‘ 𝑅 ) )
40	37 38 39	syl2an	⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → ( 𝐴 ‘ 𝑙 ) ∈ ( Base ‘ 𝑅 ) )
41		simp3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → 𝐿 ∈ 𝐵 )
42	41	ad2antrr	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) → 𝐿 ∈ 𝐵 )
43		fznn0sub	⊢ ( 𝑙 ∈ ( 0 ... 𝑘 ) → ( 𝑘 − 𝑙 ) ∈ ℕ₀ )
44	4 2 1 28	coe1fvalcl	⊢ ( ( 𝐿 ∈ 𝐵 ∧ ( 𝑘 − 𝑙 ) ∈ ℕ₀ ) → ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ∈ ( Base ‘ 𝑅 ) )
45	42 43 44	syl2an	⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ∈ ( Base ‘ 𝑅 ) )
46	28 8	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ‘ 𝑙 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ∈ ( Base ‘ 𝑅 ) )
47	35 40 45 46	syl3anc	⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ∈ ( Base ‘ 𝑅 ) )
48	47	ralrimiva	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) → ∀ 𝑙 ∈ ( 0 ... 𝑘 ) ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ∈ ( Base ‘ 𝑅 ) )
49	28 32 33 48	gsummptcl	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) ∧ 𝑘 ∈ ℕ₀ ) → ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
50	49	ralrimiva	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) → ∀ 𝑘 ∈ ℕ₀ ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
51	1 2 3 4 5 6 7 8 9 10	ply1mulgsumlem3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) ) finSupp ( 0_g ‘ 𝑅 ) )
52	51	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) → ( 𝑘 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) ) finSupp ( 0_g ‘ 𝑅 ) )
53	1 2 5 25 27 28 7 29 50 52 21	gsummoncoe1	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝑛 ) = ⦋ 𝑛 / 𝑘 ⦌ ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) )
54		vex	⊢ 𝑛 ∈ V
55		csbov2g	⊢ ( 𝑛 ∈ V → ⦋ 𝑛 / 𝑘 ⦌ ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) = ( 𝑅 Σ_g ⦋ 𝑛 / 𝑘 ⦌ ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) )
56		id	⊢ ( 𝑛 ∈ V → 𝑛 ∈ V )
57		oveq2	⊢ ( 𝑘 = 𝑛 → ( 0 ... 𝑘 ) = ( 0 ... 𝑛 ) )
58		fvoveq1	⊢ ( 𝑘 = 𝑛 → ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) = ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) )
59	58	oveq2d	⊢ ( 𝑘 = 𝑛 → ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) = ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) )
60	57 59	mpteq12dv	⊢ ( 𝑘 = 𝑛 → ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) = ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) )
61	60	adantl	⊢ ( ( 𝑛 ∈ V ∧ 𝑘 = 𝑛 ) → ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) = ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) )
62	56 61	csbied	⊢ ( 𝑛 ∈ V → ⦋ 𝑛 / 𝑘 ⦌ ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) = ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) )
63	62	oveq2d	⊢ ( 𝑛 ∈ V → ( 𝑅 Σ_g ⦋ 𝑛 / 𝑘 ⦌ ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) = ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) )
64	55 63	eqtrd	⊢ ( 𝑛 ∈ V → ⦋ 𝑛 / 𝑘 ⦌ ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) = ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) )
65	54 64	mp1i	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) → ⦋ 𝑛 / 𝑘 ⦌ ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) = ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) )
66		fveq2	⊢ ( 𝑙 = 𝑖 → ( 𝐴 ‘ 𝑙 ) = ( 𝐴 ‘ 𝑖 ) )
67	3	fveq1i	⊢ ( 𝐴 ‘ 𝑖 ) = ( ( coe₁ ‘ 𝐾 ) ‘ 𝑖 )
68	66 67	eqtrdi	⊢ ( 𝑙 = 𝑖 → ( 𝐴 ‘ 𝑙 ) = ( ( coe₁ ‘ 𝐾 ) ‘ 𝑖 ) )
69		oveq2	⊢ ( 𝑙 = 𝑖 → ( 𝑛 − 𝑙 ) = ( 𝑛 − 𝑖 ) )
70	69	fveq2d	⊢ ( 𝑙 = 𝑖 → ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) = ( 𝐶 ‘ ( 𝑛 − 𝑖 ) ) )
71	4	fveq1i	⊢ ( 𝐶 ‘ ( 𝑛 − 𝑖 ) ) = ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑛 − 𝑖 ) )
72	70 71	eqtrdi	⊢ ( 𝑙 = 𝑖 → ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) = ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑛 − 𝑖 ) ) )
73	68 72	oveq12d	⊢ ( 𝑙 = 𝑖 → ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) = ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑖 ) ∗ ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑛 − 𝑖 ) ) ) )
74	73	cbvmptv	⊢ ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) = ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑖 ) ∗ ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑛 − 𝑖 ) ) ) )
75	74	a1i	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) → ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) = ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑖 ) ∗ ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑛 − 𝑖 ) ) ) ) )
76	75	oveq2d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) → ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑛 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑛 − 𝑙 ) ) ) ) ) = ( 𝑅 Σ_g ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑖 ) ∗ ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑛 − 𝑖 ) ) ) ) ) )
77	53 65 76	3eqtrrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) → ( 𝑅 Σ_g ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe₁ ‘ 𝐾 ) ‘ 𝑖 ) ∗ ( ( coe₁ ‘ 𝐿 ) ‘ ( 𝑛 − 𝑖 ) ) ) ) ) = ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝑛 ) )
78	13 23 77	3eqtrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ₀ ) → ( ( coe₁ ‘ ( 𝐾 × 𝐿 ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝑛 ) )
79	78	ralrimiva	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ∀ 𝑛 ∈ ℕ₀ ( ( coe₁ ‘ ( 𝐾 × 𝐿 ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝑛 ) )
80	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
81	2 6	ringcl	⊢ ( ( 𝑃 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( 𝐾 × 𝐿 ) ∈ 𝐵 )
82	80 81	syl3an1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( 𝐾 × 𝐿 ) ∈ 𝐵 )
83		eqid	⊢ ( 0_g ‘ 𝑃 ) = ( 0_g ‘ 𝑃 )
84		ringcmn	⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ CMnd )
85	80 84	syl	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ CMnd )
86	85	3ad2ant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → 𝑃 ∈ CMnd )
87		nn0ex	⊢ ℕ₀ ∈ V
88	87	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ℕ₀ ∈ V )
89	1	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
90	89	3ad2ant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → 𝑃 ∈ LMod )
91	90	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → 𝑃 ∈ LMod )
92	31	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → 𝑅 ∈ CMnd )
93		fzfid	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → ( 0 ... 𝑘 ) ∈ Fin )
94		simpll1	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → 𝑅 ∈ Ring )
95	36	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → 𝐾 ∈ 𝐵 )
96	95 38 39	syl2an	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → ( 𝐴 ‘ 𝑙 ) ∈ ( Base ‘ 𝑅 ) )
97	41	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → 𝐿 ∈ 𝐵 )
98	97 43 44	syl2an	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ∈ ( Base ‘ 𝑅 ) )
99	94 96 98 46	syl3anc	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ∈ ( Base ‘ 𝑅 ) )
100	99	ralrimiva	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → ∀ 𝑙 ∈ ( 0 ... 𝑘 ) ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ∈ ( Base ‘ 𝑅 ) )
101	28 92 93 100	gsummptcl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
102	26	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → 𝑅 ∈ Ring )
103	1	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
104	102 103	syl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
105	104	fveq2d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
106	101 105	eleqtrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
107	9 2	mgpbas	⊢ 𝐵 = ( Base ‘ 𝑀 )
108	9	ringmgp	⊢ ( 𝑃 ∈ Ring → 𝑀 ∈ Mnd )
109	80 108	syl	⊢ ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
110	109	3ad2ant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → 𝑀 ∈ Mnd )
111	110	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → 𝑀 ∈ Mnd )
112		simpr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → 𝑘 ∈ ℕ₀ )
113	5 1 2	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )
114	113	3ad2ant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
115	114	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → 𝑋 ∈ 𝐵 )
116	107 10 111 112 115	mulgnn0cld	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 )
117		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
118		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
119	2 117 7 118	lmodvscl	⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 ) → ( ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
120	91 106 116 119	syl3anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → ( ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
121	120	fmpttd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) ) : ℕ₀ ⟶ 𝐵 )
122	1 2 3 4 5 6 7 8 9 10	ply1mulgsumlem4	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0_g ‘ 𝑃 ) )
123	2 83 86 88 121 122	gsumcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) ) ) ∈ 𝐵 )
124		eqid	⊢ ( coe₁ ‘ ( 𝐾 × 𝐿 ) ) = ( coe₁ ‘ ( 𝐾 × 𝐿 ) )
125		eqid	⊢ ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) ) ) ) = ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) ) ) )
126	1 2 124 125	ply1coe1eq	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐾 × 𝐿 ) ∈ 𝐵 ∧ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) ) ) ∈ 𝐵 ) → ( ∀ 𝑛 ∈ ℕ₀ ( ( coe₁ ‘ ( 𝐾 × 𝐿 ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝑛 ) ↔ ( 𝐾 × 𝐿 ) = ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
127	26 82 123 126	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( ∀ 𝑛 ∈ ℕ₀ ( ( coe₁ ‘ ( 𝐾 × 𝐿 ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝑛 ) ↔ ( 𝐾 × 𝐿 ) = ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
128	79 127	mpbid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐿 ∈ 𝐵 ) → ( 𝐾 × 𝐿 ) = ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝑅 Σ_g ( 𝑙 ∈ ( 0 ... 𝑘 ) ↦ ( ( 𝐴 ‘ 𝑙 ) ∗ ( 𝐶 ‘ ( 𝑘 − 𝑙 ) ) ) ) ) · ( 𝑘 ↑ 𝑋 ) ) ) ) )

Metamath Proof Explorer

Theorem ply1mulgsum

Proof