Step | Hyp | Ref
| Expression |
1 | | numclwwlk.c |
. . 3
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛)) |
2 | | numclwwlk.f |
. . 3
⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝐶‘𝑛) ∣ (𝑤‘0) = 𝑣}) |
3 | | numclwwlk.g |
. . 3
⊢ 𝐺 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝐶‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) = (𝑤‘0))}) |
4 | | numclwwlk.t |
. . 3
⊢ 𝑇 = (𝑤 ∈ (𝑋𝐺𝑁) ↦ 〈(𝑤 substr 〈0, (𝑁 − 2)〉), (𝑤‘(𝑁 − 1))〉) |
5 | 1, 2, 3, 4 | numclwlk1lem2f 26619 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑇:(𝑋𝐺𝑁)⟶((𝑋𝐹(𝑁 − 2)) × (〈𝑉, 𝐸〉 Neighbors 𝑋))) |
6 | 1, 2, 3, 4 | numclwlk1lem2fv 26620 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑝 ∈ (𝑋𝐺𝑁) → (𝑇‘𝑝) = 〈(𝑝 substr 〈0, (𝑁 − 2)〉), (𝑝‘(𝑁 − 1))〉)) |
7 | 6 | imp 444 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑝 ∈ (𝑋𝐺𝑁)) → (𝑇‘𝑝) = 〈(𝑝 substr 〈0, (𝑁 − 2)〉), (𝑝‘(𝑁 − 1))〉) |
8 | 7 | adantrr 749 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑝 ∈ (𝑋𝐺𝑁) ∧ 𝑢 ∈ (𝑋𝐺𝑁))) → (𝑇‘𝑝) = 〈(𝑝 substr 〈0, (𝑁 − 2)〉), (𝑝‘(𝑁 − 1))〉) |
9 | 1, 2, 3, 4 | numclwlk1lem2fv 26620 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑢 ∈ (𝑋𝐺𝑁) → (𝑇‘𝑢) = 〈(𝑢 substr 〈0, (𝑁 − 2)〉), (𝑢‘(𝑁 − 1))〉)) |
10 | 9 | imp 444 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑢 ∈ (𝑋𝐺𝑁)) → (𝑇‘𝑢) = 〈(𝑢 substr 〈0, (𝑁 − 2)〉), (𝑢‘(𝑁 − 1))〉) |
11 | 10 | adantrl 748 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑝 ∈ (𝑋𝐺𝑁) ∧ 𝑢 ∈ (𝑋𝐺𝑁))) → (𝑇‘𝑢) = 〈(𝑢 substr 〈0, (𝑁 − 2)〉), (𝑢‘(𝑁 − 1))〉) |
12 | 8, 11 | eqeq12d 2625 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑝 ∈ (𝑋𝐺𝑁) ∧ 𝑢 ∈ (𝑋𝐺𝑁))) → ((𝑇‘𝑝) = (𝑇‘𝑢) ↔ 〈(𝑝 substr 〈0, (𝑁 − 2)〉), (𝑝‘(𝑁 − 1))〉 = 〈(𝑢 substr 〈0, (𝑁 − 2)〉), (𝑢‘(𝑁 − 1))〉)) |
13 | | ovex 6577 |
. . . . . 6
⊢ (𝑝 substr 〈0, (𝑁 − 2)〉) ∈
V |
14 | | fvex 6113 |
. . . . . 6
⊢ (𝑝‘(𝑁 − 1)) ∈ V |
15 | 13, 14 | opth 4871 |
. . . . 5
⊢
(〈(𝑝 substr
〈0, (𝑁 −
2)〉), (𝑝‘(𝑁 − 1))〉 =
〈(𝑢 substr 〈0,
(𝑁 − 2)〉),
(𝑢‘(𝑁 − 1))〉 ↔ ((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑢 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑢‘(𝑁 − 1)))) |
16 | | uzuzle23 11605 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈
(ℤ≥‘2)) |
17 | 1, 2, 3 | numclwwlkovgelim 26616 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑝 ∈ (𝑋𝐺𝑁) → ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))))) |
18 | 16, 17 | syl3an3 1353 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑝 ∈ (𝑋𝐺𝑁) → ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))))) |
19 | 1, 2, 3 | numclwwlkovgelim 26616 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑢 ∈ (𝑋𝐺𝑁) → ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0))))) |
20 | 16, 19 | syl3an3 1353 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑢 ∈ (𝑋𝐺𝑁) → ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0))))) |
21 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) → 𝑝 ∈ Word 𝑉) |
22 | 21 | ad2antrl 760 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0))))) → 𝑝 ∈ Word 𝑉) |
23 | | simprll 798 |
. . . . . . . . . . 11
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0)))) → 𝑢 ∈ Word 𝑉) |
24 | 23 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0))))) → 𝑢 ∈ Word 𝑉) |
25 | | eleq1 2676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 = (#‘𝑝) → (𝑁 ∈ (ℤ≥‘3)
↔ (#‘𝑝) ∈
(ℤ≥‘3))) |
26 | 25 | eqcoms 2618 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑝) = 𝑁 → (𝑁 ∈ (ℤ≥‘3)
↔ (#‘𝑝) ∈
(ℤ≥‘3))) |
27 | | eluz2 11569 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑝) ∈
(ℤ≥‘3) ↔ (3 ∈ ℤ ∧ (#‘𝑝) ∈ ℤ ∧ 3 ≤
(#‘𝑝))) |
28 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑝) ∈
ℤ → 1 ∈ ℝ) |
29 | | 3re 10971 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 3 ∈
ℝ |
30 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑝) ∈
ℤ → 3 ∈ ℝ) |
31 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑝) ∈
ℤ → (#‘𝑝)
∈ ℝ) |
32 | 28, 30, 31 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑝) ∈
ℤ → (1 ∈ ℝ ∧ 3 ∈ ℝ ∧ (#‘𝑝) ∈
ℝ)) |
33 | | 1lt3 11073 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 <
3 |
34 | | ltletr 10008 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
∈ ℝ ∧ 3 ∈ ℝ ∧ (#‘𝑝) ∈ ℝ) → ((1 < 3 ∧ 3
≤ (#‘𝑝)) → 1
< (#‘𝑝))) |
35 | 34 | expd 451 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1
∈ ℝ ∧ 3 ∈ ℝ ∧ (#‘𝑝) ∈ ℝ) → (1 < 3 → (3
≤ (#‘𝑝) → 1
< (#‘𝑝)))) |
36 | 32, 33, 35 | mpisyl 21 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑝) ∈
ℤ → (3 ≤ (#‘𝑝) → 1 < (#‘𝑝))) |
37 | 36 | imp 444 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝑝) ∈
ℤ ∧ 3 ≤ (#‘𝑝)) → 1 < (#‘𝑝)) |
38 | 37 | 3adant1 1072 |
. . . . . . . . . . . . . . . . 17
⊢ ((3
∈ ℤ ∧ (#‘𝑝) ∈ ℤ ∧ 3 ≤ (#‘𝑝)) → 1 < (#‘𝑝)) |
39 | 27, 38 | sylbi 206 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑝) ∈
(ℤ≥‘3) → 1 < (#‘𝑝)) |
40 | 26, 39 | syl6bi 242 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑝) = 𝑁 → (𝑁 ∈ (ℤ≥‘3)
→ 1 < (#‘𝑝))) |
41 | 40 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘3) → ((#‘𝑝) = 𝑁 → 1 < (#‘𝑝))) |
42 | 41 | 3ad2ant3 1077 |
. . . . . . . . . . . . 13
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((#‘𝑝) = 𝑁 → 1 < (#‘𝑝))) |
43 | 42 | com12 32 |
. . . . . . . . . . . 12
⊢
((#‘𝑝) = 𝑁 → ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 1 < (#‘𝑝))) |
44 | 43 | ad3antlr 763 |
. . . . . . . . . . 11
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0)))) → ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 1 < (#‘𝑝))) |
45 | 44 | impcom 445 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0))))) → 1 < (#‘𝑝)) |
46 | | 2swrd2eqwrdeq 13544 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ Word 𝑉 ∧ 𝑢 ∈ Word 𝑉 ∧ 1 < (#‘𝑝)) → (𝑝 = 𝑢 ↔ ((#‘𝑝) = (#‘𝑢) ∧ ((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑢 substr 〈0, ((#‘𝑝) − 2)〉) ∧ (𝑝‘((#‘𝑝) − 2)) = (𝑢‘((#‘𝑝) − 2)) ∧ ( lastS ‘𝑝) = ( lastS ‘𝑢))))) |
47 | 22, 24, 45, 46 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0))))) → (𝑝 = 𝑢 ↔ ((#‘𝑝) = (#‘𝑢) ∧ ((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑢 substr 〈0, ((#‘𝑝) − 2)〉) ∧ (𝑝‘((#‘𝑝) − 2)) = (𝑢‘((#‘𝑝) − 2)) ∧ ( lastS ‘𝑝) = ( lastS ‘𝑢))))) |
48 | | eqtr3 2631 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝑝) =
𝑁 ∧ (#‘𝑢) = 𝑁) → (#‘𝑝) = (#‘𝑢)) |
49 | 48 | expcom 450 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑢) = 𝑁 → ((#‘𝑝) = 𝑁 → (#‘𝑝) = (#‘𝑢))) |
50 | 49 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) → ((#‘𝑝) = 𝑁 → (#‘𝑝) = (#‘𝑢))) |
51 | 50 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0))) → ((#‘𝑝) = 𝑁 → (#‘𝑝) = (#‘𝑢))) |
52 | 51 | com12 32 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑝) = 𝑁 → (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0))) → (#‘𝑝) = (#‘𝑢))) |
53 | 52 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) → (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0))) → (#‘𝑝) = (#‘𝑢))) |
54 | 53 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) → (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0))) → (#‘𝑝) = (#‘𝑢))) |
55 | 54 | imp 444 |
. . . . . . . . . . 11
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0)))) → (#‘𝑝) = (#‘𝑢)) |
56 | 55 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0))))) → (#‘𝑝) = (#‘𝑢)) |
57 | 56 | biantrurd 528 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘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 ‘𝑢))))) |
58 | | 3anan12 1044 |
. . . . . . . . . . 11
⊢ (((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑢 substr 〈0, ((#‘𝑝) − 2)〉) ∧ (𝑝‘((#‘𝑝) − 2)) = (𝑢‘((#‘𝑝) − 2)) ∧ ( lastS
‘𝑝) = ( lastS
‘𝑢)) ↔ ((𝑝‘((#‘𝑝) − 2)) = (𝑢‘((#‘𝑝) − 2)) ∧ ((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑢 substr 〈0, ((#‘𝑝) − 2)〉) ∧ (
lastS ‘𝑝) = ( lastS
‘𝑢)))) |
59 | 58 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘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
‘𝑢))))) |
60 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝‘0) = 𝑋 → ((𝑝‘(𝑁 − 2)) = (𝑝‘0) ↔ (𝑝‘(𝑁 − 2)) = 𝑋)) |
61 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 = (#‘𝑝) → (𝑁 − 2) = ((#‘𝑝) − 2)) |
62 | 61 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑝) = 𝑁 → (𝑁 − 2) = ((#‘𝑝) − 2)) |
63 | 62 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑝) = 𝑁 → (𝑝‘(𝑁 − 2)) = (𝑝‘((#‘𝑝) − 2))) |
64 | 63 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑝) = 𝑁 → ((𝑝‘(𝑁 − 2)) = 𝑋 ↔ (𝑝‘((#‘𝑝) − 2)) = 𝑋)) |
65 | 64 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑝) = 𝑁 → ((𝑝‘(𝑁 − 2)) = 𝑋 → (𝑝‘((#‘𝑝) − 2)) = 𝑋)) |
66 | 65 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝‘(𝑁 − 2)) = 𝑋 → ((#‘𝑝) = 𝑁 → (𝑝‘((#‘𝑝) − 2)) = 𝑋)) |
67 | 60, 66 | syl6bi 242 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝‘0) = 𝑋 → ((𝑝‘(𝑁 − 2)) = (𝑝‘0) → ((#‘𝑝) = 𝑁 → (𝑝‘((#‘𝑝) − 2)) = 𝑋))) |
68 | 67 | imp 444 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0)) → ((#‘𝑝) = 𝑁 → (𝑝‘((#‘𝑝) − 2)) = 𝑋)) |
69 | 68 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑝) = 𝑁 → (((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0)) → (𝑝‘((#‘𝑝) − 2)) = 𝑋)) |
70 | 69 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) → (((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0)) → (𝑝‘((#‘𝑝) − 2)) = 𝑋)) |
71 | 70 | imp 444 |
. . . . . . . . . . . . . 14
⊢ (((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) → (𝑝‘((#‘𝑝) − 2)) = 𝑋) |
72 | 71 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0)))) → (𝑝‘((#‘𝑝) − 2)) = 𝑋) |
73 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑝) = 𝑁 → ((#‘𝑝) − 2) = (𝑁 − 2)) |
74 | 73 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑝) = 𝑁 → (𝑢‘((#‘𝑝) − 2)) = (𝑢‘(𝑁 − 2))) |
75 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑢‘0) = (𝑢‘(𝑁 − 2)) → ((𝑢‘0) = 𝑋 ↔ (𝑢‘(𝑁 − 2)) = 𝑋)) |
76 | 75 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑢‘(𝑁 − 2)) = (𝑢‘0) → ((𝑢‘0) = 𝑋 ↔ (𝑢‘(𝑁 − 2)) = 𝑋)) |
77 | 76 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑢‘(𝑁 − 2)) = (𝑢‘0) → ((𝑢‘0) = 𝑋 → (𝑢‘(𝑁 − 2)) = 𝑋)) |
78 | 77 | impcom 445 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0)) → (𝑢‘(𝑁 − 2)) = 𝑋) |
79 | 78 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0))) → (𝑢‘(𝑁 − 2)) = 𝑋) |
80 | 74, 79 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘𝑝) =
𝑁 ∧ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0)))) → (𝑢‘((#‘𝑝) − 2)) = 𝑋) |
81 | 80 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑝) = 𝑁 → (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0))) → (𝑢‘((#‘𝑝) − 2)) = 𝑋)) |
82 | 81 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) → (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0))) → (𝑢‘((#‘𝑝) − 2)) = 𝑋)) |
83 | 82 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) → (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0))) → (𝑢‘((#‘𝑝) − 2)) = 𝑋)) |
84 | 83 | imp 444 |
. . . . . . . . . . . . 13
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0)))) → (𝑢‘((#‘𝑝) − 2)) = 𝑋) |
85 | 72, 84 | eqtr4d 2647 |
. . . . . . . . . . . 12
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0)))) → (𝑝‘((#‘𝑝) − 2)) = (𝑢‘((#‘𝑝) − 2))) |
86 | 85 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0))))) → (𝑝‘((#‘𝑝) − 2)) = (𝑢‘((#‘𝑝) − 2))) |
87 | 86 | biantrurd 528 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘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
‘𝑢))))) |
88 | 73 | opeq2d 4347 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑝) = 𝑁 → 〈0, ((#‘𝑝) − 2)〉 = 〈0,
(𝑁 −
2)〉) |
89 | 88 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑝) = 𝑁 → (𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑝 substr 〈0, (𝑁 − 2)〉)) |
90 | 88 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑝) = 𝑁 → (𝑢 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑢 substr 〈0, (𝑁 − 2)〉)) |
91 | 89, 90 | eqeq12d 2625 |
. . . . . . . . . . . . 13
⊢
((#‘𝑝) = 𝑁 → ((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑢 substr 〈0, ((#‘𝑝) − 2)〉) ↔ (𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑢 substr 〈0, (𝑁 −
2)〉))) |
92 | 91 | ad3antlr 763 |
. . . . . . . . . . . 12
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0)))) → ((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑢 substr 〈0, ((#‘𝑝) − 2)〉) ↔ (𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑢 substr 〈0, (𝑁 −
2)〉))) |
93 | 92 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0))))) → ((𝑝 substr 〈0, ((#‘𝑝) − 2)〉) = (𝑢 substr 〈0, ((#‘𝑝) − 2)〉) ↔ (𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑢 substr 〈0, (𝑁 −
2)〉))) |
94 | | lsw 13204 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ Word 𝑉 → ( lastS ‘𝑝) = (𝑝‘((#‘𝑝) − 1))) |
95 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑝) = 𝑁 → ((#‘𝑝) − 1) = (𝑁 − 1)) |
96 | 95 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑝) = 𝑁 → (𝑝‘((#‘𝑝) − 1)) = (𝑝‘(𝑁 − 1))) |
97 | 94, 96 | sylan9eq 2664 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) → ( lastS ‘𝑝) = (𝑝‘(𝑁 − 1))) |
98 | 97 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) → ( lastS ‘𝑝) = (𝑝‘(𝑁 − 1))) |
99 | | lsw 13204 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ Word 𝑉 → ( lastS ‘𝑢) = (𝑢‘((#‘𝑢) − 1))) |
100 | 99 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) → ( lastS ‘𝑢) = (𝑢‘((#‘𝑢) − 1))) |
101 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 = (#‘𝑢) → (𝑁 − 1) = ((#‘𝑢) − 1)) |
102 | 101 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑢) = 𝑁 → (𝑁 − 1) = ((#‘𝑢) − 1)) |
103 | 102 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑢) = 𝑁 → (𝑢‘(𝑁 − 1)) = (𝑢‘((#‘𝑢) − 1))) |
104 | 103 | eqeq2d 2620 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑢) = 𝑁 → (( lastS ‘𝑢) = (𝑢‘(𝑁 − 1)) ↔ ( lastS ‘𝑢) = (𝑢‘((#‘𝑢) − 1)))) |
105 | 104 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) → (( lastS ‘𝑢) = (𝑢‘(𝑁 − 1)) ↔ ( lastS ‘𝑢) = (𝑢‘((#‘𝑢) − 1)))) |
106 | 100, 105 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) → ( lastS ‘𝑢) = (𝑢‘(𝑁 − 1))) |
107 | 106 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0))) → ( lastS ‘𝑢) = (𝑢‘(𝑁 − 1))) |
108 | 98, 107 | eqeqan12d 2626 |
. . . . . . . . . . . 12
⊢ ((((𝑝 ∈ Word 𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0)))) → (( lastS ‘𝑝) = ( lastS ‘𝑢) ↔ (𝑝‘(𝑁 − 1)) = (𝑢‘(𝑁 − 1)))) |
109 | 108 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0))))) → (( lastS ‘𝑝) = ( lastS ‘𝑢) ↔ (𝑝‘(𝑁 − 1)) = (𝑢‘(𝑁 − 1)))) |
110 | 93, 109 | anbi12d 743 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘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))))) |
111 | 59, 87, 110 | 3bitr2d 295 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘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))))) |
112 | 47, 57, 111 | 3bitr2d 295 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0))))) → (𝑝 = 𝑢 ↔ ((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑢 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑢‘(𝑁 − 1))))) |
113 | 112 | exbiri 650 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((((𝑝 ∈ Word
𝑉 ∧ (#‘𝑝) = 𝑁) ∧ ((𝑝‘0) = 𝑋 ∧ (𝑝‘(𝑁 − 2)) = (𝑝‘0))) ∧ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = 𝑁) ∧ ((𝑢‘0) = 𝑋 ∧ (𝑢‘(𝑁 − 2)) = (𝑢‘0)))) → (((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑢 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑢‘(𝑁 − 1))) → 𝑝 = 𝑢))) |
114 | 18, 20, 113 | syl2and 499 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑝 ∈ (𝑋𝐺𝑁) ∧ 𝑢 ∈ (𝑋𝐺𝑁)) → (((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑢 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑢‘(𝑁 − 1))) → 𝑝 = 𝑢))) |
115 | 114 | imp 444 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑝 ∈ (𝑋𝐺𝑁) ∧ 𝑢 ∈ (𝑋𝐺𝑁))) → (((𝑝 substr 〈0, (𝑁 − 2)〉) = (𝑢 substr 〈0, (𝑁 − 2)〉) ∧ (𝑝‘(𝑁 − 1)) = (𝑢‘(𝑁 − 1))) → 𝑝 = 𝑢)) |
116 | 15, 115 | syl5bi 231 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑝 ∈ (𝑋𝐺𝑁) ∧ 𝑢 ∈ (𝑋𝐺𝑁))) → (〈(𝑝 substr 〈0, (𝑁 − 2)〉), (𝑝‘(𝑁 − 1))〉 = 〈(𝑢 substr 〈0, (𝑁 − 2)〉), (𝑢‘(𝑁 − 1))〉 → 𝑝 = 𝑢)) |
117 | 12, 116 | sylbid 229 |
. . 3
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ (𝑝 ∈ (𝑋𝐺𝑁) ∧ 𝑢 ∈ (𝑋𝐺𝑁))) → ((𝑇‘𝑝) = (𝑇‘𝑢) → 𝑝 = 𝑢)) |
118 | 117 | ralrimivva 2954 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ∀𝑝 ∈
(𝑋𝐺𝑁)∀𝑢 ∈ (𝑋𝐺𝑁)((𝑇‘𝑝) = (𝑇‘𝑢) → 𝑝 = 𝑢)) |
119 | | dff13 6416 |
. 2
⊢ (𝑇:(𝑋𝐺𝑁)–1-1→((𝑋𝐹(𝑁 − 2)) × (〈𝑉, 𝐸〉 Neighbors 𝑋)) ↔ (𝑇:(𝑋𝐺𝑁)⟶((𝑋𝐹(𝑁 − 2)) × (〈𝑉, 𝐸〉 Neighbors 𝑋)) ∧ ∀𝑝 ∈ (𝑋𝐺𝑁)∀𝑢 ∈ (𝑋𝐺𝑁)((𝑇‘𝑝) = (𝑇‘𝑢) → 𝑝 = 𝑢))) |
120 | 5, 118, 119 | sylanbrc 695 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑇:(𝑋𝐺𝑁)–1-1→((𝑋𝐹(𝑁 − 2)) × (〈𝑉, 𝐸〉 Neighbors 𝑋))) |