cygznlem2a

	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	cygznlem2a	$⊢ φ \to F : {Base}_{Y} ⟶ B$

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		fvexd	$⊢ (φ \land m \in ℤ) \to L (m) \in V$
11		cyggrp	$⊢ G \in CycGrp \to G \in Grp$
12	7 11	syl	$⊢ φ \to G \in Grp$
13	12	adantr	$⊢ (φ \land m \in ℤ) \to G \in Grp$
14		simpr	$⊢ (φ \land m \in ℤ) \to m \in ℤ$
15	6	ssrab3	$⊢ E \subseteq B$
16	15 8	sselid	$⊢ φ \to X \in B$
17	16	adantr	$⊢ (φ \land m \in ℤ) \to X \in B$
18	1 4	mulgcl	$⊢ (G \in Grp \land m \in ℤ \land X \in B) \to m \underset{˙}{\cdot} X \in B$
19	13 14 17 18	syl3anc	$⊢ (φ \land m \in ℤ) \to m \underset{˙}{\cdot} X \in B$
20		fveq2	$⊢ m = k \to L (m) = L (k)$
21		oveq1	$⊢ m = k \to m \underset{˙}{\cdot} X = k \underset{˙}{\cdot} X$
22	1 2 3 4 5 6 7 8	cygznlem1	$⊢ (φ \land (m \in ℤ \land k \in ℤ)) \to (L (m) = L (k) \leftrightarrow m \underset{˙}{\cdot} X = k \underset{˙}{\cdot} X)$
23	22	biimpd	$⊢ (φ \land (m \in ℤ \land k \in ℤ)) \to (L (m) = L (k) \to m \underset{˙}{\cdot} X = k \underset{˙}{\cdot} X)$
24	23	exp32	$⊢ φ \to (m \in ℤ \to (k \in ℤ \to (L (m) = L (k) \to m \underset{˙}{\cdot} X = k \underset{˙}{\cdot} X)))$
25	24	3imp2	$⊢ (φ \land (m \in ℤ \land k \in ℤ \land L (m) = L (k))) \to m \underset{˙}{\cdot} X = k \underset{˙}{\cdot} X$
26	9 10 19 20 21 25	fliftfund	$⊢ φ \to Fun F$
27	9 10 19	fliftf	$⊢ φ \to (Fun F \leftrightarrow F : ran (m \in ℤ ⟼ L (m)) ⟶ B)$
28	26 27	mpbid	$⊢ φ \to F : ran (m \in ℤ ⟼ L (m)) ⟶ B$
29		hashcl	$⊢ B \in Fin \to \|B\| \in ℕ_{0}$
30	29	adantl	$⊢ (φ \land B \in Fin) \to \|B\| \in ℕ_{0}$
31		0nn0	$⊢ 0 \in ℕ_{0}$
32	31	a1i	$⊢ (φ \land \neg B \in Fin) \to 0 \in ℕ_{0}$
33	30 32	ifclda	$⊢ φ \to if (B \in Fin, \|B\|, 0) \in ℕ_{0}$
34	2 33	eqeltrid	$⊢ φ \to N \in ℕ_{0}$
35		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
36	3 35 5	znzrhfo	$⊢ N \in ℕ_{0} \to L : ℤ \underset{onto}{⟶} {Base}_{Y}$
37	34 36	syl	$⊢ φ \to L : ℤ \underset{onto}{⟶} {Base}_{Y}$
38		fof	$⊢ L : ℤ \underset{onto}{⟶} {Base}_{Y} \to L : ℤ ⟶ {Base}_{Y}$
39	37 38	syl	$⊢ φ \to L : ℤ ⟶ {Base}_{Y}$
40	39	feqmptd	$⊢ φ \to L = (m \in ℤ ⟼ L (m))$
41	40	rneqd	$⊢ φ \to ran L = ran (m \in ℤ ⟼ L (m))$
42		forn	$⊢ L : ℤ \underset{onto}{⟶} {Base}_{Y} \to ran L = {Base}_{Y}$
43	37 42	syl	$⊢ φ \to ran L = {Base}_{Y}$
44	41 43	eqtr3d	$⊢ φ \to ran (m \in ℤ ⟼ L (m)) = {Base}_{Y}$
45	44	feq2d	$⊢ φ \to (F : ran (m \in ℤ ⟼ L (m)) ⟶ B \leftrightarrow F : {Base}_{Y} ⟶ B)$
46	28 45	mpbid	$⊢ φ \to F : {Base}_{Y} ⟶ B$

Metamath Proof Explorer

Theorem cygznlem2a

Proof