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 ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) → ( 𝐹 “ 𝑋 ) ∈ ( SubMgm ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 imassrn ⊢ ( 𝐹 “ 𝑋 ) ⊆ ran 𝐹
2 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
3 eqid ⊢ ( Base ‘ 𝑁 ) = ( Base ‘ 𝑁 )
4 2 3 mgmhmf ⊢ ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) → 𝐹 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
5 4 adantr ⊢ ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) → 𝐹 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
6 5 frnd ⊢ ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) → ran 𝐹 ⊆ ( Base ‘ 𝑁 ) )
7 1 6 sstrid ⊢ ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) → ( 𝐹 “ 𝑋 ) ⊆ ( Base ‘ 𝑁 ) )
8 simpll ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) )
9 2 submgmss ⊢ ( 𝑋 ∈ ( SubMgm ‘ 𝑀 ) → 𝑋 ⊆ ( Base ‘ 𝑀 ) )
10 9 adantl ⊢ ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) → 𝑋 ⊆ ( Base ‘ 𝑀 ) )
11 10 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → 𝑋 ⊆ ( Base ‘ 𝑀 ) )
12 simprl ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → 𝑧 ∈ 𝑋 )
13 11 12 sseldd ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → 𝑧 ∈ ( Base ‘ 𝑀 ) )
14 simprr ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑋 )
15 11 14 sseldd ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → 𝑥 ∈ ( Base ‘ 𝑀 ) )
16 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
17 eqid ⊢ ( +g ‘ 𝑁 ) = ( +g ‘ 𝑁 )
18 2 16 17 mgmhmlin ⊢ ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐹 ‘ ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ) = ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) )
19 8 13 15 18 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ) = ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) )
20 5 ffnd ⊢ ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) → 𝐹 Fn ( Base ‘ 𝑀 ) )
21 20 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → 𝐹 Fn ( Base ‘ 𝑀 ) )
22 16 submgmcl ⊢ ( ( 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ∈ 𝑋 )
23 22 3expb ⊢ ( ( 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ∈ 𝑋 )
24 23 adantll ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ∈ 𝑋 )
25 fnfvima ⊢ ( ( 𝐹 Fn ( Base ‘ 𝑀 ) ∧ 𝑋 ⊆ ( Base ‘ 𝑀 ) ∧ ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) )
26 21 11 24 25 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) )
27 19 26 eqeltrrd ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) )
28 27 anassrs ⊢ ( ( ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) )
29 28 ralrimiva ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) ∧ 𝑧 ∈ 𝑋 ) → ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) )
30 oveq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) = ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) )
31 30 eleq1d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) ) )
32 31 ralima ⊢ ( ( 𝐹 Fn ( Base ‘ 𝑀 ) ∧ 𝑋 ⊆ ( Base ‘ 𝑀 ) ) → ( ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) ) )
33 20 10 32 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) → ( ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) ) )
34 33 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) ) )
35 29 34 mpbird ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) ∧ 𝑧 ∈ 𝑋 ) → ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) )
36 35 ralrimiva ⊢ ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) → ∀ 𝑧 ∈ 𝑋 ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) )
37 oveq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑧 ) → ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) = ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) )
38 37 eleq1d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑧 ) → ( ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ) )
39 38 ralbidv ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑧 ) → ( ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ) )
40 39 ralima ⊢ ( ( 𝐹 Fn ( Base ‘ 𝑀 ) ∧ 𝑋 ⊆ ( Base ‘ 𝑀 ) ) → ( ∀ 𝑥 ∈ ( 𝐹 “ 𝑋 ) ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ) )
41 20 10 40 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) → ( ∀ 𝑥 ∈ ( 𝐹 “ 𝑋 ) ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ) )
42 36 41 mpbird ⊢ ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) → ∀ 𝑥 ∈ ( 𝐹 “ 𝑋 ) ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) )
43 mgmhmrcl ⊢ ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) → ( 𝑀 ∈ Mgm ∧ 𝑁 ∈ Mgm ) )
44 43 simprd ⊢ ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) → 𝑁 ∈ Mgm )
45 44 adantr ⊢ ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) → 𝑁 ∈ Mgm )
46 3 17 issubmgm ⊢ ( 𝑁 ∈ Mgm → ( ( 𝐹 “ 𝑋 ) ∈ ( SubMgm ‘ 𝑁 ) ↔ ( ( 𝐹 “ 𝑋 ) ⊆ ( Base ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ ( 𝐹 “ 𝑋 ) ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ) ) )
47 45 46 syl ⊢ ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) → ( ( 𝐹 “ 𝑋 ) ∈ ( SubMgm ‘ 𝑁 ) ↔ ( ( 𝐹 “ 𝑋 ) ⊆ ( Base ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ ( 𝐹 “ 𝑋 ) ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ) ) )
48 7 42 47 mpbir2and ⊢ ( ( 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑀 ) ) → ( 𝐹 “ 𝑋 ) ∈ ( SubMgm ‘ 𝑁 ) )