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.i	$$⊢\phi \to I\in V$$
	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.i	$$⊢\phi \to I\in V$$
8		mhmcoaddmpl.h	$$⊢\phi \to H\in \left(R\mathrm{MndHom}S\right)$$
9		mhmcoaddmpl.f	$$⊢\phi \to F\in B$$
10		mhmcoaddmpl.g	$$⊢\phi \to G\in B$$
11		fvexd	$$⊢\phi \to {\mathrm{Base}}_R\in \mathrm{V}$$
12		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
13	12	rabex	$$⊢\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
14	13	a1i	$$⊢\phi \to \left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
15		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
16		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\}$$
17	1 15 3 16 9	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	11 14 17	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)$$
19	1 15 3 16 10	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$$
20	11 14 19	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)$$
21		eqid	$$⊢{+}_R={+}_R$$
22		eqid	$$⊢{+}_S={+}_S$$
23	15 21 22	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)$$
24	8 18 20 23	syl3anc	$$⊢\phi \to H\circ \left(F{{+}_R}_{f}G\right)=\left(H\circ F\right){{+}_S}_f\left(H\circ G\right)$$
25	1 3 21 5 9 10	mpladd	$$⊢\phi \to F\underset{\dot{}}{+}G=F{{+}_R}_{f}G$$
26	25	coeq2d	$$⊢\phi \to H\circ \left(F\underset{\dot{}}{+}G\right)=H\circ \left(F{{+}_R}_{f}G\right)$$
27	1 2 3 4 7 8 9	mhmcompl	$$⊢\phi \to H\circ F\in C$$
28	1 2 3 4 7 8 10	mhmcompl	$$⊢\phi \to H\circ G\in C$$
29	2 4 22 6 27 28	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)$$
30	24 26 29	3eqtr4d	$$⊢\phi \to H\circ \left(F\underset{\dot{}}{+}G\right)=\left(H\circ F\right)\underset{\dot{}}{✚}\left(H\circ G\right)$$