This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cygth

Description: The "fundamental theorem of cyclic groups". Cyclic groups are exactly the additive groups ZZ / n ZZ , for 0 <_ n (where n = 0 is the infinite cyclic group ZZ ), up to isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Assertion cygth ( 𝐺 ∈ CycGrp ↔ ∃ 𝑛 ∈ ℕ0 𝐺 ≃𝑔 ( ℤ/nℤ ‘ 𝑛 ) )

Proof

Step Hyp Ref Expression
1 hashcl ⊢ ( ( Base ‘ 𝐺 ) ∈ Fin → ( ♯ ‘ ( Base ‘ 𝐺 ) ) ∈ ℕ0 )
2 1 adantl ⊢ ( ( 𝐺 ∈ CycGrp ∧ ( Base ‘ 𝐺 ) ∈ Fin ) → ( ♯ ‘ ( Base ‘ 𝐺 ) ) ∈ ℕ0 )
3 0nn0 ⊢ 0 ∈ ℕ0
4 3 a1i ⊢ ( ( 𝐺 ∈ CycGrp ∧ ¬ ( Base ‘ 𝐺 ) ∈ Fin ) → 0 ∈ ℕ0 )
5 2 4 ifclda ⊢ ( 𝐺 ∈ CycGrp → if ( ( Base ‘ 𝐺 ) ∈ Fin , ( ♯ ‘ ( Base ‘ 𝐺 ) ) , 0 ) ∈ ℕ0 )
6 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
7 eqid ⊢ if ( ( Base ‘ 𝐺 ) ∈ Fin , ( ♯ ‘ ( Base ‘ 𝐺 ) ) , 0 ) = if ( ( Base ‘ 𝐺 ) ∈ Fin , ( ♯ ‘ ( Base ‘ 𝐺 ) ) , 0 )
8 eqid ⊢ ( ℤ/nℤ ‘ if ( ( Base ‘ 𝐺 ) ∈ Fin , ( ♯ ‘ ( Base ‘ 𝐺 ) ) , 0 ) ) = ( ℤ/nℤ ‘ if ( ( Base ‘ 𝐺 ) ∈ Fin , ( ♯ ‘ ( Base ‘ 𝐺 ) ) , 0 ) )
9 6 7 8 cygzn ⊢ ( 𝐺 ∈ CycGrp → 𝐺 ≃𝑔 ( ℤ/nℤ ‘ if ( ( Base ‘ 𝐺 ) ∈ Fin , ( ♯ ‘ ( Base ‘ 𝐺 ) ) , 0 ) ) )
10 fveq2 ⊢ ( 𝑛 = if ( ( Base ‘ 𝐺 ) ∈ Fin , ( ♯ ‘ ( Base ‘ 𝐺 ) ) , 0 ) → ( ℤ/nℤ ‘ 𝑛 ) = ( ℤ/nℤ ‘ if ( ( Base ‘ 𝐺 ) ∈ Fin , ( ♯ ‘ ( Base ‘ 𝐺 ) ) , 0 ) ) )
11 10 breq2d ⊢ ( 𝑛 = if ( ( Base ‘ 𝐺 ) ∈ Fin , ( ♯ ‘ ( Base ‘ 𝐺 ) ) , 0 ) → ( 𝐺 ≃𝑔 ( ℤ/nℤ ‘ 𝑛 ) ↔ 𝐺 ≃𝑔 ( ℤ/nℤ ‘ if ( ( Base ‘ 𝐺 ) ∈ Fin , ( ♯ ‘ ( Base ‘ 𝐺 ) ) , 0 ) ) ) )
12 11 rspcev ⊢ ( ( if ( ( Base ‘ 𝐺 ) ∈ Fin , ( ♯ ‘ ( Base ‘ 𝐺 ) ) , 0 ) ∈ ℕ0 ∧ 𝐺 ≃𝑔 ( ℤ/nℤ ‘ if ( ( Base ‘ 𝐺 ) ∈ Fin , ( ♯ ‘ ( Base ‘ 𝐺 ) ) , 0 ) ) ) → ∃ 𝑛 ∈ ℕ0 𝐺 ≃𝑔 ( ℤ/nℤ ‘ 𝑛 ) )
13 5 9 12 syl2anc ⊢ ( 𝐺 ∈ CycGrp → ∃ 𝑛 ∈ ℕ0 𝐺 ≃𝑔 ( ℤ/nℤ ‘ 𝑛 ) )
14 gicsym ⊢ ( 𝐺 ≃𝑔 ( ℤ/nℤ ‘ 𝑛 ) → ( ℤ/nℤ ‘ 𝑛 ) ≃𝑔 𝐺 )
15 eqid ⊢ ( ℤ/nℤ ‘ 𝑛 ) = ( ℤ/nℤ ‘ 𝑛 )
16 15 zncyg ⊢ ( 𝑛 ∈ ℕ0 → ( ℤ/nℤ ‘ 𝑛 ) ∈ CycGrp )
17 giccyg ⊢ ( ( ℤ/nℤ ‘ 𝑛 ) ≃𝑔 𝐺 → ( ( ℤ/nℤ ‘ 𝑛 ) ∈ CycGrp → 𝐺 ∈ CycGrp ) )
18 14 16 17 syl2imc ⊢ ( 𝑛 ∈ ℕ0 → ( 𝐺 ≃𝑔 ( ℤ/nℤ ‘ 𝑛 ) → 𝐺 ∈ CycGrp ) )
19 18 rexlimiv ⊢ ( ∃ 𝑛 ∈ ℕ0 𝐺 ≃𝑔 ( ℤ/nℤ ‘ 𝑛 ) → 𝐺 ∈ CycGrp )
20 13 19 impbii ⊢ ( 𝐺 ∈ CycGrp ↔ ∃ 𝑛 ∈ ℕ0 𝐺 ≃𝑔 ( ℤ/nℤ ‘ 𝑛 ) )