Metamath Proof Explorer

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 = ( Base ` G )
grpgimcanon.2 
|- .+^ = ( +f ` G )
grpgimcanon.3 
|- H = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+^ >. }
Assertion grpgimcanon 
|- ( G e. Grp -> ( _I |` B ) e. ( G GrpIso H ) )

Proof

Step Hyp Ref Expression
1 grpgimcanon.1 
 |-  B = ( Base ` G )
2 grpgimcanon.2 
 |-  .+^ = ( +f ` G )
3 grpgimcanon.3 
 |-  H = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+^ >. }
4 1 idghm 
 |-  ( G e. Grp -> ( _I |` B ) e. ( G GrpHom G ) )
5 1 a1i 
 |-  ( G e. Grp -> B = ( Base ` G ) )
6 1 fvexi 
 |-  B e. _V
7 3 grpbase 
 |-  ( B e. _V -> B = ( Base ` H ) )
8 6 7 ax-mp 
 |-  B = ( Base ` H )
9 8 a1i 
 |-  ( G e. Grp -> B = ( Base ` H ) )
10 eqidd 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` G ) y ) )
11 eqid 
 |-  ( +g ` G ) = ( +g ` G )
12 1 11 2 plusfval 
 |-  ( ( x e. B /\ y e. B ) -> ( x .+^ y ) = ( x ( +g ` G ) y ) )
13 12 adantl 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( x .+^ y ) = ( x ( +g ` G ) y ) )
14 1 2 grpplusf 
 |-  ( G e. Grp -> .+^ : ( B X. B ) --> B )
15 6 6 xpex 
 |-  ( B X. B ) e. _V
16 fex2 
 |-  ( ( .+^ : ( B X. B ) --> B /\ ( B X. B ) e. _V /\ B e. _V ) -> .+^ e. _V )
17 15 6 16 mp3an23 
 |-  ( .+^ : ( B X. B ) --> B -> .+^ e. _V )
18 3 grpplusg 
 |-  ( .+^ e. _V -> .+^ = ( +g ` H ) )
19 14 17 18 3syl 
 |-  ( G e. Grp -> .+^ = ( +g ` H ) )
20 19 oveqdr 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( x .+^ y ) = ( x ( +g ` H ) y ) )
21 13 20 eqtr3d 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` H ) y ) )
22 5 5 5 9 10 21 ghmpropd 
 |-  ( G e. Grp -> ( G GrpHom G ) = ( G GrpHom H ) )
23 4 22 eleqtrd 
 |-  ( G e. Grp -> ( _I |` B ) e. ( G GrpHom H ) )
24 f1oi 
 |-  ( _I |` B ) : B -1-1-onto-> B
25 1 8 isgim 
 |-  ( ( _I |` B ) e. ( G GrpIso H ) <-> ( ( _I |` B ) e. ( G GrpHom H ) /\ ( _I |` B ) : B -1-1-onto-> B ) )
26 23 24 25 sylanblrc 
 |-  ( G e. Grp -> ( _I |` B ) e. ( G GrpIso H ) )