Metamath Proof Explorer

Theorem giccyg

Description: Cyclicity is a group property, i.e. it is preserved under isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Assertion giccyg ⊢ G ≃ 𝑔 H → G ∈ CycGrp → H ∈ CycGrp

Proof

Step Hyp Ref Expression
1 brgic ⊢ G ≃ 𝑔 H ↔ G GrpIso H ≠ ∅
2 n0 ⊢ G GrpIso H ≠ ∅ ↔ ∃ f f ∈ G GrpIso H
3 gimghm ⊢ f ∈ G GrpIso H → f ∈ G GrpHom H
4 eqid ⊢ Base G = Base G
5 eqid ⊢ Base H = Base H
6 4 5 gimf1o ⊢ f ∈ G GrpIso H → f : Base G ⟶ 1-1 onto Base H
7 f1ofo ⊢ f : Base G ⟶ 1-1 onto Base H → f : Base G ⟶ onto Base H
8 6 7 syl ⊢ f ∈ G GrpIso H → f : Base G ⟶ onto Base H
9 4 5 ghmcyg ⊢ f ∈ G GrpHom H ∧ f : Base G ⟶ onto Base H → G ∈ CycGrp → H ∈ CycGrp
10 3 8 9 syl2anc ⊢ f ∈ G GrpIso H → G ∈ CycGrp → H ∈ CycGrp
11 10 exlimiv ⊢ ∃ f f ∈ G GrpIso H → G ∈ CycGrp → H ∈ CycGrp
12 2 11 sylbi ⊢ G GrpIso H ≠ ∅ → G ∈ CycGrp → H ∈ CycGrp
13 1 12 sylbi ⊢ G ≃ 𝑔 H → G ∈ CycGrp → H ∈ CycGrp