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 )