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