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	$$⊢Y={\mathrm{Poly}}_1\left(R\right)$$
	coe1mul3.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Y$$
	coe1mul3.u	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	coe1mul3.b	$$⊢B={\mathrm{Base}}_Y$$
	coe1mul3.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	coe1mul3.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	coe1mul3.f1	$$⊢\phi \to F\in B$$
	coe1mul3.f2	$$⊢\phi \to I\in {\mathbb{N}}_0$$
	coe1mul3.f3	$$⊢\phi \to D\left(F\right)\le I$$
	coe1mul3.g1	$$⊢\phi \to G\in B$$
	coe1mul3.g2	$$⊢\phi \to J\in {\mathbb{N}}_0$$
	coe1mul3.g3	$$⊢\phi \to D\left(G\right)\le J$$
Assertion	coe1mul3	$$⊢\phi \to {\mathrm{coe}}_1\left(F\underset{\dot{}}{\bullet }G\right)\left(I+J\right)={\mathrm{coe}}_1\left(F\right)\left(I\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(J\right)$$

Proof

Step	Hyp	Ref	Expression
1		coe1mul3.s	$$⊢Y={\mathrm{Poly}}_1\left(R\right)$$
2		coe1mul3.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Y$$
3		coe1mul3.u	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		coe1mul3.b	$$⊢B={\mathrm{Base}}_Y$$
5		coe1mul3.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
6		coe1mul3.r	$$⊢\phi \to R\in \mathrm{Ring}$$
7		coe1mul3.f1	$$⊢\phi \to F\in B$$
8		coe1mul3.f2	$$⊢\phi \to I\in {\mathbb{N}}_0$$
9		coe1mul3.f3	$$⊢\phi \to D\left(F\right)\le I$$
10		coe1mul3.g1	$$⊢\phi \to G\in B$$
11		coe1mul3.g2	$$⊢\phi \to J\in {\mathbb{N}}_0$$
12		coe1mul3.g3	$$⊢\phi \to D\left(G\right)\le J$$
13	1 2 3 4	coe1mul	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to {\mathrm{coe}}_1\left(F\underset{\dot{}}{\bullet }G\right)=\left(x\in {\mathbb{N}}_0⟼\underset{y=0}{\overset{x}{{\sum }_R}}\left({\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(x-y\right)\right)\right)$$
14	6 7 10 13	syl3anc	$$⊢\phi \to {\mathrm{coe}}_1\left(F\underset{\dot{}}{\bullet }G\right)=\left(x\in {\mathbb{N}}_0⟼\underset{y=0}{\overset{x}{{\sum }_R}}\left({\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(x-y\right)\right)\right)$$
15	14	fveq1d	$$⊢\phi \to {\mathrm{coe}}_1\left(F\underset{\dot{}}{\bullet }G\right)\left(I+J\right)=\left(x\in {\mathbb{N}}_0⟼\underset{y=0}{\overset{x}{{\sum }_R}}\left({\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(x-y\right)\right)\right)\left(I+J\right)$$
16	8 11	nn0addcld	$$⊢\phi \to I+J\in {\mathbb{N}}_0$$
17		oveq2	$$⊢x=I+J\to \left(0\dots x\right)=\left(0\dots I+J\right)$$
18		fvoveq1	$$⊢x=I+J\to {\mathrm{coe}}_1\left(G\right)\left(x-y\right)={\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)$$
19	18	oveq2d	$$⊢x=I+J\to {\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(x-y\right)={\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)$$
20	17 19	mpteq12dv	$$⊢x=I+J\to \left(y\in \left(0\dots x\right)⟼{\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(x-y\right)\right)=\left(y\in \left(0\dots I+J\right)⟼{\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)\right)$$
21	20	oveq2d	$$⊢x=I+J\to \underset{y=0}{\overset{x}{{\sum }_R}}\left({\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(x-y\right)\right)=\underset{y=0}{\overset{I+J}{{\sum }_R}}\left({\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)\right)$$
22		eqid	$$⊢\left(x\in {\mathbb{N}}_0⟼\underset{y=0}{\overset{x}{{\sum }_R}}\left({\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(x-y\right)\right)\right)=\left(x\in {\mathbb{N}}_0⟼\underset{y=0}{\overset{x}{{\sum }_R}}\left({\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(x-y\right)\right)\right)$$
23		ovex	$$⊢\underset{y=0}{\overset{I+J}{{\sum }_R}}\left({\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)\right)\in \mathrm{V}$$
24	21 22 23	fvmpt	$$⊢I+J\in {\mathbb{N}}_0\to \left(x\in {\mathbb{N}}_0⟼\underset{y=0}{\overset{x}{{\sum }_R}}\left({\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(x-y\right)\right)\right)\left(I+J\right)=\underset{y=0}{\overset{I+J}{{\sum }_R}}\left({\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)\right)$$
25	16 24	syl	$$⊢\phi \to \left(x\in {\mathbb{N}}_0⟼\underset{y=0}{\overset{x}{{\sum }_R}}\left({\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(x-y\right)\right)\right)\left(I+J\right)=\underset{y=0}{\overset{I+J}{{\sum }_R}}\left({\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)\right)$$
26		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
27		eqid	$$⊢0_R=0_R$$
28		ringmnd	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Mnd}$$
29	6 28	syl	$$⊢\phi \to R\in \mathrm{Mnd}$$
30		ovexd	$$⊢\phi \to \left(0\dots I+J\right)\in \mathrm{V}$$
31	8	nn0red	$$⊢\phi \to I\in ℝ$$
32		nn0addge1	$$⊢\left(I\in ℝ\wedge J\in {\mathbb{N}}_0\right)\to I\le I+J$$
33	31 11 32	syl2anc	$$⊢\phi \to I\le I+J$$
34		fznn0	$$⊢I+J\in {\mathbb{N}}_0\to \left(I\in \left(0\dots I+J\right)\leftrightarrow \left(I\in {\mathbb{N}}_0\wedge I\le I+J\right)\right)$$
35	16 34	syl	$$⊢\phi \to \left(I\in \left(0\dots I+J\right)\leftrightarrow \left(I\in {\mathbb{N}}_0\wedge I\le I+J\right)\right)$$
36	8 33 35	mpbir2and	$$⊢\phi \to I\in \left(0\dots I+J\right)$$
37	6	adantr	$$⊢\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\to R\in \mathrm{Ring}$$
38		eqid	$$⊢{\mathrm{coe}}_1\left(F\right)={\mathrm{coe}}_1\left(F\right)$$
39	38 4 1 26	coe1f	$$⊢F\in B\to {\mathrm{coe}}_1\left(F\right):{\mathbb{N}}_0⟶{\mathrm{Base}}_R$$
40	7 39	syl	$$⊢\phi \to {\mathrm{coe}}_1\left(F\right):{\mathbb{N}}_0⟶{\mathrm{Base}}_R$$
41		elfznn0	$$⊢y\in \left(0\dots I+J\right)\to y\in {\mathbb{N}}_0$$
42		ffvelcdm	$$⊢\left({\mathrm{coe}}_1\left(F\right):{\mathbb{N}}_0⟶{\mathrm{Base}}_R\wedge y\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(F\right)\left(y\right)\in {\mathrm{Base}}_R$$
43	40 41 42	syl2an	$$⊢\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\to {\mathrm{coe}}_1\left(F\right)\left(y\right)\in {\mathrm{Base}}_R$$
44		eqid	$$⊢{\mathrm{coe}}_1\left(G\right)={\mathrm{coe}}_1\left(G\right)$$
45	44 4 1 26	coe1f	$$⊢G\in B\to {\mathrm{coe}}_1\left(G\right):{\mathbb{N}}_0⟶{\mathrm{Base}}_R$$
46	10 45	syl	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right):{\mathbb{N}}_0⟶{\mathrm{Base}}_R$$
47		fznn0sub	$$⊢y\in \left(0\dots I+J\right)\to I+J-y\in {\mathbb{N}}_0$$
48		ffvelcdm	$$⊢\left({\mathrm{coe}}_1\left(G\right):{\mathbb{N}}_0⟶{\mathrm{Base}}_R\wedge I+J-y\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)\in {\mathrm{Base}}_R$$
49	46 47 48	syl2an	$$⊢\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\to {\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)\in {\mathrm{Base}}_R$$
50	26 3	ringcl	$$⊢\left(R\in \mathrm{Ring}\wedge {\mathrm{coe}}_1\left(F\right)\left(y\right)\in {\mathrm{Base}}_R\wedge {\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)\in {\mathrm{Base}}_R\right)\to {\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)\in {\mathrm{Base}}_R$$
51	37 43 49 50	syl3anc	$$⊢\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\to {\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)\in {\mathrm{Base}}_R$$
52	51	fmpttd	$$⊢\phi \to \left(y\in \left(0\dots I+J\right)⟼{\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)\right):\left(0\dots I+J\right)⟶{\mathrm{Base}}_R$$
53		eldifsn	$$⊢y\in \left(\left(0\dots I+J\right)\setminus \left\{I\right\}\right)\leftrightarrow \left(y\in \left(0\dots I+J\right)\wedge y\ne I\right)$$
54	41	adantl	$$⊢\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\to y\in {\mathbb{N}}_0$$
55	54	nn0red	$$⊢\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\to y\in ℝ$$
56	31	adantr	$$⊢\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\to I\in ℝ$$
57	55 56	lttri2d	$$⊢\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\to \left(y\ne I\leftrightarrow \left(y<I\vee I<y\right)\right)$$
58	10	ad2antrr	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge y<I\right)\to G\in B$$
59	47	adantl	$$⊢\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\to I+J-y\in {\mathbb{N}}_0$$
60	59	adantr	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge y<I\right)\to I+J-y\in {\mathbb{N}}_0$$
61	5 1 4	deg1xrcl	$$⊢G\in B\to D\left(G\right)\in {ℝ}^{*}$$
62	10 61	syl	$$⊢\phi \to D\left(G\right)\in {ℝ}^{*}$$
63	62	ad2antrr	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge y<I\right)\to D\left(G\right)\in {ℝ}^{*}$$
64	11	nn0red	$$⊢\phi \to J\in ℝ$$
65	64	rexrd	$$⊢\phi \to J\in {ℝ}^{*}$$
66	65	ad2antrr	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge y<I\right)\to J\in {ℝ}^{*}$$
67	16	nn0red	$$⊢\phi \to I+J\in ℝ$$
68	67	adantr	$$⊢\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\to I+J\in ℝ$$
69	68 55	resubcld	$$⊢\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\to I+J-y\in ℝ$$
70	69	rexrd	$$⊢\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\to I+J-y\in {ℝ}^{*}$$
71	70	adantr	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge y<I\right)\to I+J-y\in {ℝ}^{*}$$
72	12	ad2antrr	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge y<I\right)\to D\left(G\right)\le J$$
73	64	adantr	$$⊢\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\to J\in ℝ$$
74	55 56 73	ltadd1d	$$⊢\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\to \left(y<I\leftrightarrow y+J<I+J\right)$$
75	55 73 68	ltaddsub2d	$$⊢\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\to \left(y+J<I+J\leftrightarrow J<I+J-y\right)$$
76	74 75	bitrd	$$⊢\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\to \left(y<I\leftrightarrow J<I+J-y\right)$$
77	76	biimpa	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge y<I\right)\to J<I+J-y$$
78	63 66 71 72 77	xrlelttrd	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge y<I\right)\to D\left(G\right)<I+J-y$$
79	5 1 4 27 44	deg1lt	$$⊢\left(G\in B\wedge I+J-y\in {\mathbb{N}}_0\wedge D\left(G\right)<I+J-y\right)\to {\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)=0_R$$
80	58 60 78 79	syl3anc	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge y<I\right)\to {\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)=0_R$$
81	80	oveq2d	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge y<I\right)\to {\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)={\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{0}_R$$
82	26 3 27	ringrz	$$⊢\left(R\in \mathrm{Ring}\wedge {\mathrm{coe}}_1\left(F\right)\left(y\right)\in {\mathrm{Base}}_R\right)\to {\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{0}_R=0_R$$
83	37 43 82	syl2anc	$$⊢\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\to {\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{0}_R=0_R$$
84	83	adantr	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge y<I\right)\to {\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{0}_R=0_R$$
85	81 84	eqtrd	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge y<I\right)\to {\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)=0_R$$
86	7	ad2antrr	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge I<y\right)\to F\in B$$
87	54	adantr	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge I<y\right)\to y\in {\mathbb{N}}_0$$
88	5 1 4	deg1xrcl	$$⊢F\in B\to D\left(F\right)\in {ℝ}^{*}$$
89	7 88	syl	$$⊢\phi \to D\left(F\right)\in {ℝ}^{*}$$
90	89	ad2antrr	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge I<y\right)\to D\left(F\right)\in {ℝ}^{*}$$
91	31	rexrd	$$⊢\phi \to I\in {ℝ}^{*}$$
92	91	ad2antrr	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge I<y\right)\to I\in {ℝ}^{*}$$
93	55	rexrd	$$⊢\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\to y\in {ℝ}^{*}$$
94	93	adantr	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge I<y\right)\to y\in {ℝ}^{*}$$
95	9	ad2antrr	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge I<y\right)\to D\left(F\right)\le I$$
96		simpr	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge I<y\right)\to I<y$$
97	90 92 94 95 96	xrlelttrd	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge I<y\right)\to D\left(F\right)<y$$
98	5 1 4 27 38	deg1lt	$$⊢\left(F\in B\wedge y\in {\mathbb{N}}_0\wedge D\left(F\right)<y\right)\to {\mathrm{coe}}_1\left(F\right)\left(y\right)=0_R$$
99	86 87 97 98	syl3anc	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge I<y\right)\to {\mathrm{coe}}_1\left(F\right)\left(y\right)=0_R$$
100	99	oveq1d	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge I<y\right)\to {\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)=0_R\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)$$
101	26 3 27	ringlz	$$⊢\left(R\in \mathrm{Ring}\wedge {\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)\in {\mathrm{Base}}_R\right)\to 0_R\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)=0_R$$
102	37 49 101	syl2anc	$$⊢\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\to 0_R\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)=0_R$$
103	102	adantr	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge I<y\right)\to 0_R\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)=0_R$$
104	100 103	eqtrd	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge I<y\right)\to {\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)=0_R$$
105	85 104	jaodan	$$⊢\left(\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\wedge \left(y<I\vee I<y\right)\right)\to {\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)=0_R$$
106	105	ex	$$⊢\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\to \left(\left(y<I\vee I<y\right)\to {\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)=0_R\right)$$
107	57 106	sylbid	$$⊢\left(\phi \wedge y\in \left(0\dots I+J\right)\right)\to \left(y\ne I\to {\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)=0_R\right)$$
108	107	impr	$$⊢\left(\phi \wedge \left(y\in \left(0\dots I+J\right)\wedge y\ne I\right)\right)\to {\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)=0_R$$
109	53 108	sylan2b	$$⊢\left(\phi \wedge y\in \left(\left(0\dots I+J\right)\setminus \left\{I\right\}\right)\right)\to {\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)=0_R$$
110	109 30	suppss2	$$⊢\phi \to \left(y\in \left(0\dots I+J\right)⟼{\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)\right)\mathrm{supp}{0}_R\subseteq \left\{I\right\}$$
111	26 27 29 30 36 52 110	gsumpt	$$⊢\phi \to \underset{y=0}{\overset{I+J}{{\sum }_R}}\left({\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)\right)=\left(y\in \left(0\dots I+J\right)⟼{\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)\right)\left(I\right)$$
112		fveq2	$$⊢y=I\to {\mathrm{coe}}_1\left(F\right)\left(y\right)={\mathrm{coe}}_1\left(F\right)\left(I\right)$$
113		oveq2	$$⊢y=I\to I+J-y=I+J-I$$
114	113	fveq2d	$$⊢y=I\to {\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)={\mathrm{coe}}_1\left(G\right)\left(I+J-I\right)$$
115	112 114	oveq12d	$$⊢y=I\to {\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)={\mathrm{coe}}_1\left(F\right)\left(I\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-I\right)$$
116		eqid	$$⊢\left(y\in \left(0\dots I+J\right)⟼{\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)\right)=\left(y\in \left(0\dots I+J\right)⟼{\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)\right)$$
117		ovex	$$⊢{\mathrm{coe}}_1\left(F\right)\left(I\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-I\right)\in \mathrm{V}$$
118	115 116 117	fvmpt	$$⊢I\in \left(0\dots I+J\right)\to \left(y\in \left(0\dots I+J\right)⟼{\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)\right)\left(I\right)={\mathrm{coe}}_1\left(F\right)\left(I\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-I\right)$$
119	36 118	syl	$$⊢\phi \to \left(y\in \left(0\dots I+J\right)⟼{\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)\right)\left(I\right)={\mathrm{coe}}_1\left(F\right)\left(I\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-I\right)$$
120	8	nn0cnd	$$⊢\phi \to I\in ℂ$$
121	11	nn0cnd	$$⊢\phi \to J\in ℂ$$
122	120 121	pncan2d	$$⊢\phi \to I+J-I=J$$
123	122	fveq2d	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(I+J-I\right)={\mathrm{coe}}_1\left(G\right)\left(J\right)$$
124	123	oveq2d	$$⊢\phi \to {\mathrm{coe}}_1\left(F\right)\left(I\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-I\right)={\mathrm{coe}}_1\left(F\right)\left(I\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(J\right)$$
125	111 119 124	3eqtrd	$$⊢\phi \to \underset{y=0}{\overset{I+J}{{\sum }_R}}\left({\mathrm{coe}}_1\left(F\right)\left(y\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(I+J-y\right)\right)={\mathrm{coe}}_1\left(F\right)\left(I\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(J\right)$$
126	15 25 125	3eqtrd	$$⊢\phi \to {\mathrm{coe}}_1\left(F\underset{\dot{}}{\bullet }G\right)\left(I+J\right)={\mathrm{coe}}_1\left(F\right)\left(I\right)\underset{\dot{}}{·}{\mathrm{coe}}_1\left(G\right)\left(J\right)$$