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 ) )