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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	grpgimcanon.2	⊢ ⨣ = ( +𝑓 ‘ 𝐺 )
	grpgimcanon.3	⊢ 𝐻 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ }
Assertion	grpgimcanon	⊢ ( 𝐺 ∈ Grp → ( I ↾ 𝐵 ) ∈ ( 𝐺 GrpIso 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		grpgimcanon.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		grpgimcanon.2	⊢ ⨣ = ( +𝑓 ‘ 𝐺 )
3		grpgimcanon.3	⊢ 𝐻 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ }
4	1	idghm	⊢ ( 𝐺 ∈ Grp → ( I ↾ 𝐵 ) ∈ ( 𝐺 GrpHom 𝐺 ) )
5	1	a1i	⊢ ( 𝐺 ∈ Grp → 𝐵 = ( Base ‘ 𝐺 ) )
6	1	fvexi	⊢ 𝐵 ∈ V
7	3	grpbase	⊢ ( 𝐵 ∈ V → 𝐵 = ( Base ‘ 𝐻 ) )
8	6 7	ax-mp	⊢ 𝐵 = ( Base ‘ 𝐻 )
9	8	a1i	⊢ ( 𝐺 ∈ Grp → 𝐵 = ( Base ‘ 𝐻 ) )
10		eqidd	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
11		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
12	1 11 2	plusfval	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ⨣ 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
13	12	adantl	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ⨣ 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
14	1 2	grpplusf	⊢ ( 𝐺 ∈ Grp → ⨣ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
15	6 6	xpex	⊢ ( 𝐵 × 𝐵 ) ∈ V
16		fex2	⊢ ( ( ⨣ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ∧ ( 𝐵 × 𝐵 ) ∈ V ∧ 𝐵 ∈ V ) → ⨣ ∈ V )
17	15 6 16	mp3an23	⊢ ( ⨣ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 → ⨣ ∈ V )
18	3	grpplusg	⊢ ( ⨣ ∈ V → ⨣ = ( +g ‘ 𝐻 ) )
19	14 17 18	3syl	⊢ ( 𝐺 ∈ Grp → ⨣ = ( +g ‘ 𝐻 ) )
20	19	oveqdr	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ⨣ 𝑦 ) = ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) )
21	13 20	eqtr3d	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐻 ) 𝑦 ) )
22	5 5 5 9 10 21	ghmpropd	⊢ ( 𝐺 ∈ Grp → ( 𝐺 GrpHom 𝐺 ) = ( 𝐺 GrpHom 𝐻 ) )
23	4 22	eleqtrd	⊢ ( 𝐺 ∈ Grp → ( I ↾ 𝐵 ) ∈ ( 𝐺 GrpHom 𝐻 ) )
24		f1oi	⊢ ( I ↾ 𝐵 ) : 𝐵 ⟶1-1onto 𝐵
25	1 8	isgim	⊢ ( ( I ↾ 𝐵 ) ∈ ( 𝐺 GrpIso 𝐻 ) ↔ ( ( I ↾ 𝐵 ) ∈ ( 𝐺 GrpHom 𝐻 ) ∧ ( I ↾ 𝐵 ) : 𝐵 ⟶1-1onto 𝐵 ) )
26	23 24 25	sylanblrc	⊢ ( 𝐺 ∈ Grp → ( I ↾ 𝐵 ) ∈ ( 𝐺 GrpIso 𝐻 ) )