Theorem cygznlem2a

Description: Lemma for cygzn . (Contributed by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Hypotheses	cygzn.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	cygzn.n	⊢ 𝑁 = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 )
	cygzn.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
	cygzn.m	⊢ · = ( .g ‘ 𝐺 )
	cygzn.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
	cygzn.e	⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 }
	cygzn.g	⊢ ( 𝜑 → 𝐺 ∈ CycGrp )
	cygzn.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
	cygzn.f	⊢ 𝐹 = ran ( 𝑚 ∈ ℤ ↦ ⟨ ( 𝐿 ‘ 𝑚 ) , ( 𝑚 · 𝑋 ) ⟩ )
Assertion	cygznlem2a	⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝑌 ) ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		cygzn.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		cygzn.n	⊢ 𝑁 = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 )
3		cygzn.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
4		cygzn.m	⊢ · = ( .g ‘ 𝐺 )
5		cygzn.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
6		cygzn.e	⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 }
7		cygzn.g	⊢ ( 𝜑 → 𝐺 ∈ CycGrp )
8		cygzn.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
9		cygzn.f	⊢ 𝐹 = ran ( 𝑚 ∈ ℤ ↦ ⟨ ( 𝐿 ‘ 𝑚 ) , ( 𝑚 · 𝑋 ) ⟩ )
10		fvexd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( 𝐿 ‘ 𝑚 ) ∈ V )
11		cyggrp	⊢ ( 𝐺 ∈ CycGrp → 𝐺 ∈ Grp )
12	7 11	syl	⊢ ( 𝜑 → 𝐺 ∈ Grp )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → 𝐺 ∈ Grp )
14		simpr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → 𝑚 ∈ ℤ )
15	6	ssrab3	⊢ 𝐸 ⊆ 𝐵
16	15 8	sseldi	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → 𝑋 ∈ 𝐵 )
18	1 4	mulgcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑚 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑚 · 𝑋 ) ∈ 𝐵 )
19	13 14 17 18	syl3anc	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( 𝑚 · 𝑋 ) ∈ 𝐵 )
20		fveq2	⊢ ( 𝑚 = 𝑘 → ( 𝐿 ‘ 𝑚 ) = ( 𝐿 ‘ 𝑘 ) )
21		oveq1	⊢ ( 𝑚 = 𝑘 → ( 𝑚 · 𝑋 ) = ( 𝑘 · 𝑋 ) )
22	1 2 3 4 5 6 7 8	cygznlem1	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝐿 ‘ 𝑚 ) = ( 𝐿 ‘ 𝑘 ) ↔ ( 𝑚 · 𝑋 ) = ( 𝑘 · 𝑋 ) ) )
23	22	biimpd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝐿 ‘ 𝑚 ) = ( 𝐿 ‘ 𝑘 ) → ( 𝑚 · 𝑋 ) = ( 𝑘 · 𝑋 ) ) )
24	23	exp32	⊢ ( 𝜑 → ( 𝑚 ∈ ℤ → ( 𝑘 ∈ ℤ → ( ( 𝐿 ‘ 𝑚 ) = ( 𝐿 ‘ 𝑘 ) → ( 𝑚 · 𝑋 ) = ( 𝑘 · 𝑋 ) ) ) ) )
25	24	3imp2	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ ( 𝐿 ‘ 𝑚 ) = ( 𝐿 ‘ 𝑘 ) ) ) → ( 𝑚 · 𝑋 ) = ( 𝑘 · 𝑋 ) )
26	9 10 19 20 21 25	fliftfund	⊢ ( 𝜑 → Fun 𝐹 )
27	9 10 19	fliftf	⊢ ( 𝜑 → ( Fun 𝐹 ↔ 𝐹 : ran ( 𝑚 ∈ ℤ ↦ ( 𝐿 ‘ 𝑚 ) ) ⟶ 𝐵 ) )
28	26 27	mpbid	⊢ ( 𝜑 → 𝐹 : ran ( 𝑚 ∈ ℤ ↦ ( 𝐿 ‘ 𝑚 ) ) ⟶ 𝐵 )
29		hashcl	⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
30	29	adantl	⊢ ( ( 𝜑 ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
31		0nn0	⊢ 0 ∈ ℕ0
32	31	a1i	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ Fin ) → 0 ∈ ℕ0 )
33	30 32	ifclda	⊢ ( 𝜑 → if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ∈ ℕ0 )
34	2 33	eqeltrid	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
35		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
36	3 35 5	znzrhfo	⊢ ( 𝑁 ∈ ℕ0 → 𝐿 : ℤ –onto→ ( Base ‘ 𝑌 ) )
37	34 36	syl	⊢ ( 𝜑 → 𝐿 : ℤ –onto→ ( Base ‘ 𝑌 ) )
38		fof	⊢ ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑌 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) )
39	37 38	syl	⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) )
40	39	feqmptd	⊢ ( 𝜑 → 𝐿 = ( 𝑚 ∈ ℤ ↦ ( 𝐿 ‘ 𝑚 ) ) )
41	40	rneqd	⊢ ( 𝜑 → ran 𝐿 = ran ( 𝑚 ∈ ℤ ↦ ( 𝐿 ‘ 𝑚 ) ) )
42		forn	⊢ ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑌 ) → ran 𝐿 = ( Base ‘ 𝑌 ) )
43	37 42	syl	⊢ ( 𝜑 → ran 𝐿 = ( Base ‘ 𝑌 ) )
44	41 43	eqtr3d	⊢ ( 𝜑 → ran ( 𝑚 ∈ ℤ ↦ ( 𝐿 ‘ 𝑚 ) ) = ( Base ‘ 𝑌 ) )
45	44	feq2d	⊢ ( 𝜑 → ( 𝐹 : ran ( 𝑚 ∈ ℤ ↦ ( 𝐿 ‘ 𝑚 ) ) ⟶ 𝐵 ↔ 𝐹 : ( Base ‘ 𝑌 ) ⟶ 𝐵 ) )
46	28 45	mpbid	⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝑌 ) ⟶ 𝐵 )