cygznlem3

Description: A cyclic group with n elements is isomorphic to ZZ / n ZZ . (Contributed by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	cygzn.b	$⊢ B = {Base}_{G}$
	cygzn.n	$⊢ N = if (B \in Fin, \|B\|, 0)$
	cygzn.y	$⊢ Y = ℤ / N ℤ$
	cygzn.m	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	cygzn.l	$⊢ L = ℤRHom (Y)$
	cygzn.e	$⊢ E = \{x \in B \| ran (n \in ℤ ⟼ n \underset{˙}{\cdot} x) = B\}$
	cygzn.g	$⊢ φ \to G \in CycGrp$
	cygzn.x	$⊢ φ \to X \in E$
	cygzn.f	$⊢ F = ran (m \in ℤ ⟼ ⟨L (m), m \underset{˙}{\cdot} X⟩)$
Assertion	cygznlem3	$⊢ φ \to G ≃_{𝑔} Y$

Proof

Step	Hyp	Ref	Expression
1		cygzn.b	$⊢ B = {Base}_{G}$
2		cygzn.n	$⊢ N = if (B \in Fin, \|B\|, 0)$
3		cygzn.y	$⊢ Y = ℤ / N ℤ$
4		cygzn.m	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
5		cygzn.l	$⊢ L = ℤRHom (Y)$
6		cygzn.e	$⊢ E = \{x \in B \| ran (n \in ℤ ⟼ n \underset{˙}{\cdot} x) = B\}$
7		cygzn.g	$⊢ φ \to G \in CycGrp$
8		cygzn.x	$⊢ φ \to X \in E$
9		cygzn.f	$⊢ F = ran (m \in ℤ ⟼ ⟨L (m), m \underset{˙}{\cdot} X⟩)$
10		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
11		eqid	$⊢ +_{Y} = +_{Y}$
12		eqid	$⊢ +_{G} = +_{G}$
13		hashcl	$⊢ B \in Fin \to \|B\| \in ℕ_{0}$
14	13	adantl	$⊢ (φ \land B \in Fin) \to \|B\| \in ℕ_{0}$
15		0nn0	$⊢ 0 \in ℕ_{0}$
16	15	a1i	$⊢ (φ \land \neg B \in Fin) \to 0 \in ℕ_{0}$
17	14 16	ifclda	$⊢ φ \to if (B \in Fin, \|B\|, 0) \in ℕ_{0}$
18	2 17	eqeltrid	$⊢ φ \to N \in ℕ_{0}$
19	3	zncrng	$⊢ N \in ℕ_{0} \to Y \in CRing$
20		crngring	$⊢ Y \in CRing \to Y \in Ring$
21		ringgrp	$⊢ Y \in Ring \to Y \in Grp$
22	18 19 20 21	4syl	$⊢ φ \to Y \in Grp$
23		cyggrp	$⊢ G \in CycGrp \to G \in Grp$
24	7 23	syl	$⊢ φ \to G \in Grp$
25	1 2 3 4 5 6 7 8 9	cygznlem2a	$⊢ φ \to F : {Base}_{Y} ⟶ B$
26	3 10 5	znzrhfo	$⊢ N \in ℕ_{0} \to L : ℤ \underset{onto}{⟶} {Base}_{Y}$
27	18 26	syl	$⊢ φ \to L : ℤ \underset{onto}{⟶} {Base}_{Y}$
28		foelrn	$⊢ (L : ℤ \underset{onto}{⟶} {Base}_{Y} \land a \in {Base}_{Y}) \to \exists i \in ℤ a = L (i)$
29	27 28	sylan	$⊢ (φ \land a \in {Base}_{Y}) \to \exists i \in ℤ a = L (i)$
30		foelrn	$⊢ (L : ℤ \underset{onto}{⟶} {Base}_{Y} \land b \in {Base}_{Y}) \to \exists j \in ℤ b = L (j)$
31	27 30	sylan	$⊢ (φ \land b \in {Base}_{Y}) \to \exists j \in ℤ b = L (j)$
32	29 31	anim12dan	$⊢ (φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y})) \to (\exists i \in ℤ a = L (i) \land \exists j \in ℤ b = L (j))$
33		reeanv	$⊢ \exists i \in ℤ \exists j \in ℤ (a = L (i) \land b = L (j)) \leftrightarrow (\exists i \in ℤ a = L (i) \land \exists j \in ℤ b = L (j))$
34	24	adantr	$⊢ (φ \land (i \in ℤ \land j \in ℤ)) \to G \in Grp$
35		simprl	$⊢ (φ \land (i \in ℤ \land j \in ℤ)) \to i \in ℤ$
36		simprr	$⊢ (φ \land (i \in ℤ \land j \in ℤ)) \to j \in ℤ$
37	1 4 6	iscyggen	$⊢ X \in E \leftrightarrow (X \in B \land ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) = B)$
38	37	simplbi	$⊢ X \in E \to X \in B$
39	8 38	syl	$⊢ φ \to X \in B$
40	39	adantr	$⊢ (φ \land (i \in ℤ \land j \in ℤ)) \to X \in B$
41	1 4 12	mulgdir	$⊢ (G \in Grp \land (i \in ℤ \land j \in ℤ \land X \in B)) \to (i + j) \underset{˙}{\cdot} X = (i \underset{˙}{\cdot} X) +_{G} (j \underset{˙}{\cdot} X)$
42	34 35 36 40 41	syl13anc	$⊢ (φ \land (i \in ℤ \land j \in ℤ)) \to (i + j) \underset{˙}{\cdot} X = (i \underset{˙}{\cdot} X) +_{G} (j \underset{˙}{\cdot} X)$
43	18 19	syl	$⊢ φ \to Y \in CRing$
44	5	zrhrhm	$⊢ Y \in Ring \to L \in (ℤ_{ring} RingHom Y)$
45		rhmghm	$⊢ L \in (ℤ_{ring} RingHom Y) \to L \in (ℤ_{ring} GrpHom Y)$
46	43 20 44 45	4syl	$⊢ φ \to L \in (ℤ_{ring} GrpHom Y)$
47	46	adantr	$⊢ (φ \land (i \in ℤ \land j \in ℤ)) \to L \in (ℤ_{ring} GrpHom Y)$
48		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
49		zringplusg	$⊢ + = +_{ℤ_{ring}}$
50	48 49 11	ghmlin	$⊢ (L \in (ℤ_{ring} GrpHom Y) \land i \in ℤ \land j \in ℤ) \to L (i + j) = L (i) +_{Y} L (j)$
51	47 35 36 50	syl3anc	$⊢ (φ \land (i \in ℤ \land j \in ℤ)) \to L (i + j) = L (i) +_{Y} L (j)$
52	51	fveq2d	$⊢ (φ \land (i \in ℤ \land j \in ℤ)) \to F (L (i + j)) = F (L (i) +_{Y} L (j))$
53		zaddcl	$⊢ (i \in ℤ \land j \in ℤ) \to i + j \in ℤ$
54	1 2 3 4 5 6 7 8 9	cygznlem2	$⊢ (φ \land i + j \in ℤ) \to F (L (i + j)) = (i + j) \underset{˙}{\cdot} X$
55	53 54	sylan2	$⊢ (φ \land (i \in ℤ \land j \in ℤ)) \to F (L (i + j)) = (i + j) \underset{˙}{\cdot} X$
56	52 55	eqtr3d	$⊢ (φ \land (i \in ℤ \land j \in ℤ)) \to F (L (i) +_{Y} L (j)) = (i + j) \underset{˙}{\cdot} X$
57	1 2 3 4 5 6 7 8 9	cygznlem2	$⊢ (φ \land i \in ℤ) \to F (L (i)) = i \underset{˙}{\cdot} X$
58	57	adantrr	$⊢ (φ \land (i \in ℤ \land j \in ℤ)) \to F (L (i)) = i \underset{˙}{\cdot} X$
59	1 2 3 4 5 6 7 8 9	cygznlem2	$⊢ (φ \land j \in ℤ) \to F (L (j)) = j \underset{˙}{\cdot} X$
60	59	adantrl	$⊢ (φ \land (i \in ℤ \land j \in ℤ)) \to F (L (j)) = j \underset{˙}{\cdot} X$
61	58 60	oveq12d	$⊢ (φ \land (i \in ℤ \land j \in ℤ)) \to F (L (i)) +_{G} F (L (j)) = (i \underset{˙}{\cdot} X) +_{G} (j \underset{˙}{\cdot} X)$
62	42 56 61	3eqtr4d	$⊢ (φ \land (i \in ℤ \land j \in ℤ)) \to F (L (i) +_{Y} L (j)) = F (L (i)) +_{G} F (L (j))$
63		oveq12	$⊢ (a = L (i) \land b = L (j)) \to a +_{Y} b = L (i) +_{Y} L (j)$
64	63	fveq2d	$⊢ (a = L (i) \land b = L (j)) \to F (a +_{Y} b) = F (L (i) +_{Y} L (j))$
65		fveq2	$⊢ a = L (i) \to F (a) = F (L (i))$
66		fveq2	$⊢ b = L (j) \to F (b) = F (L (j))$
67	65 66	oveqan12d	$⊢ (a = L (i) \land b = L (j)) \to F (a) +_{G} F (b) = F (L (i)) +_{G} F (L (j))$
68	64 67	eqeq12d	$⊢ (a = L (i) \land b = L (j)) \to (F (a +_{Y} b) = F (a) +_{G} F (b) \leftrightarrow F (L (i) +_{Y} L (j)) = F (L (i)) +_{G} F (L (j)))$
69	62 68	syl5ibrcom	$⊢ (φ \land (i \in ℤ \land j \in ℤ)) \to ((a = L (i) \land b = L (j)) \to F (a +_{Y} b) = F (a) +_{G} F (b))$
70	69	rexlimdvva	$⊢ φ \to (\exists i \in ℤ \exists j \in ℤ (a = L (i) \land b = L (j)) \to F (a +_{Y} b) = F (a) +_{G} F (b))$
71	33 70	syl5bir	$⊢ φ \to ((\exists i \in ℤ a = L (i) \land \exists j \in ℤ b = L (j)) \to F (a +_{Y} b) = F (a) +_{G} F (b))$
72	71	imp	$⊢ (φ \land (\exists i \in ℤ a = L (i) \land \exists j \in ℤ b = L (j))) \to F (a +_{Y} b) = F (a) +_{G} F (b)$
73	32 72	syldan	$⊢ (φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y})) \to F (a +_{Y} b) = F (a) +_{G} F (b)$
74	10 1 11 12 22 24 25 73	isghmd	$⊢ φ \to F \in (Y GrpHom G)$
75	58 60	eqeq12d	$⊢ (φ \land (i \in ℤ \land j \in ℤ)) \to (F (L (i)) = F (L (j)) \leftrightarrow i \underset{˙}{\cdot} X = j \underset{˙}{\cdot} X)$
76	1 2 3 4 5 6 7 8	cygznlem1	$⊢ (φ \land (i \in ℤ \land j \in ℤ)) \to (L (i) = L (j) \leftrightarrow i \underset{˙}{\cdot} X = j \underset{˙}{\cdot} X)$
77	75 76	bitr4d	$⊢ (φ \land (i \in ℤ \land j \in ℤ)) \to (F (L (i)) = F (L (j)) \leftrightarrow L (i) = L (j))$
78	77	biimpd	$⊢ (φ \land (i \in ℤ \land j \in ℤ)) \to (F (L (i)) = F (L (j)) \to L (i) = L (j))$
79	65 66	eqeqan12d	$⊢ (a = L (i) \land b = L (j)) \to (F (a) = F (b) \leftrightarrow F (L (i)) = F (L (j)))$
80		eqeq12	$⊢ (a = L (i) \land b = L (j)) \to (a = b \leftrightarrow L (i) = L (j))$
81	79 80	imbi12d	$⊢ (a = L (i) \land b = L (j)) \to ((F (a) = F (b) \to a = b) \leftrightarrow (F (L (i)) = F (L (j)) \to L (i) = L (j)))$
82	78 81	syl5ibrcom	$⊢ (φ \land (i \in ℤ \land j \in ℤ)) \to ((a = L (i) \land b = L (j)) \to (F (a) = F (b) \to a = b))$
83	82	rexlimdvva	$⊢ φ \to (\exists i \in ℤ \exists j \in ℤ (a = L (i) \land b = L (j)) \to (F (a) = F (b) \to a = b))$
84	33 83	syl5bir	$⊢ φ \to ((\exists i \in ℤ a = L (i) \land \exists j \in ℤ b = L (j)) \to (F (a) = F (b) \to a = b))$
85	84	imp	$⊢ (φ \land (\exists i \in ℤ a = L (i) \land \exists j \in ℤ b = L (j))) \to (F (a) = F (b) \to a = b)$
86	32 85	syldan	$⊢ (φ \land (a \in {Base}_{Y} \land b \in {Base}_{Y})) \to (F (a) = F (b) \to a = b)$
87	86	ralrimivva	$⊢ φ \to \forall a \in {Base}_{Y} \forall b \in {Base}_{Y} (F (a) = F (b) \to a = b)$
88		dff13	$⊢ F : {Base}_{Y} \underset{1-1}{⟶} B \leftrightarrow (F : {Base}_{Y} ⟶ B \land \forall a \in {Base}_{Y} \forall b \in {Base}_{Y} (F (a) = F (b) \to a = b))$
89	25 87 88	sylanbrc	$⊢ φ \to F : {Base}_{Y} \underset{1-1}{⟶} B$
90	1 4 6	iscyggen2	$⊢ G \in Grp \to (X \in E \leftrightarrow (X \in B \land \forall z \in B \exists n \in ℤ z = n \underset{˙}{\cdot} X))$
91	24 90	syl	$⊢ φ \to (X \in E \leftrightarrow (X \in B \land \forall z \in B \exists n \in ℤ z = n \underset{˙}{\cdot} X))$
92	8 91	mpbid	$⊢ φ \to (X \in B \land \forall z \in B \exists n \in ℤ z = n \underset{˙}{\cdot} X)$
93	92	simprd	$⊢ φ \to \forall z \in B \exists n \in ℤ z = n \underset{˙}{\cdot} X$
94		oveq1	$⊢ n = j \to n \underset{˙}{\cdot} X = j \underset{˙}{\cdot} X$
95	94	eqeq2d	$⊢ n = j \to (z = n \underset{˙}{\cdot} X \leftrightarrow z = j \underset{˙}{\cdot} X)$
96	95	cbvrexvw	$⊢ \exists n \in ℤ z = n \underset{˙}{\cdot} X \leftrightarrow \exists j \in ℤ z = j \underset{˙}{\cdot} X$
97	27	adantr	$⊢ (φ \land z \in B) \to L : ℤ \underset{onto}{⟶} {Base}_{Y}$
98		fof	$⊢ L : ℤ \underset{onto}{⟶} {Base}_{Y} \to L : ℤ ⟶ {Base}_{Y}$
99	97 98	syl	$⊢ (φ \land z \in B) \to L : ℤ ⟶ {Base}_{Y}$
100	99	ffvelrnda	$⊢ ((φ \land z \in B) \land j \in ℤ) \to L (j) \in {Base}_{Y}$
101	59	adantlr	$⊢ ((φ \land z \in B) \land j \in ℤ) \to F (L (j)) = j \underset{˙}{\cdot} X$
102	101	eqcomd	$⊢ ((φ \land z \in B) \land j \in ℤ) \to j \underset{˙}{\cdot} X = F (L (j))$
103		fveq2	$⊢ a = L (j) \to F (a) = F (L (j))$
104	103	rspceeqv	$⊢ (L (j) \in {Base}_{Y} \land j \underset{˙}{\cdot} X = F (L (j))) \to \exists a \in {Base}_{Y} j \underset{˙}{\cdot} X = F (a)$
105	100 102 104	syl2anc	$⊢ ((φ \land z \in B) \land j \in ℤ) \to \exists a \in {Base}_{Y} j \underset{˙}{\cdot} X = F (a)$
106		eqeq1	$⊢ z = j \underset{˙}{\cdot} X \to (z = F (a) \leftrightarrow j \underset{˙}{\cdot} X = F (a))$
107	106	rexbidv	$⊢ z = j \underset{˙}{\cdot} X \to (\exists a \in {Base}_{Y} z = F (a) \leftrightarrow \exists a \in {Base}_{Y} j \underset{˙}{\cdot} X = F (a))$
108	105 107	syl5ibrcom	$⊢ ((φ \land z \in B) \land j \in ℤ) \to (z = j \underset{˙}{\cdot} X \to \exists a \in {Base}_{Y} z = F (a))$
109	108	rexlimdva	$⊢ (φ \land z \in B) \to (\exists j \in ℤ z = j \underset{˙}{\cdot} X \to \exists a \in {Base}_{Y} z = F (a))$
110	96 109	syl5bi	$⊢ (φ \land z \in B) \to (\exists n \in ℤ z = n \underset{˙}{\cdot} X \to \exists a \in {Base}_{Y} z = F (a))$
111	110	ralimdva	$⊢ φ \to (\forall z \in B \exists n \in ℤ z = n \underset{˙}{\cdot} X \to \forall z \in B \exists a \in {Base}_{Y} z = F (a))$
112	93 111	mpd	$⊢ φ \to \forall z \in B \exists a \in {Base}_{Y} z = F (a)$
113		dffo3	$⊢ F : {Base}_{Y} \underset{onto}{⟶} B \leftrightarrow (F : {Base}_{Y} ⟶ B \land \forall z \in B \exists a \in {Base}_{Y} z = F (a))$
114	25 112 113	sylanbrc	$⊢ φ \to F : {Base}_{Y} \underset{onto}{⟶} B$
115		df-f1o	$⊢ F : {Base}_{Y} \underset{1-1 onto}{⟶} B \leftrightarrow (F : {Base}_{Y} \underset{1-1}{⟶} B \land F : {Base}_{Y} \underset{onto}{⟶} B)$
116	89 114 115	sylanbrc	$⊢ φ \to F : {Base}_{Y} \underset{1-1 onto}{⟶} B$
117	10 1	isgim	$⊢ F \in (Y GrpIso G) \leftrightarrow (F \in (Y GrpHom G) \land F : {Base}_{Y} \underset{1-1 onto}{⟶} B)$
118	74 116 117	sylanbrc	$⊢ φ \to F \in (Y GrpIso G)$
119		brgici	$⊢ F \in (Y GrpIso G) \to Y ≃_{𝑔} G$
120		gicsym	$⊢ Y ≃_{𝑔} G \to G ≃_{𝑔} Y$
121	118 119 120	3syl	$⊢ φ \to G ≃_{𝑔} Y$

Metamath Proof Explorer

Theorem cygznlem3

Proof