Metamath Proof Explorer

Theorem wwlksnextwrd

Description: Lemma for wwlksnextbij . (Contributed by Alexander van der Vekens, 5-Aug-2018) (Revised by AV, 18-Apr-2021) (Revised by AV, 27-Oct-2022)

Ref Expression
Hypotheses wwlksnextbij0.v ⊢V=Vtx⁡G
wwlksnextbij0.e ⊢E=Edg⁡G
wwlksnextbij0.d ⊢D=w∈WordV|w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E
Assertion wwlksnextwrd ⊢W∈NWWalksNG→D=w∈N+1WWalksNG|wprefixN+1=W∧lastS⁡WlastS⁡w∈E

Proof

Step Hyp Ref Expression
1 wwlksnextbij0.v ⊢V=Vtx⁡G
2 wwlksnextbij0.e ⊢E=Edg⁡G
3 wwlksnextbij0.d ⊢D=w∈WordV|w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E
4 3anass ⊢w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E↔w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E
5 4 bianass ⊢w∈WordV∧w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E↔w∈WordV∧w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E
6 1 wwlknbp ⊢W∈NWWalksNG→G∈V∧N∈ℕ0∧W∈WordV
7 simpl ⊢N∈ℕ0∧w∈WordV∧w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E→N∈ℕ0
8 simpl ⊢w∈WordV∧w=N+2→w∈WordV
9 nn0re ⊢N∈ℕ0→N∈ℝ
10 2re ⊢2∈ℝ
11 10 a1i ⊢N∈ℕ0→2∈ℝ
12 nn0ge0 ⊢N∈ℕ0→0≤N
13 2pos ⊢0<2
14 13 a1i ⊢N∈ℕ0→0<2
15 9 11 12 14 addgegt0d ⊢N∈ℕ0→0<N+2
16 15 adantr ⊢N∈ℕ0∧w∈WordV∧w=N+2→0<N+2
17 breq2 ⊢w=N+2→0<w↔0<N+2
18 17 ad2antll ⊢N∈ℕ0∧w∈WordV∧w=N+2→0<w↔0<N+2
19 16 18 mpbird ⊢N∈ℕ0∧w∈WordV∧w=N+2→0<w
20 hashgt0n0 ⊢w∈WordV∧0<w→w≠∅
21 8 19 20 syl2an2 ⊢N∈ℕ0∧w∈WordV∧w=N+2→w≠∅
22 lswcl ⊢w∈WordV∧w≠∅→lastS⁡w∈V
23 8 21 22 syl2an2 ⊢N∈ℕ0∧w∈WordV∧w=N+2→lastS⁡w∈V
24 23 adantrr ⊢N∈ℕ0∧w∈WordV∧w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E→lastS⁡w∈V
25 pfxcl ⊢w∈WordV→wprefixN+1∈WordV
26 eleq1 ⊢W=wprefixN+1→W∈WordV↔wprefixN+1∈WordV
27 25 26 imbitrrid ⊢W=wprefixN+1→w∈WordV→W∈WordV
28 27 eqcoms ⊢wprefixN+1=W→w∈WordV→W∈WordV
29 28 adantr ⊢wprefixN+1=W∧lastS⁡WlastS⁡w∈E→w∈WordV→W∈WordV
30 29 com12 ⊢w∈WordV→wprefixN+1=W∧lastS⁡WlastS⁡w∈E→W∈WordV
31 30 adantr ⊢w∈WordV∧w=N+2→wprefixN+1=W∧lastS⁡WlastS⁡w∈E→W∈WordV
32 31 imp ⊢w∈WordV∧w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E→W∈WordV
33 32 adantl ⊢N∈ℕ0∧w∈WordV∧w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E→W∈WordV
34 oveq1 ⊢W=wprefixN+1→W++⟨“lastS⁡w”⟩=wprefixN+1++⟨“lastS⁡w”⟩
35 34 eqcoms ⊢wprefixN+1=W→W++⟨“lastS⁡w”⟩=wprefixN+1++⟨“lastS⁡w”⟩
36 35 adantr ⊢wprefixN+1=W∧lastS⁡WlastS⁡w∈E→W++⟨“lastS⁡w”⟩=wprefixN+1++⟨“lastS⁡w”⟩
37 36 ad2antll ⊢N∈ℕ0∧w∈WordV∧w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E→W++⟨“lastS⁡w”⟩=wprefixN+1++⟨“lastS⁡w”⟩
38 oveq1 ⊢w=N+2→w−1=N+2-1
39 38 adantl ⊢w∈WordV∧w=N+2→w−1=N+2-1
40 nn0cn ⊢N∈ℕ0→N∈ℂ
41 2cnd ⊢N∈ℕ0→2∈ℂ
42 1cnd ⊢N∈ℕ0→1∈ℂ
43 40 41 42 addsubassd ⊢N∈ℕ0→N+2-1=N+2-1
44 2m1e1 ⊢2−1=1
45 44 a1i ⊢N∈ℕ0→2−1=1
46 45 oveq2d ⊢N∈ℕ0→N+2-1=N+1
47 43 46 eqtrd ⊢N∈ℕ0→N+2-1=N+1
48 39 47 sylan9eqr ⊢N∈ℕ0∧w∈WordV∧w=N+2→w−1=N+1
49 48 oveq2d ⊢N∈ℕ0∧w∈WordV∧w=N+2→wprefixw−1=wprefixN+1
50 49 oveq1d ⊢N∈ℕ0∧w∈WordV∧w=N+2→wprefixw−1++⟨“lastS⁡w”⟩=wprefixN+1++⟨“lastS⁡w”⟩
51 pfxlswccat ⊢w∈WordV∧w≠∅→wprefixw−1++⟨“lastS⁡w”⟩=w
52 8 21 51 syl2an2 ⊢N∈ℕ0∧w∈WordV∧w=N+2→wprefixw−1++⟨“lastS⁡w”⟩=w
53 50 52 eqtr3d ⊢N∈ℕ0∧w∈WordV∧w=N+2→wprefixN+1++⟨“lastS⁡w”⟩=w
54 53 adantrr ⊢N∈ℕ0∧w∈WordV∧w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E→wprefixN+1++⟨“lastS⁡w”⟩=w
55 37 54 eqtr2d ⊢N∈ℕ0∧w∈WordV∧w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E→w=W++⟨“lastS⁡w”⟩
56 simprrr ⊢N∈ℕ0∧w∈WordV∧w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E→lastS⁡WlastS⁡w∈E
57 1 2 wwlksnextbi ⊢N∈ℕ0∧lastS⁡w∈V∧W∈WordV∧w=W++⟨“lastS⁡w”⟩∧lastS⁡WlastS⁡w∈E→w∈N+1WWalksNG↔W∈NWWalksNG
58 7 24 33 55 56 57 syl23anc ⊢N∈ℕ0∧w∈WordV∧w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E→w∈N+1WWalksNG↔W∈NWWalksNG
59 58 exbiri ⊢N∈ℕ0→w∈WordV∧w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E→W∈NWWalksNG→w∈N+1WWalksNG
60 59 com23 ⊢N∈ℕ0→W∈NWWalksNG→w∈WordV∧w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E→w∈N+1WWalksNG
61 60 3ad2ant2 ⊢G∈V∧N∈ℕ0∧W∈WordV→W∈NWWalksNG→w∈WordV∧w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E→w∈N+1WWalksNG
62 6 61 mpcom ⊢W∈NWWalksNG→w∈WordV∧w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E→w∈N+1WWalksNG
63 62 expcomd ⊢W∈NWWalksNG→wprefixN+1=W∧lastS⁡WlastS⁡w∈E→w∈WordV∧w=N+2→w∈N+1WWalksNG
64 63 imp ⊢W∈NWWalksNG∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E→w∈WordV∧w=N+2→w∈N+1WWalksNG
65 1 2 wwlknp ⊢w∈N+1WWalksNG→w∈WordV∧w=N+1+1∧∀i∈0..^N+1w⁡iw⁡i+1∈E
66 40 42 42 addassd ⊢N∈ℕ0→N+1+1=N+1+1
67 1p1e2 ⊢1+1=2
68 67 a1i ⊢N∈ℕ0→1+1=2
69 68 oveq2d ⊢N∈ℕ0→N+1+1=N+2
70 66 69 eqtrd ⊢N∈ℕ0→N+1+1=N+2
71 70 eqeq2d ⊢N∈ℕ0→w=N+1+1↔w=N+2
72 71 biimpd ⊢N∈ℕ0→w=N+1+1→w=N+2
73 72 adantr ⊢N∈ℕ0∧W∈WordV→w=N+1+1→w=N+2
74 73 com12 ⊢w=N+1+1→N∈ℕ0∧W∈WordV→w=N+2
75 74 adantl ⊢w∈WordV∧w=N+1+1→N∈ℕ0∧W∈WordV→w=N+2
76 simpl ⊢w∈WordV∧w=N+1+1→w∈WordV
77 75 76 jctild ⊢w∈WordV∧w=N+1+1→N∈ℕ0∧W∈WordV→w∈WordV∧w=N+2
78 77 3adant3 ⊢w∈WordV∧w=N+1+1∧∀i∈0..^N+1w⁡iw⁡i+1∈E→N∈ℕ0∧W∈WordV→w∈WordV∧w=N+2
79 65 78 syl ⊢w∈N+1WWalksNG→N∈ℕ0∧W∈WordV→w∈WordV∧w=N+2
80 79 com12 ⊢N∈ℕ0∧W∈WordV→w∈N+1WWalksNG→w∈WordV∧w=N+2
81 80 3adant1 ⊢G∈V∧N∈ℕ0∧W∈WordV→w∈N+1WWalksNG→w∈WordV∧w=N+2
82 6 81 syl ⊢W∈NWWalksNG→w∈N+1WWalksNG→w∈WordV∧w=N+2
83 82 adantr ⊢W∈NWWalksNG∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E→w∈N+1WWalksNG→w∈WordV∧w=N+2
84 64 83 impbid ⊢W∈NWWalksNG∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E→w∈WordV∧w=N+2↔w∈N+1WWalksNG
85 84 ex ⊢W∈NWWalksNG→wprefixN+1=W∧lastS⁡WlastS⁡w∈E→w∈WordV∧w=N+2↔w∈N+1WWalksNG
86 85 pm5.32rd ⊢W∈NWWalksNG→w∈WordV∧w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E↔w∈N+1WWalksNG∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E
87 5 86 bitrid ⊢W∈NWWalksNG→w∈WordV∧w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E↔w∈N+1WWalksNG∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E
88 87 rabbidva2 ⊢W∈NWWalksNG→w∈WordV|w=N+2∧wprefixN+1=W∧lastS⁡WlastS⁡w∈E=w∈N+1WWalksNG|wprefixN+1=W∧lastS⁡WlastS⁡w∈E
89 3 88 eqtrid ⊢W∈NWWalksNG→D=w∈N+1WWalksNG|wprefixN+1=W∧lastS⁡WlastS⁡w∈E