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

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 )