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 φ A V B V C V D V
3wlkd.n φ A B A C B C B D C D
3wlkd.e φ A B I J B C I K C D I L
Assertion 3wlkdlem10 φ k 0 ..^ F P k P k + 1 I F k

Proof

Step Hyp Ref Expression
1 3wlkd.p P = ⟨“ ABCD ”⟩
2 3wlkd.f F = ⟨“ JKL ”⟩
3 3wlkd.s φ A V B V C V D V
4 3wlkd.n φ A B A C B C B D C D
5 3wlkd.e φ A B I J B C I K C D I L
6 1 2 3 4 5 3wlkdlem9 φ A B I F 0 B C I F 1 C D I F 2
7 1 2 3 3wlkdlem3 φ P 0 = A P 1 = B P 2 = C P 3 = D
8 preq12 P 0 = A P 1 = B P 0 P 1 = A B
9 8 adantr P 0 = A P 1 = B P 2 = C P 3 = D P 0 P 1 = A B
10 9 sseq1d P 0 = A P 1 = B P 2 = C P 3 = D P 0 P 1 I F 0 A B I F 0
11 simplr P 0 = A P 1 = B P 2 = C P 3 = D P 1 = B
12 simprl P 0 = A P 1 = B P 2 = C P 3 = D P 2 = C
13 11 12 preq12d P 0 = A P 1 = B P 2 = C P 3 = D P 1 P 2 = B C
14 13 sseq1d P 0 = A P 1 = B P 2 = C P 3 = D P 1 P 2 I F 1 B C I F 1
15 preq12 P 2 = C P 3 = D P 2 P 3 = C D
16 15 adantl P 0 = A P 1 = B P 2 = C P 3 = D P 2 P 3 = C D
17 16 sseq1d P 0 = A P 1 = B P 2 = C P 3 = D P 2 P 3 I F 2 C D I F 2
18 10 14 17 3anbi123d P 0 = A P 1 = B P 2 = C P 3 = D P 0 P 1 I F 0 P 1 P 2 I F 1 P 2 P 3 I F 2 A B I F 0 B C I F 1 C D I F 2
19 7 18 syl φ P 0 P 1 I F 0 P 1 P 2 I F 1 P 2 P 3 I F 2 A B I F 0 B C I F 1 C D I F 2
20 6 19 mpbird φ P 0 P 1 I F 0 P 1 P 2 I F 1 P 2 P 3 I F 2
21 1 2 3wlkdlem2 0 ..^ F = 0 1 2
22 21 raleqi k 0 ..^ F P k P k + 1 I F k k 0 1 2 P k P k + 1 I F k
23 c0ex 0 V
24 1ex 1 V
25 2ex 2 V
26 fveq2 k = 0 P k = P 0
27 fv0p1e1 k = 0 P k + 1 = P 1
28 26 27 preq12d k = 0 P k P k + 1 = P 0 P 1
29 2fveq3 k = 0 I F k = I F 0
30 28 29 sseq12d k = 0 P k P k + 1 I F k P 0 P 1 I F 0
31 fveq2 k = 1 P k = P 1
32 oveq1 k = 1 k + 1 = 1 + 1
33 1p1e2 1 + 1 = 2
34 32 33 eqtrdi k = 1 k + 1 = 2
35 34 fveq2d k = 1 P k + 1 = P 2
36 31 35 preq12d k = 1 P k P k + 1 = P 1 P 2
37 2fveq3 k = 1 I F k = I F 1
38 36 37 sseq12d k = 1 P k P k + 1 I F k P 1 P 2 I F 1
39 fveq2 k = 2 P k = P 2
40 oveq1 k = 2 k + 1 = 2 + 1
41 2p1e3 2 + 1 = 3
42 40 41 eqtrdi k = 2 k + 1 = 3
43 42 fveq2d k = 2 P k + 1 = P 3
44 39 43 preq12d k = 2 P k P k + 1 = P 2 P 3
45 2fveq3 k = 2 I F k = I F 2
46 44 45 sseq12d k = 2 P k P k + 1 I F k P 2 P 3 I F 2
47 23 24 25 30 38 46 raltp k 0 1 2 P k P k + 1 I F k P 0 P 1 I F 0 P 1 P 2 I F 1 P 2 P 3 I F 2
48 22 47 bitri k 0 ..^ F P k P k + 1 I F k P 0 P 1 I F 0 P 1 P 2 I F 1 P 2 P 3 I F 2
49 20 48 sylibr φ k 0 ..^ F P k P k + 1 I F k