Metamath Proof Explorer

Theorem mhmfmhm

Description: The function fulfilling the conditions of mhmmnd is a monoid homomorphism. (Contributed by Thierry Arnoux, 26-Jan-2020)

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

Proof

Step Hyp Ref Expression
1 ghmgrp.f 
 |-  ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
2 ghmgrp.x 
 |-  X = ( Base ` G )
3 ghmgrp.y 
 |-  Y = ( Base ` H )
4 ghmgrp.p 
 |-  .+ = ( +g ` G )
5 ghmgrp.q 
 |-  .+^ = ( +g ` H )
6 ghmgrp.1 
 |-  ( ph -> F : X -onto-> Y )
7 mhmmnd.3 
 |-  ( ph -> G e. Mnd )
8 1 2 3 4 5 6 7 mhmmnd 
 |-  ( ph -> H e. Mnd )
9 fof 
 |-  ( F : X -onto-> Y -> F : X --> Y )
10 6 9 syl 
 |-  ( ph -> F : X --> Y )
11 1 3expb 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
12 11 ralrimivva 
 |-  ( ph -> A. x e. X A. y e. X ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
13 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
14 1 2 3 4 5 6 7 13 mhmid 
 |-  ( ph -> ( F ` ( 0g ` G ) ) = ( 0g ` H ) )
15 10 12 14 3jca 
 |-  ( ph -> ( F : X --> Y /\ A. x e. X A. y e. X ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` ( 0g ` G ) ) = ( 0g ` H ) ) )
16 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
17 2 3 4 5 13 16 ismhm 
 |-  ( F e. ( G MndHom H ) <-> ( ( G e. Mnd /\ H e. Mnd ) /\ ( F : X --> Y /\ A. x e. X A. y e. X ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` ( 0g ` G ) ) = ( 0g ` H ) ) ) )
18 7 8 15 17 syl21anbrc 
 |-  ( ph -> F e. ( G MndHom H ) )