Metamath Proof Explorer

Theorem wlkiswwlks2lem3

Description: Lemma 3 for wlkiswwlks2 . (Contributed by Alexander van der Vekens, 20-Jul-2018)

Ref Expression
Hypothesis wlkiswwlks2lem.f ⊢ F = x ∈ 0 ..^ P − 1 ⟼ E -1 ⁡ P ⁡ x P ⁡ x + 1
Assertion wlkiswwlks2lem3 ⊢ P ∈ Word V ∧ 1 ≤ P → P : 0 … F ⟶ V

Proof

Step Hyp Ref Expression
1 wlkiswwlks2lem.f ⊢ F = x ∈ 0 ..^ P − 1 ⟼ E -1 ⁡ P ⁡ x P ⁡ x + 1
2 1 wlkiswwlks2lem1 ⊢ P ∈ Word V ∧ 1 ≤ P → F = P − 1
3 wrdf ⊢ P ∈ Word V → P : 0 ..^ P ⟶ V
4 lencl ⊢ P ∈ Word V → P ∈ ℕ 0
5 nn0z ⊢ P ∈ ℕ 0 → P ∈ ℤ
6 fzoval ⊢ P ∈ ℤ → 0 ..^ P = 0 … P − 1
7 5 6 syl ⊢ P ∈ ℕ 0 → 0 ..^ P = 0 … P − 1
8 oveq2 ⊢ P − 1 = F → 0 … P − 1 = 0 … F
9 8 eqcoms ⊢ F = P − 1 → 0 … P − 1 = 0 … F
10 7 9 sylan9eq ⊢ P ∈ ℕ 0 ∧ F = P − 1 → 0 ..^ P = 0 … F
11 10 feq2d ⊢ P ∈ ℕ 0 ∧ F = P − 1 → P : 0 ..^ P ⟶ V ↔ P : 0 … F ⟶ V
12 11 biimpcd ⊢ P : 0 ..^ P ⟶ V → P ∈ ℕ 0 ∧ F = P − 1 → P : 0 … F ⟶ V
13 12 expd ⊢ P : 0 ..^ P ⟶ V → P ∈ ℕ 0 → F = P − 1 → P : 0 … F ⟶ V
14 3 4 13 sylc ⊢ P ∈ Word V → F = P − 1 → P : 0 … F ⟶ V
15 14 adantr ⊢ P ∈ Word V ∧ 1 ≤ P → F = P − 1 → P : 0 … F ⟶ V
16 2 15 mpd ⊢ P ∈ Word V ∧ 1 ≤ P → P : 0 … F ⟶ V