Metamath Proof Explorer

Theorem ghmcyg

Description: The image of a cyclic group under a surjective group homomorphism is cyclic. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses cygctb.1 ⊢B=BaseG
ghmcyg.1 ⊢C=BaseH
Assertion ghmcyg ⊢F∈GGrpHomH∧F:B⟶ontoC→G∈CycGrp→H∈CycGrp

Proof

Step Hyp Ref Expression
1 cygctb.1 ⊢B=BaseG
2 ghmcyg.1 ⊢C=BaseH
3 eqid ⊢⋅G=⋅G
4 1 3 iscyg ⊢G∈CycGrp↔G∈Grp∧∃x∈Bran⁡n∈ℤ⟼n⋅Gx=B
5 4 simprbi ⊢G∈CycGrp→∃x∈Bran⁡n∈ℤ⟼n⋅Gx=B
6 eqid ⊢⋅H=⋅H
7 ghmgrp2 ⊢F∈GGrpHomH→H∈Grp
8 7 ad2antrr ⊢F∈GGrpHomH∧F:B⟶ontoC∧x∈B∧ran⁡n∈ℤ⟼n⋅Gx=B→H∈Grp
9 fof ⊢F:B⟶ontoC→F:B⟶C
10 9 ad2antlr ⊢F∈GGrpHomH∧F:B⟶ontoC∧x∈B∧ran⁡n∈ℤ⟼n⋅Gx=B→F:B⟶C
11 simprl ⊢F∈GGrpHomH∧F:B⟶ontoC∧x∈B∧ran⁡n∈ℤ⟼n⋅Gx=B→x∈B
12 10 11 ffvelcdmd ⊢F∈GGrpHomH∧F:B⟶ontoC∧x∈B∧ran⁡n∈ℤ⟼n⋅Gx=B→F⁡x∈C
13 simplr ⊢F∈GGrpHomH∧F:B⟶ontoC∧x∈B∧ran⁡n∈ℤ⟼n⋅Gx=B→F:B⟶ontoC
14 foeq2 ⊢ran⁡n∈ℤ⟼n⋅Gx=B→F:ran⁡n∈ℤ⟼n⋅Gx⟶ontoC↔F:B⟶ontoC
15 14 ad2antll ⊢F∈GGrpHomH∧F:B⟶ontoC∧x∈B∧ran⁡n∈ℤ⟼n⋅Gx=B→F:ran⁡n∈ℤ⟼n⋅Gx⟶ontoC↔F:B⟶ontoC
16 13 15 mpbird ⊢F∈GGrpHomH∧F:B⟶ontoC∧x∈B∧ran⁡n∈ℤ⟼n⋅Gx=B→F:ran⁡n∈ℤ⟼n⋅Gx⟶ontoC
17 foelrn ⊢F:ran⁡n∈ℤ⟼n⋅Gx⟶ontoC∧y∈C→∃z∈ran⁡n∈ℤ⟼n⋅Gxy=F⁡z
18 16 17 sylan ⊢F∈GGrpHomH∧F:B⟶ontoC∧x∈B∧ran⁡n∈ℤ⟼n⋅Gx=B∧y∈C→∃z∈ran⁡n∈ℤ⟼n⋅Gxy=F⁡z
19 ovex ⊢m⋅Gx∈V
20 19 rgenw ⊢∀m∈ℤm⋅Gx∈V
21 oveq1 ⊢n=m→n⋅Gx=m⋅Gx
22 21 cbvmptv ⊢n∈ℤ⟼n⋅Gx=m∈ℤ⟼m⋅Gx
23 fveq2 ⊢z=m⋅Gx→F⁡z=F⁡m⋅Gx
24 23 eqeq2d ⊢z=m⋅Gx→y=F⁡z↔y=F⁡m⋅Gx
25 22 24 rexrnmptw ⊢∀m∈ℤm⋅Gx∈V→∃z∈ran⁡n∈ℤ⟼n⋅Gxy=F⁡z↔∃m∈ℤy=F⁡m⋅Gx
26 20 25 ax-mp ⊢∃z∈ran⁡n∈ℤ⟼n⋅Gxy=F⁡z↔∃m∈ℤy=F⁡m⋅Gx
27 18 26 sylib ⊢F∈GGrpHomH∧F:B⟶ontoC∧x∈B∧ran⁡n∈ℤ⟼n⋅Gx=B∧y∈C→∃m∈ℤy=F⁡m⋅Gx
28 simp-4l ⊢F∈GGrpHomH∧F:B⟶ontoC∧x∈B∧ran⁡n∈ℤ⟼n⋅Gx=B∧y∈C∧m∈ℤ→F∈GGrpHomH
29 simpr ⊢F∈GGrpHomH∧F:B⟶ontoC∧x∈B∧ran⁡n∈ℤ⟼n⋅Gx=B∧y∈C∧m∈ℤ→m∈ℤ
30 11 ad2antrr ⊢F∈GGrpHomH∧F:B⟶ontoC∧x∈B∧ran⁡n∈ℤ⟼n⋅Gx=B∧y∈C∧m∈ℤ→x∈B
31 1 3 6 ghmmulg ⊢F∈GGrpHomH∧m∈ℤ∧x∈B→F⁡m⋅Gx=m⋅HF⁡x
32 28 29 30 31 syl3anc ⊢F∈GGrpHomH∧F:B⟶ontoC∧x∈B∧ran⁡n∈ℤ⟼n⋅Gx=B∧y∈C∧m∈ℤ→F⁡m⋅Gx=m⋅HF⁡x
33 32 eqeq2d ⊢F∈GGrpHomH∧F:B⟶ontoC∧x∈B∧ran⁡n∈ℤ⟼n⋅Gx=B∧y∈C∧m∈ℤ→y=F⁡m⋅Gx↔y=m⋅HF⁡x
34 33 rexbidva ⊢F∈GGrpHomH∧F:B⟶ontoC∧x∈B∧ran⁡n∈ℤ⟼n⋅Gx=B∧y∈C→∃m∈ℤy=F⁡m⋅Gx↔∃m∈ℤy=m⋅HF⁡x
35 27 34 mpbid ⊢F∈GGrpHomH∧F:B⟶ontoC∧x∈B∧ran⁡n∈ℤ⟼n⋅Gx=B∧y∈C→∃m∈ℤy=m⋅HF⁡x
36 2 6 8 12 35 iscygd ⊢F∈GGrpHomH∧F:B⟶ontoC∧x∈B∧ran⁡n∈ℤ⟼n⋅Gx=B→H∈CycGrp
37 36 rexlimdvaa ⊢F∈GGrpHomH∧F:B⟶ontoC→∃x∈Bran⁡n∈ℤ⟼n⋅Gx=B→H∈CycGrp
38 5 37 syl5 ⊢F∈GGrpHomH∧F:B⟶ontoC→G∈CycGrp→H∈CycGrp