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 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 )