frgpcyg

Description: A free group is cyclic iff it has zero or one generator. (Contributed by Mario Carneiro, 21-Apr-2016) (Proof shortened by AV, 18-Apr-2021)

		Ref	Expression
	Hypothesis	frgpcyg.g	$⊢ G = freeGrp (I)$
	Assertion	frgpcyg	$⊢ I ≼ 1_{𝑜} \leftrightarrow G \in CycGrp$

Proof

Step	Hyp	Ref	Expression
1		frgpcyg.g	$⊢ G = freeGrp (I)$
2		brdom2	$⊢ I ≼ 1_{𝑜} \leftrightarrow (I ≺ 1_{𝑜} \lor I \approx 1_{𝑜})$
3		sdom1	$⊢ I ≺ 1_{𝑜} \leftrightarrow I = \emptyset$
4		fveq2	$⊢ I = \emptyset \to freeGrp (I) = freeGrp (\emptyset)$
5	1 4	eqtrid	$⊢ I = \emptyset \to G = freeGrp (\emptyset)$
6		0ex	$⊢ \emptyset \in V$
7		eqid	$⊢ freeGrp (\emptyset) = freeGrp (\emptyset)$
8	7	frgpgrp	$⊢ \emptyset \in V \to freeGrp (\emptyset) \in Grp$
9	6 8	ax-mp	$⊢ freeGrp (\emptyset) \in Grp$
10		eqid	$⊢ {Base}_{freeGrp (\emptyset)} = {Base}_{freeGrp (\emptyset)}$
11	7 10	0frgp	$⊢ {Base}_{freeGrp (\emptyset)} \approx 1_{𝑜}$
12	10	0cyg	$⊢ (freeGrp (\emptyset) \in Grp \land {Base}_{freeGrp (\emptyset)} \approx 1_{𝑜}) \to freeGrp (\emptyset) \in CycGrp$
13	9 11 12	mp2an	$⊢ freeGrp (\emptyset) \in CycGrp$
14	5 13	eqeltrdi	$⊢ I = \emptyset \to G \in CycGrp$
15	3 14	sylbi	$⊢ I ≺ 1_{𝑜} \to G \in CycGrp$
16		eqid	$⊢ {Base}_{G} = {Base}_{G}$
17		eqid	$⊢ \cdot_{G} = \cdot_{G}$
18		relen	$⊢ Rel \approx$
19	18	brrelex1i	$⊢ I \approx 1_{𝑜} \to I \in V$
20	1	frgpgrp	$⊢ I \in V \to G \in Grp$
21	19 20	syl	$⊢ I \approx 1_{𝑜} \to G \in Grp$
22		eqid	$⊢ ~_{FG} (I) = ~_{FG} (I)$
23		eqid	$⊢ {var}_{FGrp} (I) = {var}_{FGrp} (I)$
24	22 23 1 16	vrgpf	$⊢ I \in V \to {var}_{FGrp} (I) : I ⟶ {Base}_{G}$
25	19 24	syl	$⊢ I \approx 1_{𝑜} \to {var}_{FGrp} (I) : I ⟶ {Base}_{G}$
26		en1uniel	$⊢ I \approx 1_{𝑜} \to ⋃ I \in I$
27	25 26	ffvelrnd	$⊢ I \approx 1_{𝑜} \to {var}_{FGrp} (I) (⋃ I) \in {Base}_{G}$
28		zringgrp	$⊢ ℤ_{ring} \in Grp$
29	19	uniexd	$⊢ I \approx 1_{𝑜} \to ⋃ I \in V$
30		1zzd	$⊢ I \approx 1_{𝑜} \to 1 \in ℤ$
31	29 30	fsnd	$⊢ I \approx 1_{𝑜} \to \{⟨⋃ I, 1⟩\} : \{⋃ I\} ⟶ ℤ$
32		en1b	$⊢ I \approx 1_{𝑜} \leftrightarrow I = \{⋃ I\}$
33	32	biimpi	$⊢ I \approx 1_{𝑜} \to I = \{⋃ I\}$
34	33	feq2d	$⊢ I \approx 1_{𝑜} \to (\{⟨⋃ I, 1⟩\} : I ⟶ ℤ \leftrightarrow \{⟨⋃ I, 1⟩\} : \{⋃ I\} ⟶ ℤ)$
35	31 34	mpbird	$⊢ I \approx 1_{𝑜} \to \{⟨⋃ I, 1⟩\} : I ⟶ ℤ$
36		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
37	1 36 23	frgpup3	$⊢ (ℤ_{ring} \in Grp \land I \in V \land \{⟨⋃ I, 1⟩\} : I ⟶ ℤ) \to \exists! f \in (G GrpHom ℤ_{ring}) f \circ {var}_{FGrp} (I) = \{⟨⋃ I, 1⟩\}$
38	28 19 35 37	mp3an2i	$⊢ I \approx 1_{𝑜} \to \exists! f \in (G GrpHom ℤ_{ring}) f \circ {var}_{FGrp} (I) = \{⟨⋃ I, 1⟩\}$
39	38	adantr	$⊢ (I \approx 1_{𝑜} \land x \in {Base}_{G}) \to \exists! f \in (G GrpHom ℤ_{ring}) f \circ {var}_{FGrp} (I) = \{⟨⋃ I, 1⟩\}$
40		reurex	$⊢ \exists! f \in (G GrpHom ℤ_{ring}) f \circ {var}_{FGrp} (I) = \{⟨⋃ I, 1⟩\} \to \exists f \in (G GrpHom ℤ_{ring}) f \circ {var}_{FGrp} (I) = \{⟨⋃ I, 1⟩\}$
41	39 40	syl	$⊢ (I \approx 1_{𝑜} \land x \in {Base}_{G}) \to \exists f \in (G GrpHom ℤ_{ring}) f \circ {var}_{FGrp} (I) = \{⟨⋃ I, 1⟩\}$
42		fveq1	$⊢ f \circ {var}_{FGrp} (I) = \{⟨⋃ I, 1⟩\} \to (f \circ {var}_{FGrp} (I)) (⋃ I) = \{⟨⋃ I, 1⟩\} (⋃ I)$
43	25 26	fvco3d	$⊢ I \approx 1_{𝑜} \to (f \circ {var}_{FGrp} (I)) (⋃ I) = f ({var}_{FGrp} (I) (⋃ I))$
44		1z	$⊢ 1 \in ℤ$
45		fvsng	$⊢ (⋃ I \in V \land 1 \in ℤ) \to \{⟨⋃ I, 1⟩\} (⋃ I) = 1$
46	29 44 45	sylancl	$⊢ I \approx 1_{𝑜} \to \{⟨⋃ I, 1⟩\} (⋃ I) = 1$
47	43 46	eqeq12d	$⊢ I \approx 1_{𝑜} \to ((f \circ {var}_{FGrp} (I)) (⋃ I) = \{⟨⋃ I, 1⟩\} (⋃ I) \leftrightarrow f ({var}_{FGrp} (I) (⋃ I)) = 1)$
48	42 47	syl5ib	$⊢ I \approx 1_{𝑜} \to (f \circ {var}_{FGrp} (I) = \{⟨⋃ I, 1⟩\} \to f ({var}_{FGrp} (I) (⋃ I)) = 1)$
49	48	ad2antrr	$⊢ ((I \approx 1_{𝑜} \land x \in {Base}_{G}) \land f \in (G GrpHom ℤ_{ring})) \to (f \circ {var}_{FGrp} (I) = \{⟨⋃ I, 1⟩\} \to f ({var}_{FGrp} (I) (⋃ I)) = 1)$
50	16 36	ghmf	$⊢ f \in (G GrpHom ℤ_{ring}) \to f : {Base}_{G} ⟶ ℤ$
51	50	ad2antrl	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to f : {Base}_{G} ⟶ ℤ$
52	51	ffvelrnda	$⊢ ((I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \land x \in {Base}_{G}) \to f (x) \in ℤ$
53	52	an32s	$⊢ ((I \approx 1_{𝑜} \land x \in {Base}_{G}) \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to f (x) \in ℤ$
54		mptresid	$⊢ {I ↾}_{{Base}_{G}} = (x \in {Base}_{G} ⟼ x)$
55	1 16 23	frgpup3	$⊢ (G \in Grp \land I \in V \land {var}_{FGrp} (I) : I ⟶ {Base}_{G}) \to \exists! g \in (G GrpHom G) g \circ {var}_{FGrp} (I) = {var}_{FGrp} (I)$
56	21 19 25 55	syl3anc	$⊢ I \approx 1_{𝑜} \to \exists! g \in (G GrpHom G) g \circ {var}_{FGrp} (I) = {var}_{FGrp} (I)$
57		reurmo	$⊢ \exists! g \in (G GrpHom G) g \circ {var}_{FGrp} (I) = {var}_{FGrp} (I) \to \exists^{*} g \in (G GrpHom G) g \circ {var}_{FGrp} (I) = {var}_{FGrp} (I)$
58	56 57	syl	$⊢ I \approx 1_{𝑜} \to \exists^{*} g \in (G GrpHom G) g \circ {var}_{FGrp} (I) = {var}_{FGrp} (I)$
59	58	adantr	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to \exists^{*} g \in (G GrpHom G) g \circ {var}_{FGrp} (I) = {var}_{FGrp} (I)$
60	21	adantr	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to G \in Grp$
61	16	idghm	$⊢ G \in Grp \to {I ↾}_{{Base}_{G}} \in (G GrpHom G)$
62	60 61	syl	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to {I ↾}_{{Base}_{G}} \in (G GrpHom G)$
63	25	adantr	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to {var}_{FGrp} (I) : I ⟶ {Base}_{G}$
64		fcoi2	$⊢ {var}_{FGrp} (I) : I ⟶ {Base}_{G} \to ({I ↾}_{{Base}_{G}}) \circ {var}_{FGrp} (I) = {var}_{FGrp} (I)$
65	63 64	syl	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to ({I ↾}_{{Base}_{G}}) \circ {var}_{FGrp} (I) = {var}_{FGrp} (I)$
66	51	feqmptd	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to f = (x \in {Base}_{G} ⟼ f (x))$
67		eqidd	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to (n \in ℤ ⟼ n \cdot_{G} {var}_{FGrp} (I) (⋃ I)) = (n \in ℤ ⟼ n \cdot_{G} {var}_{FGrp} (I) (⋃ I))$
68		oveq1	$⊢ n = f (x) \to n \cdot_{G} {var}_{FGrp} (I) (⋃ I) = f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I)$
69	52 66 67 68	fmptco	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to (n \in ℤ ⟼ n \cdot_{G} {var}_{FGrp} (I) (⋃ I)) \circ f = (x \in {Base}_{G} ⟼ f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I))$
70	27	adantr	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to {var}_{FGrp} (I) (⋃ I) \in {Base}_{G}$
71		eqid	$⊢ (n \in ℤ ⟼ n \cdot_{G} {var}_{FGrp} (I) (⋃ I)) = (n \in ℤ ⟼ n \cdot_{G} {var}_{FGrp} (I) (⋃ I))$
72	17 71 16	mulgghm2	$⊢ (G \in Grp \land {var}_{FGrp} (I) (⋃ I) \in {Base}_{G}) \to (n \in ℤ ⟼ n \cdot_{G} {var}_{FGrp} (I) (⋃ I)) \in (ℤ_{ring} GrpHom G)$
73	60 70 72	syl2anc	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to (n \in ℤ ⟼ n \cdot_{G} {var}_{FGrp} (I) (⋃ I)) \in (ℤ_{ring} GrpHom G)$
74		simprl	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to f \in (G GrpHom ℤ_{ring})$
75		ghmco	$⊢ ((n \in ℤ ⟼ n \cdot_{G} {var}_{FGrp} (I) (⋃ I)) \in (ℤ_{ring} GrpHom G) \land f \in (G GrpHom ℤ_{ring})) \to (n \in ℤ ⟼ n \cdot_{G} {var}_{FGrp} (I) (⋃ I)) \circ f \in (G GrpHom G)$
76	73 74 75	syl2anc	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to (n \in ℤ ⟼ n \cdot_{G} {var}_{FGrp} (I) (⋃ I)) \circ f \in (G GrpHom G)$
77	69 76	eqeltrrd	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to (x \in {Base}_{G} ⟼ f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I)) \in (G GrpHom G)$
78	33	adantr	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to I = \{⋃ I\}$
79	78	eleq2d	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to (y \in I \leftrightarrow y \in \{⋃ I\})$
80		simprr	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to f ({var}_{FGrp} (I) (⋃ I)) = 1$
81	80	oveq1d	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to f ({var}_{FGrp} (I) (⋃ I)) \cdot_{G} {var}_{FGrp} (I) (⋃ I) = 1 \cdot_{G} {var}_{FGrp} (I) (⋃ I)$
82	16 17	mulg1	$⊢ {var}_{FGrp} (I) (⋃ I) \in {Base}_{G} \to 1 \cdot_{G} {var}_{FGrp} (I) (⋃ I) = {var}_{FGrp} (I) (⋃ I)$
83	70 82	syl	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to 1 \cdot_{G} {var}_{FGrp} (I) (⋃ I) = {var}_{FGrp} (I) (⋃ I)$
84	81 83	eqtrd	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to f ({var}_{FGrp} (I) (⋃ I)) \cdot_{G} {var}_{FGrp} (I) (⋃ I) = {var}_{FGrp} (I) (⋃ I)$
85		elsni	$⊢ y \in \{⋃ I\} \to y = ⋃ I$
86	85	fveq2d	$⊢ y \in \{⋃ I\} \to {var}_{FGrp} (I) (y) = {var}_{FGrp} (I) (⋃ I)$
87	86	fveq2d	$⊢ y \in \{⋃ I\} \to f ({var}_{FGrp} (I) (y)) = f ({var}_{FGrp} (I) (⋃ I))$
88	87	oveq1d	$⊢ y \in \{⋃ I\} \to f ({var}_{FGrp} (I) (y)) \cdot_{G} {var}_{FGrp} (I) (⋃ I) = f ({var}_{FGrp} (I) (⋃ I)) \cdot_{G} {var}_{FGrp} (I) (⋃ I)$
89	88 86	eqeq12d	$⊢ y \in \{⋃ I\} \to (f ({var}_{FGrp} (I) (y)) \cdot_{G} {var}_{FGrp} (I) (⋃ I) = {var}_{FGrp} (I) (y) \leftrightarrow f ({var}_{FGrp} (I) (⋃ I)) \cdot_{G} {var}_{FGrp} (I) (⋃ I) = {var}_{FGrp} (I) (⋃ I))$
90	84 89	syl5ibrcom	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to (y \in \{⋃ I\} \to f ({var}_{FGrp} (I) (y)) \cdot_{G} {var}_{FGrp} (I) (⋃ I) = {var}_{FGrp} (I) (y))$
91	79 90	sylbid	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to (y \in I \to f ({var}_{FGrp} (I) (y)) \cdot_{G} {var}_{FGrp} (I) (⋃ I) = {var}_{FGrp} (I) (y))$
92	91	imp	$⊢ ((I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \land y \in I) \to f ({var}_{FGrp} (I) (y)) \cdot_{G} {var}_{FGrp} (I) (⋃ I) = {var}_{FGrp} (I) (y)$
93	92	mpteq2dva	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to (y \in I ⟼ f ({var}_{FGrp} (I) (y)) \cdot_{G} {var}_{FGrp} (I) (⋃ I)) = (y \in I ⟼ {var}_{FGrp} (I) (y))$
94	63	ffvelrnda	$⊢ ((I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \land y \in I) \to {var}_{FGrp} (I) (y) \in {Base}_{G}$
95	63	feqmptd	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to {var}_{FGrp} (I) = (y \in I ⟼ {var}_{FGrp} (I) (y))$
96		eqidd	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to (x \in {Base}_{G} ⟼ f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I)) = (x \in {Base}_{G} ⟼ f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I))$
97		fveq2	$⊢ x = {var}_{FGrp} (I) (y) \to f (x) = f ({var}_{FGrp} (I) (y))$
98	97	oveq1d	$⊢ x = {var}_{FGrp} (I) (y) \to f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I) = f ({var}_{FGrp} (I) (y)) \cdot_{G} {var}_{FGrp} (I) (⋃ I)$
99	94 95 96 98	fmptco	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to (x \in {Base}_{G} ⟼ f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I)) \circ {var}_{FGrp} (I) = (y \in I ⟼ f ({var}_{FGrp} (I) (y)) \cdot_{G} {var}_{FGrp} (I) (⋃ I))$
100	93 99 95	3eqtr4d	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to (x \in {Base}_{G} ⟼ f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I)) \circ {var}_{FGrp} (I) = {var}_{FGrp} (I)$
101		coeq1	$⊢ g = {I ↾}_{{Base}_{G}} \to g \circ {var}_{FGrp} (I) = ({I ↾}_{{Base}_{G}}) \circ {var}_{FGrp} (I)$
102	101	eqeq1d	$⊢ g = {I ↾}_{{Base}_{G}} \to (g \circ {var}_{FGrp} (I) = {var}_{FGrp} (I) \leftrightarrow ({I ↾}_{{Base}_{G}}) \circ {var}_{FGrp} (I) = {var}_{FGrp} (I))$
103		coeq1	$⊢ g = (x \in {Base}_{G} ⟼ f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I)) \to g \circ {var}_{FGrp} (I) = (x \in {Base}_{G} ⟼ f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I)) \circ {var}_{FGrp} (I)$
104	103	eqeq1d	$⊢ g = (x \in {Base}_{G} ⟼ f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I)) \to (g \circ {var}_{FGrp} (I) = {var}_{FGrp} (I) \leftrightarrow (x \in {Base}_{G} ⟼ f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I)) \circ {var}_{FGrp} (I) = {var}_{FGrp} (I))$
105	102 104	rmoi	$⊢ (\exists^{*} g \in (G GrpHom G) g \circ {var}_{FGrp} (I) = {var}_{FGrp} (I) \land ({I ↾}_{{Base}_{G}} \in (G GrpHom G) \land ({I ↾}_{{Base}_{G}}) \circ {var}_{FGrp} (I) = {var}_{FGrp} (I)) \land ((x \in {Base}_{G} ⟼ f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I)) \in (G GrpHom G) \land (x \in {Base}_{G} ⟼ f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I)) \circ {var}_{FGrp} (I) = {var}_{FGrp} (I))) \to {I ↾}_{{Base}_{G}} = (x \in {Base}_{G} ⟼ f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I))$
106	59 62 65 77 100 105	syl122anc	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to {I ↾}_{{Base}_{G}} = (x \in {Base}_{G} ⟼ f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I))$
107	54 106	eqtr3id	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to (x \in {Base}_{G} ⟼ x) = (x \in {Base}_{G} ⟼ f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I))$
108		mpteqb	$⊢ \forall x \in {Base}_{G} x \in {Base}_{G} \to ((x \in {Base}_{G} ⟼ x) = (x \in {Base}_{G} ⟼ f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I)) \leftrightarrow \forall x \in {Base}_{G} x = f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I))$
109		id	$⊢ x \in {Base}_{G} \to x \in {Base}_{G}$
110	108 109	mprg	$⊢ (x \in {Base}_{G} ⟼ x) = (x \in {Base}_{G} ⟼ f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I)) \leftrightarrow \forall x \in {Base}_{G} x = f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I)$
111	107 110	sylib	$⊢ (I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to \forall x \in {Base}_{G} x = f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I)$
112	111	r19.21bi	$⊢ ((I \approx 1_{𝑜} \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \land x \in {Base}_{G}) \to x = f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I)$
113	112	an32s	$⊢ ((I \approx 1_{𝑜} \land x \in {Base}_{G}) \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to x = f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I)$
114	68	rspceeqv	$⊢ (f (x) \in ℤ \land x = f (x) \cdot_{G} {var}_{FGrp} (I) (⋃ I)) \to \exists n \in ℤ x = n \cdot_{G} {var}_{FGrp} (I) (⋃ I)$
115	53 113 114	syl2anc	$⊢ ((I \approx 1_{𝑜} \land x \in {Base}_{G}) \land (f \in (G GrpHom ℤ_{ring}) \land f ({var}_{FGrp} (I) (⋃ I)) = 1)) \to \exists n \in ℤ x = n \cdot_{G} {var}_{FGrp} (I) (⋃ I)$
116	115	expr	$⊢ ((I \approx 1_{𝑜} \land x \in {Base}_{G}) \land f \in (G GrpHom ℤ_{ring})) \to (f ({var}_{FGrp} (I) (⋃ I)) = 1 \to \exists n \in ℤ x = n \cdot_{G} {var}_{FGrp} (I) (⋃ I))$
117	49 116	syld	$⊢ ((I \approx 1_{𝑜} \land x \in {Base}_{G}) \land f \in (G GrpHom ℤ_{ring})) \to (f \circ {var}_{FGrp} (I) = \{⟨⋃ I, 1⟩\} \to \exists n \in ℤ x = n \cdot_{G} {var}_{FGrp} (I) (⋃ I))$
118	117	rexlimdva	$⊢ (I \approx 1_{𝑜} \land x \in {Base}_{G}) \to (\exists f \in (G GrpHom ℤ_{ring}) f \circ {var}_{FGrp} (I) = \{⟨⋃ I, 1⟩\} \to \exists n \in ℤ x = n \cdot_{G} {var}_{FGrp} (I) (⋃ I))$
119	41 118	mpd	$⊢ (I \approx 1_{𝑜} \land x \in {Base}_{G}) \to \exists n \in ℤ x = n \cdot_{G} {var}_{FGrp} (I) (⋃ I)$
120	16 17 21 27 119	iscygd	$⊢ I \approx 1_{𝑜} \to G \in CycGrp$
121	15 120	jaoi	$⊢ (I ≺ 1_{𝑜} \lor I \approx 1_{𝑜}) \to G \in CycGrp$
122	2 121	sylbi	$⊢ I ≼ 1_{𝑜} \to G \in CycGrp$
123		cygabl	$⊢ G \in CycGrp \to G \in Abel$
124	1	frgpnabl	$⊢ 1_{𝑜} ≺ I \to \neg G \in Abel$
125	124	con2i	$⊢ G \in Abel \to \neg 1_{𝑜} ≺ I$
126		ablgrp	$⊢ G \in Abel \to G \in Grp$
127		eqid	$⊢ 0_{G} = 0_{G}$
128	16 127	grpidcl	$⊢ G \in Grp \to 0_{G} \in {Base}_{G}$
129	1 16	elbasfv	$⊢ 0_{G} \in {Base}_{G} \to I \in V$
130	126 128 129	3syl	$⊢ G \in Abel \to I \in V$
131		1onn	$⊢ 1_{𝑜} \in ω$
132		nnfi	$⊢ 1_{𝑜} \in ω \to 1_{𝑜} \in Fin$
133	131 132	ax-mp	$⊢ 1_{𝑜} \in Fin$
134		fidomtri2	$⊢ (I \in V \land 1_{𝑜} \in Fin) \to (I ≼ 1_{𝑜} \leftrightarrow \neg 1_{𝑜} ≺ I)$
135	130 133 134	sylancl	$⊢ G \in Abel \to (I ≼ 1_{𝑜} \leftrightarrow \neg 1_{𝑜} ≺ I)$
136	125 135	mpbird	$⊢ G \in Abel \to I ≼ 1_{𝑜}$
137	123 136	syl	$⊢ G \in CycGrp \to I ≼ 1_{𝑜}$
138	122 137	impbii	$⊢ I ≼ 1_{𝑜} \leftrightarrow G \in CycGrp$

Metamath Proof Explorer

Theorem frgpcyg

Proof