Metamath Proof Explorer


Theorem 3wlkdlem10

Description: Lemma 10 for 3wlkd . (Contributed by Alexander van der Vekens, 12-Nov-2017) (Revised by AV, 7-Feb-2021)

Ref Expression
Hypotheses 3wlkd.p P=⟨“ABCD”⟩
3wlkd.f F=⟨“JKL”⟩
3wlkd.s φAVBVCVDV
3wlkd.n φABACBCBDCD
3wlkd.e φABIJBCIKCDIL
Assertion 3wlkdlem10 φk0..^FPkPk+1IFk

Proof

Step Hyp Ref Expression
1 3wlkd.p P=⟨“ABCD”⟩
2 3wlkd.f F=⟨“JKL”⟩
3 3wlkd.s φAVBVCVDV
4 3wlkd.n φABACBCBDCD
5 3wlkd.e φABIJBCIKCDIL
6 1 2 3 4 5 3wlkdlem9 φABIF0BCIF1CDIF2
7 1 2 3 3wlkdlem3 φP0=AP1=BP2=CP3=D
8 preq12 P0=AP1=BP0P1=AB
9 8 adantr P0=AP1=BP2=CP3=DP0P1=AB
10 9 sseq1d P0=AP1=BP2=CP3=DP0P1IF0ABIF0
11 simplr P0=AP1=BP2=CP3=DP1=B
12 simprl P0=AP1=BP2=CP3=DP2=C
13 11 12 preq12d P0=AP1=BP2=CP3=DP1P2=BC
14 13 sseq1d P0=AP1=BP2=CP3=DP1P2IF1BCIF1
15 preq12 P2=CP3=DP2P3=CD
16 15 adantl P0=AP1=BP2=CP3=DP2P3=CD
17 16 sseq1d P0=AP1=BP2=CP3=DP2P3IF2CDIF2
18 10 14 17 3anbi123d P0=AP1=BP2=CP3=DP0P1IF0P1P2IF1P2P3IF2ABIF0BCIF1CDIF2
19 7 18 syl φP0P1IF0P1P2IF1P2P3IF2ABIF0BCIF1CDIF2
20 6 19 mpbird φP0P1IF0P1P2IF1P2P3IF2
21 1 2 3wlkdlem2 0..^F=012
22 21 raleqi k0..^FPkPk+1IFkk012PkPk+1IFk
23 c0ex 0V
24 1ex 1V
25 2ex 2V
26 fveq2 k=0Pk=P0
27 fv0p1e1 k=0Pk+1=P1
28 26 27 preq12d k=0PkPk+1=P0P1
29 2fveq3 k=0IFk=IF0
30 28 29 sseq12d k=0PkPk+1IFkP0P1IF0
31 fveq2 k=1Pk=P1
32 oveq1 k=1k+1=1+1
33 1p1e2 1+1=2
34 32 33 eqtrdi k=1k+1=2
35 34 fveq2d k=1Pk+1=P2
36 31 35 preq12d k=1PkPk+1=P1P2
37 2fveq3 k=1IFk=IF1
38 36 37 sseq12d k=1PkPk+1IFkP1P2IF1
39 fveq2 k=2Pk=P2
40 oveq1 k=2k+1=2+1
41 2p1e3 2+1=3
42 40 41 eqtrdi k=2k+1=3
43 42 fveq2d k=2Pk+1=P3
44 39 43 preq12d k=2PkPk+1=P2P3
45 2fveq3 k=2IFk=IF2
46 44 45 sseq12d k=2PkPk+1IFkP2P3IF2
47 23 24 25 30 38 46 raltp k012PkPk+1IFkP0P1IF0P1P2IF1P2P3IF2
48 22 47 bitri k0..^FPkPk+1IFkP0P1IF0P1P2IF1P2P3IF2
49 20 48 sylibr φk0..^FPkPk+1IFk