Metamath Proof Explorer


Theorem 0cyg

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

Ref Expression
Hypothesis cygctb.1 𝐵 = ( Base ‘ 𝐺 )
Assertion 0cyg ( ( 𝐺 ∈ Grp ∧ 𝐵 ≈ 1o ) → 𝐺 ∈ CycGrp )

Proof

Step Hyp Ref Expression
1 cygctb.1 𝐵 = ( Base ‘ 𝐺 )
2 eqid ( .g𝐺 ) = ( .g𝐺 )
3 simpl ( ( 𝐺 ∈ Grp ∧ 𝐵 ≈ 1o ) → 𝐺 ∈ Grp )
4 eqid ( 0g𝐺 ) = ( 0g𝐺 )
5 1 4 grpidcl ( 𝐺 ∈ Grp → ( 0g𝐺 ) ∈ 𝐵 )
6 5 adantr ( ( 𝐺 ∈ Grp ∧ 𝐵 ≈ 1o ) → ( 0g𝐺 ) ∈ 𝐵 )
7 0z 0 ∈ ℤ
8 en1eqsn ( ( ( 0g𝐺 ) ∈ 𝐵𝐵 ≈ 1o ) → 𝐵 = { ( 0g𝐺 ) } )
9 5 8 sylan ( ( 𝐺 ∈ Grp ∧ 𝐵 ≈ 1o ) → 𝐵 = { ( 0g𝐺 ) } )
10 9 eleq2d ( ( 𝐺 ∈ Grp ∧ 𝐵 ≈ 1o ) → ( 𝑥𝐵𝑥 ∈ { ( 0g𝐺 ) } ) )
11 10 biimpa ( ( ( 𝐺 ∈ Grp ∧ 𝐵 ≈ 1o ) ∧ 𝑥𝐵 ) → 𝑥 ∈ { ( 0g𝐺 ) } )
12 velsn ( 𝑥 ∈ { ( 0g𝐺 ) } ↔ 𝑥 = ( 0g𝐺 ) )
13 11 12 sylib ( ( ( 𝐺 ∈ Grp ∧ 𝐵 ≈ 1o ) ∧ 𝑥𝐵 ) → 𝑥 = ( 0g𝐺 ) )
14 1 4 2 mulg0 ( ( 0g𝐺 ) ∈ 𝐵 → ( 0 ( .g𝐺 ) ( 0g𝐺 ) ) = ( 0g𝐺 ) )
15 6 14 syl ( ( 𝐺 ∈ Grp ∧ 𝐵 ≈ 1o ) → ( 0 ( .g𝐺 ) ( 0g𝐺 ) ) = ( 0g𝐺 ) )
16 15 adantr ( ( ( 𝐺 ∈ Grp ∧ 𝐵 ≈ 1o ) ∧ 𝑥𝐵 ) → ( 0 ( .g𝐺 ) ( 0g𝐺 ) ) = ( 0g𝐺 ) )
17 13 16 eqtr4d ( ( ( 𝐺 ∈ Grp ∧ 𝐵 ≈ 1o ) ∧ 𝑥𝐵 ) → 𝑥 = ( 0 ( .g𝐺 ) ( 0g𝐺 ) ) )
18 oveq1 ( 𝑛 = 0 → ( 𝑛 ( .g𝐺 ) ( 0g𝐺 ) ) = ( 0 ( .g𝐺 ) ( 0g𝐺 ) ) )
19 18 rspceeqv ( ( 0 ∈ ℤ ∧ 𝑥 = ( 0 ( .g𝐺 ) ( 0g𝐺 ) ) ) → ∃ 𝑛 ∈ ℤ 𝑥 = ( 𝑛 ( .g𝐺 ) ( 0g𝐺 ) ) )
20 7 17 19 sylancr ( ( ( 𝐺 ∈ Grp ∧ 𝐵 ≈ 1o ) ∧ 𝑥𝐵 ) → ∃ 𝑛 ∈ ℤ 𝑥 = ( 𝑛 ( .g𝐺 ) ( 0g𝐺 ) ) )
21 1 2 3 6 20 iscygd ( ( 𝐺 ∈ Grp ∧ 𝐵 ≈ 1o ) → 𝐺 ∈ CycGrp )