Metamath Proof Explorer

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 = ( Base ` W )
imasmhm.f 
|- ( ph -> F : B --> C )
imasmhm.1 
|- .+ = ( +g ` W )
imasmhm.2 
|- ( ( ph /\ ( a e. B /\ b e. B ) /\ ( p e. B /\ q e. B ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) ) )
imasghm.w 
|- ( ph -> W e. Grp )
Assertion imasghm 
|- ( ph -> ( ( F "s W ) e. Grp /\ F e. ( W GrpHom ( F "s W ) ) ) )

Proof

Step Hyp Ref Expression
1 imasmhm.b 
 |-  B = ( Base ` W )
2 imasmhm.f 
 |-  ( ph -> F : B --> C )
3 imasmhm.1 
 |-  .+ = ( +g ` W )
4 imasmhm.2 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) /\ ( p e. B /\ q e. B ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) ) )
5 imasghm.w 
 |-  ( ph -> W e. Grp )
6 eqidd 
 |-  ( ph -> ( F "s W ) = ( F "s W ) )
7 1 a1i 
 |-  ( ph -> B = ( Base ` W ) )
8 3 a1i 
 |-  ( ph -> .+ = ( +g ` W ) )
9 fimadmfo 
 |-  ( F : B --> C -> F : B -onto-> ( F " B ) )
10 2 9 syl 
 |-  ( ph -> F : B -onto-> ( F " B ) )
11 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
12 6 7 8 10 4 5 11 imasgrp 
 |-  ( ph -> ( ( F "s W ) e. Grp /\ ( F ` ( 0g ` W ) ) = ( 0g ` ( F "s W ) ) ) )
13 12 simpld 
 |-  ( ph -> ( F "s W ) e. Grp )
14 eqid 
 |-  ( Base ` ( F "s W ) ) = ( Base ` ( F "s W ) )
15 eqid 
 |-  ( +g ` ( F "s W ) ) = ( +g ` ( F "s W ) )
16 fof 
 |-  ( F : B -onto-> ( F " B ) -> F : B --> ( F " B ) )
17 10 16 syl 
 |-  ( ph -> F : B --> ( F " B ) )
18 6 7 10 5 imasbas 
 |-  ( ph -> ( F " B ) = ( Base ` ( F "s W ) ) )
19 18 feq3d 
 |-  ( ph -> ( F : B --> ( F " B ) <-> F : B --> ( Base ` ( F "s W ) ) ) )
20 17 19 mpbid 
 |-  ( ph -> F : B --> ( Base ` ( F "s W ) ) )
21 10 4 6 7 5 3 15 imasaddval 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( ( F ` x ) ( +g ` ( F "s W ) ) ( F ` y ) ) = ( F ` ( x .+ y ) ) )
22 21 3expb 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( F ` x ) ( +g ` ( F "s W ) ) ( F ` y ) ) = ( F ` ( x .+ y ) ) )
23 22 eqcomd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) ( +g ` ( F "s W ) ) ( F ` y ) ) )
24 1 14 3 15 5 13 20 23 isghmd 
 |-  ( ph -> F e. ( W GrpHom ( F "s W ) ) )
25 13 24 jca 
 |-  ( ph -> ( ( F "s W ) e. Grp /\ F e. ( W GrpHom ( F "s W ) ) ) )