cycsubgcl

Description: The set of integer powers of an element A of a group forms a subgroup containing A , called the cyclic group generated by the element A . (Contributed by Mario Carneiro, 13-Jan-2015)

	Ref	Expression
Hypotheses	cycsubg.x	$⊢ X = {Base}_{G}$
	cycsubg.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	cycsubg.f	$⊢ F = (x \in ℤ ⟼ x \underset{˙}{\cdot} A)$
Assertion	cycsubgcl	$⊢ (G \in Grp \land A \in X) \to (ran F \in SubGrp (G) \land A \in ran F)$

Proof

Step	Hyp	Ref	Expression
1		cycsubg.x	$⊢ X = {Base}_{G}$
2		cycsubg.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		cycsubg.f	$⊢ F = (x \in ℤ ⟼ x \underset{˙}{\cdot} A)$
4	1 2	mulgcl	$⊢ (G \in Grp \land x \in ℤ \land A \in X) \to x \underset{˙}{\cdot} A \in X$
5	4	3expa	$⊢ ((G \in Grp \land x \in ℤ) \land A \in X) \to x \underset{˙}{\cdot} A \in X$
6	5	an32s	$⊢ ((G \in Grp \land A \in X) \land x \in ℤ) \to x \underset{˙}{\cdot} A \in X$
7	6 3	fmptd	$⊢ (G \in Grp \land A \in X) \to F : ℤ ⟶ X$
8	7	frnd	$⊢ (G \in Grp \land A \in X) \to ran F \subseteq X$
9	7	ffnd	$⊢ (G \in Grp \land A \in X) \to F Fn ℤ$
10		1z	$⊢ 1 \in ℤ$
11		fnfvelrn	$⊢ (F Fn ℤ \land 1 \in ℤ) \to F (1) \in ran F$
12	9 10 11	sylancl	$⊢ (G \in Grp \land A \in X) \to F (1) \in ran F$
13	12	ne0d	$⊢ (G \in Grp \land A \in X) \to ran F \neq \emptyset$
14		df-3an	$⊢ (m \in ℤ \land n \in ℤ \land A \in X) \leftrightarrow ((m \in ℤ \land n \in ℤ) \land A \in X)$
15		eqid	$⊢ +_{G} = +_{G}$
16	1 2 15	mulgdir	$⊢ (G \in Grp \land (m \in ℤ \land n \in ℤ \land A \in X)) \to (m + n) \underset{˙}{\cdot} A = (m \underset{˙}{\cdot} A) +_{G} (n \underset{˙}{\cdot} A)$
17	14 16	sylan2br	$⊢ (G \in Grp \land ((m \in ℤ \land n \in ℤ) \land A \in X)) \to (m + n) \underset{˙}{\cdot} A = (m \underset{˙}{\cdot} A) +_{G} (n \underset{˙}{\cdot} A)$
18	17	anass1rs	$⊢ ((G \in Grp \land A \in X) \land (m \in ℤ \land n \in ℤ)) \to (m + n) \underset{˙}{\cdot} A = (m \underset{˙}{\cdot} A) +_{G} (n \underset{˙}{\cdot} A)$
19		zaddcl	$⊢ (m \in ℤ \land n \in ℤ) \to m + n \in ℤ$
20	19	adantl	$⊢ ((G \in Grp \land A \in X) \land (m \in ℤ \land n \in ℤ)) \to m + n \in ℤ$
21		oveq1	$⊢ x = m + n \to x \underset{˙}{\cdot} A = (m + n) \underset{˙}{\cdot} A$
22		ovex	$⊢ (m + n) \underset{˙}{\cdot} A \in V$
23	21 3 22	fvmpt	$⊢ m + n \in ℤ \to F (m + n) = (m + n) \underset{˙}{\cdot} A$
24	20 23	syl	$⊢ ((G \in Grp \land A \in X) \land (m \in ℤ \land n \in ℤ)) \to F (m + n) = (m + n) \underset{˙}{\cdot} A$
25		oveq1	$⊢ x = m \to x \underset{˙}{\cdot} A = m \underset{˙}{\cdot} A$
26		ovex	$⊢ m \underset{˙}{\cdot} A \in V$
27	25 3 26	fvmpt	$⊢ m \in ℤ \to F (m) = m \underset{˙}{\cdot} A$
28	27	ad2antrl	$⊢ ((G \in Grp \land A \in X) \land (m \in ℤ \land n \in ℤ)) \to F (m) = m \underset{˙}{\cdot} A$
29		oveq1	$⊢ x = n \to x \underset{˙}{\cdot} A = n \underset{˙}{\cdot} A$
30		ovex	$⊢ n \underset{˙}{\cdot} A \in V$
31	29 3 30	fvmpt	$⊢ n \in ℤ \to F (n) = n \underset{˙}{\cdot} A$
32	31	ad2antll	$⊢ ((G \in Grp \land A \in X) \land (m \in ℤ \land n \in ℤ)) \to F (n) = n \underset{˙}{\cdot} A$
33	28 32	oveq12d	$⊢ ((G \in Grp \land A \in X) \land (m \in ℤ \land n \in ℤ)) \to F (m) +_{G} F (n) = (m \underset{˙}{\cdot} A) +_{G} (n \underset{˙}{\cdot} A)$
34	18 24 33	3eqtr4d	$⊢ ((G \in Grp \land A \in X) \land (m \in ℤ \land n \in ℤ)) \to F (m + n) = F (m) +_{G} F (n)$
35		fnfvelrn	$⊢ (F Fn ℤ \land m + n \in ℤ) \to F (m + n) \in ran F$
36	9 19 35	syl2an	$⊢ ((G \in Grp \land A \in X) \land (m \in ℤ \land n \in ℤ)) \to F (m + n) \in ran F$
37	34 36	eqeltrrd	$⊢ ((G \in Grp \land A \in X) \land (m \in ℤ \land n \in ℤ)) \to F (m) +_{G} F (n) \in ran F$
38	37	anassrs	$⊢ (((G \in Grp \land A \in X) \land m \in ℤ) \land n \in ℤ) \to F (m) +_{G} F (n) \in ran F$
39	38	ralrimiva	$⊢ ((G \in Grp \land A \in X) \land m \in ℤ) \to \forall n \in ℤ F (m) +_{G} F (n) \in ran F$
40		oveq2	$⊢ v = F (n) \to F (m) +_{G} v = F (m) +_{G} F (n)$
41	40	eleq1d	$⊢ v = F (n) \to (F (m) +_{G} v \in ran F \leftrightarrow F (m) +_{G} F (n) \in ran F)$
42	41	ralrn	$⊢ F Fn ℤ \to (\forall v \in ran F F (m) +_{G} v \in ran F \leftrightarrow \forall n \in ℤ F (m) +_{G} F (n) \in ran F)$
43	9 42	syl	$⊢ (G \in Grp \land A \in X) \to (\forall v \in ran F F (m) +_{G} v \in ran F \leftrightarrow \forall n \in ℤ F (m) +_{G} F (n) \in ran F)$
44	43	adantr	$⊢ ((G \in Grp \land A \in X) \land m \in ℤ) \to (\forall v \in ran F F (m) +_{G} v \in ran F \leftrightarrow \forall n \in ℤ F (m) +_{G} F (n) \in ran F)$
45	39 44	mpbird	$⊢ ((G \in Grp \land A \in X) \land m \in ℤ) \to \forall v \in ran F F (m) +_{G} v \in ran F$
46		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
47	1 2 46	mulgneg	$⊢ (G \in Grp \land m \in ℤ \land A \in X) \to (- m) \underset{˙}{\cdot} A = {inv}_{g} (G) (m \underset{˙}{\cdot} A)$
48	47	3expa	$⊢ ((G \in Grp \land m \in ℤ) \land A \in X) \to (- m) \underset{˙}{\cdot} A = {inv}_{g} (G) (m \underset{˙}{\cdot} A)$
49	48	an32s	$⊢ ((G \in Grp \land A \in X) \land m \in ℤ) \to (- m) \underset{˙}{\cdot} A = {inv}_{g} (G) (m \underset{˙}{\cdot} A)$
50		znegcl	$⊢ m \in ℤ \to - m \in ℤ$
51	50	adantl	$⊢ ((G \in Grp \land A \in X) \land m \in ℤ) \to - m \in ℤ$
52		oveq1	$⊢ x = - m \to x \underset{˙}{\cdot} A = (- m) \underset{˙}{\cdot} A$
53		ovex	$⊢ (- m) \underset{˙}{\cdot} A \in V$
54	52 3 53	fvmpt	$⊢ - m \in ℤ \to F (- m) = (- m) \underset{˙}{\cdot} A$
55	51 54	syl	$⊢ ((G \in Grp \land A \in X) \land m \in ℤ) \to F (- m) = (- m) \underset{˙}{\cdot} A$
56	27	adantl	$⊢ ((G \in Grp \land A \in X) \land m \in ℤ) \to F (m) = m \underset{˙}{\cdot} A$
57	56	fveq2d	$⊢ ((G \in Grp \land A \in X) \land m \in ℤ) \to {inv}_{g} (G) (F (m)) = {inv}_{g} (G) (m \underset{˙}{\cdot} A)$
58	49 55 57	3eqtr4d	$⊢ ((G \in Grp \land A \in X) \land m \in ℤ) \to F (- m) = {inv}_{g} (G) (F (m))$
59		fnfvelrn	$⊢ (F Fn ℤ \land - m \in ℤ) \to F (- m) \in ran F$
60	9 50 59	syl2an	$⊢ ((G \in Grp \land A \in X) \land m \in ℤ) \to F (- m) \in ran F$
61	58 60	eqeltrrd	$⊢ ((G \in Grp \land A \in X) \land m \in ℤ) \to {inv}_{g} (G) (F (m)) \in ran F$
62	45 61	jca	$⊢ ((G \in Grp \land A \in X) \land m \in ℤ) \to (\forall v \in ran F F (m) +_{G} v \in ran F \land {inv}_{g} (G) (F (m)) \in ran F)$
63	62	ralrimiva	$⊢ (G \in Grp \land A \in X) \to \forall m \in ℤ (\forall v \in ran F F (m) +_{G} v \in ran F \land {inv}_{g} (G) (F (m)) \in ran F)$
64		oveq1	$⊢ u = F (m) \to u +_{G} v = F (m) +_{G} v$
65	64	eleq1d	$⊢ u = F (m) \to (u +_{G} v \in ran F \leftrightarrow F (m) +_{G} v \in ran F)$
66	65	ralbidv	$⊢ u = F (m) \to (\forall v \in ran F u +_{G} v \in ran F \leftrightarrow \forall v \in ran F F (m) +_{G} v \in ran F)$
67		fveq2	$⊢ u = F (m) \to {inv}_{g} (G) (u) = {inv}_{g} (G) (F (m))$
68	67	eleq1d	$⊢ u = F (m) \to ({inv}_{g} (G) (u) \in ran F \leftrightarrow {inv}_{g} (G) (F (m)) \in ran F)$
69	66 68	anbi12d	$⊢ u = F (m) \to ((\forall v \in ran F u +_{G} v \in ran F \land {inv}_{g} (G) (u) \in ran F) \leftrightarrow (\forall v \in ran F F (m) +_{G} v \in ran F \land {inv}_{g} (G) (F (m)) \in ran F))$
70	69	ralrn	$⊢ F Fn ℤ \to (\forall u \in ran F (\forall v \in ran F u +_{G} v \in ran F \land {inv}_{g} (G) (u) \in ran F) \leftrightarrow \forall m \in ℤ (\forall v \in ran F F (m) +_{G} v \in ran F \land {inv}_{g} (G) (F (m)) \in ran F))$
71	9 70	syl	$⊢ (G \in Grp \land A \in X) \to (\forall u \in ran F (\forall v \in ran F u +_{G} v \in ran F \land {inv}_{g} (G) (u) \in ran F) \leftrightarrow \forall m \in ℤ (\forall v \in ran F F (m) +_{G} v \in ran F \land {inv}_{g} (G) (F (m)) \in ran F))$
72	63 71	mpbird	$⊢ (G \in Grp \land A \in X) \to \forall u \in ran F (\forall v \in ran F u +_{G} v \in ran F \land {inv}_{g} (G) (u) \in ran F)$
73	1 15 46	issubg2	$⊢ G \in Grp \to (ran F \in SubGrp (G) \leftrightarrow (ran F \subseteq X \land ran F \neq \emptyset \land \forall u \in ran F (\forall v \in ran F u +_{G} v \in ran F \land {inv}_{g} (G) (u) \in ran F)))$
74	73	adantr	$⊢ (G \in Grp \land A \in X) \to (ran F \in SubGrp (G) \leftrightarrow (ran F \subseteq X \land ran F \neq \emptyset \land \forall u \in ran F (\forall v \in ran F u +_{G} v \in ran F \land {inv}_{g} (G) (u) \in ran F)))$
75	8 13 72 74	mpbir3and	$⊢ (G \in Grp \land A \in X) \to ran F \in SubGrp (G)$
76		oveq1	$⊢ x = 1 \to x \underset{˙}{\cdot} A = 1 \underset{˙}{\cdot} A$
77		ovex	$⊢ 1 \underset{˙}{\cdot} A \in V$
78	76 3 77	fvmpt	$⊢ 1 \in ℤ \to F (1) = 1 \underset{˙}{\cdot} A$
79	10 78	ax-mp	$⊢ F (1) = 1 \underset{˙}{\cdot} A$
80	1 2	mulg1	$⊢ A \in X \to 1 \underset{˙}{\cdot} A = A$
81	80	adantl	$⊢ (G \in Grp \land A \in X) \to 1 \underset{˙}{\cdot} A = A$
82	79 81	eqtrid	$⊢ (G \in Grp \land A \in X) \to F (1) = A$
83	82 12	eqeltrrd	$⊢ (G \in Grp \land A \in X) \to A \in ran F$
84	75 83	jca	$⊢ (G \in Grp \land A \in X) \to (ran F \in SubGrp (G) \land A \in ran F)$

Metamath Proof Explorer

Theorem cycsubgcl

Proof