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 M MgmHom N X SubMgm M F X SubMgm N

Proof

Step Hyp Ref Expression
1 imassrn F X ran F
2 eqid Base M = Base M
3 eqid Base N = Base N
4 2 3 mgmhmf F M MgmHom N F : Base M Base N
5 4 adantr F M MgmHom N X SubMgm M F : Base M Base N
6 5 frnd F M MgmHom N X SubMgm M ran F Base N
7 1 6 sstrid F M MgmHom N X SubMgm M F X Base N
8 simpll F M MgmHom N X SubMgm M z X x X F M MgmHom N
9 2 submgmss X SubMgm M X Base M
10 9 adantl F M MgmHom N X SubMgm M X Base M
11 10 adantr F M MgmHom N X SubMgm M z X x X X Base M
12 simprl F M MgmHom N X SubMgm M z X x X z X
13 11 12 sseldd F M MgmHom N X SubMgm M z X x X z Base M
14 simprr F M MgmHom N X SubMgm M z X x X x X
15 11 14 sseldd F M MgmHom N X SubMgm M z X x X x Base M
16 eqid + M = + M
17 eqid + N = + N
18 2 16 17 mgmhmlin F M MgmHom N z Base M x Base M F z + M x = F z + N F x
19 8 13 15 18 syl3anc F M MgmHom N X SubMgm M z X x X F z + M x = F z + N F x
20 5 ffnd F M MgmHom N X SubMgm M F Fn Base M
21 20 adantr F M MgmHom N X SubMgm M z X x X F Fn Base M
22 16 submgmcl X SubMgm M z X x X z + M x X
23 22 3expb X SubMgm M z X x X z + M x X
24 23 adantll F M MgmHom N X SubMgm M z X x X z + M x X
25 fnfvima F Fn Base M X Base M z + M x X F z + M x F X
26 21 11 24 25 syl3anc F M MgmHom N X SubMgm M z X x X F z + M x F X
27 19 26 eqeltrrd F M MgmHom N X SubMgm M z X x X F z + N F x F X
28 27 anassrs F M MgmHom N X SubMgm M z X x X F z + N F x F X
29 28 ralrimiva F M MgmHom N X SubMgm M z X x X F z + N F x F X
30 oveq2 y = F x F z + N y = F z + N F x
31 30 eleq1d y = F x F z + N y F X F z + N F x F X
32 31 ralima F Fn Base M X Base M y F X F z + N y F X x X F z + N F x F X
33 20 10 32 syl2anc F M MgmHom N X SubMgm M y F X F z + N y F X x X F z + N F x F X
34 33 adantr F M MgmHom N X SubMgm M z X y F X F z + N y F X x X F z + N F x F X
35 29 34 mpbird F M MgmHom N X SubMgm M z X y F X F z + N y F X
36 35 ralrimiva F M MgmHom N X SubMgm M z X y F X F z + N y F X
37 oveq1 x = F z x + N y = F z + N y
38 37 eleq1d x = F z x + N y F X F z + N y F X
39 38 ralbidv x = F z y F X x + N y F X y F X F z + N y F X
40 39 ralima F Fn Base M X Base M x F X y F X x + N y F X z X y F X F z + N y F X
41 20 10 40 syl2anc F M MgmHom N X SubMgm M x F X y F X x + N y F X z X y F X F z + N y F X
42 36 41 mpbird F M MgmHom N X SubMgm M x F X y F X x + N y F X
43 mgmhmrcl F M MgmHom N M Mgm N Mgm
44 43 simprd F M MgmHom N N Mgm
45 44 adantr F M MgmHom N X SubMgm M N Mgm
46 3 17 issubmgm N Mgm F X SubMgm N F X Base N x F X y F X x + N y F X
47 45 46 syl F M MgmHom N X SubMgm M F X SubMgm N F X Base N x F X y F X x + N y F X
48 7 42 47 mpbir2and F M MgmHom N X SubMgm M F X SubMgm N