Theorem ismhmd

Description: Deduction version of ismhm . (Contributed by SN, 27-Jul-2024)

	Ref	Expression
Hypotheses	ismhmd.b	$$⊢B={\mathrm{Base}}_S$$
	ismhmd.c	$$⊢C={\mathrm{Base}}_T$$
	ismhmd.p	$$⊢\underset{\dot{}}{+}={+}_S$$
	ismhmd.q	$$⊢\underset{\dot{}}{⨣}={+}_T$$
	ismhmd.0	$$⊢\underset{\dot{}}{0}=0_S$$
	ismhmd.z	$$⊢Z=0_T$$
	ismhmd.s	$$⊢\phi \to S\in \mathrm{Mnd}$$
	ismhmd.t	$$⊢\phi \to T\in \mathrm{Mnd}$$
	ismhmd.f	$$⊢\phi \to F:B⟶C$$
	ismhmd.a	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to F\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)$$
	ismhmd.h	$$⊢\phi \to F\left(\underset{\dot{}}{0}\right)=Z$$
Assertion	ismhmd	$$⊢\phi \to F\in \left(S\mathrm{MndHom}T\right)$$

Proof

Step	Hyp	Ref	Expression
1		ismhmd.b	$$⊢B={\mathrm{Base}}_S$$
2		ismhmd.c	$$⊢C={\mathrm{Base}}_T$$
3		ismhmd.p	$$⊢\underset{\dot{}}{+}={+}_S$$
4		ismhmd.q	$$⊢\underset{\dot{}}{⨣}={+}_T$$
5		ismhmd.0	$$⊢\underset{\dot{}}{0}=0_S$$
6		ismhmd.z	$$⊢Z=0_T$$
7		ismhmd.s	$$⊢\phi \to S\in \mathrm{Mnd}$$
8		ismhmd.t	$$⊢\phi \to T\in \mathrm{Mnd}$$
9		ismhmd.f	$$⊢\phi \to F:B⟶C$$
10		ismhmd.a	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to F\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)$$
11		ismhmd.h	$$⊢\phi \to F\left(\underset{\dot{}}{0}\right)=Z$$
12	10	ralrimivva	$$⊢\phi \to \forall x\in B\forall y\in BF\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)$$
13	9 12 11	3jca	$$⊢\phi \to \left(F:B⟶C\wedge \forall x\in B\forall y\in BF\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)\wedge F\left(\underset{\dot{}}{0}\right)=Z\right)$$
14	1 2 3 4 5 6	ismhm	$$⊢F\in \left(S\mathrm{MndHom}T\right)\leftrightarrow \left(\left(S\in \mathrm{Mnd}\wedge T\in \mathrm{Mnd}\right)\wedge \left(F:B⟶C\wedge \forall x\in B\forall y\in BF\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)\wedge F\left(\underset{\dot{}}{0}\right)=Z\right)\right)$$
15	7 8 13 14	syl21anbrc	$$⊢\phi \to F\in \left(S\mathrm{MndHom}T\right)$$