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 = Base G
ghmcyg.1 ⊢ C = Base H
Assertion ghmcyg ⊢ F ∈ G GrpHom H ∧ F : B ⟶ onto C → G ∈ CycGrp → H ∈ CycGrp

Proof

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