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 M MndHom N X SubMnd M F X SubMnd 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 mhmf F M MndHom N F : Base M Base N
5 4 adantr F M MndHom N X SubMnd M F : Base M Base N
6 5 frnd F M MndHom N X SubMnd M ran F Base N
7 1 6 sstrid F M MndHom N X SubMnd M F X Base N
8 eqid 0 M = 0 M
9 eqid 0 N = 0 N
10 8 9 mhm0 F M MndHom N F 0 M = 0 N
11 10 adantr F M MndHom N X SubMnd M F 0 M = 0 N
12 5 ffnd F M MndHom N X SubMnd M F Fn Base M
13 2 submss X SubMnd M X Base M
14 13 adantl F M MndHom N X SubMnd M X Base M
15 8 subm0cl X SubMnd M 0 M X
16 15 adantl F M MndHom N X SubMnd M 0 M X
17 fnfvima F Fn Base M X Base M 0 M X F 0 M F X
18 12 14 16 17 syl3anc F M MndHom N X SubMnd M F 0 M F X
19 11 18 eqeltrrd F M MndHom N X SubMnd M 0 N F X
20 simpl F M MndHom N X SubMnd M F M MndHom N
21 eqidd F M MndHom N X SubMnd M + M = + M
22 eqidd F M MndHom N X SubMnd M + N = + N
23 eqid + M = + M
24 23 submcl X SubMnd M z X x X z + M x X
25 24 3adant1l F M MndHom N X SubMnd M z X x X z + M x X
26 20 14 21 22 25 mhmimalem F M MndHom N X SubMnd M x F X y F X x + N y F X
27 mhmrcl2 F M MndHom N N Mnd
28 27 adantr F M MndHom N X SubMnd M N Mnd
29 eqid + N = + N
30 3 9 29 issubm N Mnd F X SubMnd N F X Base N 0 N F X x F X y F X x + N y F X
31 28 30 syl F M MndHom N X SubMnd M F X SubMnd N F X Base N 0 N F X x F X y F X x + N y F X
32 7 19 26 31 mpbir3and F M MndHom N X SubMnd M F X SubMnd N