Theorem grpgimcanon

Description: The result of "canonicalizing" a group by discarding unneeded structural components and ensuring that the group operation is a binary operation is isomorphic to the original group. (Contributed by Eric Schmidt, 24-Oct-2026)

	Ref	Expression
Hypotheses	grpgimcanon.1	$$⊢B={\mathrm{Base}}_G$$
	grpgimcanon.2	$$⊢\underset{\dot{}}{⨣}={+}_{𝑓}\left(G\right)$$
	grpgimcanon.3	$$⊢H=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{⨣}⟩\right\}$$
Assertion	grpgimcanon	$$⊢G\in \mathrm{Grp}\to {\mathrm{I}\upharpoonright }_B\in \left(G\mathrm{GrpIso}H\right)$$

Proof

Step	Hyp	Ref	Expression
1		grpgimcanon.1	$$⊢B={\mathrm{Base}}_G$$
2		grpgimcanon.2	$$⊢\underset{\dot{}}{⨣}={+}_{𝑓}\left(G\right)$$
3		grpgimcanon.3	$$⊢H=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{⨣}⟩\right\}$$
4	1	idghm	$$⊢G\in \mathrm{Grp}\to {\mathrm{I}\upharpoonright }_B\in \left(G\mathrm{GrpHom}G\right)$$
5	1	a1i	$$⊢G\in \mathrm{Grp}\to B={\mathrm{Base}}_G$$
6	1	fvexi	$$⊢B\in \mathrm{V}$$
7	3	grpbase	$$⊢B\in \mathrm{V}\to B={\mathrm{Base}}_H$$
8	6 7	ax-mp	$$⊢B={\mathrm{Base}}_H$$
9	8	a1i	$$⊢G\in \mathrm{Grp}\to B={\mathrm{Base}}_H$$
10		eqidd	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{G}y=x{+}_{G}y$$
11		eqid	$$⊢{+}_G={+}_G$$
12	1 11 2	plusfval	$$⊢\left(x\in B\wedge y\in B\right)\to x\underset{\dot{}}{⨣}y=x{+}_{G}y$$
13	12	adantl	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge y\in B\right)\right)\to x\underset{\dot{}}{⨣}y=x{+}_{G}y$$
14	1 2	grpplusf	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{⨣}:B\times B⟶B$$
15	6 6	xpex	$$⊢B\times B\in \mathrm{V}$$
16		fex2	$$⊢\left(\underset{\dot{}}{⨣}:B\times B⟶B\wedge B\times B\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \underset{\dot{}}{⨣}\in \mathrm{V}$$
17	15 6 16	mp3an23	$$⊢\underset{\dot{}}{⨣}:B\times B⟶B\to \underset{\dot{}}{⨣}\in \mathrm{V}$$
18	3	grpplusg	$$⊢\underset{\dot{}}{⨣}\in \mathrm{V}\to \underset{\dot{}}{⨣}={+}_H$$
19	14 17 18	3syl	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{⨣}={+}_H$$
20	19	oveqdr	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge y\in B\right)\right)\to x\underset{\dot{}}{⨣}y=x{+}_{H}y$$
21	13 20	eqtr3d	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{G}y=x{+}_{H}y$$
22	5 5 5 9 10 21	ghmpropd	$$⊢G\in \mathrm{Grp}\to G\mathrm{GrpHom}G=G\mathrm{GrpHom}H$$
23	4 22	eleqtrd	$$⊢G\in \mathrm{Grp}\to {\mathrm{I}\upharpoonright }_B\in \left(G\mathrm{GrpHom}H\right)$$
24		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_B\right):B\underset{1-1\; onto}{⟶}B$$
25	1 8	isgim	$$⊢{\mathrm{I}\upharpoonright }_B\in \left(G\mathrm{GrpIso}H\right)\leftrightarrow \left({\mathrm{I}\upharpoonright }_B\in \left(G\mathrm{GrpHom}H\right)\wedge \left({\mathrm{I}\upharpoonright }_B\right):B\underset{1-1\; onto}{⟶}B\right)$$
26	23 24 25	sylanblrc	$$⊢G\in \mathrm{Grp}\to {\mathrm{I}\upharpoonright }_B\in \left(G\mathrm{GrpIso}H\right)$$