Metamath Proof Explorer


Theorem wlkp1lem8

Description: Lemma for wlkp1 . (Contributed by AV, 6-Mar-2021)

Ref Expression
Hypotheses wlkp1.v V = Vtx G
wlkp1.i I = iEdg G
wlkp1.f φ Fun I
wlkp1.a φ I Fin
wlkp1.b φ B W
wlkp1.c φ C V
wlkp1.d φ ¬ B dom I
wlkp1.w φ F Walks G P
wlkp1.n N = F
wlkp1.e φ E Edg G
wlkp1.x φ P N C E
wlkp1.u φ iEdg S = I B E
wlkp1.h H = F N B
wlkp1.q Q = P N + 1 C
wlkp1.s φ Vtx S = V
wlkp1.l φ C = P N E = C
Assertion wlkp1lem8 φ k 0 ..^ H if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k

Proof

Step Hyp Ref Expression
1 wlkp1.v V = Vtx G
2 wlkp1.i I = iEdg G
3 wlkp1.f φ Fun I
4 wlkp1.a φ I Fin
5 wlkp1.b φ B W
6 wlkp1.c φ C V
7 wlkp1.d φ ¬ B dom I
8 wlkp1.w φ F Walks G P
9 wlkp1.n N = F
10 wlkp1.e φ E Edg G
11 wlkp1.x φ P N C E
12 wlkp1.u φ iEdg S = I B E
13 wlkp1.h H = F N B
14 wlkp1.q Q = P N + 1 C
15 wlkp1.s φ Vtx S = V
16 wlkp1.l φ C = P N E = C
17 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 wlkp1lem6 φ k 0 ..^ N Q k = P k Q k + 1 = P k + 1 iEdg S H k = I F k
18 10 elfvexd φ G V
19 1 2 iswlkg G V F Walks G P F Word dom I P : 0 F V k 0 ..^ F if- P k = P k + 1 I F k = P k P k P k + 1 I F k
20 18 19 syl φ F Walks G P F Word dom I P : 0 F V k 0 ..^ F if- P k = P k + 1 I F k = P k P k P k + 1 I F k
21 9 eqcomi F = N
22 21 oveq2i 0 ..^ F = 0 ..^ N
23 22 raleqi k 0 ..^ F if- P k = P k + 1 I F k = P k P k P k + 1 I F k k 0 ..^ N if- P k = P k + 1 I F k = P k P k P k + 1 I F k
24 23 biimpi k 0 ..^ F if- P k = P k + 1 I F k = P k P k P k + 1 I F k k 0 ..^ N if- P k = P k + 1 I F k = P k P k P k + 1 I F k
25 24 3ad2ant3 F Word dom I P : 0 F V k 0 ..^ F if- P k = P k + 1 I F k = P k P k P k + 1 I F k k 0 ..^ N if- P k = P k + 1 I F k = P k P k P k + 1 I F k
26 20 25 syl6bi φ F Walks G P k 0 ..^ N if- P k = P k + 1 I F k = P k P k P k + 1 I F k
27 8 26 mpd φ k 0 ..^ N if- P k = P k + 1 I F k = P k P k P k + 1 I F k
28 eqeq12 Q k = P k Q k + 1 = P k + 1 Q k = Q k + 1 P k = P k + 1
29 28 3adant3 Q k = P k Q k + 1 = P k + 1 iEdg S H k = I F k Q k = Q k + 1 P k = P k + 1
30 simp3 Q k = P k Q k + 1 = P k + 1 iEdg S H k = I F k iEdg S H k = I F k
31 simp1 Q k = P k Q k + 1 = P k + 1 iEdg S H k = I F k Q k = P k
32 31 sneqd Q k = P k Q k + 1 = P k + 1 iEdg S H k = I F k Q k = P k
33 30 32 eqeq12d Q k = P k Q k + 1 = P k + 1 iEdg S H k = I F k iEdg S H k = Q k I F k = P k
34 preq12 Q k = P k Q k + 1 = P k + 1 Q k Q k + 1 = P k P k + 1
35 34 3adant3 Q k = P k Q k + 1 = P k + 1 iEdg S H k = I F k Q k Q k + 1 = P k P k + 1
36 35 30 sseq12d Q k = P k Q k + 1 = P k + 1 iEdg S H k = I F k Q k Q k + 1 iEdg S H k P k P k + 1 I F k
37 29 33 36 ifpbi123d Q k = P k Q k + 1 = P k + 1 iEdg S H k = I F k if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k if- P k = P k + 1 I F k = P k P k P k + 1 I F k
38 37 biimprd Q k = P k Q k + 1 = P k + 1 iEdg S H k = I F k if- P k = P k + 1 I F k = P k P k P k + 1 I F k if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k
39 38 ral2imi k 0 ..^ N Q k = P k Q k + 1 = P k + 1 iEdg S H k = I F k k 0 ..^ N if- P k = P k + 1 I F k = P k P k P k + 1 I F k k 0 ..^ N if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k
40 17 27 39 sylc φ k 0 ..^ N if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k
41 1 2 3 4 5 6 7 8 9 10 11 12 13 wlkp1lem3 φ iEdg S H N = I B E B
42 41 adantr φ Q N = Q N + 1 iEdg S H N = I B E B
43 5 10 7 3jca φ B W E Edg G ¬ B dom I
44 43 adantr φ Q N = Q N + 1 B W E Edg G ¬ B dom I
45 fsnunfv B W E Edg G ¬ B dom I I B E B = E
46 44 45 syl φ Q N = Q N + 1 I B E B = E
47 fveq2 x = N Q x = Q N
48 fveq2 x = N P x = P N
49 47 48 eqeq12d x = N Q x = P x Q N = P N
50 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 wlkp1lem5 φ x 0 N Q x = P x
51 2 wlkf F Walks G P F Word dom I
52 lencl F Word dom I F 0
53 9 eleq1i N 0 F 0
54 elnn0uz N 0 N 0
55 53 54 sylbb1 F 0 N 0
56 52 55 syl F Word dom I N 0
57 8 51 56 3syl φ N 0
58 57 54 sylibr φ N 0
59 nn0fz0 N 0 N 0 N
60 58 59 sylib φ N 0 N
61 49 50 60 rspcdva φ Q N = P N
62 14 fveq1i Q N + 1 = P N + 1 C N + 1
63 ovex N + 1 V
64 1 2 3 4 5 6 7 8 9 wlkp1lem1 φ ¬ N + 1 dom P
65 fsnunfv N + 1 V C V ¬ N + 1 dom P P N + 1 C N + 1 = C
66 63 6 64 65 mp3an2i φ P N + 1 C N + 1 = C
67 62 66 syl5eq φ Q N + 1 = C
68 67 eqeq2d φ P N = Q N + 1 P N = C
69 eqcom P N = C C = P N
70 68 69 bitrdi φ P N = Q N + 1 C = P N
71 sneq C = P N C = P N
72 71 adantl φ C = P N C = P N
73 16 72 eqtrd φ C = P N E = P N
74 73 ex φ C = P N E = P N
75 70 74 sylbid φ P N = Q N + 1 E = P N
76 eqeq1 Q N = P N Q N = Q N + 1 P N = Q N + 1
77 sneq Q N = P N Q N = P N
78 77 eqeq2d Q N = P N E = Q N E = P N
79 76 78 imbi12d Q N = P N Q N = Q N + 1 E = Q N P N = Q N + 1 E = P N
80 75 79 syl5ibrcom φ Q N = P N Q N = Q N + 1 E = Q N
81 61 80 mpd φ Q N = Q N + 1 E = Q N
82 81 imp φ Q N = Q N + 1 E = Q N
83 42 46 82 3eqtrd φ Q N = Q N + 1 iEdg S H N = Q N
84 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 wlkp1lem7 φ Q N Q N + 1 iEdg S H N
85 84 adantr φ ¬ Q N = Q N + 1 Q N Q N + 1 iEdg S H N
86 83 85 ifpimpda φ if- Q N = Q N + 1 iEdg S H N = Q N Q N Q N + 1 iEdg S H N
87 1 2 3 4 5 6 7 8 9 10 11 12 13 wlkp1lem2 φ H = N + 1
88 87 oveq2d φ 0 ..^ H = 0 ..^ N + 1
89 fzosplitsn N 0 0 ..^ N + 1 = 0 ..^ N N
90 57 89 syl φ 0 ..^ N + 1 = 0 ..^ N N
91 88 90 eqtrd φ 0 ..^ H = 0 ..^ N N
92 91 raleqdv φ k 0 ..^ H if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k k 0 ..^ N N if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k
93 ralunb k 0 ..^ N N if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k k 0 ..^ N if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k k N if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k
94 93 a1i φ k 0 ..^ N N if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k k 0 ..^ N if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k k N if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k
95 9 fvexi N V
96 wkslem1 k = N if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k if- Q N = Q N + 1 iEdg S H N = Q N Q N Q N + 1 iEdg S H N
97 96 ralsng N V k N if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k if- Q N = Q N + 1 iEdg S H N = Q N Q N Q N + 1 iEdg S H N
98 95 97 mp1i φ k N if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k if- Q N = Q N + 1 iEdg S H N = Q N Q N Q N + 1 iEdg S H N
99 98 anbi2d φ k 0 ..^ N if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k k N if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k k 0 ..^ N if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k if- Q N = Q N + 1 iEdg S H N = Q N Q N Q N + 1 iEdg S H N
100 92 94 99 3bitrd φ k 0 ..^ H if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k k 0 ..^ N if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k if- Q N = Q N + 1 iEdg S H N = Q N Q N Q N + 1 iEdg S H N
101 40 86 100 mpbir2and φ k 0 ..^ H if- Q k = Q k + 1 iEdg S H k = Q k Q k Q k + 1 iEdg S H k