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 ∈ Word V | w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E
Assertion wwlksnextwrd ⊢ W ∈ N WWalksN G → D = w ∈ N + 1 WWalksN G | w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E

Proof

Step Hyp Ref Expression
1 wwlksnextbij0.v ⊢ V = Vtx ⁡ G
2 wwlksnextbij0.e ⊢ E = Edg ⁡ G
3 wwlksnextbij0.d ⊢ D = w ∈ Word V | w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E
4 3anass ⊢ w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E ↔ w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E
5 4 bianass ⊢ w ∈ Word V ∧ w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E ↔ w ∈ Word V ∧ w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E
6 1 wwlknbp ⊢ W ∈ N WWalksN G → G ∈ V ∧ N ∈ ℕ 0 ∧ W ∈ Word V
7 simpl ⊢ N ∈ ℕ 0 ∧ w ∈ Word V ∧ w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E → N ∈ ℕ 0
8 simpl ⊢ w ∈ Word V ∧ w = N + 2 → w ∈ Word V
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 ∈ Word V ∧ w = N + 2 → 0 < N + 2
17 breq2 ⊢ w = N + 2 → 0 < w ↔ 0 < N + 2
18 17 ad2antll ⊢ N ∈ ℕ 0 ∧ w ∈ Word V ∧ w = N + 2 → 0 < w ↔ 0 < N + 2
19 16 18 mpbird ⊢ N ∈ ℕ 0 ∧ w ∈ Word V ∧ w = N + 2 → 0 < w
20 hashgt0n0 ⊢ w ∈ Word V ∧ 0 < w → w ≠ ∅
21 8 19 20 syl2an2 ⊢ N ∈ ℕ 0 ∧ w ∈ Word V ∧ w = N + 2 → w ≠ ∅
22 lswcl ⊢ w ∈ Word V ∧ w ≠ ∅ → lastS ⁡ w ∈ V
23 8 21 22 syl2an2 ⊢ N ∈ ℕ 0 ∧ w ∈ Word V ∧ w = N + 2 → lastS ⁡ w ∈ V
24 23 adantrr ⊢ N ∈ ℕ 0 ∧ w ∈ Word V ∧ w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E → lastS ⁡ w ∈ V
25 pfxcl ⊢ w ∈ Word V → w prefix N + 1 ∈ Word V
26 eleq1 ⊢ W = w prefix N + 1 → W ∈ Word V ↔ w prefix N + 1 ∈ Word V
27 25 26 imbitrrid ⊢ W = w prefix N + 1 → w ∈ Word V → W ∈ Word V
28 27 eqcoms ⊢ w prefix N + 1 = W → w ∈ Word V → W ∈ Word V
29 28 adantr ⊢ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E → w ∈ Word V → W ∈ Word V
30 29 com12 ⊢ w ∈ Word V → w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E → W ∈ Word V
31 30 adantr ⊢ w ∈ Word V ∧ w = N + 2 → w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E → W ∈ Word V
32 31 imp ⊢ w ∈ Word V ∧ w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E → W ∈ Word V
33 32 adantl ⊢ N ∈ ℕ 0 ∧ w ∈ Word V ∧ w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E → W ∈ Word V
34 oveq1 ⊢ W = w prefix N + 1 → W ++ ⟨“ lastS ⁡ w ”⟩ = w prefix N + 1 ++ ⟨“ lastS ⁡ w ”⟩
35 34 eqcoms ⊢ w prefix N + 1 = W → W ++ ⟨“ lastS ⁡ w ”⟩ = w prefix N + 1 ++ ⟨“ lastS ⁡ w ”⟩
36 35 adantr ⊢ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E → W ++ ⟨“ lastS ⁡ w ”⟩ = w prefix N + 1 ++ ⟨“ lastS ⁡ w ”⟩
37 36 ad2antll ⊢ N ∈ ℕ 0 ∧ w ∈ Word V ∧ w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E → W ++ ⟨“ lastS ⁡ w ”⟩ = w prefix N + 1 ++ ⟨“ lastS ⁡ w ”⟩
38 oveq1 ⊢ w = N + 2 → w − 1 = N + 2 - 1
39 38 adantl ⊢ w ∈ Word V ∧ 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 ∈ Word V ∧ w = N + 2 → w − 1 = N + 1
49 48 oveq2d ⊢ N ∈ ℕ 0 ∧ w ∈ Word V ∧ w = N + 2 → w prefix w − 1 = w prefix N + 1
50 49 oveq1d ⊢ N ∈ ℕ 0 ∧ w ∈ Word V ∧ w = N + 2 → w prefix w − 1 ++ ⟨“ lastS ⁡ w ”⟩ = w prefix N + 1 ++ ⟨“ lastS ⁡ w ”⟩
51 pfxlswccat ⊢ w ∈ Word V ∧ w ≠ ∅ → w prefix w − 1 ++ ⟨“ lastS ⁡ w ”⟩ = w
52 8 21 51 syl2an2 ⊢ N ∈ ℕ 0 ∧ w ∈ Word V ∧ w = N + 2 → w prefix w − 1 ++ ⟨“ lastS ⁡ w ”⟩ = w
53 50 52 eqtr3d ⊢ N ∈ ℕ 0 ∧ w ∈ Word V ∧ w = N + 2 → w prefix N + 1 ++ ⟨“ lastS ⁡ w ”⟩ = w
54 53 adantrr ⊢ N ∈ ℕ 0 ∧ w ∈ Word V ∧ w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E → w prefix N + 1 ++ ⟨“ lastS ⁡ w ”⟩ = w
55 37 54 eqtr2d ⊢ N ∈ ℕ 0 ∧ w ∈ Word V ∧ w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E → w = W ++ ⟨“ lastS ⁡ w ”⟩
56 simprrr ⊢ N ∈ ℕ 0 ∧ w ∈ Word V ∧ w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E → lastS ⁡ W lastS ⁡ w ∈ E
57 1 2 wwlksnextbi ⊢ N ∈ ℕ 0 ∧ lastS ⁡ w ∈ V ∧ W ∈ Word V ∧ w = W ++ ⟨“ lastS ⁡ w ”⟩ ∧ lastS ⁡ W lastS ⁡ w ∈ E → w ∈ N + 1 WWalksN G ↔ W ∈ N WWalksN G
58 7 24 33 55 56 57 syl23anc ⊢ N ∈ ℕ 0 ∧ w ∈ Word V ∧ w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E → w ∈ N + 1 WWalksN G ↔ W ∈ N WWalksN G
59 58 exbiri ⊢ N ∈ ℕ 0 → w ∈ Word V ∧ w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E → W ∈ N WWalksN G → w ∈ N + 1 WWalksN G
60 59 com23 ⊢ N ∈ ℕ 0 → W ∈ N WWalksN G → w ∈ Word V ∧ w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E → w ∈ N + 1 WWalksN G
61 60 3ad2ant2 ⊢ G ∈ V ∧ N ∈ ℕ 0 ∧ W ∈ Word V → W ∈ N WWalksN G → w ∈ Word V ∧ w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E → w ∈ N + 1 WWalksN G
62 6 61 mpcom ⊢ W ∈ N WWalksN G → w ∈ Word V ∧ w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E → w ∈ N + 1 WWalksN G
63 62 expcomd ⊢ W ∈ N WWalksN G → w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E → w ∈ Word V ∧ w = N + 2 → w ∈ N + 1 WWalksN G
64 63 imp ⊢ W ∈ N WWalksN G ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E → w ∈ Word V ∧ w = N + 2 → w ∈ N + 1 WWalksN G
65 1 2 wwlknp ⊢ w ∈ N + 1 WWalksN G → w ∈ Word V ∧ w = N + 1 + 1 ∧ ∀ i ∈ 0 ..^ N + 1 w ⁡ i w ⁡ 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 ∈ Word V → w = N + 1 + 1 → w = N + 2
74 73 com12 ⊢ w = N + 1 + 1 → N ∈ ℕ 0 ∧ W ∈ Word V → w = N + 2
75 74 adantl ⊢ w ∈ Word V ∧ w = N + 1 + 1 → N ∈ ℕ 0 ∧ W ∈ Word V → w = N + 2
76 simpl ⊢ w ∈ Word V ∧ w = N + 1 + 1 → w ∈ Word V
77 75 76 jctild ⊢ w ∈ Word V ∧ w = N + 1 + 1 → N ∈ ℕ 0 ∧ W ∈ Word V → w ∈ Word V ∧ w = N + 2
78 77 3adant3 ⊢ w ∈ Word V ∧ w = N + 1 + 1 ∧ ∀ i ∈ 0 ..^ N + 1 w ⁡ i w ⁡ i + 1 ∈ E → N ∈ ℕ 0 ∧ W ∈ Word V → w ∈ Word V ∧ w = N + 2
79 65 78 syl ⊢ w ∈ N + 1 WWalksN G → N ∈ ℕ 0 ∧ W ∈ Word V → w ∈ Word V ∧ w = N + 2
80 79 com12 ⊢ N ∈ ℕ 0 ∧ W ∈ Word V → w ∈ N + 1 WWalksN G → w ∈ Word V ∧ w = N + 2
81 80 3adant1 ⊢ G ∈ V ∧ N ∈ ℕ 0 ∧ W ∈ Word V → w ∈ N + 1 WWalksN G → w ∈ Word V ∧ w = N + 2
82 6 81 syl ⊢ W ∈ N WWalksN G → w ∈ N + 1 WWalksN G → w ∈ Word V ∧ w = N + 2
83 82 adantr ⊢ W ∈ N WWalksN G ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E → w ∈ N + 1 WWalksN G → w ∈ Word V ∧ w = N + 2
84 64 83 impbid ⊢ W ∈ N WWalksN G ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E → w ∈ Word V ∧ w = N + 2 ↔ w ∈ N + 1 WWalksN G
85 84 ex ⊢ W ∈ N WWalksN G → w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E → w ∈ Word V ∧ w = N + 2 ↔ w ∈ N + 1 WWalksN G
86 85 pm5.32rd ⊢ W ∈ N WWalksN G → w ∈ Word V ∧ w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E ↔ w ∈ N + 1 WWalksN G ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E
87 5 86 bitrid ⊢ W ∈ N WWalksN G → w ∈ Word V ∧ w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E ↔ w ∈ N + 1 WWalksN G ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E
88 87 rabbidva2 ⊢ W ∈ N WWalksN G → w ∈ Word V | w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E = w ∈ N + 1 WWalksN G | w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E
89 3 88 eqtrid ⊢ W ∈ N WWalksN G → D = w ∈ N + 1 WWalksN G | w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E