This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 sselid ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
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 ‘ 𝑌 ) ⟶ 𝐵 )