Metamath Proof Explorer

Theorem mhmima

Description: The homomorphic image of a submonoid is a submonoid. (Contributed by Mario Carneiro, 10-Mar-2015) (Proof shortened by AV, 8-Mar-2025)

Ref Expression
Assertion mhmima 
|- ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) -> ( F " X ) e. ( SubMnd ` N ) )

Proof

Step Hyp Ref Expression
1 imassrn 
 |-  ( F " X ) C_ ran F
2 eqid 
 |-  ( Base ` M ) = ( Base ` M )
3 eqid 
 |-  ( Base ` N ) = ( Base ` N )
4 2 3 mhmf 
 |-  ( F e. ( M MndHom N ) -> F : ( Base ` M ) --> ( Base ` N ) )
5 4 adantr 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) -> F : ( Base ` M ) --> ( Base ` N ) )
6 5 frnd 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) -> ran F C_ ( Base ` N ) )
7 1 6 sstrid 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) -> ( F " X ) C_ ( Base ` N ) )
8 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
9 eqid 
 |-  ( 0g ` N ) = ( 0g ` N )
10 8 9 mhm0 
 |-  ( F e. ( M MndHom N ) -> ( F ` ( 0g ` M ) ) = ( 0g ` N ) )
11 10 adantr 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) -> ( F ` ( 0g ` M ) ) = ( 0g ` N ) )
12 5 ffnd 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) -> F Fn ( Base ` M ) )
13 2 submss 
 |-  ( X e. ( SubMnd ` M ) -> X C_ ( Base ` M ) )
14 13 adantl 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) -> X C_ ( Base ` M ) )
15 8 subm0cl 
 |-  ( X e. ( SubMnd ` M ) -> ( 0g ` M ) e. X )
16 15 adantl 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) -> ( 0g ` M ) e. X )
17 fnfvima 
 |-  ( ( F Fn ( Base ` M ) /\ X C_ ( Base ` M ) /\ ( 0g ` M ) e. X ) -> ( F ` ( 0g ` M ) ) e. ( F " X ) )
18 12 14 16 17 syl3anc 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) -> ( F ` ( 0g ` M ) ) e. ( F " X ) )
19 11 18 eqeltrrd 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) -> ( 0g ` N ) e. ( F " X ) )
20 simpl 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) -> F e. ( M MndHom N ) )
21 eqidd 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) -> ( +g ` M ) = ( +g ` M ) )
22 eqidd 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) -> ( +g ` N ) = ( +g ` N ) )
23 eqid 
 |-  ( +g ` M ) = ( +g ` M )
24 23 submcl 
 |-  ( ( X e. ( SubMnd ` M ) /\ z e. X /\ x e. X ) -> ( z ( +g ` M ) x ) e. X )
25 24 3adant1l 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) /\ z e. X /\ x e. X ) -> ( z ( +g ` M ) x ) e. X )
26 20 14 21 22 25 mhmimalem 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) -> A. x e. ( F " X ) A. y e. ( F " X ) ( x ( +g ` N ) y ) e. ( F " X ) )
27 mhmrcl2 
 |-  ( F e. ( M MndHom N ) -> N e. Mnd )
28 27 adantr 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) -> N e. Mnd )
29 eqid 
 |-  ( +g ` N ) = ( +g ` N )
30 3 9 29 issubm 
 |-  ( N e. Mnd -> ( ( F " X ) e. ( SubMnd ` N ) <-> ( ( F " X ) C_ ( Base ` N ) /\ ( 0g ` N ) e. ( F " X ) /\ A. x e. ( F " X ) A. y e. ( F " X ) ( x ( +g ` N ) y ) e. ( F " X ) ) ) )
31 28 30 syl 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) -> ( ( F " X ) e. ( SubMnd ` N ) <-> ( ( F " X ) C_ ( Base ` N ) /\ ( 0g ` N ) e. ( F " X ) /\ A. x e. ( F " X ) A. y e. ( F " X ) ( x ( +g ` N ) y ) e. ( F " X ) ) ) )
32 7 19 26 31 mpbir3and 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) -> ( F " X ) e. ( SubMnd ` N ) )