Theorem mhmcoaddmpl

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

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

Proof

Step	Hyp	Ref	Expression
1		mhmcoaddmpl.p	$$⊢P=I\mathrm{mPoly}R$$
2		mhmcoaddmpl.q	$$⊢Q=I\mathrm{mPoly}S$$
3		mhmcoaddmpl.b	$$⊢B={\mathrm{Base}}_P$$
4		mhmcoaddmpl.c	$$⊢C={\mathrm{Base}}_Q$$
5		mhmcoaddmpl.1	$$⊢\underset{\dot{}}{+}={+}_P$$
6		mhmcoaddmpl.2	$$⊢\underset{\dot{}}{✚}={+}_Q$$
7		mhmcoaddmpl.h	$$⊢\phi \to H\in \left(R\mathrm{MndHom}S\right)$$
8		mhmcoaddmpl.f	$$⊢\phi \to F\in B$$
9		mhmcoaddmpl.g	$$⊢\phi \to G\in B$$
10		fvexd	$$⊢\phi \to {\mathrm{Base}}_R\in \mathrm{V}$$
11		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\}$$
12		ovexd	$$⊢\phi \to {{\mathbb{N}}_0}^I\in \mathrm{V}$$
13	11 12	rabexd	$$⊢\phi \to \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
14		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
15	1 14 3 11 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$$
16	10 13 15	elmapdd	$$⊢\phi \to F\in \left({{\mathrm{Base}}_R}^{\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}\right)$$
17	1 14 3 11 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$$
18	10 13 17	elmapdd	$$⊢\phi \to G\in \left({{\mathrm{Base}}_R}^{\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}\right)$$
19		eqid	$$⊢{+}_R={+}_R$$
20		eqid	$$⊢{+}_S={+}_S$$
21	14 19 20	mhmvlin	$$⊢\left(H\in \left(R\mathrm{MndHom}S\right)\wedge F\in \left({{\mathrm{Base}}_R}^{\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}\right)\wedge G\in \left({{\mathrm{Base}}_R}^{\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}\right)\right)\to H\circ \left(F{{+}_R}_{f}G\right)=\left(H\circ F\right){{+}_S}_f\left(H\circ G\right)$$
22	7 16 18 21	syl3anc	$$⊢\phi \to H\circ \left(F{{+}_R}_{f}G\right)=\left(H\circ F\right){{+}_S}_f\left(H\circ G\right)$$
23	1 3 19 5 8 9	mpladd	$$⊢\phi \to F\underset{\dot{}}{+}G=F{{+}_R}_{f}G$$
24	23	coeq2d	$$⊢\phi \to H\circ \left(F\underset{\dot{}}{+}G\right)=H\circ \left(F{{+}_R}_{f}G\right)$$
25	1 2 3 4 7 8	mhmcompl	$$⊢\phi \to H\circ F\in C$$
26	1 2 3 4 7 9	mhmcompl	$$⊢\phi \to H\circ G\in C$$
27	2 4 20 6 25 26	mpladd	$$⊢\phi \to \left(H\circ F\right)\underset{\dot{}}{✚}\left(H\circ G\right)=\left(H\circ F\right){{+}_S}_f\left(H\circ G\right)$$
28	22 24 27	3eqtr4d	$$⊢\phi \to H\circ \left(F\underset{\dot{}}{+}G\right)=\left(H\circ F\right)\underset{\dot{}}{✚}\left(H\circ G\right)$$