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 \in Grp \land B \approx 1_{𝑜}) \to G \in CycGrp$

Step	Hyp	Ref	Expression
1		cygctb.1	$⊢ B = {Base}_{G}$
2		eqid	$⊢ \cdot_{G} = \cdot_{G}$
3		simpl	$⊢ (G \in Grp \land B \approx 1_{𝑜}) \to G \in Grp$
4		eqid	$⊢ 0_{G} = 0_{G}$
5	1 4	grpidcl	$⊢ G \in Grp \to 0_{G} \in B$
6	5	adantr	$⊢ (G \in Grp \land B \approx 1_{𝑜}) \to 0_{G} \in B$
7		0z	$⊢ 0 \in ℤ$
8		en1eqsn	$⊢ (0_{G} \in B \land B \approx 1_{𝑜}) \to B = \{0_{G}\}$
9	5 8	sylan	$⊢ (G \in Grp \land B \approx 1_{𝑜}) \to B = \{0_{G}\}$
10	9	eleq2d	$⊢ (G \in Grp \land B \approx 1_{𝑜}) \to (x \in B \leftrightarrow x \in \{0_{G}\})$
11	10	biimpa	$⊢ ((G \in Grp \land B \approx 1_{𝑜}) \land x \in B) \to x \in \{0_{G}\}$
12		velsn	$⊢ x \in \{0_{G}\} \leftrightarrow x = 0_{G}$
13	11 12	sylib	$⊢ ((G \in Grp \land B \approx 1_{𝑜}) \land x \in B) \to x = 0_{G}$
14	1 4 2	mulg0	$⊢ 0_{G} \in B \to 0 \cdot_{G} 0_{G} = 0_{G}$
15	6 14	syl	$⊢ (G \in Grp \land B \approx 1_{𝑜}) \to 0 \cdot_{G} 0_{G} = 0_{G}$
16	15	adantr	$⊢ ((G \in Grp \land B \approx 1_{𝑜}) \land x \in B) \to 0 \cdot_{G} 0_{G} = 0_{G}$
17	13 16	eqtr4d	$⊢ ((G \in Grp \land B \approx 1_{𝑜}) \land x \in B) \to x = 0 \cdot_{G} 0_{G}$
18		oveq1	$⊢ n = 0 \to n \cdot_{G} 0_{G} = 0 \cdot_{G} 0_{G}$
19	18	rspceeqv	$⊢ (0 \in ℤ \land x = 0 \cdot_{G} 0_{G}) \to \exists n \in ℤ x = n \cdot_{G} 0_{G}$
20	7 17 19	sylancr	$⊢ ((G \in Grp \land B \approx 1_{𝑜}) \land x \in B) \to \exists n \in ℤ x = n \cdot_{G} 0_{G}$
21	1 2 3 6 20	iscygd	$⊢ (G \in Grp \land B \approx 1_{𝑜}) \to G \in CycGrp$

Metamath Proof Explorer