Metamath Proof Explorer

Theorem mhmima

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

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 simpll 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) /\ ( z e. X /\ x e. X ) ) -> F e. ( M MndHom N ) )
21 14 adantr 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) /\ ( z e. X /\ x e. X ) ) -> X C_ ( Base ` M ) )
22 simprl 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) /\ ( z e. X /\ x e. X ) ) -> z e. X )
23 21 22 sseldd 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) /\ ( z e. X /\ x e. X ) ) -> z e. ( Base ` M ) )
24 simprr 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) /\ ( z e. X /\ x e. X ) ) -> x e. X )
25 21 24 sseldd 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) /\ ( z e. X /\ x e. X ) ) -> x e. ( Base ` M ) )
26 eqid 
 |-  ( +g ` M ) = ( +g ` M )
27 eqid 
 |-  ( +g ` N ) = ( +g ` N )
28 2 26 27 mhmlin 
 |-  ( ( F e. ( M MndHom N ) /\ z e. ( Base ` M ) /\ x e. ( Base ` M ) ) -> ( F ` ( z ( +g ` M ) x ) ) = ( ( F ` z ) ( +g ` N ) ( F ` x ) ) )
29 20 23 25 28 syl3anc 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) /\ ( z e. X /\ x e. X ) ) -> ( F ` ( z ( +g ` M ) x ) ) = ( ( F ` z ) ( +g ` N ) ( F ` x ) ) )
30 12 adantr 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) /\ ( z e. X /\ x e. X ) ) -> F Fn ( Base ` M ) )
31 26 submcl 
 |-  ( ( X e. ( SubMnd ` M ) /\ z e. X /\ x e. X ) -> ( z ( +g ` M ) x ) e. X )
32 31 3expb 
 |-  ( ( X e. ( SubMnd ` M ) /\ ( z e. X /\ x e. X ) ) -> ( z ( +g ` M ) x ) e. X )
33 32 adantll 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) /\ ( z e. X /\ x e. X ) ) -> ( z ( +g ` M ) x ) e. X )
34 fnfvima 
 |-  ( ( F Fn ( Base ` M ) /\ X C_ ( Base ` M ) /\ ( z ( +g ` M ) x ) e. X ) -> ( F ` ( z ( +g ` M ) x ) ) e. ( F " X ) )
35 30 21 33 34 syl3anc 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) /\ ( z e. X /\ x e. X ) ) -> ( F ` ( z ( +g ` M ) x ) ) e. ( F " X ) )
36 29 35 eqeltrrd 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) /\ ( z e. X /\ x e. X ) ) -> ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) )
37 36 anassrs 
 |-  ( ( ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) /\ z e. X ) /\ x e. X ) -> ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) )
38 37 ralrimiva 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) /\ z e. X ) -> A. x e. X ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) )
39 oveq2 
 |-  ( y = ( F ` x ) -> ( ( F ` z ) ( +g ` N ) y ) = ( ( F ` z ) ( +g ` N ) ( F ` x ) ) )
40 39 eleq1d 
 |-  ( y = ( F ` x ) -> ( ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) <-> ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) ) )
41 40 ralima 
 |-  ( ( F Fn ( Base ` M ) /\ X C_ ( Base ` M ) ) -> ( A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) <-> A. x e. X ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) ) )
42 12 14 41 syl2anc 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) -> ( A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) <-> A. x e. X ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) ) )
43 42 adantr 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) /\ z e. X ) -> ( A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) <-> A. x e. X ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) ) )
44 38 43 mpbird 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) /\ z e. X ) -> A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) )
45 44 ralrimiva 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) -> A. z e. X A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) )
46 oveq1 
 |-  ( x = ( F ` z ) -> ( x ( +g ` N ) y ) = ( ( F ` z ) ( +g ` N ) y ) )
47 46 eleq1d 
 |-  ( x = ( F ` z ) -> ( ( x ( +g ` N ) y ) e. ( F " X ) <-> ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) ) )
48 47 ralbidv 
 |-  ( x = ( F ` z ) -> ( A. y e. ( F " X ) ( x ( +g ` N ) y ) e. ( F " X ) <-> A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) ) )
49 48 ralima 
 |-  ( ( F Fn ( Base ` M ) /\ X C_ ( Base ` M ) ) -> ( A. x e. ( F " X ) A. y e. ( F " X ) ( x ( +g ` N ) y ) e. ( F " X ) <-> A. z e. X A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) ) )
50 12 14 49 syl2anc 
 |-  ( ( 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 ) <-> A. z e. X A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) ) )
51 45 50 mpbird 
 |-  ( ( 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 ) )
52 mhmrcl2 
 |-  ( F e. ( M MndHom N ) -> N e. Mnd )
53 52 adantr 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) -> N e. Mnd )
54 3 9 27 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 ) ) ) )
55 53 54 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 ) ) ) )
56 7 19 51 55 mpbir3and 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubMnd ` M ) ) -> ( F " X ) e. ( SubMnd ` N ) )