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 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 ffvelrnd ( ( ( ( 𝜑𝑎𝑌 ) ∧ 𝑖𝑋 ) ∧ ( 𝐹𝑖 ) = 𝑎 ) → ( 𝐹 ‘ ( ( 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 foelrni ( ( 𝐹 : 𝑋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 )