This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ghmcmn

Description: The image of a commutative monoid G under a group homomorphism F is a commutative monoid. (Contributed by Thierry Arnoux, 26-Jan-2020)

Ref Expression
Hypotheses ghmabl.x 
|- X = ( Base ` G )
ghmabl.y 
|- Y = ( Base ` H )
ghmabl.p 
|- .+ = ( +g ` G )
ghmabl.q 
|- .+^ = ( +g ` H )
ghmabl.f 
|- ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
ghmabl.1 
|- ( ph -> F : X -onto-> Y )
ghmcmn.3 
|- ( ph -> G e. CMnd )
Assertion ghmcmn 
|- ( ph -> H e. CMnd )

Proof

Step Hyp Ref Expression
1 ghmabl.x 
 |-  X = ( Base ` G )
2 ghmabl.y 
 |-  Y = ( Base ` H )
3 ghmabl.p 
 |-  .+ = ( +g ` G )
4 ghmabl.q 
 |-  .+^ = ( +g ` H )
5 ghmabl.f 
 |-  ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
6 ghmabl.1 
 |-  ( ph -> F : X -onto-> Y )
7 ghmcmn.3 
 |-  ( ph -> G e. CMnd )
8 cmnmnd 
 |-  ( G e. CMnd -> G e. Mnd )
9 7 8 syl 
 |-  ( ph -> G e. Mnd )
10 5 1 2 3 4 6 9 mhmmnd 
 |-  ( ph -> H e. Mnd )
11 simp-6l 
 |-  ( ( ( ( ( ( ( ph /\ i e. Y ) /\ j e. Y ) /\ a e. X ) /\ ( F ` a ) = i ) /\ b e. X ) /\ ( F ` b ) = j ) -> ph )
12 11 7 syl 
 |-  ( ( ( ( ( ( ( ph /\ i e. Y ) /\ j e. Y ) /\ a e. X ) /\ ( F ` a ) = i ) /\ b e. X ) /\ ( F ` b ) = j ) -> G e. CMnd )
13 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ i e. Y ) /\ j e. Y ) /\ a e. X ) /\ ( F ` a ) = i ) /\ b e. X ) /\ ( F ` b ) = j ) -> a e. X )
14 simplr 
 |-  ( ( ( ( ( ( ( ph /\ i e. Y ) /\ j e. Y ) /\ a e. X ) /\ ( F ` a ) = i ) /\ b e. X ) /\ ( F ` b ) = j ) -> b e. X )
15 1 3 cmncom 
 |-  ( ( G e. CMnd /\ a e. X /\ b e. X ) -> ( a .+ b ) = ( b .+ a ) )
16 12 13 14 15 syl3anc 
 |-  ( ( ( ( ( ( ( ph /\ i e. Y ) /\ j e. Y ) /\ a e. X ) /\ ( F ` a ) = i ) /\ b e. X ) /\ ( F ` b ) = j ) -> ( a .+ b ) = ( b .+ a ) )
17 16 fveq2d 
 |-  ( ( ( ( ( ( ( ph /\ i e. Y ) /\ j e. Y ) /\ a e. X ) /\ ( F ` a ) = i ) /\ b e. X ) /\ ( F ` b ) = j ) -> ( F ` ( a .+ b ) ) = ( F ` ( b .+ a ) ) )
18 11 5 syl3an1 
 |-  ( ( ( ( ( ( ( ( ph /\ i e. Y ) /\ j e. Y ) /\ a e. X ) /\ ( F ` a ) = i ) /\ b e. X ) /\ ( F ` b ) = j ) /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
19 18 13 14 mhmlem 
 |-  ( ( ( ( ( ( ( ph /\ i e. Y ) /\ j e. Y ) /\ a e. X ) /\ ( F ` a ) = i ) /\ b e. X ) /\ ( F ` b ) = j ) -> ( F ` ( a .+ b ) ) = ( ( F ` a ) .+^ ( F ` b ) ) )
20 18 14 13 mhmlem 
 |-  ( ( ( ( ( ( ( ph /\ i e. Y ) /\ j e. Y ) /\ a e. X ) /\ ( F ` a ) = i ) /\ b e. X ) /\ ( F ` b ) = j ) -> ( F ` ( b .+ a ) ) = ( ( F ` b ) .+^ ( F ` a ) ) )
21 17 19 20 3eqtr3d 
 |-  ( ( ( ( ( ( ( ph /\ i e. Y ) /\ j e. Y ) /\ a e. X ) /\ ( F ` a ) = i ) /\ b e. X ) /\ ( F ` b ) = j ) -> ( ( F ` a ) .+^ ( F ` b ) ) = ( ( F ` b ) .+^ ( F ` a ) ) )
22 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ i e. Y ) /\ j e. Y ) /\ a e. X ) /\ ( F ` a ) = i ) /\ b e. X ) /\ ( F ` b ) = j ) -> ( F ` a ) = i )
23 simpr 
 |-  ( ( ( ( ( ( ( ph /\ i e. Y ) /\ j e. Y ) /\ a e. X ) /\ ( F ` a ) = i ) /\ b e. X ) /\ ( F ` b ) = j ) -> ( F ` b ) = j )
24 22 23 oveq12d 
 |-  ( ( ( ( ( ( ( ph /\ i e. Y ) /\ j e. Y ) /\ a e. X ) /\ ( F ` a ) = i ) /\ b e. X ) /\ ( F ` b ) = j ) -> ( ( F ` a ) .+^ ( F ` b ) ) = ( i .+^ j ) )
25 23 22 oveq12d 
 |-  ( ( ( ( ( ( ( ph /\ i e. Y ) /\ j e. Y ) /\ a e. X ) /\ ( F ` a ) = i ) /\ b e. X ) /\ ( F ` b ) = j ) -> ( ( F ` b ) .+^ ( F ` a ) ) = ( j .+^ i ) )
26 21 24 25 3eqtr3d 
 |-  ( ( ( ( ( ( ( ph /\ i e. Y ) /\ j e. Y ) /\ a e. X ) /\ ( F ` a ) = i ) /\ b e. X ) /\ ( F ` b ) = j ) -> ( i .+^ j ) = ( j .+^ i ) )
27 foelcdmi 
 |-  ( ( F : X -onto-> Y /\ j e. Y ) -> E. b e. X ( F ` b ) = j )
28 6 27 sylan 
 |-  ( ( ph /\ j e. Y ) -> E. b e. X ( F ` b ) = j )
29 28 ad5ant13 
 |-  ( ( ( ( ( ph /\ i e. Y ) /\ j e. Y ) /\ a e. X ) /\ ( F ` a ) = i ) -> E. b e. X ( F ` b ) = j )
30 26 29 r19.29a 
 |-  ( ( ( ( ( ph /\ i e. Y ) /\ j e. Y ) /\ a e. X ) /\ ( F ` a ) = i ) -> ( i .+^ j ) = ( j .+^ i ) )
31 foelcdmi 
 |-  ( ( F : X -onto-> Y /\ i e. Y ) -> E. a e. X ( F ` a ) = i )
32 6 31 sylan 
 |-  ( ( ph /\ i e. Y ) -> E. a e. X ( F ` a ) = i )
33 32 adantr 
 |-  ( ( ( ph /\ i e. Y ) /\ j e. Y ) -> E. a e. X ( F ` a ) = i )
34 30 33 r19.29a 
 |-  ( ( ( ph /\ i e. Y ) /\ j e. Y ) -> ( i .+^ j ) = ( j .+^ i ) )
35 34 anasss 
 |-  ( ( ph /\ ( i e. Y /\ j e. Y ) ) -> ( i .+^ j ) = ( j .+^ i ) )
36 35 ralrimivva 
 |-  ( ph -> A. i e. Y A. j e. Y ( i .+^ j ) = ( j .+^ i ) )
37 2 4 iscmn 
 |-  ( H e. CMnd <-> ( H e. Mnd /\ A. i e. Y A. j e. Y ( i .+^ j ) = ( j .+^ i ) ) )
38 10 36 37 sylanbrc 
 |-  ( ph -> H e. CMnd )