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	⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ( 𝐹 ‘ ( 𝐿 ‘ 𝑀 ) ) = ( 𝑀 · 𝑋 ) )