Theorem psropprmul

Description: Reversing multiplication in a ring reverses multiplication in the power series ring. (Contributed by Stefan O'Rear, 27-Mar-2015)

	Ref	Expression
Hypotheses	psropprmul.y	$$⊢Y=I\mathrm{mPwSer}R$$
	psropprmul.s	$$⊢S={opp}_r\left(R\right)$$
	psropprmul.z	$$⊢Z=I\mathrm{mPwSer}S$$
	psropprmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
	psropprmul.u	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Z$$
	psropprmul.b	$$⊢B={\mathrm{Base}}_Y$$
Assertion	psropprmul	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to F\underset{\dot{}}{\bullet }G=G\underset{\dot{}}{·}F$$

Proof

Step	Hyp	Ref	Expression
1		psropprmul.y	$$⊢Y=I\mathrm{mPwSer}R$$
2		psropprmul.s	$$⊢S={opp}_r\left(R\right)$$
3		psropprmul.z	$$⊢Z=I\mathrm{mPwSer}S$$
4		psropprmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_Y$$
5		psropprmul.u	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Z$$
6		psropprmul.b	$$⊢B={\mathrm{Base}}_Y$$
7		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
8		eqid	$$⊢0_R=0_R$$
9		ringcmn	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{CMnd}$$
10	9	3ad2ant1	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to R\in \mathrm{CMnd}$$
11	10	adantr	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to R\in \mathrm{CMnd}$$
12		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
13	12	rabex	$$⊢\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
14	13	rabex	$$⊢\left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\in \mathrm{V}$$
15	14	a1i	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\in \mathrm{V}$$
16		simpll1	$$⊢\left(\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\right)\to R\in \mathrm{Ring}$$
17		eqid	$$⊢\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
18		simp3	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to G\in B$$
19	1 7 17 6 18	psrelbas	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to G:\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
20	19	adantr	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to G:\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
21		elrabi	$$⊢e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\to e\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
22		ffvelcdm	$$⊢\left(G:\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R\wedge e\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to G\left(e\right)\in {\mathrm{Base}}_R$$
23	20 21 22	syl2an	$$⊢\left(\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\right)\to G\left(e\right)\in {\mathrm{Base}}_R$$
24		simp2	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to F\in B$$
25	1 7 17 6 24	psrelbas	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to F:\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
26	25	ad2antrr	$$⊢\left(\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\right)\to F:\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
27		ssrab2	$$⊢\left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\subseteq \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
28		eqid	$$⊢\left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}=\left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}$$
29	17 28	psrbagconcl	$$⊢\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\right)\to b{-}_{f}e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}$$
30	29	adantll	$$⊢\left(\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\right)\to b{-}_{f}e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}$$
31	27 30	sselid	$$⊢\left(\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\right)\to b{-}_{f}e\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
32	26 31	ffvelcdmd	$$⊢\left(\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\right)\to F\left(b{-}_{f}e\right)\in {\mathrm{Base}}_R$$
33		eqid	$$⊢{\cdot }_R={\cdot }_R$$
34	7 33	ringcl	$$⊢\left(R\in \mathrm{Ring}\wedge G\left(e\right)\in {\mathrm{Base}}_R\wedge F\left(b{-}_{f}e\right)\in {\mathrm{Base}}_R\right)\to G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\in {\mathrm{Base}}_R$$
35	16 23 32 34	syl3anc	$$⊢\left(\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\right)\to G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\in {\mathrm{Base}}_R$$
36	35	fmpttd	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right):\left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟶{\mathrm{Base}}_R$$
37		mptexg	$$⊢\left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\in \mathrm{V}\to \left(e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)\in \mathrm{V}$$
38	14 37	mp1i	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)\in \mathrm{V}$$
39		funmpt	$$⊢\mathrm{Fun}\left(e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)$$
40	39	a1i	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \mathrm{Fun}\left(e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)$$
41		fvexd	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to 0_R\in \mathrm{V}$$
42	17	psrbaglefi	$$⊢b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\to \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\in \mathrm{Fin}$$
43	42	adantl	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\in \mathrm{Fin}$$
44		suppssdm	$$⊢\left(e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)\mathrm{supp}{0}_R\subseteq \mathrm{dom}\left(e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)$$
45		eqid	$$⊢\left(e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)=\left(e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)$$
46	45	dmmptss	$$⊢\mathrm{dom}\left(e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)\subseteq \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}$$
47	44 46	sstri	$$⊢\left(e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)\mathrm{supp}{0}_R\subseteq \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}$$
48	47	a1i	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)\mathrm{supp}{0}_R\subseteq \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}$$
49		suppssfifsupp	$$⊢\left(\left(\left(e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)\wedge 0_R\in \mathrm{V}\right)\wedge \left(\left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\in \mathrm{Fin}\wedge \left(e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)\mathrm{supp}{0}_R\subseteq \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\right)\right)\to {finSupp}_{0_R}\left(\left(e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)\right)$$
50	38 40 41 43 48 49	syl32anc	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to {finSupp}_{0_R}\left(\left(e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)\right)$$
51	17 28	psrbagconf1o	$$⊢b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\to \left(c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼b{-}_{f}c\right):\left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\underset{1-1\; onto}{⟶}\left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}$$
52	51	adantl	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼b{-}_{f}c\right):\left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\underset{1-1\; onto}{⟶}\left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}$$
53	7 8 11 15 36 50 52	gsumf1o	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \underset{e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}}{{\sum }_R}\left(G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)={\sum }_R\left(\left(e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)\circ \left(c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼b{-}_{f}c\right)\right)$$
54	17 28	psrbagconcl	$$⊢\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\right)\to b{-}_{f}c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}$$
55	54	adantll	$$⊢\left(\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\right)\to b{-}_{f}c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}$$
56		eqidd	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼b{-}_{f}c\right)=\left(c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼b{-}_{f}c\right)$$
57		eqidd	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)=\left(e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)$$
58		fveq2	$$⊢e=b{-}_{f}c\to G\left(e\right)=G\left(b{-}_{f}c\right)$$
59		oveq2	$$⊢e=b{-}_{f}c\to b{-}_{f}e=b{-}_f\left(b{-}_{f}c\right)$$
60	59	fveq2d	$$⊢e=b{-}_{f}c\to F\left(b{-}_{f}e\right)=F\left(b{-}_f\left(b{-}_{f}c\right)\right)$$
61	58 60	oveq12d	$$⊢e=b{-}_{f}c\to G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)=G\left(b{-}_{f}c\right){\cdot }_{R}F\left(b{-}_f\left(b{-}_{f}c\right)\right)$$
62	55 56 57 61	fmptco	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)\circ \left(c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼b{-}_{f}c\right)=\left(c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(b{-}_{f}c\right){\cdot }_{R}F\left(b{-}_f\left(b{-}_{f}c\right)\right)\right)$$
63		reldmpsr	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mPwSer}$$
64	1 6 63	strov2rcl	$$⊢G\in B\to I\in \mathrm{V}$$
65	64	3ad2ant3	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to I\in \mathrm{V}$$
66	65	ad2antrr	$$⊢\left(\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\right)\to I\in \mathrm{V}$$
67	17	psrbagf	$$⊢b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\to b:I⟶{\mathbb{N}}_0$$
68	67	adantl	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to b:I⟶{\mathbb{N}}_0$$
69	68	adantr	$$⊢\left(\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\right)\to b:I⟶{\mathbb{N}}_0$$
70		elrabi	$$⊢c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\to c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
71	17	psrbagf	$$⊢c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\to c:I⟶{\mathbb{N}}_0$$
72	70 71	syl	$$⊢c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\to c:I⟶{\mathbb{N}}_0$$
73	72	adantl	$$⊢\left(\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\right)\to c:I⟶{\mathbb{N}}_0$$
74		nn0cn	$$⊢e\in {\mathbb{N}}_0\to e\in ℂ$$
75		nn0cn	$$⊢f\in {\mathbb{N}}_0\to f\in ℂ$$
76		nncan	$$⊢\left(e\in ℂ\wedge f\in ℂ\right)\to e-\left(e-f\right)=f$$
77	74 75 76	syl2an	$$⊢\left(e\in {\mathbb{N}}_0\wedge f\in {\mathbb{N}}_0\right)\to e-\left(e-f\right)=f$$
78	77	adantl	$$⊢\left(\left(\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\right)\wedge \left(e\in {\mathbb{N}}_0\wedge f\in {\mathbb{N}}_0\right)\right)\to e-\left(e-f\right)=f$$
79	66 69 73 78	caonncan	$$⊢\left(\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\right)\to b{-}_f\left(b{-}_{f}c\right)=c$$
80	79	fveq2d	$$⊢\left(\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\right)\to F\left(b{-}_f\left(b{-}_{f}c\right)\right)=F\left(c\right)$$
81	80	oveq2d	$$⊢\left(\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\right)\to G\left(b{-}_{f}c\right){\cdot }_{R}F\left(b{-}_f\left(b{-}_{f}c\right)\right)=G\left(b{-}_{f}c\right){\cdot }_{R}F\left(c\right)$$
82		eqid	$$⊢{\cdot }_S={\cdot }_S$$
83	7 33 2 82	opprmul	$$⊢F\left(c\right){\cdot }_{S}G\left(b{-}_{f}c\right)=G\left(b{-}_{f}c\right){\cdot }_{R}F\left(c\right)$$
84	81 83	eqtr4di	$$⊢\left(\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}\right)\to G\left(b{-}_{f}c\right){\cdot }_{R}F\left(b{-}_f\left(b{-}_{f}c\right)\right)=F\left(c\right){\cdot }_{S}G\left(b{-}_{f}c\right)$$
85	84	mpteq2dva	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(b{-}_{f}c\right){\cdot }_{R}F\left(b{-}_f\left(b{-}_{f}c\right)\right)\right)=\left(c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼F\left(c\right){\cdot }_{S}G\left(b{-}_{f}c\right)\right)$$
86	62 85	eqtrd	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)\circ \left(c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼b{-}_{f}c\right)=\left(c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼F\left(c\right){\cdot }_{S}G\left(b{-}_{f}c\right)\right)$$
87	86	oveq2d	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to {\sum }_R\left(\left(e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)\circ \left(c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼b{-}_{f}c\right)\right)=\underset{c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}}{{\sum }_R}\left(F\left(c\right){\cdot }_{S}G\left(b{-}_{f}c\right)\right)$$
88	14	mptex	$$⊢\left(c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼F\left(c\right){\cdot }_{S}G\left(b{-}_{f}c\right)\right)\in \mathrm{V}$$
89	88	a1i	$$⊢R\in \mathrm{Ring}\to \left(c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}⟼F\left(c\right){\cdot }_{S}G\left(b{-}_{f}c\right)\right)\in \mathrm{V}$$
90		id	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Ring}$$
91	2	fvexi	$$⊢S\in \mathrm{V}$$
92	91	a1i	$$⊢R\in \mathrm{Ring}\to S\in \mathrm{V}$$
93	2 7	opprbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_S$$
94	93	a1i	$$⊢R\in \mathrm{Ring}\to {\mathrm{Base}}_R={\mathrm{Base}}_S$$
95		eqid	$$⊢{+}_R={+}_R$$
96	2 95	oppradd	$$⊢{+}_R={+}_S$$
97	96	a1i	$$⊢R\in \mathrm{Ring}\to {+}_R={+}_S$$
98	89 90 92 94 97	gsumpropd	$$⊢R\in \mathrm{Ring}\to \underset{c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}}{{\sum }_R}\left(F\left(c\right){\cdot }_{S}G\left(b{-}_{f}c\right)\right)=\underset{c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}}{{\sum }_S}\left(F\left(c\right){\cdot }_{S}G\left(b{-}_{f}c\right)\right)$$
99	98	3ad2ant1	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to \underset{c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}}{{\sum }_R}\left(F\left(c\right){\cdot }_{S}G\left(b{-}_{f}c\right)\right)=\underset{c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}}{{\sum }_S}\left(F\left(c\right){\cdot }_{S}G\left(b{-}_{f}c\right)\right)$$
100	99	adantr	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \underset{c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}}{{\sum }_R}\left(F\left(c\right){\cdot }_{S}G\left(b{-}_{f}c\right)\right)=\underset{c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}}{{\sum }_S}\left(F\left(c\right){\cdot }_{S}G\left(b{-}_{f}c\right)\right)$$
101	53 87 100	3eqtrd	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \underset{e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}}{{\sum }_R}\left(G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)=\underset{c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}}{{\sum }_S}\left(F\left(c\right){\cdot }_{S}G\left(b{-}_{f}c\right)\right)$$
102	101	mpteq2dva	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to \left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}}{{\sum }_R}\left(G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)\right)=\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}}{{\sum }_S}\left(F\left(c\right){\cdot }_{S}G\left(b{-}_{f}c\right)\right)\right)$$
103	1 6 33 4 17 18 24	psrmulfval	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to G\underset{\dot{}}{·}F=\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{e\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}}{{\sum }_R}\left(G\left(e\right){\cdot }_{R}F\left(b{-}_{f}e\right)\right)\right)$$
104		eqid	$$⊢{\mathrm{Base}}_Z={\mathrm{Base}}_Z$$
105	93	a1i	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to {\mathrm{Base}}_R={\mathrm{Base}}_S$$
106	105	psrbaspropd	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}$$
107	1	fveq2i	$$⊢{\mathrm{Base}}_Y={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
108	6 107	eqtri	$$⊢B={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
109	3	fveq2i	$$⊢{\mathrm{Base}}_Z={\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}$$
110	106 108 109	3eqtr4g	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to B={\mathrm{Base}}_Z$$
111	24 110	eleqtrd	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to F\in {\mathrm{Base}}_Z$$
112	18 110	eleqtrd	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to G\in {\mathrm{Base}}_Z$$
113	3 104 82 5 17 111 112	psrmulfval	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to F\underset{\dot{}}{\bullet }G=\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{c\in \left\{d\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|d{\le }_{f}b\right\}}{{\sum }_S}\left(F\left(c\right){\cdot }_{S}G\left(b{-}_{f}c\right)\right)\right)$$
114	102 103 113	3eqtr4rd	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to F\underset{\dot{}}{\bullet }G=G\underset{\dot{}}{·}F$$