Step | Hyp | Ref
| Expression |
1 | | extwwlkfab.v |
. . 3
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | extwwlkfab.f |
. . 3
⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣}) |
3 | | extwwlkfab.c |
. . 3
⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) = (𝑤‘0))}) |
4 | | numclwwlk.t |
. . 3
⊢ 𝑇 = (𝑢 ∈ (𝑋𝐶𝑁) ↦ 〈(𝑢 substr 〈0, (𝑁 − 2)〉), (𝑢‘(𝑁 − 1))〉) |
5 | 1, 2, 3, 4 | numclwlk1lem2f 27225 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑇:(𝑋𝐶𝑁)⟶((𝑋𝐹(𝑁 − 2)) × (𝐺 NeighbVtx 𝑋))) |
6 | 1, 2, 3, 4 | numclwlk1lem2fv 27226 |
. . . . . 6
⊢ (𝑝 ∈ (𝑋𝐶𝑁) → (𝑇‘𝑝) = 〈(𝑝 substr 〈0, (𝑁 − 2)〉), (𝑝‘(𝑁 − 1))〉) |
7 | 6 | ad2antrl 764 |
. . . . 5
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → (𝑇‘𝑝) = 〈(𝑝 substr 〈0, (𝑁 − 2)〉), (𝑝‘(𝑁 − 1))〉) |
8 | 1, 2, 3, 4 | numclwlk1lem2fv 27226 |
. . . . . 6
⊢ (𝑎 ∈ (𝑋𝐶𝑁) → (𝑇‘𝑎) = 〈(𝑎 substr 〈0, (𝑁 − 2)〉), (𝑎‘(𝑁 − 1))〉) |
9 | 8 | ad2antll 765 |
. . . . 5
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → (𝑇‘𝑎) = 〈(𝑎 substr 〈0, (𝑁 − 2)〉), (𝑎‘(𝑁 − 1))〉) |
10 | 7, 9 | eqeq12d 2637 |
. . . 4
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → ((𝑇‘𝑝) = (𝑇‘𝑎) ↔ 〈(𝑝 substr 〈0, (𝑁 − 2)〉), (𝑝‘(𝑁 − 1))〉 = 〈(𝑎 substr 〈0, (𝑁 − 2)〉), (𝑎‘(𝑁 − 1))〉)) |
11 | | ovex 6678 |
. . . . . 6
⊢ (𝑝 substr 〈0, (𝑁 − 2)〉) ∈
V |
12 | | fvex 6201 |
. . . . . 6
⊢ (𝑝‘(𝑁 − 1)) ∈ V |
13 | 11, 12 | opth 4945 |
. . . . 5
⊢
(〈(𝑝 substr
〈0, (𝑁 −
2)〉), (𝑝‘(𝑁 − 1))〉 =
〈(𝑎 substr 〈0,
(𝑁 − 2)〉),
(𝑎‘(𝑁 − 1))〉 ↔ ((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) |
14 | | uzuzle23 11729 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈
(ℤ≥‘2)) |
15 | 3 | numclwwlkovgel 27221 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑝 ∈ (𝑋𝐶𝑁) ↔ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0)))) |
16 | 14, 15 | sylan2 491 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑝 ∈ (𝑋𝐶𝑁) ↔ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0)))) |
17 | 1 | clwwlknbp 26885 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ (𝑁 ClWWalksN 𝐺) → (𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁)) |
18 | 17 | 3ad2ant1 1082 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0)) → (𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁)) |
19 | | 3simpc 1060 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0)) → ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) |
20 | 18, 19 | jca 554 |
. . . . . . . . 9
⊢ ((𝑝 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0)) → ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0)))) |
21 | 16, 20 | syl6bi 243 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑝 ∈ (𝑋𝐶𝑁) → ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))))) |
22 | 21 | 3adant1 1079 |
. . . . . . 7
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑝 ∈ (𝑋𝐶𝑁) → ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))))) |
23 | 3 | numclwwlkovgel 27221 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑎 ∈ (𝑋𝐶𝑁) ↔ (𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0)))) |
24 | 14, 23 | sylan2 491 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑎 ∈ (𝑋𝐶𝑁) ↔ (𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0)))) |
25 | 1 | clwwlknbp 26885 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (𝑁 ClWWalksN 𝐺) → (𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁)) |
26 | 25 | 3ad2ant1 1082 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0)) → (𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁)) |
27 | | 3simpc 1060 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0)) → ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))) |
28 | 26, 27 | jca 554 |
. . . . . . . . 9
⊢ ((𝑎 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0)) → ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0)))) |
29 | 24, 28 | syl6bi 243 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑎 ∈ (𝑋𝐶𝑁) → ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))))) |
30 | 29 | 3adant1 1079 |
. . . . . . 7
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑎 ∈ (𝑋𝐶𝑁) → ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))))) |
31 | | simpll 790 |
. . . . . . . . . . 11
⊢ (((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) → 𝑝 ∈ Word 𝑉) |
32 | 31 | ad2antrl 764 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))))) → 𝑝 ∈ Word 𝑉) |
33 | | simprll 802 |
. . . . . . . . . . 11
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0)))) → 𝑎 ∈ Word 𝑉) |
34 | 33 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))))) → 𝑎 ∈ Word 𝑉) |
35 | | eleq1 2689 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 = (#‘𝑝) → (𝑁 ∈ (ℤ≥‘3)
↔ (#‘𝑝) ∈
(ℤ≥‘3))) |
36 | 35 | eqcoms 2630 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑝) = 𝑁 → (𝑁 ∈ (ℤ≥‘3)
↔ (#‘𝑝) ∈
(ℤ≥‘3))) |
37 | | eluz2 11693 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑝) ∈
(ℤ≥‘3) ↔ (3 ∈ ℤ ∧ (#‘𝑝) ∈ ℤ ∧ 3 ≤
(#‘𝑝))) |
38 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑝) ∈
ℤ → 1 ∈ ℝ) |
39 | | 3re 11094 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 3 ∈
ℝ |
40 | 39 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑝) ∈
ℤ → 3 ∈ ℝ) |
41 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑝) ∈
ℤ → (#‘𝑝)
∈ ℝ) |
42 | 38, 40, 41 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑝) ∈
ℤ → (1 ∈ ℝ ∧ 3 ∈ ℝ ∧ (#‘𝑝) ∈
ℝ)) |
43 | | 1lt3 11196 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 <
3 |
44 | | ltletr 10129 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
∈ ℝ ∧ 3 ∈ ℝ ∧ (#‘𝑝) ∈ ℝ) → ((1 < 3 ∧ 3
≤ (#‘𝑝)) → 1
< (#‘𝑝))) |
45 | 44 | expd 452 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1
∈ ℝ ∧ 3 ∈ ℝ ∧ (#‘𝑝) ∈ ℝ) → (1 < 3 → (3
≤ (#‘𝑝) → 1
< (#‘𝑝)))) |
46 | 42, 43, 45 | mpisyl 21 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑝) ∈
ℤ → (3 ≤ (#‘𝑝) → 1 < (#‘𝑝))) |
47 | 46 | imp 445 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝑝) ∈
ℤ ∧ 3 ≤ (#‘𝑝)) → 1 < (#‘𝑝)) |
48 | 47 | 3adant1 1079 |
. . . . . . . . . . . . . . . . 17
⊢ ((3
∈ ℤ ∧ (#‘𝑝) ∈ ℤ ∧ 3 ≤ (#‘𝑝)) → 1 < (#‘𝑝)) |
49 | 37, 48 | sylbi 207 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑝) ∈
(ℤ≥‘3) → 1 < (#‘𝑝)) |
50 | 36, 49 | syl6bi 243 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑝) = 𝑁 → (𝑁 ∈ (ℤ≥‘3)
→ 1 < (#‘𝑝))) |
51 | 50 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘3) → ((#‘𝑝) = 𝑁 → 1 < (#‘𝑝))) |
52 | 51 | 3ad2ant3 1084 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((#‘𝑝) = 𝑁 → 1 < (#‘𝑝))) |
53 | 52 | com12 32 |
. . . . . . . . . . . 12
⊢
((#‘𝑝) = 𝑁 → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 1 < (#‘𝑝))) |
54 | 53 | ad3antlr 767 |
. . . . . . . . . . 11
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0)))) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 1 < (#‘𝑝))) |
55 | 54 | impcom 446 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))))) → 1 < (#‘𝑝)) |
56 | | 2swrd2eqwrdeq 13696 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ Word 𝑉 ∧ 𝑎 ∈ Word 𝑉 ∧ 1 < (#‘𝑝)) → (𝑝 = 𝑎 ↔ ((#‘𝑝) = (#‘𝑎) ∧ ((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) − 2)〉) ∧ (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)) ∧ ( lastS ‘𝑝) = ( lastS ‘𝑎))))) |
57 | 32, 34, 55, 56 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))))) → (𝑝 = 𝑎 ↔ ((#‘𝑝) = (#‘𝑎) ∧ ((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) − 2)〉) ∧ (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)) ∧ ( lastS ‘𝑝) = ( lastS ‘𝑎))))) |
58 | | eqtr3 2643 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝑝) =
𝑁 ∧ (#‘𝑎) = 𝑁) → (#‘𝑝) = (#‘𝑎)) |
59 | 58 | expcom 451 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑎) = 𝑁 → ((#‘𝑝) = 𝑁 → (#‘𝑝) = (#‘𝑎))) |
60 | 59 | ad2antlr 763 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))) → ((#‘𝑝) = 𝑁 → (#‘𝑝) = (#‘𝑎))) |
61 | 60 | com12 32 |
. . . . . . . . . . . . 13
⊢
((#‘𝑝) = 𝑁 → (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))) → (#‘𝑝) = (#‘𝑎))) |
62 | 61 | ad2antlr 763 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) → (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))) → (#‘𝑝) = (#‘𝑎))) |
63 | 62 | imp 445 |
. . . . . . . . . . 11
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0)))) → (#‘𝑝) = (#‘𝑎)) |
64 | 63 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))))) → (#‘𝑝) = (#‘𝑎)) |
65 | 64 | biantrurd 529 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))))) → (((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) − 2)〉) ∧ (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)) ∧ ( lastS ‘𝑝) = ( lastS ‘𝑎)) ↔ ((#‘𝑝) = (#‘𝑎) ∧ ((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) − 2)〉) ∧ (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)) ∧ ( lastS ‘𝑝) = ( lastS ‘𝑎))))) |
66 | | 3anan12 1051 |
. . . . . . . . . . 11
⊢ (((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) − 2)〉) ∧ (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)) ∧ ( lastS
‘𝑝) = ( lastS
‘𝑎)) ↔ ((𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)) ∧ ((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) − 2)〉) ∧ (
lastS ‘𝑝) = ( lastS
‘𝑎)))) |
67 | 66 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))))) → (((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) − 2)〉) ∧ (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)) ∧ ( lastS ‘𝑝) = ( lastS ‘𝑎)) ↔ ((𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)) ∧ ((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) − 2)〉) ∧ ( lastS
‘𝑝) = ( lastS
‘𝑎))))) |
68 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝‘0) = 𝑋 → ((𝑝‘(𝑁 − 2)) = (𝑝‘0) ↔ (𝑝‘(𝑁 − 2)) = 𝑋)) |
69 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 = (#‘𝑝) → (𝑁 − 2) = ((#‘𝑝) − 2)) |
70 | 69 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑝) = 𝑁 → (𝑁 − 2) = ((#‘𝑝) − 2)) |
71 | 70 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑝) = 𝑁 → (𝑝‘(𝑁 − 2)) = (𝑝‘((#‘𝑝) − 2))) |
72 | 71 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑝) = 𝑁 → ((𝑝‘(𝑁 − 2)) = 𝑋 ↔ (𝑝‘((#‘𝑝) − 2)) = 𝑋)) |
73 | 72 | biimpcd 239 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝‘(𝑁 − 2)) = 𝑋 → ((#‘𝑝) = 𝑁 → (𝑝‘((#‘𝑝) − 2)) = 𝑋)) |
74 | 68, 73 | syl6bi 243 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝‘0) = 𝑋 → ((𝑝‘(𝑁 − 2)) = (𝑝‘0) → ((#‘𝑝) = 𝑁 → (𝑝‘((#‘𝑝) − 2)) = 𝑋))) |
75 | 74 | imp 445 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0)) → ((#‘𝑝) = 𝑁 → (𝑝‘((#‘𝑝) − 2)) = 𝑋)) |
76 | 75 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑝) = 𝑁 → (((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0)) → (𝑝‘((#‘𝑝) − 2)) = 𝑋)) |
77 | 76 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) → (((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0)) → (𝑝‘((#‘𝑝) − 2)) = 𝑋)) |
78 | 77 | imp 445 |
. . . . . . . . . . . . . 14
⊢ (((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) → (𝑝‘((#‘𝑝) − 2)) = 𝑋) |
79 | 78 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0)))) → (𝑝‘((#‘𝑝) − 2)) = 𝑋) |
80 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑝) = 𝑁 → ((#‘𝑝) − 2) = (𝑁 − 2)) |
81 | 80 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑝) = 𝑁 → (𝑎‘((#‘𝑝) − 2)) = (𝑎‘(𝑁 − 2))) |
82 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎‘0) = (𝑎‘(𝑁 − 2)) → ((𝑎‘0) = 𝑋 ↔ (𝑎‘(𝑁 − 2)) = 𝑋)) |
83 | 82 | eqcoms 2630 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎‘(𝑁 − 2)) = (𝑎‘0) → ((𝑎‘0) = 𝑋 ↔ (𝑎‘(𝑁 − 2)) = 𝑋)) |
84 | 83 | biimpac 503 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0)) → (𝑎‘(𝑁 − 2)) = 𝑋) |
85 | 84 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))) → (𝑎‘(𝑁 − 2)) = 𝑋) |
86 | 81, 85 | sylan9eq 2676 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑝) =
𝑁 ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0)))) → (𝑎‘((#‘𝑝) − 2)) = 𝑋) |
87 | 86 | ad4ant24 1298 |
. . . . . . . . . . . . 13
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0)))) → (𝑎‘((#‘𝑝) − 2)) = 𝑋) |
88 | 79, 87 | eqtr4d 2659 |
. . . . . . . . . . . 12
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0)))) → (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2))) |
89 | 88 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))))) → (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2))) |
90 | 89 | biantrurd 529 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))))) → (((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) − 2)〉) ∧ ( lastS
‘𝑝) = ( lastS
‘𝑎)) ↔ ((𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)) ∧ ((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) − 2)〉) ∧ (
lastS ‘𝑝) = ( lastS
‘𝑎))))) |
91 | 80 | opeq2d 4409 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑝) = 𝑁 → 〈0, ((#‘𝑝) − 2)〉 = 〈0,
(𝑁 −
2)〉) |
92 | 91 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑝) = 𝑁 → (𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑝 substr 〈0, (𝑁 − 2)〉)) |
93 | 91 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑝) = 𝑁 → (𝑎 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉)) |
94 | 92, 93 | eqeq12d 2637 |
. . . . . . . . . . . . 13
⊢
((#‘𝑝) = 𝑁 → ((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) − 2)〉) ↔ (𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 −
2)〉))) |
95 | 94 | ad3antlr 767 |
. . . . . . . . . . . 12
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0)))) → ((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) − 2)〉) ↔ (𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 −
2)〉))) |
96 | 95 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))))) → ((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) − 2)〉) ↔ (𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 −
2)〉))) |
97 | | lsw 13351 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ Word 𝑉 → ( lastS ‘𝑝) = (𝑝‘((#‘𝑝) − 1))) |
98 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑝) = 𝑁 → ((#‘𝑝) − 1) = (𝑁 − 1)) |
99 | 98 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑝) = 𝑁 → (𝑝‘((#‘𝑝) − 1)) = (𝑝‘(𝑁 − 1))) |
100 | 97, 99 | sylan9eq 2676 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) → ( lastS ‘𝑝) = (𝑝‘(𝑁 − 1))) |
101 | 100 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) → ( lastS ‘𝑝) = (𝑝‘(𝑁 − 1))) |
102 | | lsw 13351 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ Word 𝑉 → ( lastS ‘𝑎) = (𝑎‘((#‘𝑎) − 1))) |
103 | 102 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) → ( lastS ‘𝑎) = (𝑎‘((#‘𝑎) − 1))) |
104 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 = (#‘𝑎) → (𝑁 − 1) = ((#‘𝑎) − 1)) |
105 | 104 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑎) = 𝑁 → (𝑁 − 1) = ((#‘𝑎) − 1)) |
106 | 105 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑎) = 𝑁 → (𝑎‘(𝑁 − 1)) = (𝑎‘((#‘𝑎) − 1))) |
107 | 106 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑎) = 𝑁 → (( lastS ‘𝑎) = (𝑎‘(𝑁 − 1)) ↔ ( lastS ‘𝑎) = (𝑎‘((#‘𝑎) − 1)))) |
108 | 107 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) → (( lastS ‘𝑎) = (𝑎‘(𝑁 − 1)) ↔ ( lastS ‘𝑎) = (𝑎‘((#‘𝑎) − 1)))) |
109 | 103, 108 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) → ( lastS ‘𝑎) = (𝑎‘(𝑁 − 1))) |
110 | 109 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))) → ( lastS ‘𝑎) = (𝑎‘(𝑁 − 1))) |
111 | 101, 110 | eqeqan12d 2638 |
. . . . . . . . . . . 12
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0)))) → (( lastS ‘𝑝) = ( lastS ‘𝑎) ↔ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) |
112 | 111 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))))) → (( lastS ‘𝑝) = ( lastS ‘𝑎) ↔ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1)))) |
113 | 96, 112 | anbi12d 747 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))))) → (((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) − 2)〉) ∧ ( lastS
‘𝑝) = ( lastS
‘𝑎)) ↔ ((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))))) |
114 | 67, 90, 113 | 3bitr2d 296 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))))) → (((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑎 substr 〈0, ((#‘𝑝) − 2)〉) ∧ (𝑝‘((#‘𝑝) − 2)) = (𝑎‘((#‘𝑝) − 2)) ∧ ( lastS ‘𝑝) = ( lastS ‘𝑎)) ↔ ((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))))) |
115 | 57, 65, 114 | 3bitr2d 296 |
. . . . . . . 8
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0))))) → (𝑝 = 𝑎 ↔ ((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))))) |
116 | 115 | exbiri 652 |
. . . . . . 7
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = 𝑁) ∧ ((𝑎‘0) = 𝑋 ∧ (𝑎‘(𝑁 − 2)) = (𝑎‘0)))) → (((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → 𝑝 = 𝑎))) |
117 | 22, 30, 116 | syl2and 500 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁)) → (((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → 𝑝 = 𝑎))) |
118 | 117 | imp 445 |
. . . . 5
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → (((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑎 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑎‘(𝑁 − 1))) → 𝑝 = 𝑎)) |
119 | 13, 118 | syl5bi 232 |
. . . 4
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → (〈(𝑝 substr 〈0, (𝑁 − 2)〉), (𝑝‘(𝑁 − 1))〉 = 〈(𝑎 substr 〈0, (𝑁 − 2)〉), (𝑎‘(𝑁 − 1))〉 → 𝑝 = 𝑎)) |
120 | 10, 119 | sylbid 230 |
. . 3
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑝 ∈ (𝑋𝐶𝑁) ∧ 𝑎 ∈ (𝑋𝐶𝑁))) → ((𝑇‘𝑝) = (𝑇‘𝑎) → 𝑝 = 𝑎)) |
121 | 120 | ralrimivva 2971 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ∀𝑝 ∈
(𝑋𝐶𝑁)∀𝑎 ∈ (𝑋𝐶𝑁)((𝑇‘𝑝) = (𝑇‘𝑎) → 𝑝 = 𝑎)) |
122 | | dff13 6512 |
. 2
⊢ (𝑇:(𝑋𝐶𝑁)–1-1→((𝑋𝐹(𝑁 − 2)) × (𝐺 NeighbVtx 𝑋)) ↔ (𝑇:(𝑋𝐶𝑁)⟶((𝑋𝐹(𝑁 − 2)) × (𝐺 NeighbVtx 𝑋)) ∧ ∀𝑝 ∈ (𝑋𝐶𝑁)∀𝑎 ∈ (𝑋𝐶𝑁)((𝑇‘𝑝) = (𝑇‘𝑎) → 𝑝 = 𝑎))) |
123 | 5, 121, 122 | sylanbrc 698 |
1
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑇:(𝑋𝐶𝑁)–1-1→((𝑋𝐹(𝑁 − 2)) × (𝐺 NeighbVtx 𝑋))) |