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=x0..^P1E-1PxPx+1
Assertion wlkiswwlks2lem2 P0I0..^P1FI=E-1PIPI+1

Proof

Step Hyp Ref Expression
1 wlkiswwlks2lem.f F=x0..^P1E-1PxPx+1
2 fveq2 x=IPx=PI
3 fvoveq1 x=IPx+1=PI+1
4 2 3 preq12d x=IPxPx+1=PIPI+1
5 4 fveq2d x=IE-1PxPx+1=E-1PIPI+1
6 simpr P0I0..^P1I0..^P1
7 fvexd P0I0..^P1E-1PIPI+1V
8 1 5 6 7 fvmptd3 P0I0..^P1FI=E-1PIPI+1