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 ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → ( 𝐹𝑋 ) ∈ ( SubMnd ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 imassrn ( 𝐹𝑋 ) ⊆ ran 𝐹
2 eqid ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
3 eqid ( Base ‘ 𝑁 ) = ( Base ‘ 𝑁 )
4 2 3 mhmf ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) → 𝐹 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
5 4 adantr ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → 𝐹 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
6 5 frnd ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → ran 𝐹 ⊆ ( Base ‘ 𝑁 ) )
7 1 6 sstrid ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → ( 𝐹𝑋 ) ⊆ ( Base ‘ 𝑁 ) )
8 eqid ( 0g𝑀 ) = ( 0g𝑀 )
9 eqid ( 0g𝑁 ) = ( 0g𝑁 )
10 8 9 mhm0 ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) → ( 𝐹 ‘ ( 0g𝑀 ) ) = ( 0g𝑁 ) )
11 10 adantr ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → ( 𝐹 ‘ ( 0g𝑀 ) ) = ( 0g𝑁 ) )
12 5 ffnd ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → 𝐹 Fn ( Base ‘ 𝑀 ) )
13 2 submss ( 𝑋 ∈ ( SubMnd ‘ 𝑀 ) → 𝑋 ⊆ ( Base ‘ 𝑀 ) )
14 13 adantl ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → 𝑋 ⊆ ( Base ‘ 𝑀 ) )
15 8 subm0cl ( 𝑋 ∈ ( SubMnd ‘ 𝑀 ) → ( 0g𝑀 ) ∈ 𝑋 )
16 15 adantl ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → ( 0g𝑀 ) ∈ 𝑋 )
17 fnfvima ( ( 𝐹 Fn ( Base ‘ 𝑀 ) ∧ 𝑋 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g𝑀 ) ∈ 𝑋 ) → ( 𝐹 ‘ ( 0g𝑀 ) ) ∈ ( 𝐹𝑋 ) )
18 12 14 16 17 syl3anc ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → ( 𝐹 ‘ ( 0g𝑀 ) ) ∈ ( 𝐹𝑋 ) )
19 11 18 eqeltrrd ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → ( 0g𝑁 ) ∈ ( 𝐹𝑋 ) )
20 simpl ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) )
21 eqidd ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → ( +g𝑀 ) = ( +g𝑀 ) )
22 eqidd ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → ( +g𝑁 ) = ( +g𝑁 ) )
23 eqid ( +g𝑀 ) = ( +g𝑀 )
24 23 submcl ( ( 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ∧ 𝑧𝑋𝑥𝑋 ) → ( 𝑧 ( +g𝑀 ) 𝑥 ) ∈ 𝑋 )
25 24 3adant1l ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ 𝑧𝑋𝑥𝑋 ) → ( 𝑧 ( +g𝑀 ) 𝑥 ) ∈ 𝑋 )
26 20 14 21 22 25 mhmimalem ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → ∀ 𝑥 ∈ ( 𝐹𝑋 ) ∀ 𝑦 ∈ ( 𝐹𝑋 ) ( 𝑥 ( +g𝑁 ) 𝑦 ) ∈ ( 𝐹𝑋 ) )
27 mhmrcl2 ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) → 𝑁 ∈ Mnd )
28 27 adantr ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → 𝑁 ∈ Mnd )
29 eqid ( +g𝑁 ) = ( +g𝑁 )
30 3 9 29 issubm ( 𝑁 ∈ Mnd → ( ( 𝐹𝑋 ) ∈ ( SubMnd ‘ 𝑁 ) ↔ ( ( 𝐹𝑋 ) ⊆ ( Base ‘ 𝑁 ) ∧ ( 0g𝑁 ) ∈ ( 𝐹𝑋 ) ∧ ∀ 𝑥 ∈ ( 𝐹𝑋 ) ∀ 𝑦 ∈ ( 𝐹𝑋 ) ( 𝑥 ( +g𝑁 ) 𝑦 ) ∈ ( 𝐹𝑋 ) ) ) )
31 28 30 syl ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → ( ( 𝐹𝑋 ) ∈ ( SubMnd ‘ 𝑁 ) ↔ ( ( 𝐹𝑋 ) ⊆ ( Base ‘ 𝑁 ) ∧ ( 0g𝑁 ) ∈ ( 𝐹𝑋 ) ∧ ∀ 𝑥 ∈ ( 𝐹𝑋 ) ∀ 𝑦 ∈ ( 𝐹𝑋 ) ( 𝑥 ( +g𝑁 ) 𝑦 ) ∈ ( 𝐹𝑋 ) ) ) )
32 7 19 26 31 mpbir3and ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → ( 𝐹𝑋 ) ∈ ( SubMnd ‘ 𝑁 ) )