Step | Hyp | Ref
| Expression |
1 | | av-extwwlkfab.v |
. . 3
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | av-extwwlkfab.f |
. . 3
⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑣}) |
3 | | av-extwwlkfab.c |
. . 3
⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑛 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) = (𝑤‘0))}) |
4 | | av-numclwwlk.t |
. . 3
⊢ 𝑇 = (𝑤 ∈ (𝑋𝐶𝑁) ↦ 〈(𝑤 substr 〈0, (𝑁 − 2)〉), (𝑤‘(𝑁 − 1))〉) |
5 | 1, 2, 3, 4 | av-numclwlk1lem2f 41522 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑇:(𝑋𝐶𝑁)⟶((𝑋𝐹(𝑁 − 2)) × (𝐺 NeighbVtx 𝑋))) |
6 | | elxp 5055 |
. . . . 5
⊢ (𝑝 ∈ ((𝑋𝐹(𝑁 − 2)) × (𝐺 NeighbVtx 𝑋)) ↔ ∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (𝐺 NeighbVtx 𝑋)))) |
7 | 1, 2, 3 | av-numclwlk1lem2foa 41521 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (𝐺 NeighbVtx 𝑋)) → ((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) ∈ (𝑋𝐶𝑁))) |
8 | 7 | com12 32 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (𝐺 NeighbVtx 𝑋)) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑎 ++
〈“𝑋”〉) ++ 〈“𝑏”〉) ∈ (𝑋𝐶𝑁))) |
9 | 8 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (𝐺 NeighbVtx 𝑋))) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑎 ++
〈“𝑋”〉) ++ 〈“𝑏”〉) ∈ (𝑋𝐶𝑁))) |
10 | 9 | imp 444 |
. . . . . . . 8
⊢ (((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (𝐺 NeighbVtx 𝑋))) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ ((𝑎 ++
〈“𝑋”〉) ++ 〈“𝑏”〉) ∈ (𝑋𝐶𝑁)) |
11 | | simpl 472 |
. . . . . . . . 9
⊢ ((((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) ∈ (𝑋𝐶𝑁) ∧ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (𝐺 NeighbVtx 𝑋))) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))))
→ ((𝑎 ++
〈“𝑋”〉) ++ 〈“𝑏”〉) ∈ (𝑋𝐶𝑁)) |
12 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = ((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) → (𝑇‘𝑥) = (𝑇‘((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉))) |
13 | 12 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑥 = ((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) → (𝑝 = (𝑇‘𝑥) ↔ 𝑝 = (𝑇‘((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉)))) |
14 | 1, 2, 3, 4 | av-numclwlk1lem2fv 41523 |
. . . . . . . . . . . 12
⊢ (((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) ∈ (𝑋𝐶𝑁) → (𝑇‘((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉)) = 〈(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) substr 〈0, (𝑁 − 2)〉), (((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉) |
15 | 14 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) ∈ (𝑋𝐶𝑁) ∧ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (𝐺 NeighbVtx 𝑋))) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))))
→ (𝑇‘((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)) = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉) |
16 | 15 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ ((((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) ∈ (𝑋𝐶𝑁) ∧ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (𝐺 NeighbVtx 𝑋))) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))))
→ (𝑝 = (𝑇‘((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉)) ↔ 𝑝 = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉)) |
17 | 13, 16 | sylan9bbr 733 |
. . . . . . . . 9
⊢
(((((𝑎 ++
〈“𝑋”〉) ++ 〈“𝑏”〉) ∈ (𝑋𝐶𝑁) ∧ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (𝐺 NeighbVtx 𝑋))) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))))
∧ 𝑥 = ((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)) → (𝑝 = (𝑇‘𝑥) ↔ 𝑝 = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉)) |
18 | | simprll 798 |
. . . . . . . . . 10
⊢ ((((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) ∈ (𝑋𝐶𝑁) ∧ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (𝐺 NeighbVtx 𝑋))) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))))
→ 𝑝 = 〈𝑎, 𝑏〉) |
19 | 1 | nbgrisvtx 40581 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ USGraph ∧ 𝑏 ∈ (𝐺 NeighbVtx 𝑋)) → 𝑏 ∈ 𝑉) |
20 | 19 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ USGraph → (𝑏 ∈ (𝐺 NeighbVtx 𝑋) → 𝑏 ∈ 𝑉)) |
21 | 20 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑏 ∈ (𝐺 NeighbVtx 𝑋) → 𝑏 ∈ 𝑉)) |
22 | | simp1 1054 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝐺 ∈ USGraph
) |
23 | | uz3m2nn 11607 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ ℕ) |
24 | 23 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 2) ∈
ℕ) |
25 | | simp2 1055 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑋 ∈ 𝑉) |
26 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
27 | 2, 1, 26 | av-numclwwlkovfel2 41514 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ USGraph ∧ (𝑁 − 2) ∈ ℕ ∧
𝑋 ∈ 𝑉) → (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ↔ ((𝑎 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑎) − 1)){(𝑎‘𝑖), (𝑎‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑎), (𝑎‘0)} ∈ (Edg‘𝐺)) ∧ (#‘𝑎) = (𝑁 − 2) ∧ (𝑎‘0) = 𝑋))) |
28 | 22, 24, 25, 27 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ↔ ((𝑎 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑎) − 1)){(𝑎‘𝑖), (𝑎‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑎), (𝑎‘0)} ∈ (Edg‘𝐺)) ∧ (#‘𝑎) = (𝑁 − 2) ∧ (𝑎‘0) = 𝑋))) |
29 | | df-3an 1033 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑎) − 1)){(𝑎‘𝑖), (𝑎‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑎), (𝑎‘0)} ∈ (Edg‘𝐺)) ∧ (#‘𝑎) = (𝑁 − 2) ∧ (𝑎‘0) = 𝑋) ↔ (((𝑎 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑎) − 1)){(𝑎‘𝑖), (𝑎‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑎), (𝑎‘0)} ∈ (Edg‘𝐺)) ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑎‘0) = 𝑋)) |
30 | 28, 29 | syl6bb 275 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ↔ (((𝑎 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑎) − 1)){(𝑎‘𝑖), (𝑎‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑎), (𝑎‘0)} ∈ (Edg‘𝐺)) ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑎‘0) = 𝑋))) |
31 | | simplll 794 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → 𝑎 ∈ Word 𝑉) |
32 | | s1cl 13235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑋 ∈ 𝑉 → 〈“𝑋”〉 ∈ Word 𝑉) |
33 | 32 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 〈“𝑋”〉 ∈ Word 𝑉) |
34 | 33 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 〈“𝑋”〉 ∈ Word 𝑉) |
35 | 34 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → 〈“𝑋”〉 ∈ Word 𝑉) |
36 | | s1cl 13235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑏 ∈ 𝑉 → 〈“𝑏”〉 ∈ Word 𝑉) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → 〈“𝑏”〉 ∈ Word 𝑉) |
38 | | ccatass 13224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑎 ∈ Word 𝑉 ∧ 〈“𝑋”〉 ∈ Word 𝑉 ∧ 〈“𝑏”〉 ∈ Word 𝑉) → ((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) = (𝑎 ++ (〈“𝑋”〉 ++
〈“𝑏”〉))) |
39 | 38 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑎 ∈ Word 𝑉 ∧ 〈“𝑋”〉 ∈ Word 𝑉 ∧ 〈“𝑏”〉 ∈ Word 𝑉) → (((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉) =
((𝑎 ++ (〈“𝑋”〉 ++
〈“𝑏”〉)) substr 〈0, (𝑁 −
2)〉)) |
40 | 31, 35, 37, 39 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → (((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉) =
((𝑎 ++ (〈“𝑋”〉 ++
〈“𝑏”〉)) substr 〈0, (𝑁 −
2)〉)) |
41 | | ccatcl 13212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((〈“𝑋”〉 ∈ Word 𝑉 ∧ 〈“𝑏”〉 ∈ Word 𝑉) → (〈“𝑋”〉 ++ 〈“𝑏”〉) ∈ Word 𝑉) |
42 | 34, 36, 41 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → (〈“𝑋”〉 ++
〈“𝑏”〉) ∈ Word 𝑉) |
43 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) → (#‘𝑎) = (𝑁 − 2)) |
44 | 43 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) → (𝑁 − 2) = (#‘𝑎)) |
45 | 44 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑁 − 2) =
(#‘𝑎)) |
46 | 45 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → (𝑁 − 2) = (#‘𝑎)) |
47 | | swrdccatid 13348 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑎 ∈ Word 𝑉 ∧ (〈“𝑋”〉 ++ 〈“𝑏”〉) ∈ Word 𝑉 ∧ (𝑁 − 2) = (#‘𝑎)) → ((𝑎 ++ (〈“𝑋”〉 ++ 〈“𝑏”〉)) substr 〈0,
(𝑁 − 2)〉) =
𝑎) |
48 | 31, 42, 46, 47 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → ((𝑎 ++ (〈“𝑋”〉 ++ 〈“𝑏”〉)) substr 〈0,
(𝑁 − 2)〉) =
𝑎) |
49 | 40, 48 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → 𝑎 = (((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 −
2)〉)) |
50 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) ∈ V |
51 | | lsw 13204 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) ∈ V → ( lastS
‘((𝑎 ++
〈“𝑋”〉) ++ 〈“𝑏”〉)) = (((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘((#‘((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)) − 1))) |
52 | 50, 51 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ( lastS
‘((𝑎 ++
〈“𝑋”〉) ++ 〈“𝑏”〉)) = (((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘((#‘((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)) − 1)) |
53 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) → 𝑎 ∈ Word 𝑉) |
54 | | ccatcl 13212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑎 ∈ Word 𝑉 ∧ 〈“𝑋”〉 ∈ Word 𝑉) → (𝑎 ++ 〈“𝑋”〉) ∈ Word 𝑉) |
55 | 53, 33, 54 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑎 ++
〈“𝑋”〉) ∈ Word 𝑉) |
56 | | lswccats1 13263 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑎 ++ 〈“𝑋”〉) ∈ Word 𝑉 ∧ 𝑏 ∈ 𝑉) → ( lastS ‘((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉)) = 𝑏) |
57 | 55, 56 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → ( lastS ‘((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)) = 𝑏) |
58 | | ccatlen 13213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑎 ++ 〈“𝑋”〉) ∈ Word 𝑉 ∧ 〈“𝑏”〉 ∈ Word 𝑉) → (#‘((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)) = ((#‘(𝑎 ++ 〈“𝑋”〉)) +
(#‘〈“𝑏”〉))) |
59 | 55, 36, 58 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → (#‘((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)) = ((#‘(𝑎 ++ 〈“𝑋”〉)) +
(#‘〈“𝑏”〉))) |
60 | 53, 33 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑎 ∈ Word 𝑉 ∧ 〈“𝑋”〉 ∈ Word 𝑉)) |
61 | 60 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → (𝑎 ∈ Word 𝑉 ∧ 〈“𝑋”〉 ∈ Word 𝑉)) |
62 | | ccatlen 13213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑎 ∈ Word 𝑉 ∧ 〈“𝑋”〉 ∈ Word 𝑉) → (#‘(𝑎 ++ 〈“𝑋”〉)) = ((#‘𝑎) + (#‘〈“𝑋”〉))) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → (#‘(𝑎 ++ 〈“𝑋”〉)) =
((#‘𝑎) +
(#‘〈“𝑋”〉))) |
64 | | s1len 13238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(#‘〈“𝑏”〉) = 1 |
65 | 64 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) →
(#‘〈“𝑏”〉) = 1) |
66 | 63, 65 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → ((#‘(𝑎 ++ 〈“𝑋”〉)) +
(#‘〈“𝑏”〉)) = (((#‘𝑎) + (#‘〈“𝑋”〉)) +
1)) |
67 | | s1len 13238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(#‘〈“𝑋”〉) = 1 |
68 | 67 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (#‘〈“𝑋”〉) = 1) |
69 | 43, 68 | oveqan12d 6568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ ((#‘𝑎) +
(#‘〈“𝑋”〉)) = ((𝑁 − 2) + 1)) |
70 | 69 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (((#‘𝑎) +
(#‘〈“𝑋”〉)) + 1) = (((𝑁 − 2) + 1) + 1)) |
71 | | eluzelcn 11575 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℂ) |
72 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑁 ∈ ℂ → 𝑁 ∈
ℂ) |
73 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑁 ∈ ℂ → 2 ∈
ℂ) |
74 | 72, 73 | subcld 10271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑁 ∈ ℂ → (𝑁 − 2) ∈
ℂ) |
75 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑁 ∈ ℂ → 1 ∈
ℂ) |
76 | 74, 75, 75 | addassd 9941 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑁 ∈ ℂ → (((𝑁 − 2) + 1) + 1) = ((𝑁 − 2) + (1 +
1))) |
77 | | 1p1e2 11011 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (1 + 1) =
2 |
78 | 77 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑁 ∈ ℂ → (1 + 1) =
2) |
79 | 78 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑁 ∈ ℂ → ((𝑁 − 2) + (1 + 1)) = ((𝑁 − 2) +
2)) |
80 | 76, 79 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 ∈ ℂ → (((𝑁 − 2) + 1) + 1) = ((𝑁 − 2) +
2)) |
81 | 71, 80 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈
(ℤ≥‘3) → (((𝑁 − 2) + 1) + 1) = ((𝑁 − 2) + 2)) |
82 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 ∈
(ℤ≥‘3) → 2 ∈ ℂ) |
83 | 71, 82 | npcand 10275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑁 − 2) + 2) = 𝑁) |
84 | 81, 83 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈
(ℤ≥‘3) → (((𝑁 − 2) + 1) + 1) = 𝑁) |
85 | 84 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑁 − 2) + 1)
+ 1) = 𝑁) |
86 | 85 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (((𝑁 − 2) + 1)
+ 1) = 𝑁) |
87 | 70, 86 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (((#‘𝑎) +
(#‘〈“𝑋”〉)) + 1) = 𝑁) |
88 | 87 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → (((#‘𝑎) + (#‘〈“𝑋”〉)) + 1) = 𝑁) |
89 | 59, 66, 88 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → (#‘((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)) = 𝑁) |
90 | 89 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → ((#‘((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)) − 1) = (𝑁 − 1)) |
91 | 90 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → (((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉)‘((#‘((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)) − 1)) = (((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))) |
92 | 52, 57, 91 | 3eqtr3a 2668 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → 𝑏 = (((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉)‘(𝑁 − 1))) |
93 | 49, 92 | opeq12d 4348 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉) |
94 | 93 | exp31 628 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑏 ∈ 𝑉 → 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉))) |
95 | 94 | 3ad2antl1 1216 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑎 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑎) − 1)){(𝑎‘𝑖), (𝑎‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑎), (𝑎‘0)} ∈ (Edg‘𝐺)) ∧ (#‘𝑎) = (𝑁 − 2)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑏 ∈ 𝑉 → 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉))) |
96 | 95 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑎 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑎) − 1)){(𝑎‘𝑖), (𝑎‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑎), (𝑎‘0)} ∈ (Edg‘𝐺)) ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑎‘0) = 𝑋) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑏 ∈ 𝑉 → 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉))) |
97 | 96 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((((𝑎 ∈ Word
𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑎) − 1)){(𝑎‘𝑖), (𝑎‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑎), (𝑎‘0)} ∈ (Edg‘𝐺)) ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑎‘0) = 𝑋) → (𝑏 ∈ 𝑉 → 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉))) |
98 | 97 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((((𝑎 ∈ Word
𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑎) − 1)){(𝑎‘𝑖), (𝑎‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑎), (𝑎‘0)} ∈ (Edg‘𝐺)) ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑎‘0) = 𝑋) → (𝑏 ∈ 𝑉 → 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉))) |
99 | 30, 98 | sylbid 229 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) → (𝑏 ∈ 𝑉 → 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉))) |
100 | 99 | com23 84 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑏 ∈ 𝑉 → (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) → 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉))) |
101 | 21, 100 | syld 46 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑏 ∈ (𝐺 NeighbVtx 𝑋) → (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) → 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉))) |
102 | 101 | com13 86 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) → (𝑏 ∈ (𝐺 NeighbVtx 𝑋) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) substr 〈0, (𝑁 − 2)〉), (((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉))) |
103 | 102 | imp 444 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (𝐺 NeighbVtx 𝑋)) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) substr 〈0, (𝑁 − 2)〉), (((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉)) |
104 | 103 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (𝐺 NeighbVtx 𝑋))) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) substr 〈0, (𝑁 − 2)〉), (((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉)) |
105 | 104 | imp 444 |
. . . . . . . . . . 11
⊢ (((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (𝐺 NeighbVtx 𝑋))) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) substr 〈0, (𝑁 − 2)〉), (((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉) |
106 | 105 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) ∈ (𝑋𝐶𝑁) ∧ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (𝐺 NeighbVtx 𝑋))) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))))
→ 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) substr 〈0, (𝑁 − 2)〉), (((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉) |
107 | 18, 106 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) ∈ (𝑋𝐶𝑁) ∧ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (𝐺 NeighbVtx 𝑋))) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))))
→ 𝑝 = 〈(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) substr 〈0, (𝑁 − 2)〉), (((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉) |
108 | 11, 17, 107 | rspcedvd 3289 |
. . . . . . . 8
⊢ ((((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) ∈ (𝑋𝐶𝑁) ∧ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (𝐺 NeighbVtx 𝑋))) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))))
→ ∃𝑥 ∈
(𝑋𝐶𝑁)𝑝 = (𝑇‘𝑥)) |
109 | 10, 108 | mpancom 700 |
. . . . . . 7
⊢ (((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (𝐺 NeighbVtx 𝑋))) ∧ (𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ ∃𝑥 ∈
(𝑋𝐶𝑁)𝑝 = (𝑇‘𝑥)) |
110 | 109 | ex 449 |
. . . . . 6
⊢ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (𝐺 NeighbVtx 𝑋))) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ∃𝑥 ∈
(𝑋𝐶𝑁)𝑝 = (𝑇‘𝑥))) |
111 | 110 | exlimivv 1847 |
. . . . 5
⊢
(∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (𝐺 NeighbVtx 𝑋))) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ∃𝑥 ∈
(𝑋𝐶𝑁)𝑝 = (𝑇‘𝑥))) |
112 | 6, 111 | sylbi 206 |
. . . 4
⊢ (𝑝 ∈ ((𝑋𝐹(𝑁 − 2)) × (𝐺 NeighbVtx 𝑋)) → ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ∃𝑥 ∈
(𝑋𝐶𝑁)𝑝 = (𝑇‘𝑥))) |
113 | 112 | impcom 445 |
. . 3
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑝 ∈ ((𝑋𝐹(𝑁 − 2)) × (𝐺 NeighbVtx 𝑋))) → ∃𝑥 ∈ (𝑋𝐶𝑁)𝑝 = (𝑇‘𝑥)) |
114 | 113 | ralrimiva 2949 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ∀𝑝 ∈
((𝑋𝐹(𝑁 − 2)) × (𝐺 NeighbVtx 𝑋))∃𝑥 ∈ (𝑋𝐶𝑁)𝑝 = (𝑇‘𝑥)) |
115 | | dffo3 6282 |
. 2
⊢ (𝑇:(𝑋𝐶𝑁)–onto→((𝑋𝐹(𝑁 − 2)) × (𝐺 NeighbVtx 𝑋)) ↔ (𝑇:(𝑋𝐶𝑁)⟶((𝑋𝐹(𝑁 − 2)) × (𝐺 NeighbVtx 𝑋)) ∧ ∀𝑝 ∈ ((𝑋𝐹(𝑁 − 2)) × (𝐺 NeighbVtx 𝑋))∃𝑥 ∈ (𝑋𝐶𝑁)𝑝 = (𝑇‘𝑥))) |
116 | 5, 114, 115 | sylanbrc 695 |
1
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑇:(𝑋𝐶𝑁)–onto→((𝑋𝐹(𝑁 − 2)) × (𝐺 NeighbVtx 𝑋))) |