Metamath Proof Explorer

Theorem mgmhmima

Description: The homomorphic image of a submagma is a submagma. (Contributed by AV, 27-Feb-2020)

Ref Expression
Assertion mgmhmima 
|- ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) -> ( F " X ) e. ( SubMgm ` 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 mgmhmf 
 |-  ( F e. ( M MgmHom N ) -> F : ( Base ` M ) --> ( Base ` N ) )
5 4 adantr 
 |-  ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) -> F : ( Base ` M ) --> ( Base ` N ) )
6 5 frnd 
 |-  ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) -> ran F C_ ( Base ` N ) )
7 1 6 sstrid 
 |-  ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) -> ( F " X ) C_ ( Base ` N ) )
8 simpll 
 |-  ( ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) /\ ( z e. X /\ x e. X ) ) -> F e. ( M MgmHom N ) )
9 2 submgmss 
 |-  ( X e. ( SubMgm ` M ) -> X C_ ( Base ` M ) )
10 9 adantl 
 |-  ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) -> X C_ ( Base ` M ) )
11 10 adantr 
 |-  ( ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) /\ ( z e. X /\ x e. X ) ) -> X C_ ( Base ` M ) )
12 simprl 
 |-  ( ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) /\ ( z e. X /\ x e. X ) ) -> z e. X )
13 11 12 sseldd 
 |-  ( ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) /\ ( z e. X /\ x e. X ) ) -> z e. ( Base ` M ) )
14 simprr 
 |-  ( ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) /\ ( z e. X /\ x e. X ) ) -> x e. X )
15 11 14 sseldd 
 |-  ( ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) /\ ( z e. X /\ x e. X ) ) -> x e. ( Base ` M ) )
16 eqid 
 |-  ( +g ` M ) = ( +g ` M )
17 eqid 
 |-  ( +g ` N ) = ( +g ` N )
18 2 16 17 mgmhmlin 
 |-  ( ( F e. ( M MgmHom N ) /\ z e. ( Base ` M ) /\ x e. ( Base ` M ) ) -> ( F ` ( z ( +g ` M ) x ) ) = ( ( F ` z ) ( +g ` N ) ( F ` x ) ) )
19 8 13 15 18 syl3anc 
 |-  ( ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) /\ ( z e. X /\ x e. X ) ) -> ( F ` ( z ( +g ` M ) x ) ) = ( ( F ` z ) ( +g ` N ) ( F ` x ) ) )
20 5 ffnd 
 |-  ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) -> F Fn ( Base ` M ) )
21 20 adantr 
 |-  ( ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) /\ ( z e. X /\ x e. X ) ) -> F Fn ( Base ` M ) )
22 16 submgmcl 
 |-  ( ( X e. ( SubMgm ` M ) /\ z e. X /\ x e. X ) -> ( z ( +g ` M ) x ) e. X )
23 22 3expb 
 |-  ( ( X e. ( SubMgm ` M ) /\ ( z e. X /\ x e. X ) ) -> ( z ( +g ` M ) x ) e. X )
24 23 adantll 
 |-  ( ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) /\ ( z e. X /\ x e. X ) ) -> ( z ( +g ` M ) x ) e. X )
25 fnfvima 
 |-  ( ( F Fn ( Base ` M ) /\ X C_ ( Base ` M ) /\ ( z ( +g ` M ) x ) e. X ) -> ( F ` ( z ( +g ` M ) x ) ) e. ( F " X ) )
26 21 11 24 25 syl3anc 
 |-  ( ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) /\ ( z e. X /\ x e. X ) ) -> ( F ` ( z ( +g ` M ) x ) ) e. ( F " X ) )
27 19 26 eqeltrrd 
 |-  ( ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) /\ ( z e. X /\ x e. X ) ) -> ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) )
28 27 anassrs 
 |-  ( ( ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) /\ z e. X ) /\ x e. X ) -> ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) )
29 28 ralrimiva 
 |-  ( ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) /\ z e. X ) -> A. x e. X ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) )
30 oveq2 
 |-  ( y = ( F ` x ) -> ( ( F ` z ) ( +g ` N ) y ) = ( ( F ` z ) ( +g ` N ) ( F ` x ) ) )
31 30 eleq1d 
 |-  ( y = ( F ` x ) -> ( ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) <-> ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) ) )
32 31 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 ) ) )
33 20 10 32 syl2anc 
 |-  ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` 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 ) ) )
34 33 adantr 
 |-  ( ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` 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 ) ) )
35 29 34 mpbird 
 |-  ( ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) /\ z e. X ) -> A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) )
36 35 ralrimiva 
 |-  ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) -> A. z e. X A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) )
37 oveq1 
 |-  ( x = ( F ` z ) -> ( x ( +g ` N ) y ) = ( ( F ` z ) ( +g ` N ) y ) )
38 37 eleq1d 
 |-  ( x = ( F ` z ) -> ( ( x ( +g ` N ) y ) e. ( F " X ) <-> ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) ) )
39 38 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 ) ) )
40 39 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 ) ) )
41 20 10 40 syl2anc 
 |-  ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` 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 ) ) )
42 36 41 mpbird 
 |-  ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) -> A. x e. ( F " X ) A. y e. ( F " X ) ( x ( +g ` N ) y ) e. ( F " X ) )
43 mgmhmrcl 
 |-  ( F e. ( M MgmHom N ) -> ( M e. Mgm /\ N e. Mgm ) )
44 43 simprd 
 |-  ( F e. ( M MgmHom N ) -> N e. Mgm )
45 44 adantr 
 |-  ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) -> N e. Mgm )
46 3 17 issubmgm 
 |-  ( N e. Mgm -> ( ( F " X ) e. ( SubMgm ` N ) <-> ( ( F " X ) C_ ( Base ` N ) /\ A. x e. ( F " X ) A. y e. ( F " X ) ( x ( +g ` N ) y ) e. ( F " X ) ) ) )
47 45 46 syl 
 |-  ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) -> ( ( F " X ) e. ( SubMgm ` N ) <-> ( ( F " X ) C_ ( Base ` N ) /\ A. x e. ( F " X ) A. y e. ( F " X ) ( x ( +g ` N ) y ) e. ( F " X ) ) ) )
48 7 42 47 mpbir2and 
 |-  ( ( F e. ( M MgmHom N ) /\ X e. ( SubMgm ` M ) ) -> ( F " X ) e. ( SubMgm ` N ) )