Metamath Proof Explorer

Theorem mhmismgmhm

Description: Each monoid homomorphism is a magma homomorphism. (Contributed by AV, 29-Feb-2020)

Ref Expression
Assertion mhmismgmhm 
|- ( F e. ( R MndHom S ) -> F e. ( R MgmHom S ) )

Proof

Step Hyp Ref Expression
1 mndmgm 
 |-  ( R e. Mnd -> R e. Mgm )
2 mndmgm 
 |-  ( S e. Mnd -> S e. Mgm )
3 1 2 anim12i 
 |-  ( ( R e. Mnd /\ S e. Mnd ) -> ( R e. Mgm /\ S e. Mgm ) )
4 3simpa 
 |-  ( ( F : ( Base ` R ) --> ( Base ` S ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) /\ ( F ` ( 0g ` R ) ) = ( 0g ` S ) ) -> ( F : ( Base ` R ) --> ( Base ` S ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) )
5 3 4 anim12i 
 |-  ( ( ( R e. Mnd /\ S e. Mnd ) /\ ( F : ( Base ` R ) --> ( Base ` S ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) /\ ( F ` ( 0g ` R ) ) = ( 0g ` S ) ) ) -> ( ( R e. Mgm /\ S e. Mgm ) /\ ( F : ( Base ` R ) --> ( Base ` S ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) ) )
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 eqid 
 |-  ( Base ` S ) = ( Base ` S )
8 eqid 
 |-  ( +g ` R ) = ( +g ` R )
9 eqid 
 |-  ( +g ` S ) = ( +g ` S )
10 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
11 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
12 6 7 8 9 10 11 ismhm 
 |-  ( F e. ( R MndHom S ) <-> ( ( R e. Mnd /\ S e. Mnd ) /\ ( F : ( Base ` R ) --> ( Base ` S ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) /\ ( F ` ( 0g ` R ) ) = ( 0g ` S ) ) ) )
13 6 7 8 9 ismgmhm 
 |-  ( F e. ( R MgmHom S ) <-> ( ( R e. Mgm /\ S e. Mgm ) /\ ( F : ( Base ` R ) --> ( Base ` S ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) ) )
14 5 12 13 3imtr4i 
 |-  ( F e. ( R MndHom S ) -> F e. ( R MgmHom S ) )