Metamath Proof Explorer

Theorem mhmima

Description: The homomorphic image of a submonoid is a submonoid. (Contributed by Mario Carneiro, 10-Mar-2015)

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 simpll ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) )
21 14 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → 𝑋 ⊆ ( Base ‘ 𝑀 ) )
22 simprl ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → 𝑧 ∈ 𝑋 )
23 21 22 sseldd ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → 𝑧 ∈ ( Base ‘ 𝑀 ) )
24 simprr ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑋 )
25 21 24 sseldd ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → 𝑥 ∈ ( Base ‘ 𝑀 ) )
26 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
27 eqid ⊢ ( +g ‘ 𝑁 ) = ( +g ‘ 𝑁 )
28 2 26 27 mhmlin ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐹 ‘ ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ) = ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) )
29 20 23 25 28 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ) = ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) )
30 12 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → 𝐹 Fn ( Base ‘ 𝑀 ) )
31 26 submcl ⊢ ( ( 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ∈ 𝑋 )
32 31 3expb ⊢ ( ( 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ∈ 𝑋 )
33 32 adantll ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ∈ 𝑋 )
34 fnfvima ⊢ ( ( 𝐹 Fn ( Base ‘ 𝑀 ) ∧ 𝑋 ⊆ ( Base ‘ 𝑀 ) ∧ ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) )
35 30 21 33 34 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) )
36 29 35 eqeltrrd ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) )
37 36 anassrs ⊢ ( ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) )
38 37 ralrimiva ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ 𝑧 ∈ 𝑋 ) → ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) )
39 oveq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) = ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) )
40 39 eleq1d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) ) )
41 40 ralima ⊢ ( ( 𝐹 Fn ( Base ‘ 𝑀 ) ∧ 𝑋 ⊆ ( Base ‘ 𝑀 ) ) → ( ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) ) )
42 12 14 41 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → ( ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) ) )
43 42 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) ) )
44 38 43 mpbird ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) ∧ 𝑧 ∈ 𝑋 ) → ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) )
45 44 ralrimiva ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → ∀ 𝑧 ∈ 𝑋 ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) )
46 oveq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑧 ) → ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) = ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) )
47 46 eleq1d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑧 ) → ( ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ) )
48 47 ralbidv ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑧 ) → ( ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ) )
49 48 ralima ⊢ ( ( 𝐹 Fn ( Base ‘ 𝑀 ) ∧ 𝑋 ⊆ ( Base ‘ 𝑀 ) ) → ( ∀ 𝑥 ∈ ( 𝐹 “ 𝑋 ) ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ) )
50 12 14 49 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → ( ∀ 𝑥 ∈ ( 𝐹 “ 𝑋 ) ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ) )
51 45 50 mpbird ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → ∀ 𝑥 ∈ ( 𝐹 “ 𝑋 ) ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) )
52 mhmrcl2 ⊢ ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) → 𝑁 ∈ Mnd )
53 52 adantr ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → 𝑁 ∈ Mnd )
54 3 9 27 issubm ⊢ ( 𝑁 ∈ Mnd → ( ( 𝐹 “ 𝑋 ) ∈ ( SubMnd ‘ 𝑁 ) ↔ ( ( 𝐹 “ 𝑋 ) ⊆ ( Base ‘ 𝑁 ) ∧ ( 0g ‘ 𝑁 ) ∈ ( 𝐹 “ 𝑋 ) ∧ ∀ 𝑥 ∈ ( 𝐹 “ 𝑋 ) ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ) ) )
55 53 54 syl ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → ( ( 𝐹 “ 𝑋 ) ∈ ( SubMnd ‘ 𝑁 ) ↔ ( ( 𝐹 “ 𝑋 ) ⊆ ( Base ‘ 𝑁 ) ∧ ( 0g ‘ 𝑁 ) ∈ ( 𝐹 “ 𝑋 ) ∧ ∀ 𝑥 ∈ ( 𝐹 “ 𝑋 ) ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ) ) )
56 7 19 51 55 mpbir3and ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑀 ) ) → ( 𝐹 “ 𝑋 ) ∈ ( SubMnd ‘ 𝑁 ) )