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

Metamath Proof Explorer

Theorem cygznlem2

Description: Lemma for cygzn . (Contributed by Mario Carneiro, 21-Apr-2016) (Revised 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 cygznlem2 ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ( 𝐹 ‘ ( 𝐿 ‘ 𝑀 ) ) = ( 𝑀 · 𝑋 ) )

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 ovexd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( 𝑚 · 𝑋 ) ∈ V )
12 fveq2 ⊢ ( 𝑚 = 𝑀 → ( 𝐿 ‘ 𝑚 ) = ( 𝐿 ‘ 𝑀 ) )
13 oveq1 ⊢ ( 𝑚 = 𝑀 → ( 𝑚 · 𝑋 ) = ( 𝑀 · 𝑋 ) )
14 1 2 3 4 5 6 7 8 9 cygznlem2a ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝑌 ) ⟶ 𝐵 )
15 14 ffund ⊢ ( 𝜑 → Fun 𝐹 )
16 9 10 11 12 13 15 fliftval ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ( 𝐹 ‘ ( 𝐿 ‘ 𝑀 ) ) = ( 𝑀 · 𝑋 ) )