Theorem mhmcoaddpsr

Description: Show that the ring homomorphism in rhmpsr preserves addition. (Contributed by SN, 18-May-2025)

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