Metamath Proof Explorer

Theorem 0cyg

Description: The trivial group is cyclic. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypothesis cygctb.1 ⊢ B = Base G
Assertion 0cyg ⊢ G ∈ Grp ∧ B ≈ 1 𝑜 → G ∈ CycGrp

Proof

Step Hyp Ref Expression
1 cygctb.1 ⊢ B = Base G
2 eqid ⊢ ⋅ G = ⋅ G
3 simpl ⊢ G ∈ Grp ∧ B ≈ 1 𝑜 → G ∈ Grp
4 eqid ⊢ 0 G = 0 G
5 1 4 grpidcl ⊢ G ∈ Grp → 0 G ∈ B
6 5 adantr ⊢ G ∈ Grp ∧ B ≈ 1 𝑜 → 0 G ∈ B
7 0z ⊢ 0 ∈ ℤ
8 en1eqsn ⊢ 0 G ∈ B ∧ B ≈ 1 𝑜 → B = 0 G
9 5 8 sylan ⊢ G ∈ Grp ∧ B ≈ 1 𝑜 → B = 0 G
10 9 eleq2d ⊢ G ∈ Grp ∧ B ≈ 1 𝑜 → x ∈ B ↔ x ∈ 0 G
11 10 biimpa ⊢ G ∈ Grp ∧ B ≈ 1 𝑜 ∧ x ∈ B → x ∈ 0 G
12 velsn ⊢ x ∈ 0 G ↔ x = 0 G
13 11 12 sylib ⊢ G ∈ Grp ∧ B ≈ 1 𝑜 ∧ x ∈ B → x = 0 G
14 1 4 2 mulg0 ⊢ 0 G ∈ B → 0 ⋅ G 0 G = 0 G
15 6 14 syl ⊢ G ∈ Grp ∧ B ≈ 1 𝑜 → 0 ⋅ G 0 G = 0 G
16 15 adantr ⊢ G ∈ Grp ∧ B ≈ 1 𝑜 ∧ x ∈ B → 0 ⋅ G 0 G = 0 G
17 13 16 eqtr4d ⊢ G ∈ Grp ∧ B ≈ 1 𝑜 ∧ x ∈ B → x = 0 ⋅ G 0 G
18 oveq1 ⊢ n = 0 → n ⋅ G 0 G = 0 ⋅ G 0 G
19 18 rspceeqv ⊢ 0 ∈ ℤ ∧ x = 0 ⋅ G 0 G → ∃ n ∈ ℤ x = n ⋅ G 0 G
20 7 17 19 sylancr ⊢ G ∈ Grp ∧ B ≈ 1 𝑜 ∧ x ∈ B → ∃ n ∈ ℤ x = n ⋅ G 0 G
21 1 2 3 6 20 iscygd ⊢ G ∈ Grp ∧ B ≈ 1 𝑜 → G ∈ CycGrp