MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  numclwlk1lem2f1 Structured version   Visualization version   GIF version

Theorem numclwlk1lem2f1 27347
Description: 𝑇 is a 1-1 function. (Contributed by AV, 26-Sep-2018.) (Revised by AV, 29-May-2021.) (Proof shortened by AV, 23-Feb-2022.) (Revised by AV, 6-Mar-2022.)
Hypotheses
Ref Expression
extwwlkfab.v 𝑉 = (Vtx‘𝐺)
extwwlkfab.c 𝐶 = (𝑣𝑉, 𝑛 ∈ (ℤ‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})
extwwlkfab.f 𝐹 = (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))
numclwwlk.t 𝑇 = (𝑢 ∈ (𝑋𝐶𝑁) ↦ ⟨(𝑢 substr ⟨0, (𝑁 − 2)⟩), (𝑢‘(𝑁 − 1))⟩)
Assertion
Ref Expression
numclwlk1lem2f1 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → 𝑇:(𝑋𝐶𝑁)–1-1→(𝐹 × (𝐺 NeighbVtx 𝑋)))
Distinct variable groups:   𝑛,𝐺,𝑣,𝑤   𝑛,𝑉,𝑣,𝑤   𝑛,𝑋,𝑣,𝑤   𝑛,𝑁,𝑣,𝑤   𝑤,𝐹   𝑢,𝐶   𝑢,𝐹   𝑢,𝐺,𝑤   𝑢,𝑁   𝑢,𝑉   𝑢,𝑋   𝑢,𝑇
Allowed substitution hints:   𝐶(𝑤,𝑣,𝑛)   𝑇(𝑤,𝑣,𝑛)   𝐹(𝑣,𝑛)

Proof of Theorem numclwlk1lem2f1
Dummy variables 𝑎 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 extwwlkfab.v . . 3 𝑉 = (Vtx‘𝐺)
2 extwwlkfab.c . . 3 𝐶 = (𝑣𝑉, 𝑛 ∈ (ℤ‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})
3 extwwlkfab.f . . 3 𝐹 = (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))
4 numclwwlk.t . . 3 𝑇 = (𝑢 ∈ (𝑋𝐶𝑁) ↦ ⟨(𝑢 substr ⟨0, (𝑁 − 2)⟩), (𝑢‘(𝑁 − 1))⟩)
51, 2, 3, 4numclwlk1lem2f 27345 . 2 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → 𝑇:(𝑋𝐶𝑁)⟶(𝐹 × (𝐺 NeighbVtx 𝑋)))
61, 2, 3, 4numclwlk1lem2fv 27346 . . . . . 6 (𝑝 ∈ (𝑋𝐶𝑁) → (𝑇𝑝) = ⟨(𝑝 substr ⟨0, (𝑁 − 2)⟩), (𝑝‘(𝑁 − 1))⟩)
76ad2antrl 764 . . . . 5 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → (𝑇𝑝) = ⟨(𝑝 substr ⟨0, (𝑁 − 2)⟩), (𝑝‘(𝑁 − 1))⟩)
81, 2, 3, 4numclwlk1lem2fv 27346 . . . . . 6 (𝑎 ∈ (𝑋𝐶𝑁) → (𝑇𝑎) = ⟨(𝑎 substr ⟨0, (𝑁 − 2)⟩), (𝑎‘(𝑁 − 1))⟩)
98ad2antll 765 . . . . 5 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → (𝑇𝑎) = ⟨(𝑎 substr ⟨0, (𝑁 − 2)⟩), (𝑎‘(𝑁 − 1))⟩)
107, 9eqeq12d 2666 . . . 4 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → ((𝑇𝑝) = (𝑇𝑎) ↔ ⟨(𝑝 substr ⟨0, (𝑁 − 2)⟩), (𝑝‘(𝑁 − 1))⟩ = ⟨(𝑎 substr ⟨0, (𝑁 − 2)⟩), (𝑎‘(𝑁 − 1))⟩))
11 ovex 6718 . . . . . 6 (𝑝 substr ⟨0, (𝑁 − 2)⟩) ∈ V
12 fvex 6239 . . . . . 6 (𝑝‘(𝑁 − 1)) ∈ V
1311, 12opth 4974 . . . . 5 (⟨(𝑝 substr ⟨0, (𝑁 − 2)⟩), (𝑝‘(𝑁 − 1))⟩ = ⟨(𝑎 substr ⟨0, (𝑁 − 2)⟩), (𝑎‘(𝑁 − 1))⟩ ↔ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))))
14 uzuzle23 11767 . . . . . . . . 9 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ (ℤ‘2))
1522clwwlkel 27337 . . . . . . . . . . 11 ((𝑋𝑉𝑁 ∈ (ℤ‘2)) → (𝑝 ∈ (𝑋𝐶𝑁) ↔ (𝑝 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑝‘(𝑁 − 2)) = 𝑋)))
16 isclwwlknon 27065 . . . . . . . . . . . 12 (𝑝 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ↔ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋))
1716anbi1i 731 . . . . . . . . . . 11 ((𝑝 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ↔ ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋))
1815, 17syl6bb 276 . . . . . . . . . 10 ((𝑋𝑉𝑁 ∈ (ℤ‘2)) → (𝑝 ∈ (𝑋𝐶𝑁) ↔ ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋)))
1922clwwlkel 27337 . . . . . . . . . . 11 ((𝑋𝑉𝑁 ∈ (ℤ‘2)) → (𝑎 ∈ (𝑋𝐶𝑁) ↔ (𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)))
20 isclwwlknon 27065 . . . . . . . . . . . 12 (𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ↔ (𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋))
2120anbi1i 731 . . . . . . . . . . 11 ((𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) ↔ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋))
2219, 21syl6bb 276 . . . . . . . . . 10 ((𝑋𝑉𝑁 ∈ (ℤ‘2)) → (𝑎 ∈ (𝑋𝐶𝑁) ↔ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)))
2318, 22anbi12d 747 . . . . . . . . 9 ((𝑋𝑉𝑁 ∈ (ℤ‘2)) → ((𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁)) ↔ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋))))
2414, 23sylan2 490 . . . . . . . 8 ((𝑋𝑉𝑁 ∈ (ℤ‘3)) → ((𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁)) ↔ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋))))
25243adant1 1099 . . . . . . 7 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → ((𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁)) ↔ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋))))
261clwwlknbp 26997 . . . . . . . . . . . . . . 15 (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → (𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁))
2726adantr 480 . . . . . . . . . . . . . 14 ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) → (𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁))
2827adantr 480 . . . . . . . . . . . . 13 (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁))
29 simpr 476 . . . . . . . . . . . . . 14 ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) → (𝑝‘0) = 𝑋)
3029adantr 480 . . . . . . . . . . . . 13 (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝‘0) = 𝑋)
31 simpr 476 . . . . . . . . . . . . . 14 (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝‘(𝑁 − 2)) = 𝑋)
3229eqcomd 2657 . . . . . . . . . . . . . . 15 ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) → 𝑋 = (𝑝‘0))
3332adantr 480 . . . . . . . . . . . . . 14 (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → 𝑋 = (𝑝‘0))
3431, 33eqtrd 2685 . . . . . . . . . . . . 13 (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝‘(𝑁 − 2)) = (𝑝‘0))
3528, 30, 34jca32 557 . . . . . . . . . . . 12 (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))))
361clwwlknbp 26997 . . . . . . . . . . . . . . 15 (𝑎 ∈ (𝑁 ClWWalksN 𝐺) → (𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁))
3736adantr 480 . . . . . . . . . . . . . 14 ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) → (𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁))
3837adantr 480 . . . . . . . . . . . . 13 (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → (𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁))
39 simpr 476 . . . . . . . . . . . . . 14 ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) → (𝑎‘0) = 𝑋)
4039adantr 480 . . . . . . . . . . . . 13 (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → (𝑎‘0) = 𝑋)
41 simpr 476 . . . . . . . . . . . . . 14 (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → (𝑎‘(𝑁 − 2)) = 𝑋)
4239eqcomd 2657 . . . . . . . . . . . . . . 15 ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) → 𝑋 = (𝑎‘0))
4342adantr 480 . . . . . . . . . . . . . 14 (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → 𝑋 = (𝑎‘0))
4441, 43eqtrd 2685 . . . . . . . . . . . . 13 (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → (𝑎‘(𝑁 − 2)) = (𝑎‘0))
4538, 40, 44jca32 557 . . . . . . . . . . . 12 (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))))
46 eqtr3 2672 . . . . . . . . . . . . . . . . 17 (((#‘𝑝) = 𝑁 ∧ (#‘𝑎) = 𝑁) → (#‘𝑝) = (#‘𝑎))
4746expcom 450 . . . . . . . . . . . . . . . 16 ((#‘𝑎) = 𝑁 → ((#‘𝑝) = 𝑁 → (#‘𝑝) = (#‘𝑎)))
4847ad2antlr 763 . . . . . . . . . . . . . . 15 (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))) → ((#‘𝑝) = 𝑁 → (#‘𝑝) = (#‘𝑎)))
4948com12 32 . . . . . . . . . . . . . 14 ((#‘𝑝) = 𝑁 → (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))) → (#‘𝑝) = (#‘𝑎)))
5049ad2antlr 763 . . . . . . . . . . . . 13 (((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) → (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))) → (#‘𝑝) = (#‘𝑎)))
5150imp 444 . . . . . . . . . . . 12 ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0)))) → (#‘𝑝) = (#‘𝑎))
5235, 45, 51syl2an 493 . . . . . . . . . . 11 ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (#‘𝑝) = (#‘𝑎))
53523ad2ant2 1103 . . . . . . . . . 10 ((𝑁 ∈ (ℤ‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → (#‘𝑝) = (#‘𝑎))
5427simprd 478 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) → (#‘𝑝) = 𝑁)
5554adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (#‘𝑝) = 𝑁)
5655eqcomd 2657 . . . . . . . . . . . . . . . . . . . 20 (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → 𝑁 = (#‘𝑝))
5756adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → 𝑁 = (#‘𝑝))
5857oveq1d 6705 . . . . . . . . . . . . . . . . . 18 ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑁 − 2) = ((#‘𝑝) − 2))
5958opeq2d 4440 . . . . . . . . . . . . . . . . 17 ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → ⟨0, (𝑁 − 2)⟩ = ⟨0, ((#‘𝑝) − 2)⟩)
6059oveq2d 6706 . . . . . . . . . . . . . . . 16 ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑝 substr ⟨0, ((#‘𝑝) − 2)⟩))
6159oveq2d 6706 . . . . . . . . . . . . . . . 16 ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑎 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, ((#‘𝑝) − 2)⟩))
6260, 61eqeq12d 2666 . . . . . . . . . . . . . . 15 ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ↔ (𝑝 substr ⟨0, ((#‘𝑝) − 2)⟩) = (𝑎 substr ⟨0, ((#‘𝑝) − 2)⟩)))
6362biimpcd 239 . . . . . . . . . . . . . 14 ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) → ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝 substr ⟨0, ((#‘𝑝) − 2)⟩) = (𝑎 substr ⟨0, ((#‘𝑝) − 2)⟩)))
6463adantr 480 . . . . . . . . . . . . 13 (((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝 substr ⟨0, ((#‘𝑝) − 2)⟩) = (𝑎 substr ⟨0, ((#‘𝑝) − 2)⟩)))
6564impcom 445 . . . . . . . . . . . 12 (((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → (𝑝 substr ⟨0, ((#‘𝑝) − 2)⟩) = (𝑎 substr ⟨0, ((#‘𝑝) − 2)⟩))
6655oveq1d 6705 . . . . . . . . . . . . . . . . 17 (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → ((#‘𝑝) − 2) = (𝑁 − 2))
6766fveq2d 6233 . . . . . . . . . . . . . . . 16 (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝‘((#‘𝑝) − 2)) = (𝑝‘(𝑁 − 2)))
6867, 31eqtrd 2685 . . . . . . . . . . . . . . 15 (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) → (𝑝‘((#‘𝑝) − 2)) = 𝑋)
6968adantr 480 . . . . . . . . . . . . . 14 ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝‘((#‘𝑝) − 2)) = 𝑋)
7041eqcomd 2657 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋) → 𝑋 = (𝑎‘(𝑁 − 2)))
7170adantl 481 . . . . . . . . . . . . . . 15 ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → 𝑋 = (𝑎‘(𝑁 − 2)))
7258fveq2d 6233 . . . . . . . . . . . . . . 15 ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑎‘(𝑁 − 2)) = (𝑎‘((#‘𝑝) − 2)))
7371, 72eqtrd 2685 . . . . . . . . . . . . . 14 ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → 𝑋 = (𝑎‘((#‘𝑝) − 2)))
7469, 73eqtrd 2685 . . . . . . . . . . . . 13 ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)))
7574adantr 480 . . . . . . . . . . . 12 (((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)))
76 lsw 13384 . . . . . . . . . . . . . . . . . . . 20 (𝑝 ∈ Word 𝑉 → ( lastS ‘𝑝) = (𝑝‘((#‘𝑝) − 1)))
77 oveq1 6697 . . . . . . . . . . . . . . . . . . . . 21 ((#‘𝑝) = 𝑁 → ((#‘𝑝) − 1) = (𝑁 − 1))
7877fveq2d 6233 . . . . . . . . . . . . . . . . . . . 20 ((#‘𝑝) = 𝑁 → (𝑝‘((#‘𝑝) − 1)) = (𝑝‘(𝑁 − 1)))
7976, 78sylan9eq 2705 . . . . . . . . . . . . . . . . . . 19 ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) → ( lastS ‘𝑝) = (𝑝‘(𝑁 − 1)))
8026, 79syl 17 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → ( lastS ‘𝑝) = (𝑝‘(𝑁 − 1)))
8180eqcomd 2657 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → (𝑝‘(𝑁 − 1)) = ( lastS ‘𝑝))
8281ad3antrrr 766 . . . . . . . . . . . . . . . 16 ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑝‘(𝑁 − 1)) = ( lastS ‘𝑝))
83 lsw 13384 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 ∈ Word 𝑉 → ( lastS ‘𝑎) = (𝑎‘((#‘𝑎) − 1)))
8483adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) → ( lastS ‘𝑎) = (𝑎‘((#‘𝑎) − 1)))
85 oveq1 6697 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 = (#‘𝑎) → (𝑁 − 1) = ((#‘𝑎) − 1))
8685eqcoms 2659 . . . . . . . . . . . . . . . . . . . . . . . 24 ((#‘𝑎) = 𝑁 → (𝑁 − 1) = ((#‘𝑎) − 1))
8786fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . 23 ((#‘𝑎) = 𝑁 → (𝑎‘(𝑁 − 1)) = (𝑎‘((#‘𝑎) − 1)))
8887eqeq2d 2661 . . . . . . . . . . . . . . . . . . . . . 22 ((#‘𝑎) = 𝑁 → (( lastS ‘𝑎) = (𝑎‘(𝑁 − 1)) ↔ ( lastS ‘𝑎) = (𝑎‘((#‘𝑎) − 1))))
8988adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) → (( lastS ‘𝑎) = (𝑎‘(𝑁 − 1)) ↔ ( lastS ‘𝑎) = (𝑎‘((#‘𝑎) − 1))))
9084, 89mpbird 247 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) → ( lastS ‘𝑎) = (𝑎‘(𝑁 − 1)))
9136, 90syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ (𝑁 ClWWalksN 𝐺) → ( lastS ‘𝑎) = (𝑎‘(𝑁 − 1)))
9291eqcomd 2657 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ (𝑁 ClWWalksN 𝐺) → (𝑎‘(𝑁 − 1)) = ( lastS ‘𝑎))
9392adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) → (𝑎‘(𝑁 − 1)) = ( lastS ‘𝑎))
9493ad2antrl 764 . . . . . . . . . . . . . . . 16 ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑎‘(𝑁 − 1)) = ( lastS ‘𝑎))
9582, 94eqeq12d 2666 . . . . . . . . . . . . . . 15 ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → ((𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)) ↔ ( lastS ‘𝑝) = ( lastS ‘𝑎)))
9695biimpd 219 . . . . . . . . . . . . . 14 ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → ((𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)) → ( lastS ‘𝑝) = ( lastS ‘𝑎)))
9796adantld 482 . . . . . . . . . . . . 13 ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → ( lastS ‘𝑝) = ( lastS ‘𝑎)))
9897imp 444 . . . . . . . . . . . 12 (((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → ( lastS ‘𝑝) = ( lastS ‘𝑎))
9965, 75, 983jca 1261 . . . . . . . . . . 11 (((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → ((𝑝 substr ⟨0, ((#‘𝑝) − 2)⟩) = (𝑎 substr ⟨0, ((#‘𝑝) − 2)⟩) ∧ (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)) ∧ ( lastS ‘𝑝) = ( lastS ‘𝑎)))
100993adant1 1099 . . . . . . . . . 10 ((𝑁 ∈ (ℤ‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → ((𝑝 substr ⟨0, ((#‘𝑝) − 2)⟩) = (𝑎 substr ⟨0, ((#‘𝑝) − 2)⟩) ∧ (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)) ∧ ( lastS ‘𝑝) = ( lastS ‘𝑎)))
1011clwwlknwrd 26996 . . . . . . . . . . . . . 14 (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → 𝑝 ∈ Word 𝑉)
102101ad3antrrr 766 . . . . . . . . . . . . 13 ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → 𝑝 ∈ Word 𝑉)
1031023ad2ant2 1103 . . . . . . . . . . . 12 ((𝑁 ∈ (ℤ‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → 𝑝 ∈ Word 𝑉)
1041clwwlknwrd 26996 . . . . . . . . . . . . . . 15 (𝑎 ∈ (𝑁 ClWWalksN 𝐺) → 𝑎 ∈ Word 𝑉)
105104adantr 480 . . . . . . . . . . . . . 14 ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) → 𝑎 ∈ Word 𝑉)
106105ad2antrl 764 . . . . . . . . . . . . 13 ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → 𝑎 ∈ Word 𝑉)
1071063ad2ant2 1103 . . . . . . . . . . . 12 ((𝑁 ∈ (ℤ‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → 𝑎 ∈ Word 𝑉)
108 clwwlknlen 26994 . . . . . . . . . . . . . . . 16 (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → (#‘𝑝) = 𝑁)
109 eluz2b1 11797 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘2) ↔ (𝑁 ∈ ℤ ∧ 1 < 𝑁))
110 breq2 4689 . . . . . . . . . . . . . . . . . . 19 (𝑁 = (#‘𝑝) → (1 < 𝑁 ↔ 1 < (#‘𝑝)))
111110eqcoms 2659 . . . . . . . . . . . . . . . . . 18 ((#‘𝑝) = 𝑁 → (1 < 𝑁 ↔ 1 < (#‘𝑝)))
112111biimpcd 239 . . . . . . . . . . . . . . . . 17 (1 < 𝑁 → ((#‘𝑝) = 𝑁 → 1 < (#‘𝑝)))
113109, 112simplbiim 659 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ‘2) → ((#‘𝑝) = 𝑁 → 1 < (#‘𝑝)))
11414, 108, 113syl2imc 41 . . . . . . . . . . . . . . 15 (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → (𝑁 ∈ (ℤ‘3) → 1 < (#‘𝑝)))
115114ad3antrrr 766 . . . . . . . . . . . . . 14 ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (𝑁 ∈ (ℤ‘3) → 1 < (#‘𝑝)))
116115impcom 445 . . . . . . . . . . . . 13 ((𝑁 ∈ (ℤ‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋))) → 1 < (#‘𝑝))
1171163adant3 1101 . . . . . . . . . . . 12 ((𝑁 ∈ (ℤ‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → 1 < (#‘𝑝))
118103, 107, 1173jca 1261 . . . . . . . . . . 11 ((𝑁 ∈ (ℤ‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → (𝑝 ∈ Word 𝑉𝑎 ∈ Word 𝑉 ∧ 1 < (#‘𝑝)))
119 2swrd2eqwrdeq 13742 . . . . . . . . . . 11 ((𝑝 ∈ Word 𝑉𝑎 ∈ Word 𝑉 ∧ 1 < (#‘𝑝)) → (𝑝 = 𝑎 ↔ ((#‘𝑝) = (#‘𝑎) ∧ ((𝑝 substr ⟨0, ((#‘𝑝) − 2)⟩) = (𝑎 substr ⟨0, ((#‘𝑝) − 2)⟩) ∧ (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)) ∧ ( lastS ‘𝑝) = ( lastS ‘𝑎)))))
120118, 119syl 17 . . . . . . . . . 10 ((𝑁 ∈ (ℤ‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → (𝑝 = 𝑎 ↔ ((#‘𝑝) = (#‘𝑎) ∧ ((𝑝 substr ⟨0, ((#‘𝑝) − 2)⟩) = (𝑎 substr ⟨0, ((#‘𝑝) − 2)⟩) ∧ (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)) ∧ ( lastS ‘𝑝) = ( lastS ‘𝑎)))))
12153, 100, 120mpbir2and 977 . . . . . . . . 9 ((𝑁 ∈ (ℤ‘3) ∧ (((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) ∧ ((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) → 𝑝 = 𝑎)
1221213exp 1283 . . . . . . . 8 (𝑁 ∈ (ℤ‘3) → ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → 𝑝 = 𝑎)))
1231223ad2ant3 1104 . . . . . . 7 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → ((((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋) ∧ (𝑝‘(𝑁 − 2)) = 𝑋) ∧ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) ∧ (𝑎‘(𝑁 − 2)) = 𝑋)) → (((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → 𝑝 = 𝑎)))
12425, 123sylbid 230 . . . . . 6 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → ((𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁)) → (((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → 𝑝 = 𝑎)))
125124imp 444 . . . . 5 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → (((𝑝 substr ⟨0, (𝑁 − 2)⟩) = (𝑎 substr ⟨0, (𝑁 − 2)⟩) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → 𝑝 = 𝑎))
12613, 125syl5bi 232 . . . 4 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → (⟨(𝑝 substr ⟨0, (𝑁 − 2)⟩), (𝑝‘(𝑁 − 1))⟩ = ⟨(𝑎 substr ⟨0, (𝑁 − 2)⟩), (𝑎‘(𝑁 − 1))⟩ → 𝑝 = 𝑎))
12710, 126sylbid 230 . . 3 (((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) ∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → ((𝑇𝑝) = (𝑇𝑎) → 𝑝 = 𝑎))
128127ralrimivva 3000 . 2 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → ∀𝑝 ∈ (𝑋𝐶𝑁)∀𝑎 ∈ (𝑋𝐶𝑁)((𝑇𝑝) = (𝑇𝑎) → 𝑝 = 𝑎))
129 dff13 6552 . 2 (𝑇:(𝑋𝐶𝑁)–1-1→(𝐹 × (𝐺 NeighbVtx 𝑋)) ↔ (𝑇:(𝑋𝐶𝑁)⟶(𝐹 × (𝐺 NeighbVtx 𝑋)) ∧ ∀𝑝 ∈ (𝑋𝐶𝑁)∀𝑎 ∈ (𝑋𝐶𝑁)((𝑇𝑝) = (𝑇𝑎) → 𝑝 = 𝑎)))
1305, 128, 129sylanbrc 699 1 ((𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ (ℤ‘3)) → 𝑇:(𝑋𝐶𝑁)–1-1→(𝐹 × (𝐺 NeighbVtx 𝑋)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wral 2941  {crab 2945  cop 4216   class class class wbr 4685  cmpt 4762   × cxp 5141  wf 5922  1-1wf1 5923  cfv 5926  (class class class)co 6690  cmpt2 6692  0cc0 9974  1c1 9975   < clt 10112  cmin 10304  2c2 11108  3c3 11109  cz 11415  cuz 11725  #chash 13157  Word cword 13323   lastS clsw 13324   substr csubstr 13327  Vtxcvtx 25919  USGraphcusgr 26089   NeighbVtx cnbgr 26269   ClWWalksN cclwwlkn 26981  ClWWalksNOncclwwlknon 27060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-xnn0 11402  df-z 11416  df-uz 11726  df-fz 12365  df-fzo 12505  df-hash 13158  df-word 13331  df-lsw 13332  df-concat 13333  df-s1 13334  df-substr 13335  df-s2 13639  df-edg 25985  df-upgr 26022  df-umgr 26023  df-usgr 26091  df-nbgr 26270  df-wwlks 26778  df-wwlksn 26779  df-clwwlk 26950  df-clwwlkn 26983  df-clwwlknon 27061
This theorem is referenced by:  numclwlk1lem2f1o  27349
  Copyright terms: Public domain W3C validator