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⁡xP⁡x+1
Assertion wlkiswwlks2lem3 ⊢P∈WordV∧1≤P→P:0…F⟶V

Proof

Step Hyp Ref Expression
1 wlkiswwlks2lem.f ⊢F=x∈0..^P−1⟼E-1⁡P⁡xP⁡x+1
2 1 wlkiswwlks2lem1 ⊢P∈WordV∧1≤P→F=P−1
3 wrdf ⊢P∈WordV→P:0..^P⟶V
4 lencl ⊢P∈WordV→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∈WordV→F=P−1→P:0…F⟶V
15 14 adantr ⊢P∈WordV∧1≤P→F=P−1→P:0…F⟶V
16 2 15 mpd ⊢P∈WordV∧1≤P→P:0…F⟶V