cycsubgcyg

Description: The cyclic subgroup generated by A is a cyclic group. (Contributed by Mario Carneiro, 24-Apr-2016)

	Ref	Expression
Hypotheses	cycsubgcyg.x	$⊢ X = {Base}_{G}$
	cycsubgcyg.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	cycsubgcyg.s	$⊢ S = ran (x \in ℤ ⟼ x \underset{˙}{\cdot} A)$
Assertion	cycsubgcyg	$⊢ (G \in Grp \land A \in X) \to G ↾_{𝑠} S \in CycGrp$

Proof

Step	Hyp	Ref	Expression
1		cycsubgcyg.x	$⊢ X = {Base}_{G}$
2		cycsubgcyg.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		cycsubgcyg.s	$⊢ S = ran (x \in ℤ ⟼ x \underset{˙}{\cdot} A)$
4		eqid	$⊢ {Base}_{(G ↾_{𝑠} S)} = {Base}_{(G ↾_{𝑠} S)}$
5		eqid	$⊢ \cdot_{(G ↾_{𝑠} S)} = \cdot_{(G ↾_{𝑠} S)}$
6		eqid	$⊢ (x \in ℤ ⟼ x \underset{˙}{\cdot} A) = (x \in ℤ ⟼ x \underset{˙}{\cdot} A)$
7	1 2 6	cycsubgcl	$⊢ (G \in Grp \land A \in X) \to (ran (x \in ℤ ⟼ x \underset{˙}{\cdot} A) \in SubGrp (G) \land A \in ran (x \in ℤ ⟼ x \underset{˙}{\cdot} A))$
8	7	simpld	$⊢ (G \in Grp \land A \in X) \to ran (x \in ℤ ⟼ x \underset{˙}{\cdot} A) \in SubGrp (G)$
9	3 8	eqeltrid	$⊢ (G \in Grp \land A \in X) \to S \in SubGrp (G)$
10		eqid	$⊢ G ↾_{𝑠} S = G ↾_{𝑠} S$
11	10	subggrp	$⊢ S \in SubGrp (G) \to G ↾_{𝑠} S \in Grp$
12	9 11	syl	$⊢ (G \in Grp \land A \in X) \to G ↾_{𝑠} S \in Grp$
13	7	simprd	$⊢ (G \in Grp \land A \in X) \to A \in ran (x \in ℤ ⟼ x \underset{˙}{\cdot} A)$
14	13 3	eleqtrrdi	$⊢ (G \in Grp \land A \in X) \to A \in S$
15	10	subgbas	$⊢ S \in SubGrp (G) \to S = {Base}_{(G ↾_{𝑠} S)}$
16	9 15	syl	$⊢ (G \in Grp \land A \in X) \to S = {Base}_{(G ↾_{𝑠} S)}$
17	14 16	eleqtrd	$⊢ (G \in Grp \land A \in X) \to A \in {Base}_{(G ↾_{𝑠} S)}$
18	16	eleq2d	$⊢ (G \in Grp \land A \in X) \to (y \in S \leftrightarrow y \in {Base}_{(G ↾_{𝑠} S)})$
19	18	biimpar	$⊢ ((G \in Grp \land A \in X) \land y \in {Base}_{(G ↾_{𝑠} S)}) \to y \in S$
20		simpr	$⊢ ((G \in Grp \land A \in X) \land y \in S) \to y \in S$
21	20 3	eleqtrdi	$⊢ ((G \in Grp \land A \in X) \land y \in S) \to y \in ran (x \in ℤ ⟼ x \underset{˙}{\cdot} A)$
22		oveq1	$⊢ x = n \to x \underset{˙}{\cdot} A = n \underset{˙}{\cdot} A$
23	22	cbvmptv	$⊢ (x \in ℤ ⟼ x \underset{˙}{\cdot} A) = (n \in ℤ ⟼ n \underset{˙}{\cdot} A)$
24		ovex	$⊢ n \underset{˙}{\cdot} A \in V$
25	23 24	elrnmpti	$⊢ y \in ran (x \in ℤ ⟼ x \underset{˙}{\cdot} A) \leftrightarrow \exists n \in ℤ y = n \underset{˙}{\cdot} A$
26	21 25	sylib	$⊢ ((G \in Grp \land A \in X) \land y \in S) \to \exists n \in ℤ y = n \underset{˙}{\cdot} A$
27	9	ad2antrr	$⊢ (((G \in Grp \land A \in X) \land y \in S) \land n \in ℤ) \to S \in SubGrp (G)$
28		simpr	$⊢ (((G \in Grp \land A \in X) \land y \in S) \land n \in ℤ) \to n \in ℤ$
29	14	ad2antrr	$⊢ (((G \in Grp \land A \in X) \land y \in S) \land n \in ℤ) \to A \in S$
30	2 10 5	subgmulg	$⊢ (S \in SubGrp (G) \land n \in ℤ \land A \in S) \to n \underset{˙}{\cdot} A = n \cdot_{(G ↾_{𝑠} S)} A$
31	27 28 29 30	syl3anc	$⊢ (((G \in Grp \land A \in X) \land y \in S) \land n \in ℤ) \to n \underset{˙}{\cdot} A = n \cdot_{(G ↾_{𝑠} S)} A$
32	31	eqeq2d	$⊢ (((G \in Grp \land A \in X) \land y \in S) \land n \in ℤ) \to (y = n \underset{˙}{\cdot} A \leftrightarrow y = n \cdot_{(G ↾_{𝑠} S)} A)$
33	32	rexbidva	$⊢ ((G \in Grp \land A \in X) \land y \in S) \to (\exists n \in ℤ y = n \underset{˙}{\cdot} A \leftrightarrow \exists n \in ℤ y = n \cdot_{(G ↾_{𝑠} S)} A)$
34	26 33	mpbid	$⊢ ((G \in Grp \land A \in X) \land y \in S) \to \exists n \in ℤ y = n \cdot_{(G ↾_{𝑠} S)} A$
35	19 34	syldan	$⊢ ((G \in Grp \land A \in X) \land y \in {Base}_{(G ↾_{𝑠} S)}) \to \exists n \in ℤ y = n \cdot_{(G ↾_{𝑠} S)} A$
36	4 5 12 17 35	iscygd	$⊢ (G \in Grp \land A \in X) \to G ↾_{𝑠} S \in CycGrp$

Metamath Proof Explorer

Theorem cycsubgcyg

Proof