Theorem imasmgm2

Description: The image structure of a unital magma is a unital magma. (Contributed by Thierry Arnoux, 31-Aug-2026)

	Ref	Expression
Hypotheses	imasmgm.u	$$⊢\phi \to U=F{“}_{𝑠}R$$
	imasmgm.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
	imasmgm.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	imasmgm.f	$$⊢\phi \to F:V\underset{onto}{⟶}B$$
	imasmgm.e	$$⊢\left(\phi \wedge \left(a\in V\wedge b\in V\right)\wedge \left(p\in V\wedge q\in V\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)$$
	imasmgm2.r	$$⊢\phi \to R\in W$$
	imasmgm2.1	$$⊢\left(\phi \wedge x\in V\wedge y\in V\right)\to x\underset{\dot{}}{+}y\in V$$
	imasmgm2.2	$$⊢\phi \to \underset{\dot{}}{0}\in V$$
	imasmgm2.3	$$⊢\left(\phi \wedge x\in V\right)\to F\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x\right)=F\left(x\right)$$
	imasmgm2.4	$$⊢\left(\phi \wedge x\in V\right)\to F\left(x\underset{\dot{}}{+}\underset{\dot{}}{0}\right)=F\left(x\right)$$
Assertion	imasmgm2	$$⊢\phi \to \left(U\in \mathrm{Mgm}\wedge F\left(\underset{\dot{}}{0}\right)=0_U\right)$$

Proof

Step	Hyp	Ref	Expression
1		imasmgm.u	$$⊢\phi \to U=F{“}_{𝑠}R$$
2		imasmgm.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
3		imasmgm.p	$$⊢\underset{\dot{}}{+}={+}_R$$
4		imasmgm.f	$$⊢\phi \to F:V\underset{onto}{⟶}B$$
5		imasmgm.e	$$⊢\left(\phi \wedge \left(a\in V\wedge b\in V\right)\wedge \left(p\in V\wedge q\in V\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)$$
6		imasmgm2.r	$$⊢\phi \to R\in W$$
7		imasmgm2.1	$$⊢\left(\phi \wedge x\in V\wedge y\in V\right)\to x\underset{\dot{}}{+}y\in V$$
8		imasmgm2.2	$$⊢\phi \to \underset{\dot{}}{0}\in V$$
9		imasmgm2.3	$$⊢\left(\phi \wedge x\in V\right)\to F\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x\right)=F\left(x\right)$$
10		imasmgm2.4	$$⊢\left(\phi \wedge x\in V\right)\to F\left(x\underset{\dot{}}{+}\underset{\dot{}}{0}\right)=F\left(x\right)$$
11	1 2 4 6	imasbas	$$⊢\phi \to B={\mathrm{Base}}_U$$
12		ovex	$$⊢F{“}_{𝑠}R\in \mathrm{V}$$
13	1 12	eqeltrdi	$$⊢\phi \to U\in \mathrm{V}$$
14		eqidd	$$⊢\phi \to {+}_U={+}_U$$
15		eqid	$$⊢{+}_U={+}_U$$
16	7	3expb	$$⊢\left(\phi \wedge \left(x\in V\wedge y\in V\right)\right)\to x\underset{\dot{}}{+}y\in V$$
17	16	caovclg	$$⊢\left(\phi \wedge \left(p\in V\wedge q\in V\right)\right)\to p\underset{\dot{}}{+}q\in V$$
18	4 5 1 2 6 3 15 17	imasaddf	$$⊢\phi \to {+}_U:B\times B⟶B$$
19	18	fovcld	$$⊢\left(\phi \wedge u\in B\wedge v\in B\right)\to u{+}_{U}v\in B$$
20	11 13 14 19	ismgmd	$$⊢\phi \to U\in \mathrm{Mgm}$$
21		fof	$$⊢F:V\underset{onto}{⟶}B\to F:V⟶B$$
22	4 21	syl	$$⊢\phi \to F:V⟶B$$
23	22 8	ffvelcdmd	$$⊢\phi \to F\left(\underset{\dot{}}{0}\right)\in B$$
24		forn	$$⊢F:V\underset{onto}{⟶}B\to \mathrm{ran}F=B$$
25	4 24	syl	$$⊢\phi \to \mathrm{ran}F=B$$
26	25	eleq2d	$$⊢\phi \to \left(u\in \mathrm{ran}F\leftrightarrow u\in B\right)$$
27		fofn	$$⊢F:V\underset{onto}{⟶}B\to FFnV$$
28		fvelrnb	$$⊢FFnV\to \left(u\in \mathrm{ran}F\leftrightarrow \exists x\in VF\left(x\right)=u\right)$$
29	4 27 28	3syl	$$⊢\phi \to \left(u\in \mathrm{ran}F\leftrightarrow \exists x\in VF\left(x\right)=u\right)$$
30	26 29	bitr3d	$$⊢\phi \to \left(u\in B\leftrightarrow \exists x\in VF\left(x\right)=u\right)$$
31		simpl	$$⊢\left(\phi \wedge x\in V\right)\to \phi$$
32	8	adantr	$$⊢\left(\phi \wedge x\in V\right)\to \underset{\dot{}}{0}\in V$$
33		simpr	$$⊢\left(\phi \wedge x\in V\right)\to x\in V$$
34	4 5 1 2 6 3 15	imasaddval	$$⊢\left(\phi \wedge \underset{\dot{}}{0}\in V\wedge x\in V\right)\to F\left(\underset{\dot{}}{0}\right){+}_{U}F\left(x\right)=F\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x\right)$$
35	31 32 33 34	syl3anc	$$⊢\left(\phi \wedge x\in V\right)\to F\left(\underset{\dot{}}{0}\right){+}_{U}F\left(x\right)=F\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x\right)$$
36	35 9	eqtrd	$$⊢\left(\phi \wedge x\in V\right)\to F\left(\underset{\dot{}}{0}\right){+}_{U}F\left(x\right)=F\left(x\right)$$
37		oveq2	$$⊢F\left(x\right)=u\to F\left(\underset{\dot{}}{0}\right){+}_{U}F\left(x\right)=F\left(\underset{\dot{}}{0}\right){+}_{U}u$$
38		id	$$⊢F\left(x\right)=u\to F\left(x\right)=u$$
39	37 38	eqeq12d	$$⊢F\left(x\right)=u\to \left(F\left(\underset{\dot{}}{0}\right){+}_{U}F\left(x\right)=F\left(x\right)\leftrightarrow F\left(\underset{\dot{}}{0}\right){+}_{U}u=u\right)$$
40	36 39	syl5ibcom	$$⊢\left(\phi \wedge x\in V\right)\to \left(F\left(x\right)=u\to F\left(\underset{\dot{}}{0}\right){+}_{U}u=u\right)$$
41	40	rexlimdva	$$⊢\phi \to \left(\exists x\in VF\left(x\right)=u\to F\left(\underset{\dot{}}{0}\right){+}_{U}u=u\right)$$
42	30 41	sylbid	$$⊢\phi \to \left(u\in B\to F\left(\underset{\dot{}}{0}\right){+}_{U}u=u\right)$$
43	42	imp	$$⊢\left(\phi \wedge u\in B\right)\to F\left(\underset{\dot{}}{0}\right){+}_{U}u=u$$
44	4 5 1 2 6 3 15	imasaddval	$$⊢\left(\phi \wedge x\in V\wedge \underset{\dot{}}{0}\in V\right)\to F\left(x\right){+}_{U}F\left(\underset{\dot{}}{0}\right)=F\left(x\underset{\dot{}}{+}\underset{\dot{}}{0}\right)$$
45	32 44	mpd3an3	$$⊢\left(\phi \wedge x\in V\right)\to F\left(x\right){+}_{U}F\left(\underset{\dot{}}{0}\right)=F\left(x\underset{\dot{}}{+}\underset{\dot{}}{0}\right)$$
46	45 10	eqtrd	$$⊢\left(\phi \wedge x\in V\right)\to F\left(x\right){+}_{U}F\left(\underset{\dot{}}{0}\right)=F\left(x\right)$$
47		oveq1	$$⊢F\left(x\right)=u\to F\left(x\right){+}_{U}F\left(\underset{\dot{}}{0}\right)=u{+}_{U}F\left(\underset{\dot{}}{0}\right)$$
48	47 38	eqeq12d	$$⊢F\left(x\right)=u\to \left(F\left(x\right){+}_{U}F\left(\underset{\dot{}}{0}\right)=F\left(x\right)\leftrightarrow u{+}_{U}F\left(\underset{\dot{}}{0}\right)=u\right)$$
49	46 48	syl5ibcom	$$⊢\left(\phi \wedge x\in V\right)\to \left(F\left(x\right)=u\to u{+}_{U}F\left(\underset{\dot{}}{0}\right)=u\right)$$
50	49	rexlimdva	$$⊢\phi \to \left(\exists x\in VF\left(x\right)=u\to u{+}_{U}F\left(\underset{\dot{}}{0}\right)=u\right)$$
51	30 50	sylbid	$$⊢\phi \to \left(u\in B\to u{+}_{U}F\left(\underset{\dot{}}{0}\right)=u\right)$$
52	51	imp	$$⊢\left(\phi \wedge u\in B\right)\to u{+}_{U}F\left(\underset{\dot{}}{0}\right)=u$$
53	11 14 23 43 52	grpidd	$$⊢\phi \to F\left(\underset{\dot{}}{0}\right)=0_U$$
54	20 53	jca	$$⊢\phi \to \left(U\in \mathrm{Mgm}\wedge F\left(\underset{\dot{}}{0}\right)=0_U\right)$$