Metamath Proof Explorer

Theorem imasmhm

Description: Given a function F with homomorphic properties, build the image of a monoid. (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 ) ) ) )
imasmhm.w 
|- ( ph -> W e. Mnd )
Assertion imasmhm 
|- ( ph -> ( ( F "s W ) e. Mnd /\ F e. ( W MndHom ( 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 imasmhm.w 
 |-  ( ph -> W e. Mnd )
6 eqidd 
 |-  ( ph -> ( F "s W ) = ( F "s W ) )
7 1 a1i 
 |-  ( ph -> B = ( Base ` W ) )
8 fimadmfo 
 |-  ( F : B --> C -> F : B -onto-> ( F " B ) )
9 2 8 syl 
 |-  ( ph -> F : B -onto-> ( F " B ) )
10 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
11 6 7 3 9 4 5 10 imasmnd 
 |-  ( ph -> ( ( F "s W ) e. Mnd /\ ( F ` ( 0g ` W ) ) = ( 0g ` ( F "s W ) ) ) )
12 11 simpld 
 |-  ( ph -> ( F "s W ) e. Mnd )
13 eqid 
 |-  ( Base ` ( F "s W ) ) = ( Base ` ( F "s W ) )
14 eqid 
 |-  ( +g ` ( F "s W ) ) = ( +g ` ( F "s W ) )
15 eqid 
 |-  ( 0g ` ( F "s W ) ) = ( 0g ` ( F "s W ) )
16 fof 
 |-  ( F : B -onto-> ( F " B ) -> F : B --> ( F " B ) )
17 9 16 syl 
 |-  ( ph -> F : B --> ( F " B ) )
18 6 7 9 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 9 4 6 7 5 3 14 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 11 simprd 
 |-  ( ph -> ( F ` ( 0g ` W ) ) = ( 0g ` ( F "s W ) ) )
25 1 13 3 14 10 15 5 12 20 23 24 ismhmd 
 |-  ( ph -> F e. ( W MndHom ( F "s W ) ) )
26 12 25 jca 
 |-  ( ph -> ( ( F "s W ) e. Mnd /\ F e. ( W MndHom ( F "s W ) ) ) )