This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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