Metamath Proof Explorer

Theorem ghmgrp

Description: The image of a group G under a group homomorphism F is a group. This is a stronger result than that usually found in the literature, since the target of the homomorphism (operator O in our model) need not have any of the properties of a group as a prerequisite. (Contributed by Paul Chapman, 25-Apr-2008) (Revised by Mario Carneiro, 12-May-2014) (Revised by Thierry Arnoux, 25-Jan-2020)

Ref Expression
Hypotheses ghmgrp.f ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
ghmgrp.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
ghmgrp.y ⊢ 𝑌 = ( Base ‘ 𝐻 )
ghmgrp.p ⊢ + = ( +g ‘ 𝐺 )
ghmgrp.q ⊢ ⨣ = ( +g ‘ 𝐻 )
ghmgrp.1 ⊢ ( 𝜑 → 𝐹 : 𝑋 –onto→ 𝑌 )
ghmgrp.3 ⊢ ( 𝜑 → 𝐺 ∈ Grp )
Assertion ghmgrp ( 𝜑 → 𝐻 ∈ Grp )

Proof

Step Hyp Ref Expression
1 ghmgrp.f ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
2 ghmgrp.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
3 ghmgrp.y ⊢ 𝑌 = ( Base ‘ 𝐻 )
4 ghmgrp.p ⊢ + = ( +g ‘ 𝐺 )
5 ghmgrp.q ⊢ ⨣ = ( +g ‘ 𝐻 )
6 ghmgrp.1 ⊢ ( 𝜑 → 𝐹 : 𝑋 –onto→ 𝑌 )
7 ghmgrp.3 ⊢ ( 𝜑 → 𝐺 ∈ Grp )
8 grpmnd ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
9 7 8 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
10 1 2 3 4 5 6 9 mhmmnd ⊢ ( 𝜑 → 𝐻 ∈ Mnd )
11 fof ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → 𝐹 : 𝑋 ⟶ 𝑌 )
12 6 11 syl ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
13 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → 𝐹 : 𝑋 ⟶ 𝑌 )
14 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → 𝐺 ∈ Grp )
15 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → 𝑖 ∈ 𝑋 )
16 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
17 2 16 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑖 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ∈ 𝑋 )
18 14 15 17 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ∈ 𝑋 )
19 13 18 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ) ∈ 𝑌 )
20 1 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
21 7 17 sylan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ∈ 𝑋 )
22 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
23 20 21 22 mhmlem ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐹 ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) + 𝑖 ) ) = ( ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ) ⨣ ( 𝐹 ‘ 𝑖 ) ) )
24 23 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( 𝐹 ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) + 𝑖 ) ) = ( ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ) ⨣ ( 𝐹 ‘ 𝑖 ) ) )
25 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
26 2 4 25 16 grplinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑖 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) + 𝑖 ) = ( 0g ‘ 𝐺 ) )
27 26 fveq2d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑖 ∈ 𝑋 ) → ( 𝐹 ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) + 𝑖 ) ) = ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) )
28 14 15 27 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( 𝐹 ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) + 𝑖 ) ) = ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) )
29 1 2 3 4 5 6 9 25 mhmid ⊢ ( 𝜑 → ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐻 ) )
30 29 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐻 ) )
31 28 30 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( 𝐹 ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) + 𝑖 ) ) = ( 0g ‘ 𝐻 ) )
32 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( 𝐹 ‘ 𝑖 ) = 𝑎 )
33 32 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ) ⨣ ( 𝐹 ‘ 𝑖 ) ) = ( ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ) ⨣ 𝑎 ) )
34 24 31 33 3eqtr3rd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ) ⨣ 𝑎 ) = ( 0g ‘ 𝐻 ) )
35 oveq1 ⊢ ( 𝑓 = ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( 𝑓 ⨣ 𝑎 ) = ( ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ) ⨣ 𝑎 ) )
36 35 eqeq1d ⊢ ( 𝑓 = ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( 𝑓 ⨣ 𝑎 ) = ( 0g ‘ 𝐻 ) ↔ ( ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ) ⨣ 𝑎 ) = ( 0g ‘ 𝐻 ) ) )
37 36 rspcev ⊢ ( ( ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ) ∈ 𝑌 ∧ ( ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑖 ) ) ⨣ 𝑎 ) = ( 0g ‘ 𝐻 ) ) → ∃ 𝑓 ∈ 𝑌 ( 𝑓 ⨣ 𝑎 ) = ( 0g ‘ 𝐻 ) )
38 19 34 37 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ∃ 𝑓 ∈ 𝑌 ( 𝑓 ⨣ 𝑎 ) = ( 0g ‘ 𝐻 ) )
39 foelrni ⊢ ( ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝑎 ∈ 𝑌 ) → ∃ 𝑖 ∈ 𝑋 ( 𝐹 ‘ 𝑖 ) = 𝑎 )
40 6 39 sylan ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) → ∃ 𝑖 ∈ 𝑋 ( 𝐹 ‘ 𝑖 ) = 𝑎 )
41 38 40 r19.29a ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) → ∃ 𝑓 ∈ 𝑌 ( 𝑓 ⨣ 𝑎 ) = ( 0g ‘ 𝐻 ) )
42 41 ralrimiva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑌 ∃ 𝑓 ∈ 𝑌 ( 𝑓 ⨣ 𝑎 ) = ( 0g ‘ 𝐻 ) )
43 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
44 3 5 43 isgrp ⊢ ( 𝐻 ∈ Grp ↔ ( 𝐻 ∈ Mnd ∧ ∀ 𝑎 ∈ 𝑌 ∃ 𝑓 ∈ 𝑌 ( 𝑓 ⨣ 𝑎 ) = ( 0g ‘ 𝐻 ) ) )
45 10 42 44 sylanbrc ⊢ ( 𝜑 → 𝐻 ∈ Grp )