Theorem rhmcomulmpl

Description: Show that the ring homomorphism in rhmmpl preserves multiplication. (Contributed by SN, 8-Feb-2025)

	Ref	Expression
Hypotheses	rhmcomulmpl.p	$$⊢P=I\mathrm{mPoly}R$$
	rhmcomulmpl.q	$$⊢Q=I\mathrm{mPoly}S$$
	rhmcomulmpl.b	$$⊢B={\mathrm{Base}}_P$$
	rhmcomulmpl.c	$$⊢C={\mathrm{Base}}_Q$$
	rhmcomulmpl.1	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
	rhmcomulmpl.2	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Q$$
	rhmcomulmpl.h	$$⊢\phi \to H\in \left(R\mathrm{RingHom}S\right)$$
	rhmcomulmpl.f	$$⊢\phi \to F\in B$$
	rhmcomulmpl.g	$$⊢\phi \to G\in B$$
Assertion	rhmcomulmpl	$$⊢\phi \to H\circ \left(F\underset{\dot{}}{·}G\right)=\left(H\circ F\right)\underset{\dot{}}{\bullet }\left(H\circ G\right)$$

Proof

Step	Hyp	Ref	Expression
1		rhmcomulmpl.p	$$⊢P=I\mathrm{mPoly}R$$
2		rhmcomulmpl.q	$$⊢Q=I\mathrm{mPoly}S$$
3		rhmcomulmpl.b	$$⊢B={\mathrm{Base}}_P$$
4		rhmcomulmpl.c	$$⊢C={\mathrm{Base}}_Q$$
5		rhmcomulmpl.1	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
6		rhmcomulmpl.2	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Q$$
7		rhmcomulmpl.h	$$⊢\phi \to H\in \left(R\mathrm{RingHom}S\right)$$
8		rhmcomulmpl.f	$$⊢\phi \to F\in B$$
9		rhmcomulmpl.g	$$⊢\phi \to G\in B$$
10		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
11		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
12	10 11	rhmf	$$⊢H\in \left(R\mathrm{RingHom}S\right)\to H:{\mathrm{Base}}_R⟶{\mathrm{Base}}_S$$
13	7 12	syl	$$⊢\phi \to H:{\mathrm{Base}}_R⟶{\mathrm{Base}}_S$$
14		eqid	$$⊢\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
15		rhmrcl1	$$⊢H\in \left(R\mathrm{RingHom}S\right)\to R\in \mathrm{Ring}$$
16	7 15	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
17	1 10 3 14 8	mplelf	$$⊢\phi \to F:\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
18	1 10 3 14 9	mplelf	$$⊢\phi \to G:\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
19	14 16 17 18	rhmpsrlem2	$$⊢\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \underset{d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}}{{\sum }_R}\left(F\left(d\right){\cdot }_{R}G\left(k{-}_{f}d\right)\right)\in {\mathrm{Base}}_R$$
20	13 19	cofmpt	$$⊢\phi \to H\circ \left(k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}}{{\sum }_R}\left(F\left(d\right){\cdot }_{R}G\left(k{-}_{f}d\right)\right)\right)=\left(k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼H\left(\underset{d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}}{{\sum }_R}\left(F\left(d\right){\cdot }_{R}G\left(k{-}_{f}d\right)\right)\right)\right)$$
21		eqid	$$⊢0_R=0_R$$
22	16	ringcmnd	$$⊢\phi \to R\in \mathrm{CMnd}$$
23	22	adantr	$$⊢\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to R\in \mathrm{CMnd}$$
24		rhmrcl2	$$⊢H\in \left(R\mathrm{RingHom}S\right)\to S\in \mathrm{Ring}$$
25	7 24	syl	$$⊢\phi \to S\in \mathrm{Ring}$$
26	25	ringgrpd	$$⊢\phi \to S\in \mathrm{Grp}$$
27	26	grpmndd	$$⊢\phi \to S\in \mathrm{Mnd}$$
28	27	adantr	$$⊢\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to S\in \mathrm{Mnd}$$
29		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
30	29	rabex	$$⊢\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
31	30	rabex	$$⊢\left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}\in \mathrm{V}$$
32	31	a1i	$$⊢\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}\in \mathrm{V}$$
33		rhmghm	$$⊢H\in \left(R\mathrm{RingHom}S\right)\to H\in \left(R\mathrm{GrpHom}S\right)$$
34		ghmmhm	$$⊢H\in \left(R\mathrm{GrpHom}S\right)\to H\in \left(R\mathrm{MndHom}S\right)$$
35	7 33 34	3syl	$$⊢\phi \to H\in \left(R\mathrm{MndHom}S\right)$$
36	35	adantr	$$⊢\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to H\in \left(R\mathrm{MndHom}S\right)$$
37		eqid	$$⊢{\cdot }_R={\cdot }_R$$
38	16	ad2antrr	$$⊢\left(\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}\right)\to R\in \mathrm{Ring}$$
39		elrabi	$$⊢d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}\to d\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
40	17	ffvelcdmda	$$⊢\left(\phi \wedge d\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to F\left(d\right)\in {\mathrm{Base}}_R$$
41	39 40	sylan2	$$⊢\left(\phi \wedge d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}\right)\to F\left(d\right)\in {\mathrm{Base}}_R$$
42	41	adantlr	$$⊢\left(\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}\right)\to F\left(d\right)\in {\mathrm{Base}}_R$$
43	18	ad2antrr	$$⊢\left(\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}\right)\to G:\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
44		eqid	$$⊢\left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}=\left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}$$
45	14 44	psrbagconcl	$$⊢\left(k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}\right)\to k{-}_{f}d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}$$
46		elrabi	$$⊢k{-}_{f}d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}\to k{-}_{f}d\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
47	45 46	syl	$$⊢\left(k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}\right)\to k{-}_{f}d\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
48	47	adantll	$$⊢\left(\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}\right)\to k{-}_{f}d\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
49	43 48	ffvelcdmd	$$⊢\left(\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}\right)\to G\left(k{-}_{f}d\right)\in {\mathrm{Base}}_R$$
50	10 37 38 42 49	ringcld	$$⊢\left(\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}\right)\to F\left(d\right){\cdot }_{R}G\left(k{-}_{f}d\right)\in {\mathrm{Base}}_R$$
51	14 16 17 18	rhmpsrlem1	$$⊢\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to {finSupp}_{0_R}\left(\left(d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}⟼F\left(d\right){\cdot }_{R}G\left(k{-}_{f}d\right)\right)\right)$$
52	10 21 23 28 32 36 50 51	gsummptmhm	$$⊢\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \underset{d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}}{{\sum }_S}H\left(F\left(d\right){\cdot }_{R}G\left(k{-}_{f}d\right)\right)=H\left(\underset{d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}}{{\sum }_R}\left(F\left(d\right){\cdot }_{R}G\left(k{-}_{f}d\right)\right)\right)$$
53	7	ad2antrr	$$⊢\left(\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}\right)\to H\in \left(R\mathrm{RingHom}S\right)$$
54		eqid	$$⊢{\cdot }_S={\cdot }_S$$
55	10 37 54	rhmmul	$$⊢\left(H\in \left(R\mathrm{RingHom}S\right)\wedge F\left(d\right)\in {\mathrm{Base}}_R\wedge G\left(k{-}_{f}d\right)\in {\mathrm{Base}}_R\right)\to H\left(F\left(d\right){\cdot }_{R}G\left(k{-}_{f}d\right)\right)=H\left(F\left(d\right)\right){\cdot }_{S}H\left(G\left(k{-}_{f}d\right)\right)$$
56	53 42 49 55	syl3anc	$$⊢\left(\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}\right)\to H\left(F\left(d\right){\cdot }_{R}G\left(k{-}_{f}d\right)\right)=H\left(F\left(d\right)\right){\cdot }_{S}H\left(G\left(k{-}_{f}d\right)\right)$$
57	17	ad2antrr	$$⊢\left(\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}\right)\to F:\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
58	39	adantl	$$⊢\left(\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}\right)\to d\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
59	57 58	fvco3d	$$⊢\left(\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}\right)\to \left(H\circ F\right)\left(d\right)=H\left(F\left(d\right)\right)$$
60	43 48	fvco3d	$$⊢\left(\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}\right)\to \left(H\circ G\right)\left(k{-}_{f}d\right)=H\left(G\left(k{-}_{f}d\right)\right)$$
61	59 60	oveq12d	$$⊢\left(\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}\right)\to \left(H\circ F\right)\left(d\right){\cdot }_S\left(H\circ G\right)\left(k{-}_{f}d\right)=H\left(F\left(d\right)\right){\cdot }_{S}H\left(G\left(k{-}_{f}d\right)\right)$$
62	56 61	eqtr4d	$$⊢\left(\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}\right)\to H\left(F\left(d\right){\cdot }_{R}G\left(k{-}_{f}d\right)\right)=\left(H\circ F\right)\left(d\right){\cdot }_S\left(H\circ G\right)\left(k{-}_{f}d\right)$$
63	62	mpteq2dva	$$⊢\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}⟼H\left(F\left(d\right){\cdot }_{R}G\left(k{-}_{f}d\right)\right)\right)=\left(d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}⟼\left(H\circ F\right)\left(d\right){\cdot }_S\left(H\circ G\right)\left(k{-}_{f}d\right)\right)$$
64	63	oveq2d	$$⊢\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \underset{d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}}{{\sum }_S}H\left(F\left(d\right){\cdot }_{R}G\left(k{-}_{f}d\right)\right)=\underset{d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}}{{\sum }_S}\left(\left(H\circ F\right)\left(d\right){\cdot }_S\left(H\circ G\right)\left(k{-}_{f}d\right)\right)$$
65	52 64	eqtr3d	$$⊢\left(\phi \wedge k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to H\left(\underset{d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}}{{\sum }_R}\left(F\left(d\right){\cdot }_{R}G\left(k{-}_{f}d\right)\right)\right)=\underset{d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}}{{\sum }_S}\left(\left(H\circ F\right)\left(d\right){\cdot }_S\left(H\circ G\right)\left(k{-}_{f}d\right)\right)$$
66	65	mpteq2dva	$$⊢\phi \to \left(k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼H\left(\underset{d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}}{{\sum }_R}\left(F\left(d\right){\cdot }_{R}G\left(k{-}_{f}d\right)\right)\right)\right)=\left(k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}}{{\sum }_S}\left(\left(H\circ F\right)\left(d\right){\cdot }_S\left(H\circ G\right)\left(k{-}_{f}d\right)\right)\right)$$
67	20 66	eqtrd	$$⊢\phi \to H\circ \left(k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}}{{\sum }_R}\left(F\left(d\right){\cdot }_{R}G\left(k{-}_{f}d\right)\right)\right)=\left(k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}}{{\sum }_S}\left(\left(H\circ F\right)\left(d\right){\cdot }_S\left(H\circ G\right)\left(k{-}_{f}d\right)\right)\right)$$
68	1 3 37 5 14 8 9	mplmul	$$⊢\phi \to F\underset{\dot{}}{·}G=\left(k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}}{{\sum }_R}\left(F\left(d\right){\cdot }_{R}G\left(k{-}_{f}d\right)\right)\right)$$
69	68	coeq2d	$$⊢\phi \to H\circ \left(F\underset{\dot{}}{·}G\right)=H\circ \left(k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}}{{\sum }_R}\left(F\left(d\right){\cdot }_{R}G\left(k{-}_{f}d\right)\right)\right)$$
70	1 2 3 4 35 8	mhmcompl	$$⊢\phi \to H\circ F\in C$$
71	1 2 3 4 35 9	mhmcompl	$$⊢\phi \to H\circ G\in C$$
72	2 4 54 6 14 70 71	mplmul	$$⊢\phi \to \left(H\circ F\right)\underset{\dot{}}{\bullet }\left(H\circ G\right)=\left(k\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼\underset{d\in \left\{e\in \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}|e{\le }_{f}k\right\}}{{\sum }_S}\left(\left(H\circ F\right)\left(d\right){\cdot }_S\left(H\circ G\right)\left(k{-}_{f}d\right)\right)\right)$$
73	67 69 72	3eqtr4d	$$⊢\phi \to H\circ \left(F\underset{\dot{}}{·}G\right)=\left(H\circ F\right)\underset{\dot{}}{\bullet }\left(H\circ G\right)$$