Theorem imasghm

Description: Given a function F with homomorphic properties, build the image of a group. (Contributed by Thierry Arnoux, 2-Apr-2025)

	Ref	Expression
Hypotheses	imasmhm.b	$$⊢B={\mathrm{Base}}_W$$
	imasmhm.f	$$⊢\phi \to F:B⟶C$$
	imasmhm.1	$$⊢\underset{\dot{}}{+}={+}_W$$
	imasmhm.2	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge \left(p\in B\wedge q\in B\right)\right)\to \left(\left(F\left(a\right)=F\left(p\right)\wedge F\left(b\right)=F\left(q\right)\right)\to F\left(a\underset{\dot{}}{+}b\right)=F\left(p\underset{\dot{}}{+}q\right)\right)$$
	imasghm.w	$$⊢\phi \to W\in \mathrm{Grp}$$
Assertion	imasghm	$$⊢\phi \to \left(F{“}_{𝑠}W\in \mathrm{Grp}\wedge F\in \left(W\mathrm{GrpHom}\left(F{“}_{𝑠}W\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		imasmhm.b	$$⊢B={\mathrm{Base}}_W$$
2		imasmhm.f	$$⊢\phi \to F:B⟶C$$
3		imasmhm.1	$$⊢\underset{\dot{}}{+}={+}_W$$
4		imasmhm.2	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge \left(p\in B\wedge q\in B\right)\right)\to \left(\left(F\left(a\right)=F\left(p\right)\wedge F\left(b\right)=F\left(q\right)\right)\to F\left(a\underset{\dot{}}{+}b\right)=F\left(p\underset{\dot{}}{+}q\right)\right)$$
5		imasghm.w	$$⊢\phi \to W\in \mathrm{Grp}$$
6		eqidd	$$⊢\phi \to F{“}_{𝑠}W=F{“}_{𝑠}W$$
7	1	a1i	$$⊢\phi \to B={\mathrm{Base}}_W$$
8	3	a1i	$$⊢\phi \to \underset{\dot{}}{+}={+}_W$$
9		fimadmfo	$$⊢F:B⟶C\to F:B\underset{onto}{⟶}F\left[B\right]$$
10	2 9	syl	$$⊢\phi \to F:B\underset{onto}{⟶}F\left[B\right]$$
11		eqid	$$⊢0_W=0_W$$
12	6 7 8 10 4 5 11	imasgrp	$$⊢\phi \to \left(F{“}_{𝑠}W\in \mathrm{Grp}\wedge F\left(0_W\right)=0_{\left(F{“}_{𝑠}W\right)}\right)$$
13	12	simpld	$$⊢\phi \to F{“}_{𝑠}W\in \mathrm{Grp}$$
14		eqid	$$⊢{\mathrm{Base}}_{\left(F{“}_{𝑠}W\right)}={\mathrm{Base}}_{\left(F{“}_{𝑠}W\right)}$$
15		eqid	$$⊢{+}_{\left(F{“}_{𝑠}W\right)}={+}_{\left(F{“}_{𝑠}W\right)}$$
16		fof	$$⊢F:B\underset{onto}{⟶}F\left[B\right]\to F:B⟶F\left[B\right]$$
17	10 16	syl	$$⊢\phi \to F:B⟶F\left[B\right]$$
18	6 7 10 5	imasbas	$$⊢\phi \to F\left[B\right]={\mathrm{Base}}_{\left(F{“}_{𝑠}W\right)}$$
19	18	feq3d	$$⊢\phi \to \left(F:B⟶F\left[B\right]\leftrightarrow F:B⟶{\mathrm{Base}}_{\left(F{“}_{𝑠}W\right)}\right)$$
20	17 19	mpbid	$$⊢\phi \to F:B⟶{\mathrm{Base}}_{\left(F{“}_{𝑠}W\right)}$$
21	10 4 6 7 5 3 15	imasaddval	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to F\left(x\right){+}_{\left(F{“}_{𝑠}W\right)}F\left(y\right)=F\left(x\underset{\dot{}}{+}y\right)$$
22	21	3expb	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to F\left(x\right){+}_{\left(F{“}_{𝑠}W\right)}F\left(y\right)=F\left(x\underset{\dot{}}{+}y\right)$$
23	22	eqcomd	$$⊢\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){+}_{\left(F{“}_{𝑠}W\right)}F\left(y\right)$$
24	1 14 3 15 5 13 20 23	isghmd	$$⊢\phi \to F\in \left(W\mathrm{GrpHom}\left(F{“}_{𝑠}W\right)\right)$$
25	13 24	jca	$$⊢\phi \to \left(F{“}_{𝑠}W\in \mathrm{Grp}\wedge F\in \left(W\mathrm{GrpHom}\left(F{“}_{𝑠}W\right)\right)\right)$$