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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
ghmcyg.1 ⊢ 𝐶 = ( Base ‘ 𝐻 )
Assertion ghmcyg ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝐹 : 𝐵 –onto→ 𝐶 ) → ( 𝐺 ∈ CycGrp → 𝐻 ∈ CycGrp ) )

Proof

Step Hyp Ref Expression
1 cygctb.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ghmcyg.1 ⊢ 𝐶 = ( Base ‘ 𝐻 )
3 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
4 1 3 iscyg ⊢ ( 𝐺 ∈ CycGrp ↔ ( 𝐺 ∈ Grp ∧ ∃ 𝑥 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 ) )
5 4 simprbi ⊢ ( 𝐺 ∈ CycGrp → ∃ 𝑥 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 )
6 eqid ⊢ ( .g ‘ 𝐻 ) = ( .g ‘ 𝐻 )
7 ghmgrp2 ⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → 𝐻 ∈ Grp )
8 7 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝐹 : 𝐵 –onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 ) ) → 𝐻 ∈ Grp )
9 fof ⊢ ( 𝐹 : 𝐵 –onto→ 𝐶 → 𝐹 : 𝐵 ⟶ 𝐶 )
10 9 ad2antlr ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝐹 : 𝐵 –onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 ) ) → 𝐹 : 𝐵 ⟶ 𝐶 )
11 simprl ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝐹 : 𝐵 –onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 ) ) → 𝑥 ∈ 𝐵 )
12 10 11 ffvelrnd ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝐹 : 𝐵 –onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐶 )
13 simplr ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝐹 : 𝐵 –onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 ) ) → 𝐹 : 𝐵 –onto→ 𝐶 )
14 foeq2 ⊢ ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 → ( 𝐹 : ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) –onto→ 𝐶 ↔ 𝐹 : 𝐵 –onto→ 𝐶 ) )
15 14 ad2antll ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝐹 : 𝐵 –onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 ) ) → ( 𝐹 : ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) –onto→ 𝐶 ↔ 𝐹 : 𝐵 –onto→ 𝐶 ) )
16 13 15 mpbird ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝐹 : 𝐵 –onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 ) ) → 𝐹 : ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) –onto→ 𝐶 )
17 foelrn ⊢ ( ( 𝐹 : ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) –onto→ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ∃ 𝑧 ∈ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) 𝑦 = ( 𝐹 ‘ 𝑧 ) )
18 16 17 sylan ⊢ ( ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝐹 : 𝐵 –onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 ) ) ∧ 𝑦 ∈ 𝐶 ) → ∃ 𝑧 ∈ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) 𝑦 = ( 𝐹 ‘ 𝑧 ) )
19 ovex ⊢ ( 𝑚 ( .g ‘ 𝐺 ) 𝑥 ) ∈ V
20 19 rgenw ⊢ ∀ 𝑚 ∈ ℤ ( 𝑚 ( .g ‘ 𝐺 ) 𝑥 ) ∈ V
21 oveq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) = ( 𝑚 ( .g ‘ 𝐺 ) 𝑥 ) )
22 21 cbvmptv ⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = ( 𝑚 ∈ ℤ ↦ ( 𝑚 ( .g ‘ 𝐺 ) 𝑥 ) )
23 fveq2 ⊢ ( 𝑧 = ( 𝑚 ( .g ‘ 𝐺 ) 𝑥 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝑚 ( .g ‘ 𝐺 ) 𝑥 ) ) )
24 23 eqeq2d ⊢ ( 𝑧 = ( 𝑚 ( .g ‘ 𝐺 ) 𝑥 ) → ( 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ 𝑦 = ( 𝐹 ‘ ( 𝑚 ( .g ‘ 𝐺 ) 𝑥 ) ) ) )
25 22 24 rexrnmptw ⊢ ( ∀ 𝑚 ∈ ℤ ( 𝑚 ( .g ‘ 𝐺 ) 𝑥 ) ∈ V → ( ∃ 𝑧 ∈ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ ∃ 𝑚 ∈ ℤ 𝑦 = ( 𝐹 ‘ ( 𝑚 ( .g ‘ 𝐺 ) 𝑥 ) ) ) )
26 20 25 ax-mp ⊢ ( ∃ 𝑧 ∈ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ ∃ 𝑚 ∈ ℤ 𝑦 = ( 𝐹 ‘ ( 𝑚 ( .g ‘ 𝐺 ) 𝑥 ) ) )
27 18 26 sylib ⊢ ( ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝐹 : 𝐵 –onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 ) ) ∧ 𝑦 ∈ 𝐶 ) → ∃ 𝑚 ∈ ℤ 𝑦 = ( 𝐹 ‘ ( 𝑚 ( .g ‘ 𝐺 ) 𝑥 ) ) )
28 simp-4l ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝐹 : 𝐵 –onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 ) ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑚 ∈ ℤ ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
29 simpr ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝐹 : 𝐵 –onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 ) ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑚 ∈ ℤ ) → 𝑚 ∈ ℤ )
30 11 ad2antrr ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝐹 : 𝐵 –onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 ) ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑚 ∈ ℤ ) → 𝑥 ∈ 𝐵 )
31 1 3 6 ghmmulg ⊢ ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑚 ∈ ℤ ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑚 ( .g ‘ 𝐺 ) 𝑥 ) ) = ( 𝑚 ( .g ‘ 𝐻 ) ( 𝐹 ‘ 𝑥 ) ) )
32 28 29 30 31 syl3anc ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝐹 : 𝐵 –onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 ) ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑚 ∈ ℤ ) → ( 𝐹 ‘ ( 𝑚 ( .g ‘ 𝐺 ) 𝑥 ) ) = ( 𝑚 ( .g ‘ 𝐻 ) ( 𝐹 ‘ 𝑥 ) ) )
33 32 eqeq2d ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝐹 : 𝐵 –onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 ) ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑚 ∈ ℤ ) → ( 𝑦 = ( 𝐹 ‘ ( 𝑚 ( .g ‘ 𝐺 ) 𝑥 ) ) ↔ 𝑦 = ( 𝑚 ( .g ‘ 𝐻 ) ( 𝐹 ‘ 𝑥 ) ) ) )
34 33 rexbidva ⊢ ( ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝐹 : 𝐵 –onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 ) ) ∧ 𝑦 ∈ 𝐶 ) → ( ∃ 𝑚 ∈ ℤ 𝑦 = ( 𝐹 ‘ ( 𝑚 ( .g ‘ 𝐺 ) 𝑥 ) ) ↔ ∃ 𝑚 ∈ ℤ 𝑦 = ( 𝑚 ( .g ‘ 𝐻 ) ( 𝐹 ‘ 𝑥 ) ) ) )
35 27 34 mpbid ⊢ ( ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝐹 : 𝐵 –onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 ) ) ∧ 𝑦 ∈ 𝐶 ) → ∃ 𝑚 ∈ ℤ 𝑦 = ( 𝑚 ( .g ‘ 𝐻 ) ( 𝐹 ‘ 𝑥 ) ) )
36 2 6 8 12 35 iscygd ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝐹 : 𝐵 –onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 ) ) → 𝐻 ∈ CycGrp )
37 36 rexlimdvaa ⊢ ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝐹 : 𝐵 –onto→ 𝐶 ) → ( ∃ 𝑥 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) 𝑥 ) ) = 𝐵 → 𝐻 ∈ CycGrp ) )
38 5 37 syl5 ⊢ ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝐹 : 𝐵 –onto→ 𝐶 ) → ( 𝐺 ∈ CycGrp → 𝐻 ∈ CycGrp ) )