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 ⊢ B = Base G
cygzn.n ⊢ N = if B ∈ Fin B 0
cygzn.y ⊢ Y = ℤ/Nℤ
cygzn.m ⊢ · ˙ = ⋅ G
cygzn.l ⊢ L = ℤRHom ⁡ Y
cygzn.e ⊢ E = x ∈ B | ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B
cygzn.g ⊢ φ → G ∈ CycGrp
cygzn.x ⊢ φ → X ∈ E
cygzn.f ⊢ F = ran ⁡ m ∈ ℤ ⟼ L ⁡ m m · ˙ X
Assertion cygznlem2 ⊢ φ ∧ M ∈ ℤ → F ⁡ L ⁡ M = M · ˙ X

Proof

Step Hyp Ref Expression
1 cygzn.b ⊢ B = Base G
2 cygzn.n ⊢ N = if B ∈ Fin B 0
3 cygzn.y ⊢ Y = ℤ/Nℤ
4 cygzn.m ⊢ · ˙ = ⋅ G
5 cygzn.l ⊢ L = ℤRHom ⁡ Y
6 cygzn.e ⊢ E = x ∈ B | ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B
7 cygzn.g ⊢ φ → G ∈ CycGrp
8 cygzn.x ⊢ φ → X ∈ E
9 cygzn.f ⊢ F = ran ⁡ m ∈ ℤ ⟼ L ⁡ m m · ˙ X
10 fvexd ⊢ φ ∧ m ∈ ℤ → L ⁡ m ∈ V
11 ovexd ⊢ φ ∧ m ∈ ℤ → m · ˙ X ∈ V
12 fveq2 ⊢ m = M → L ⁡ m = L ⁡ M
13 oveq1 ⊢ m = M → m · ˙ X = M · ˙ X
14 1 2 3 4 5 6 7 8 9 cygznlem2a ⊢ φ → F : Base Y ⟶ B
15 14 ffund ⊢ φ → Fun ⁡ F
16 9 10 11 12 13 15 fliftval ⊢ φ ∧ M ∈ ℤ → F ⁡ L ⁡ M = M · ˙ X