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	$⊢ S = {PwSer}_{1} (R)$
	coe1mul2.t	$⊢ \underset{˙}{∙} = \cdot_{S}$
	coe1mul2.u	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	coe1mul2.b	$⊢ B = {Base}_{S}$
Assertion	coe1mul2	$⊢ (R \in Ring \land F \in B \land G \in B) \to {coe}_{1} (F \underset{˙}{∙} G) = (k \in ℕ_{0} ⟼ {\sum_{R}}_{x = 0}^{k} ({coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)))$

Proof

Step	Hyp	Ref	Expression
1		coe1mul2.s	$⊢ S = {PwSer}_{1} (R)$
2		coe1mul2.t	$⊢ \underset{˙}{∙} = \cdot_{S}$
3		coe1mul2.u	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		coe1mul2.b	$⊢ B = {Base}_{S}$
5		fconst6g	$⊢ k \in ℕ_{0} \to (1_{𝑜} \times \{k\}) : 1_{𝑜} ⟶ ℕ_{0}$
6		nn0ex	$⊢ ℕ_{0} \in V$
7		1on	$⊢ 1_{𝑜} \in On$
8	7	elexi	$⊢ 1_{𝑜} \in V$
9	6 8	elmap	$⊢ 1_{𝑜} \times \{k\} \in ({ℕ_{0}}^{1_{𝑜}}) \leftrightarrow (1_{𝑜} \times \{k\}) : 1_{𝑜} ⟶ ℕ_{0}$
10	5 9	sylibr	$⊢ k \in ℕ_{0} \to 1_{𝑜} \times \{k\} \in ({ℕ_{0}}^{1_{𝑜}})$
11	10	adantl	$⊢ ((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \to 1_{𝑜} \times \{k\} \in ({ℕ_{0}}^{1_{𝑜}})$
12		eqidd	$⊢ (R \in Ring \land F \in B \land G \in B) \to (k \in ℕ_{0} ⟼ 1_{𝑜} \times \{k\}) = (k \in ℕ_{0} ⟼ 1_{𝑜} \times \{k\})$
13		eqid	$⊢ 1_{𝑜} mPwSer R = 1_{𝑜} mPwSer R$
14	1 4 13	psr1bas2	$⊢ B = {Base}_{(1_{𝑜} mPwSer R)}$
15	1 13 2	psr1mulr	$⊢ \underset{˙}{∙} = \cdot_{(1_{𝑜} mPwSer R)}$
16		psr1baslem	$⊢ {ℕ_{0}}^{1_{𝑜}} = \{a \in ({ℕ_{0}}^{1_{𝑜}}) \| a^{-1} [ℕ] \in Fin\}$
17		simp2	$⊢ (R \in Ring \land F \in B \land G \in B) \to F \in B$
18		simp3	$⊢ (R \in Ring \land F \in B \land G \in B) \to G \in B$
19	13 14 3 15 16 17 18	psrmulfval	$⊢ (R \in Ring \land F \in B \land G \in B) \to F \underset{˙}{∙} G = (b \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ \underset{c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} b\}}{\sum_{R}} (F (c) \underset{˙}{\cdot} G (b -_{f} c)))$
20		breq2	$⊢ b = 1_{𝑜} \times \{k\} \to (d \leq_{f} b \leftrightarrow d \leq_{f} (1_{𝑜} \times \{k\}))$
21	20	rabbidv	$⊢ b = 1_{𝑜} \times \{k\} \to \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} b\} = \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}$
22		fvoveq1	$⊢ b = 1_{𝑜} \times \{k\} \to G (b -_{f} c) = G ((1_{𝑜} \times \{k\}) -_{f} c)$
23	22	oveq2d	$⊢ b = 1_{𝑜} \times \{k\} \to F (c) \underset{˙}{\cdot} G (b -_{f} c) = F (c) \underset{˙}{\cdot} G ((1_{𝑜} \times \{k\}) -_{f} c)$
24	21 23	mpteq12dv	$⊢ b = 1_{𝑜} \times \{k\} \to (c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} b\} ⟼ F (c) \underset{˙}{\cdot} G (b -_{f} c)) = (c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\} ⟼ F (c) \underset{˙}{\cdot} G ((1_{𝑜} \times \{k\}) -_{f} c))$
25	24	oveq2d	$⊢ b = 1_{𝑜} \times \{k\} \to \underset{c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} b\}}{\sum_{R}} (F (c) \underset{˙}{\cdot} G (b -_{f} c)) = \underset{c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}}{\sum_{R}} (F (c) \underset{˙}{\cdot} G ((1_{𝑜} \times \{k\}) -_{f} c))$
26	11 12 19 25	fmptco	$⊢ (R \in Ring \land F \in B \land G \in B) \to (F \underset{˙}{∙} G) \circ (k \in ℕ_{0} ⟼ 1_{𝑜} \times \{k\}) = (k \in ℕ_{0} ⟼ \underset{c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}}{\sum_{R}} (F (c) \underset{˙}{\cdot} G ((1_{𝑜} \times \{k\}) -_{f} c)))$
27	1	psr1ring	$⊢ R \in Ring \to S \in Ring$
28	4 2	ringcl	$⊢ (S \in Ring \land F \in B \land G \in B) \to F \underset{˙}{∙} G \in B$
29	27 28	syl3an1	$⊢ (R \in Ring \land F \in B \land G \in B) \to F \underset{˙}{∙} G \in B$
30		eqid	$⊢ {coe}_{1} (F \underset{˙}{∙} G) = {coe}_{1} (F \underset{˙}{∙} G)$
31		eqid	$⊢ (k \in ℕ_{0} ⟼ 1_{𝑜} \times \{k\}) = (k \in ℕ_{0} ⟼ 1_{𝑜} \times \{k\})$
32	30 4 1 31	coe1fval3	$⊢ F \underset{˙}{∙} G \in B \to {coe}_{1} (F \underset{˙}{∙} G) = (F \underset{˙}{∙} G) \circ (k \in ℕ_{0} ⟼ 1_{𝑜} \times \{k\})$
33	29 32	syl	$⊢ (R \in Ring \land F \in B \land G \in B) \to {coe}_{1} (F \underset{˙}{∙} G) = (F \underset{˙}{∙} G) \circ (k \in ℕ_{0} ⟼ 1_{𝑜} \times \{k\})$
34		eqid	$⊢ {Base}_{R} = {Base}_{R}$
35		eqid	$⊢ 0_{R} = 0_{R}$
36		simpl1	$⊢ ((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \to R \in Ring$
37		ringcmn	$⊢ R \in Ring \to R \in CMnd$
38	36 37	syl	$⊢ ((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \to R \in CMnd$
39		fzfi	$⊢ (0 \dots k) \in Fin$
40	39	a1i	$⊢ ((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \to (0 \dots k) \in Fin$
41		simpll1	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land x \in (0 \dots k)) \to R \in Ring$
42		simpll2	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land x \in (0 \dots k)) \to F \in B$
43		eqid	$⊢ {coe}_{1} (F) = {coe}_{1} (F)$
44	43 4 1 34	coe1f2	$⊢ F \in B \to {coe}_{1} (F) : ℕ_{0} ⟶ {Base}_{R}$
45	42 44	syl	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land x \in (0 \dots k)) \to {coe}_{1} (F) : ℕ_{0} ⟶ {Base}_{R}$
46		elfznn0	$⊢ x \in (0 \dots k) \to x \in ℕ_{0}$
47	46	adantl	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land x \in (0 \dots k)) \to x \in ℕ_{0}$
48	45 47	ffvelrnd	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land x \in (0 \dots k)) \to {coe}_{1} (F) (x) \in {Base}_{R}$
49		simpll3	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land x \in (0 \dots k)) \to G \in B$
50		eqid	$⊢ {coe}_{1} (G) = {coe}_{1} (G)$
51	50 4 1 34	coe1f2	$⊢ G \in B \to {coe}_{1} (G) : ℕ_{0} ⟶ {Base}_{R}$
52	49 51	syl	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land x \in (0 \dots k)) \to {coe}_{1} (G) : ℕ_{0} ⟶ {Base}_{R}$
53		fznn0sub	$⊢ x \in (0 \dots k) \to k - x \in ℕ_{0}$
54	53	adantl	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land x \in (0 \dots k)) \to k - x \in ℕ_{0}$
55	52 54	ffvelrnd	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land x \in (0 \dots k)) \to {coe}_{1} (G) (k - x) \in {Base}_{R}$
56	34 3	ringcl	$⊢ (R \in Ring \land {coe}_{1} (F) (x) \in {Base}_{R} \land {coe}_{1} (G) (k - x) \in {Base}_{R}) \to {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x) \in {Base}_{R}$
57	41 48 55 56	syl3anc	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land x \in (0 \dots k)) \to {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x) \in {Base}_{R}$
58	57	fmpttd	$⊢ ((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \to (x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)) : (0 \dots k) ⟶ {Base}_{R}$
59	39	elexi	$⊢ (0 \dots k) \in V$
60	59	mptex	$⊢ (x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)) \in V$
61		funmpt	$⊢ Fun (x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x))$
62		fvex	$⊢ 0_{R} \in V$
63	60 61 62	3pm3.2i	$⊢ ((x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)) \in V \land Fun (x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)) \land 0_{R} \in V)$
64		suppssdm	$⊢ (x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)) supp 0_{R} \subseteq dom (x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x))$
65		eqid	$⊢ (x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)) = (x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x))$
66	65	dmmptss	$⊢ dom (x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)) \subseteq (0 \dots k)$
67	64 66	sstri	$⊢ (x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)) supp 0_{R} \subseteq (0 \dots k)$
68	39 67	pm3.2i	$⊢ ((0 \dots k) \in Fin \land (x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)) supp 0_{R} \subseteq (0 \dots k))$
69		suppssfifsupp	$⊢ (((x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)) \in V \land Fun (x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)) \land 0_{R} \in V) \land ((0 \dots k) \in Fin \land (x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)) supp 0_{R} \subseteq (0 \dots k))) \to {finSupp}_{0_{R}} ((x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)))$
70	63 68 69	mp2an	$⊢ {finSupp}_{0_{R}} ((x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)))$
71	70	a1i	$⊢ ((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \to {finSupp}_{0_{R}} ((x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)))$
72		eqid	$⊢ \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\} = \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}$
73	72	coe1mul2lem2	$⊢ k \in ℕ_{0} \to (c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\} ⟼ c (\emptyset)) : \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\} \underset{1-1 onto}{⟶} (0 \dots k)$
74	73	adantl	$⊢ ((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \to (c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\} ⟼ c (\emptyset)) : \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\} \underset{1-1 onto}{⟶} (0 \dots k)$
75	34 35 38 40 58 71 74	gsumf1o	$⊢ ((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \to {\sum_{R}}_{x = 0}^{k} ({coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)) = \sum_{R} ((x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)) \circ (c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\} ⟼ c (\emptyset)))$
76		breq1	$⊢ d = c \to (d \leq_{f} (1_{𝑜} \times \{k\}) \leftrightarrow c \leq_{f} (1_{𝑜} \times \{k\}))$
77	76	elrab	$⊢ c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\} \leftrightarrow (c \in ({ℕ_{0}}^{1_{𝑜}}) \land c \leq_{f} (1_{𝑜} \times \{k\}))$
78	77	simprbi	$⊢ c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\} \to c \leq_{f} (1_{𝑜} \times \{k\})$
79	78	adantl	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}) \to c \leq_{f} (1_{𝑜} \times \{k\})$
80		simplr	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}) \to k \in ℕ_{0}$
81		elrabi	$⊢ c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\} \to c \in ({ℕ_{0}}^{1_{𝑜}})$
82	81	adantl	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}) \to c \in ({ℕ_{0}}^{1_{𝑜}})$
83		coe1mul2lem1	$⊢ (k \in ℕ_{0} \land c \in ({ℕ_{0}}^{1_{𝑜}})) \to (c \leq_{f} (1_{𝑜} \times \{k\}) \leftrightarrow c (\emptyset) \in (0 \dots k))$
84	80 82 83	syl2anc	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}) \to (c \leq_{f} (1_{𝑜} \times \{k\}) \leftrightarrow c (\emptyset) \in (0 \dots k))$
85	79 84	mpbid	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}) \to c (\emptyset) \in (0 \dots k)$
86		eqidd	$⊢ ((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \to (c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\} ⟼ c (\emptyset)) = (c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\} ⟼ c (\emptyset))$
87		eqidd	$⊢ ((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \to (x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)) = (x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x))$
88		fveq2	$⊢ x = c (\emptyset) \to {coe}_{1} (F) (x) = {coe}_{1} (F) (c (\emptyset))$
89		oveq2	$⊢ x = c (\emptyset) \to k - x = k - c (\emptyset)$
90	89	fveq2d	$⊢ x = c (\emptyset) \to {coe}_{1} (G) (k - x) = {coe}_{1} (G) (k - c (\emptyset))$
91	88 90	oveq12d	$⊢ x = c (\emptyset) \to {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x) = {coe}_{1} (F) (c (\emptyset)) \underset{˙}{\cdot} {coe}_{1} (G) (k - c (\emptyset))$
92	85 86 87 91	fmptco	$⊢ ((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \to (x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)) \circ (c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\} ⟼ c (\emptyset)) = (c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\} ⟼ {coe}_{1} (F) (c (\emptyset)) \underset{˙}{\cdot} {coe}_{1} (G) (k - c (\emptyset)))$
93		simpll2	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}) \to F \in B$
94	43	fvcoe1	$⊢ (F \in B \land c \in ({ℕ_{0}}^{1_{𝑜}})) \to F (c) = {coe}_{1} (F) (c (\emptyset))$
95	93 82 94	syl2anc	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}) \to F (c) = {coe}_{1} (F) (c (\emptyset))$
96		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
97		0ex	$⊢ \emptyset \in V$
98	96 6 97	mapsnconst	$⊢ c \in ({ℕ_{0}}^{1_{𝑜}}) \to c = 1_{𝑜} \times \{c (\emptyset)\}$
99	82 98	syl	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}) \to c = 1_{𝑜} \times \{c (\emptyset)\}$
100	99	oveq2d	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}) \to (1_{𝑜} \times \{k\}) -_{f} c = (1_{𝑜} \times \{k\}) -_{f} (1_{𝑜} \times \{c (\emptyset)\})$
101	7	a1i	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}) \to 1_{𝑜} \in On$
102		vex	$⊢ k \in V$
103	102	a1i	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}) \to k \in V$
104		fvexd	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}) \to c (\emptyset) \in V$
105	101 103 104	ofc12	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}) \to (1_{𝑜} \times \{k\}) -_{f} (1_{𝑜} \times \{c (\emptyset)\}) = 1_{𝑜} \times \{k - c (\emptyset)\}$
106	100 105	eqtrd	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}) \to (1_{𝑜} \times \{k\}) -_{f} c = 1_{𝑜} \times \{k - c (\emptyset)\}$
107	106	fveq2d	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}) \to G ((1_{𝑜} \times \{k\}) -_{f} c) = G (1_{𝑜} \times \{k - c (\emptyset)\})$
108		simpll3	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}) \to G \in B$
109		fznn0sub	$⊢ c (\emptyset) \in (0 \dots k) \to k - c (\emptyset) \in ℕ_{0}$
110	85 109	syl	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}) \to k - c (\emptyset) \in ℕ_{0}$
111	50	coe1fv	$⊢ (G \in B \land k - c (\emptyset) \in ℕ_{0}) \to {coe}_{1} (G) (k - c (\emptyset)) = G (1_{𝑜} \times \{k - c (\emptyset)\})$
112	108 110 111	syl2anc	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}) \to {coe}_{1} (G) (k - c (\emptyset)) = G (1_{𝑜} \times \{k - c (\emptyset)\})$
113	107 112	eqtr4d	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}) \to G ((1_{𝑜} \times \{k\}) -_{f} c) = {coe}_{1} (G) (k - c (\emptyset))$
114	95 113	oveq12d	$⊢ (((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \land c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}) \to F (c) \underset{˙}{\cdot} G ((1_{𝑜} \times \{k\}) -_{f} c) = {coe}_{1} (F) (c (\emptyset)) \underset{˙}{\cdot} {coe}_{1} (G) (k - c (\emptyset))$
115	114	mpteq2dva	$⊢ ((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \to (c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\} ⟼ F (c) \underset{˙}{\cdot} G ((1_{𝑜} \times \{k\}) -_{f} c)) = (c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\} ⟼ {coe}_{1} (F) (c (\emptyset)) \underset{˙}{\cdot} {coe}_{1} (G) (k - c (\emptyset)))$
116	92 115	eqtr4d	$⊢ ((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \to (x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)) \circ (c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\} ⟼ c (\emptyset)) = (c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\} ⟼ F (c) \underset{˙}{\cdot} G ((1_{𝑜} \times \{k\}) -_{f} c))$
117	116	oveq2d	$⊢ ((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \to \sum_{R} ((x \in (0 \dots k) ⟼ {coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)) \circ (c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\} ⟼ c (\emptyset))) = \underset{c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}}{\sum_{R}} (F (c) \underset{˙}{\cdot} G ((1_{𝑜} \times \{k\}) -_{f} c))$
118	75 117	eqtrd	$⊢ ((R \in Ring \land F \in B \land G \in B) \land k \in ℕ_{0}) \to {\sum_{R}}_{x = 0}^{k} ({coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)) = \underset{c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}}{\sum_{R}} (F (c) \underset{˙}{\cdot} G ((1_{𝑜} \times \{k\}) -_{f} c))$
119	118	mpteq2dva	$⊢ (R \in Ring \land F \in B \land G \in B) \to (k \in ℕ_{0} ⟼ {\sum_{R}}_{x = 0}^{k} ({coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x))) = (k \in ℕ_{0} ⟼ \underset{c \in \{d \in ({ℕ_{0}}^{1_{𝑜}}) \| d \leq_{f} (1_{𝑜} \times \{k\})\}}{\sum_{R}} (F (c) \underset{˙}{\cdot} G ((1_{𝑜} \times \{k\}) -_{f} c)))$
120	26 33 119	3eqtr4d	$⊢ (R \in Ring \land F \in B \land G \in B) \to {coe}_{1} (F \underset{˙}{∙} G) = (k \in ℕ_{0} ⟼ {\sum_{R}}_{x = 0}^{k} ({coe}_{1} (F) (x) \underset{˙}{\cdot} {coe}_{1} (G) (k - x)))$

Metamath Proof Explorer

Theorem coe1mul2

Proof