Metamath Proof Explorer

Theorem wlkiswwlks2lem2

Description: Lemma 2 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 wlkiswwlks2lem2 ⊢ P ∈ ℕ 0 ∧ I ∈ 0 ..^ P − 1 → F ⁡ I = E -1 ⁡ P ⁡ I P ⁡ I + 1

Proof

Step Hyp Ref Expression
1 wlkiswwlks2lem.f ⊢ F = x ∈ 0 ..^ P − 1 ⟼ E -1 ⁡ P ⁡ x P ⁡ x + 1
2 fveq2 ⊢ x = I → P ⁡ x = P ⁡ I
3 fvoveq1 ⊢ x = I → P ⁡ x + 1 = P ⁡ I + 1
4 2 3 preq12d ⊢ x = I → P ⁡ x P ⁡ x + 1 = P ⁡ I P ⁡ I + 1
5 4 fveq2d ⊢ x = I → E -1 ⁡ P ⁡ x P ⁡ x + 1 = E -1 ⁡ P ⁡ I P ⁡ I + 1
6 simpr ⊢ P ∈ ℕ 0 ∧ I ∈ 0 ..^ P − 1 → I ∈ 0 ..^ P − 1
7 fvexd ⊢ P ∈ ℕ 0 ∧ I ∈ 0 ..^ P − 1 → E -1 ⁡ P ⁡ I P ⁡ I + 1 ∈ V
8 1 5 6 7 fvmptd3 ⊢ P ∈ ℕ 0 ∧ I ∈ 0 ..^ P − 1 → F ⁡ I = E -1 ⁡ P ⁡ I P ⁡ I + 1