coe1mul2

Description: The coefficient vector of multiplication in the univariate power series ring. (Contributed by Stefan O'Rear, 25-Mar-2015)

	Ref	Expression
Hypotheses	coe1mul2.s	⊢ 𝑆 = ( PwSer₁ ‘ 𝑅 )
	coe1mul2.t	⊢ ∙ = ( ._r ‘ 𝑆 )
	coe1mul2.u	⊢ · = ( ._r ‘ 𝑅 )
	coe1mul2.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
Assertion	coe1mul2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe₁ ‘ ( 𝐹 ∙ 𝐺 ) ) = ( 𝑘 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		coe1mul2.s	⊢ 𝑆 = ( PwSer₁ ‘ 𝑅 )
2		coe1mul2.t	⊢ ∙ = ( ._r ‘ 𝑆 )
3		coe1mul2.u	⊢ · = ( ._r ‘ 𝑅 )
4		coe1mul2.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
5		fconst6g	⊢ ( 𝑘 ∈ ℕ₀ → ( 1_o × { 𝑘 } ) : 1_o ⟶ ℕ₀ )
6		nn0ex	⊢ ℕ₀ ∈ V
7		1on	⊢ 1_o ∈ On
8	7	elexi	⊢ 1_o ∈ V
9	6 8	elmap	⊢ ( ( 1_o × { 𝑘 } ) ∈ ( ℕ₀ ↑_m 1_o ) ↔ ( 1_o × { 𝑘 } ) : 1_o ⟶ ℕ₀ )
10	5 9	sylibr	⊢ ( 𝑘 ∈ ℕ₀ → ( 1_o × { 𝑘 } ) ∈ ( ℕ₀ ↑_m 1_o ) )
11	10	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → ( 1_o × { 𝑘 } ) ∈ ( ℕ₀ ↑_m 1_o ) )
12		eqidd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ₀ ↦ ( 1_o × { 𝑘 } ) ) = ( 𝑘 ∈ ℕ₀ ↦ ( 1_o × { 𝑘 } ) ) )
13		eqid	⊢ ( 1_o mPwSer 𝑅 ) = ( 1_o mPwSer 𝑅 )
14	1 4 13	psr1bas2	⊢ 𝐵 = ( Base ‘ ( 1_o mPwSer 𝑅 ) )
15	1 13 2	psr1mulr	⊢ ∙ = ( ._r ‘ ( 1_o mPwSer 𝑅 ) )
16		psr1baslem	⊢ ( ℕ₀ ↑_m 1_o ) = { 𝑎 ∈ ( ℕ₀ ↑_m 1_o ) ∣ ( ^◡ 𝑎 “ ℕ ) ∈ Fin }
17		simp2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐹 ∈ 𝐵 )
18		simp3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐺 ∈ 𝐵 )
19	13 14 3 15 16 17 18	psrmulfval	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 ∙ 𝐺 ) = ( 𝑏 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( 𝑅 Σ_g ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) · ( 𝐺 ‘ ( 𝑏 ∘_f − 𝑐 ) ) ) ) ) ) )
20		breq2	⊢ ( 𝑏 = ( 1_o × { 𝑘 } ) → ( 𝑑 ∘_r ≤ 𝑏 ↔ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) ) )
21	20	rabbidv	⊢ ( 𝑏 = ( 1_o × { 𝑘 } ) → { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ 𝑏 } = { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } )
22		fvoveq1	⊢ ( 𝑏 = ( 1_o × { 𝑘 } ) → ( 𝐺 ‘ ( 𝑏 ∘_f − 𝑐 ) ) = ( 𝐺 ‘ ( ( 1_o × { 𝑘 } ) ∘_f − 𝑐 ) ) )
23	22	oveq2d	⊢ ( 𝑏 = ( 1_o × { 𝑘 } ) → ( ( 𝐹 ‘ 𝑐 ) · ( 𝐺 ‘ ( 𝑏 ∘_f − 𝑐 ) ) ) = ( ( 𝐹 ‘ 𝑐 ) · ( 𝐺 ‘ ( ( 1_o × { 𝑘 } ) ∘_f − 𝑐 ) ) ) )
24	21 23	mpteq12dv	⊢ ( 𝑏 = ( 1_o × { 𝑘 } ) → ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) · ( 𝐺 ‘ ( 𝑏 ∘_f − 𝑐 ) ) ) ) = ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ↦ ( ( 𝐹 ‘ 𝑐 ) · ( 𝐺 ‘ ( ( 1_o × { 𝑘 } ) ∘_f − 𝑐 ) ) ) ) )
25	24	oveq2d	⊢ ( 𝑏 = ( 1_o × { 𝑘 } ) → ( 𝑅 Σ_g ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ 𝑏 } ↦ ( ( 𝐹 ‘ 𝑐 ) · ( 𝐺 ‘ ( 𝑏 ∘_f − 𝑐 ) ) ) ) ) = ( 𝑅 Σ_g ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ↦ ( ( 𝐹 ‘ 𝑐 ) · ( 𝐺 ‘ ( ( 1_o × { 𝑘 } ) ∘_f − 𝑐 ) ) ) ) ) )
26	11 12 19 25	fmptco	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( 𝐹 ∙ 𝐺 ) ∘ ( 𝑘 ∈ ℕ₀ ↦ ( 1_o × { 𝑘 } ) ) ) = ( 𝑘 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ↦ ( ( 𝐹 ‘ 𝑐 ) · ( 𝐺 ‘ ( ( 1_o × { 𝑘 } ) ∘_f − 𝑐 ) ) ) ) ) ) )
27	1	psr1ring	⊢ ( 𝑅 ∈ Ring → 𝑆 ∈ Ring )
28	4 2	ringcl	⊢ ( ( 𝑆 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 ∙ 𝐺 ) ∈ 𝐵 )
29	27 28	syl3an1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 ∙ 𝐺 ) ∈ 𝐵 )
30		eqid	⊢ ( coe₁ ‘ ( 𝐹 ∙ 𝐺 ) ) = ( coe₁ ‘ ( 𝐹 ∙ 𝐺 ) )
31		eqid	⊢ ( 𝑘 ∈ ℕ₀ ↦ ( 1_o × { 𝑘 } ) ) = ( 𝑘 ∈ ℕ₀ ↦ ( 1_o × { 𝑘 } ) )
32	30 4 1 31	coe1fval3	⊢ ( ( 𝐹 ∙ 𝐺 ) ∈ 𝐵 → ( coe₁ ‘ ( 𝐹 ∙ 𝐺 ) ) = ( ( 𝐹 ∙ 𝐺 ) ∘ ( 𝑘 ∈ ℕ₀ ↦ ( 1_o × { 𝑘 } ) ) ) )
33	29 32	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe₁ ‘ ( 𝐹 ∙ 𝐺 ) ) = ( ( 𝐹 ∙ 𝐺 ) ∘ ( 𝑘 ∈ ℕ₀ ↦ ( 1_o × { 𝑘 } ) ) ) )
34		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
35		eqid	⊢ ( 0_g ‘ 𝑅 ) = ( 0_g ‘ 𝑅 )
36		simpl1	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → 𝑅 ∈ Ring )
37		ringcmn	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
38	36 37	syl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → 𝑅 ∈ CMnd )
39		fzfi	⊢ ( 0 ... 𝑘 ) ∈ Fin
40	39	a1i	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → ( 0 ... 𝑘 ) ∈ Fin )
41		simpll1	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑥 ∈ ( 0 ... 𝑘 ) ) → 𝑅 ∈ Ring )
42		simpll2	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑥 ∈ ( 0 ... 𝑘 ) ) → 𝐹 ∈ 𝐵 )
43		eqid	⊢ ( coe₁ ‘ 𝐹 ) = ( coe₁ ‘ 𝐹 )
44	43 4 1 34	coe1f2	⊢ ( 𝐹 ∈ 𝐵 → ( coe₁ ‘ 𝐹 ) : ℕ₀ ⟶ ( Base ‘ 𝑅 ) )
45	42 44	syl	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑥 ∈ ( 0 ... 𝑘 ) ) → ( coe₁ ‘ 𝐹 ) : ℕ₀ ⟶ ( Base ‘ 𝑅 ) )
46		elfznn0	⊢ ( 𝑥 ∈ ( 0 ... 𝑘 ) → 𝑥 ∈ ℕ₀ )
47	46	adantl	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑥 ∈ ( 0 ... 𝑘 ) ) → 𝑥 ∈ ℕ₀ )
48	45 47	ffvelcdmd	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑥 ∈ ( 0 ... 𝑘 ) ) → ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
49		simpll3	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑥 ∈ ( 0 ... 𝑘 ) ) → 𝐺 ∈ 𝐵 )
50		eqid	⊢ ( coe₁ ‘ 𝐺 ) = ( coe₁ ‘ 𝐺 )
51	50 4 1 34	coe1f2	⊢ ( 𝐺 ∈ 𝐵 → ( coe₁ ‘ 𝐺 ) : ℕ₀ ⟶ ( Base ‘ 𝑅 ) )
52	49 51	syl	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑥 ∈ ( 0 ... 𝑘 ) ) → ( coe₁ ‘ 𝐺 ) : ℕ₀ ⟶ ( Base ‘ 𝑅 ) )
53		fznn0sub	⊢ ( 𝑥 ∈ ( 0 ... 𝑘 ) → ( 𝑘 − 𝑥 ) ∈ ℕ₀ )
54	53	adantl	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑥 ∈ ( 0 ... 𝑘 ) ) → ( 𝑘 − 𝑥 ) ∈ ℕ₀ )
55	52 54	ffvelcdmd	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑥 ∈ ( 0 ... 𝑘 ) ) → ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ∈ ( Base ‘ 𝑅 ) )
56	34 3	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ∈ ( Base ‘ 𝑅 ) )
57	41 48 55 56	syl3anc	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑥 ∈ ( 0 ... 𝑘 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ∈ ( Base ‘ 𝑅 ) )
58	57	fmpttd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) : ( 0 ... 𝑘 ) ⟶ ( Base ‘ 𝑅 ) )
59	39	elexi	⊢ ( 0 ... 𝑘 ) ∈ V
60	59	mptex	⊢ ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) ∈ V
61		funmpt	⊢ Fun ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) )
62		fvex	⊢ ( 0_g ‘ 𝑅 ) ∈ V
63	60 61 62	3pm3.2i	⊢ ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) ∈ V ∧ Fun ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) ∧ ( 0_g ‘ 𝑅 ) ∈ V )
64		suppssdm	⊢ ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) supp ( 0_g ‘ 𝑅 ) ) ⊆ dom ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) )
65		eqid	⊢ ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) )
66	65	dmmptss	⊢ dom ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) ⊆ ( 0 ... 𝑘 )
67	64 66	sstri	⊢ ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) supp ( 0_g ‘ 𝑅 ) ) ⊆ ( 0 ... 𝑘 )
68	39 67	pm3.2i	⊢ ( ( 0 ... 𝑘 ) ∈ Fin ∧ ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) supp ( 0_g ‘ 𝑅 ) ) ⊆ ( 0 ... 𝑘 ) )
69		suppssfifsupp	⊢ ( ( ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) ∈ V ∧ Fun ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) ∧ ( 0_g ‘ 𝑅 ) ∈ V ) ∧ ( ( 0 ... 𝑘 ) ∈ Fin ∧ ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) supp ( 0_g ‘ 𝑅 ) ) ⊆ ( 0 ... 𝑘 ) ) ) → ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) finSupp ( 0_g ‘ 𝑅 ) )
70	63 68 69	mp2an	⊢ ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) finSupp ( 0_g ‘ 𝑅 )
71	70	a1i	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) finSupp ( 0_g ‘ 𝑅 ) )
72		eqid	⊢ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } = { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) }
73	72	coe1mul2lem2	⊢ ( 𝑘 ∈ ℕ₀ → ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ↦ ( 𝑐 ‘ ∅ ) ) : { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } –1-1-onto→ ( 0 ... 𝑘 ) )
74	73	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ↦ ( 𝑐 ‘ ∅ ) ) : { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } –1-1-onto→ ( 0 ... 𝑘 ) )
75	34 35 38 40 58 71 74	gsumf1o	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → ( 𝑅 Σ_g ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) ) = ( 𝑅 Σ_g ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) ∘ ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ↦ ( 𝑐 ‘ ∅ ) ) ) ) )
76		breq1	⊢ ( 𝑑 = 𝑐 → ( 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) ↔ 𝑐 ∘_r ≤ ( 1_o × { 𝑘 } ) ) )
77	76	elrab	⊢ ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ↔ ( 𝑐 ∈ ( ℕ₀ ↑_m 1_o ) ∧ 𝑐 ∘_r ≤ ( 1_o × { 𝑘 } ) ) )
78	77	simprbi	⊢ ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } → 𝑐 ∘_r ≤ ( 1_o × { 𝑘 } ) )
79	78	adantl	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ) → 𝑐 ∘_r ≤ ( 1_o × { 𝑘 } ) )
80		simplr	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ) → 𝑘 ∈ ℕ₀ )
81		elrabi	⊢ ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } → 𝑐 ∈ ( ℕ₀ ↑_m 1_o ) )
82	81	adantl	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ) → 𝑐 ∈ ( ℕ₀ ↑_m 1_o ) )
83		coe1mul2lem1	⊢ ( ( 𝑘 ∈ ℕ₀ ∧ 𝑐 ∈ ( ℕ₀ ↑_m 1_o ) ) → ( 𝑐 ∘_r ≤ ( 1_o × { 𝑘 } ) ↔ ( 𝑐 ‘ ∅ ) ∈ ( 0 ... 𝑘 ) ) )
84	80 82 83	syl2anc	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ) → ( 𝑐 ∘_r ≤ ( 1_o × { 𝑘 } ) ↔ ( 𝑐 ‘ ∅ ) ∈ ( 0 ... 𝑘 ) ) )
85	79 84	mpbid	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ) → ( 𝑐 ‘ ∅ ) ∈ ( 0 ... 𝑘 ) )
86		eqidd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ↦ ( 𝑐 ‘ ∅ ) ) = ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ↦ ( 𝑐 ‘ ∅ ) ) )
87		eqidd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) )
88		fveq2	⊢ ( 𝑥 = ( 𝑐 ‘ ∅ ) → ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) = ( ( coe₁ ‘ 𝐹 ) ‘ ( 𝑐 ‘ ∅ ) ) )
89		oveq2	⊢ ( 𝑥 = ( 𝑐 ‘ ∅ ) → ( 𝑘 − 𝑥 ) = ( 𝑘 − ( 𝑐 ‘ ∅ ) ) )
90	89	fveq2d	⊢ ( 𝑥 = ( 𝑐 ‘ ∅ ) → ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) = ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − ( 𝑐 ‘ ∅ ) ) ) )
91	88 90	oveq12d	⊢ ( 𝑥 = ( 𝑐 ‘ ∅ ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) = ( ( ( coe₁ ‘ 𝐹 ) ‘ ( 𝑐 ‘ ∅ ) ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − ( 𝑐 ‘ ∅ ) ) ) ) )
92	85 86 87 91	fmptco	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) ∘ ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ↦ ( 𝑐 ‘ ∅ ) ) ) = ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ ( 𝑐 ‘ ∅ ) ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − ( 𝑐 ‘ ∅ ) ) ) ) ) )
93		simpll2	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ) → 𝐹 ∈ 𝐵 )
94	43	fvcoe1	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝑐 ∈ ( ℕ₀ ↑_m 1_o ) ) → ( 𝐹 ‘ 𝑐 ) = ( ( coe₁ ‘ 𝐹 ) ‘ ( 𝑐 ‘ ∅ ) ) )
95	93 82 94	syl2anc	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ) → ( 𝐹 ‘ 𝑐 ) = ( ( coe₁ ‘ 𝐹 ) ‘ ( 𝑐 ‘ ∅ ) ) )
96		df1o2	⊢ 1_o = { ∅ }
97		0ex	⊢ ∅ ∈ V
98	96 6 97	mapsnconst	⊢ ( 𝑐 ∈ ( ℕ₀ ↑_m 1_o ) → 𝑐 = ( 1_o × { ( 𝑐 ‘ ∅ ) } ) )
99	82 98	syl	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ) → 𝑐 = ( 1_o × { ( 𝑐 ‘ ∅ ) } ) )
100	99	oveq2d	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ) → ( ( 1_o × { 𝑘 } ) ∘_f − 𝑐 ) = ( ( 1_o × { 𝑘 } ) ∘_f − ( 1_o × { ( 𝑐 ‘ ∅ ) } ) ) )
101	7	a1i	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ) → 1_o ∈ On )
102		vex	⊢ 𝑘 ∈ V
103	102	a1i	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ) → 𝑘 ∈ V )
104		fvexd	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ) → ( 𝑐 ‘ ∅ ) ∈ V )
105	101 103 104	ofc12	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ) → ( ( 1_o × { 𝑘 } ) ∘_f − ( 1_o × { ( 𝑐 ‘ ∅ ) } ) ) = ( 1_o × { ( 𝑘 − ( 𝑐 ‘ ∅ ) ) } ) )
106	100 105	eqtrd	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ) → ( ( 1_o × { 𝑘 } ) ∘_f − 𝑐 ) = ( 1_o × { ( 𝑘 − ( 𝑐 ‘ ∅ ) ) } ) )
107	106	fveq2d	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ) → ( 𝐺 ‘ ( ( 1_o × { 𝑘 } ) ∘_f − 𝑐 ) ) = ( 𝐺 ‘ ( 1_o × { ( 𝑘 − ( 𝑐 ‘ ∅ ) ) } ) ) )
108		simpll3	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ) → 𝐺 ∈ 𝐵 )
109		fznn0sub	⊢ ( ( 𝑐 ‘ ∅ ) ∈ ( 0 ... 𝑘 ) → ( 𝑘 − ( 𝑐 ‘ ∅ ) ) ∈ ℕ₀ )
110	85 109	syl	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ) → ( 𝑘 − ( 𝑐 ‘ ∅ ) ) ∈ ℕ₀ )
111	50	coe1fv	⊢ ( ( 𝐺 ∈ 𝐵 ∧ ( 𝑘 − ( 𝑐 ‘ ∅ ) ) ∈ ℕ₀ ) → ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − ( 𝑐 ‘ ∅ ) ) ) = ( 𝐺 ‘ ( 1_o × { ( 𝑘 − ( 𝑐 ‘ ∅ ) ) } ) ) )
112	108 110 111	syl2anc	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ) → ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − ( 𝑐 ‘ ∅ ) ) ) = ( 𝐺 ‘ ( 1_o × { ( 𝑘 − ( 𝑐 ‘ ∅ ) ) } ) ) )
113	107 112	eqtr4d	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ) → ( 𝐺 ‘ ( ( 1_o × { 𝑘 } ) ∘_f − 𝑐 ) ) = ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − ( 𝑐 ‘ ∅ ) ) ) )
114	95 113	oveq12d	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ) → ( ( 𝐹 ‘ 𝑐 ) · ( 𝐺 ‘ ( ( 1_o × { 𝑘 } ) ∘_f − 𝑐 ) ) ) = ( ( ( coe₁ ‘ 𝐹 ) ‘ ( 𝑐 ‘ ∅ ) ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − ( 𝑐 ‘ ∅ ) ) ) ) )
115	114	mpteq2dva	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ↦ ( ( 𝐹 ‘ 𝑐 ) · ( 𝐺 ‘ ( ( 1_o × { 𝑘 } ) ∘_f − 𝑐 ) ) ) ) = ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ ( 𝑐 ‘ ∅ ) ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − ( 𝑐 ‘ ∅ ) ) ) ) ) )
116	92 115	eqtr4d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) ∘ ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ↦ ( 𝑐 ‘ ∅ ) ) ) = ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ↦ ( ( 𝐹 ‘ 𝑐 ) · ( 𝐺 ‘ ( ( 1_o × { 𝑘 } ) ∘_f − 𝑐 ) ) ) ) )
117	116	oveq2d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → ( 𝑅 Σ_g ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) ∘ ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ↦ ( 𝑐 ‘ ∅ ) ) ) ) = ( 𝑅 Σ_g ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ↦ ( ( 𝐹 ‘ 𝑐 ) · ( 𝐺 ‘ ( ( 1_o × { 𝑘 } ) ∘_f − 𝑐 ) ) ) ) ) )
118	75 117	eqtrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ₀ ) → ( 𝑅 Σ_g ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) ) = ( 𝑅 Σ_g ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ↦ ( ( 𝐹 ‘ 𝑐 ) · ( 𝐺 ‘ ( ( 1_o × { 𝑘 } ) ∘_f − 𝑐 ) ) ) ) ) )
119	118	mpteq2dva	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) ) ) = ( 𝑘 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑐 ∈ { 𝑑 ∈ ( ℕ₀ ↑_m 1_o ) ∣ 𝑑 ∘_r ≤ ( 1_o × { 𝑘 } ) } ↦ ( ( 𝐹 ‘ 𝑐 ) · ( 𝐺 ‘ ( ( 1_o × { 𝑘 } ) ∘_f − 𝑐 ) ) ) ) ) ) )
120	26 33 119	3eqtr4d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe₁ ‘ ( 𝐹 ∙ 𝐺 ) ) = ( 𝑘 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) ) ) )

Metamath Proof Explorer

Theorem coe1mul2

Proof