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 ( 𝐺 ≃𝑔 𝐻 → ( 𝐺 ∈ CycGrp → 𝐻 ∈ CycGrp ) )

Proof

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