Step | Hyp | Ref
| Expression |
1 | | clwlkfclwwlk.1 |
. . 3
⊢ 𝐴 = (1st ‘𝑐) |
2 | | clwlkfclwwlk.2 |
. . 3
⊢ 𝐵 = (2nd ‘𝑐) |
3 | | clwlkfclwwlk.c |
. . 3
⊢ 𝐶 = {𝑐 ∈ (𝑉 ClWalks 𝐸) ∣ (#‘𝐴) = 𝑁} |
4 | | clwlkfclwwlk.f |
. . 3
⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) |
5 | 1, 2, 3, 4 | clwlkfclwwlk 26371 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶⟶((𝑉 ClWWalksN 𝐸)‘𝑁)) |
6 | | clwwlknprop 26300 |
. . . . 5
⊢ (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) |
7 | 6 | adantl 481 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) |
8 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝑤) = 𝑁) → 𝑁 ∈
ℕ0) |
9 | 8 | anim2i 591 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ (#‘𝑤) = 𝑁)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑁 ∈
ℕ0)) |
10 | | df-3an 1033 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
↔ ((𝑉 ∈ V ∧
𝐸 ∈ V) ∧ 𝑁 ∈
ℕ0)) |
11 | 9, 10 | sylibr 223 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0
∧ (#‘𝑤) = 𝑁)) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈
ℕ0)) |
12 | 11 | 3adant2 1073 |
. . . . . . . . 9
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁)) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈
ℕ0)) |
13 | 12 | adantl 481 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈
ℕ0)) |
14 | | isclwwlkn 26297 |
. . . . . . . 8
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑤) = 𝑁))) |
15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) → (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑤) = 𝑁))) |
16 | | simpl1 1057 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) → 𝑉 USGrph 𝐸) |
17 | | simpr2 1061 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) → 𝑤 ∈ Word 𝑉) |
18 | | eleq1 2676 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑤) = 𝑁 → ((#‘𝑤) ∈ ℙ ↔ 𝑁 ∈
ℙ)) |
19 | | prmnn 15226 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑤) ∈
ℙ → (#‘𝑤)
∈ ℕ) |
20 | 19 | nnge1d 10940 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑤) ∈
ℙ → 1 ≤ (#‘𝑤)) |
21 | 18, 20 | syl6bir 243 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑤) = 𝑁 → (𝑁 ∈ ℙ → 1 ≤ (#‘𝑤))) |
22 | 21 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝑤) = 𝑁) → (𝑁 ∈ ℙ → 1 ≤ (#‘𝑤))) |
23 | 22 | 3ad2ant3 1077 |
. . . . . . . . . . . . 13
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁)) → (𝑁 ∈ ℙ → 1 ≤ (#‘𝑤))) |
24 | 23 | com12 32 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℙ → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁)) → 1 ≤ (#‘𝑤))) |
25 | 24 | 3ad2ant3 1077 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁)) → 1 ≤ (#‘𝑤))) |
26 | 25 | imp 444 |
. . . . . . . . . 10
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) → 1 ≤ (#‘𝑤)) |
27 | | clwlkisclwwlk2 26318 |
. . . . . . . . . 10
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑤 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑤)) → (∃𝑓 𝑓(𝑉 ClWalks 𝐸)(𝑤 ++ 〈“(𝑤‘0)”〉) ↔ 𝑤 ∈ (𝑉 ClWWalks 𝐸))) |
28 | 16, 17, 26, 27 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) → (∃𝑓 𝑓(𝑉 ClWalks 𝐸)(𝑤 ++ 〈“(𝑤‘0)”〉) ↔ 𝑤 ∈ (𝑉 ClWWalks 𝐸))) |
29 | 28 | bicomd 212 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) → (𝑤 ∈ (𝑉 ClWWalks 𝐸) ↔ ∃𝑓 𝑓(𝑉 ClWalks 𝐸)(𝑤 ++ 〈“(𝑤‘0)”〉))) |
30 | 29 | anbi1d 737 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) → ((𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑤) = 𝑁) ↔ (∃𝑓 𝑓(𝑉 ClWalks 𝐸)(𝑤 ++ 〈“(𝑤‘0)”〉) ∧ (#‘𝑤) = 𝑁))) |
31 | 15, 30 | bitrd 267 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) → (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (∃𝑓 𝑓(𝑉 ClWalks 𝐸)(𝑤 ++ 〈“(𝑤‘0)”〉) ∧ (#‘𝑤) = 𝑁))) |
32 | | df-br 4584 |
. . . . . . . . . . 11
⊢ (𝑓(𝑉 ClWalks 𝐸)(𝑤 ++ 〈“(𝑤‘0)”〉) ↔ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸)) |
33 | | simpl 472 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) → 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸)) |
34 | | prmnn 15226 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
ℕ) |
35 | 34 | nnge1d 10940 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℙ → 1 ≤
𝑁) |
36 | 35 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → 1 ≤ 𝑁) |
37 | 36 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) → 1 ≤ 𝑁) |
38 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝑤) = 𝑁 → (1 ≤ (#‘𝑤) ↔ 1 ≤ 𝑁)) |
39 | 38 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝑤) = 𝑁) → (1 ≤ (#‘𝑤) ↔ 1 ≤ 𝑁)) |
40 | 39 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁)) → (1 ≤ (#‘𝑤) ↔ 1 ≤ 𝑁)) |
41 | 40 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) → (1 ≤
(#‘𝑤) ↔ 1 ≤
𝑁)) |
42 | 37, 41 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) → 1 ≤ (#‘𝑤)) |
43 | 17, 42 | jca 553 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) → (𝑤 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑤))) |
44 | 43 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁) → (𝑤 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑤))) |
45 | | clwlkswlks 26286 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) → 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 Walks 𝐸)) |
46 | | wlklenvclwlk 26366 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑤)) → (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 Walks 𝐸) → (#‘𝑓) = (#‘𝑤))) |
47 | 44, 45, 46 | syl2im 39 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁) → (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸) → (#‘𝑓) = (#‘𝑤))) |
48 | 47 | impcom 445 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) → (#‘𝑓) = (#‘𝑤)) |
49 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑓 ∈ V |
50 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ++ 〈“(𝑤‘0)”〉) ∈
V |
51 | 49, 50 | op1st 7067 |
. . . . . . . . . . . . . . . . . . 19
⊢
(1st ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) = 𝑓 |
52 | 51 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) → (1st
‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) =
𝑓) |
53 | 52 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) →
(#‘(1st ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) =
(#‘𝑓)) |
54 | 53 | ad2antrl 760 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) → (#‘(1st
‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))
= (#‘𝑓)) |
55 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑤) = 𝑁 ↔ 𝑁 = (#‘𝑤)) |
56 | 55 | biimpi 205 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑤) = 𝑁 → 𝑁 = (#‘𝑤)) |
57 | 56 | ad2antll 761 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) → 𝑁 = (#‘𝑤)) |
58 | 48, 54, 57 | 3eqtr4d 2654 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) → (#‘(1st
‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))
= 𝑁) |
59 | 1 | fveq2i 6106 |
. . . . . . . . . . . . . . . . . 18
⊢
(#‘𝐴) =
(#‘(1st ‘𝑐)) |
60 | 59 | eqeq1i 2615 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝐴) = 𝑁 ↔ (#‘(1st
‘𝑐)) = 𝑁) |
61 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
(1st ‘𝑐) =
(1st ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) |
62 | 61 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
(#‘(1st ‘𝑐)) = (#‘(1st
‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))) |
63 | 62 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
((#‘(1st ‘𝑐)) = 𝑁 ↔ (#‘(1st
‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))
= 𝑁)) |
64 | 60, 63 | syl5bb 271 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
((#‘𝐴) = 𝑁 ↔ (#‘(1st
‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))
= 𝑁)) |
65 | 64, 3 | elrab2 3333 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ 𝐶 ↔
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (#‘(1st
‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))
= 𝑁)) |
66 | 33, 58, 65 | sylanbrc 695 |
. . . . . . . . . . . . . 14
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) → 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ 𝐶) |
67 | 43, 45, 46 | syl2im 39 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) → (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸) → (#‘𝑓) = (#‘𝑤))) |
68 | 67 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) → (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸) → (#‘𝑓) = (#‘𝑤))) |
69 | 68 | imp 444 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) ∧ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸)) → (#‘𝑓) = (#‘𝑤)) |
70 | 69 | opeq2d 4347 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) ∧ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸)) → 〈0, (#‘𝑓)〉 = 〈0,
(#‘𝑤)〉) |
71 | 70 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) ∧ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸)) → ((𝑤 ++ 〈“(𝑤‘0)”〉) substr 〈0,
(#‘𝑓)〉) =
((𝑤 ++ 〈“(𝑤‘0)”〉) substr
〈0, (#‘𝑤)〉)) |
72 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) ∧ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸)) → 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸)) |
73 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 = (#‘𝑤) → ((#‘𝑓) = 𝑁 ↔ (#‘𝑓) = (#‘𝑤))) |
74 | 73 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝑤) = 𝑁 → ((#‘𝑓) = 𝑁 ↔ (#‘𝑓) = (#‘𝑤))) |
75 | 74 | imbi2d 329 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑤) = 𝑁 → ((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸) → (#‘𝑓) = 𝑁) ↔ (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸) → (#‘𝑓) = (#‘𝑤)))) |
76 | 75 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) → ((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸) → (#‘𝑓) = 𝑁) ↔ (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸) → (#‘𝑓) = (#‘𝑤)))) |
77 | 68, 76 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) → (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸) → (#‘𝑓) = 𝑁)) |
78 | 77 | imp 444 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) ∧ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸)) → (#‘𝑓) = 𝑁) |
79 | 51 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
(1st ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) = 𝑓) |
80 | 79 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
(#‘(1st ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) =
(#‘𝑓)) |
81 | 62, 80 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
(#‘(1st ‘𝑐)) = (#‘𝑓)) |
82 | 81 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
((#‘(1st ‘𝑐)) = 𝑁 ↔ (#‘𝑓) = 𝑁)) |
83 | 60, 82 | syl5bb 271 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
((#‘𝐴) = 𝑁 ↔ (#‘𝑓) = 𝑁)) |
84 | 83, 3 | elrab2 3333 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ 𝐶 ↔
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (#‘𝑓) = 𝑁)) |
85 | 72, 78, 84 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) ∧ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸)) → 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ 𝐶) |
86 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ++ 〈“(𝑤‘0)”〉) substr
〈0, (#‘𝑓)〉)
∈ V |
87 | 59 | opeq2i 4344 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 〈0,
(#‘𝐴)〉 =
〈0, (#‘(1st ‘𝑐))〉 |
88 | 2, 87 | oveq12i 6561 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 substr 〈0, (#‘𝐴)〉) = ((2nd
‘𝑐) substr 〈0,
(#‘(1st ‘𝑐))〉) |
89 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
(2nd ‘𝑐) =
(2nd ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) |
90 | 62 | opeq2d 4347 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 → 〈0,
(#‘(1st ‘𝑐))〉 = 〈0, (#‘(1st
‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))〉) |
91 | 89, 90 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
((2nd ‘𝑐)
substr 〈0, (#‘(1st ‘𝑐))〉) = ((2nd
‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)
substr 〈0, (#‘(1st ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))〉)) |
92 | 49, 50 | op2nd 7068 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(2nd ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) = (𝑤 ++ 〈“(𝑤‘0)”〉) |
93 | 51 | fveq2i 6106 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(#‘(1st ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) =
(#‘𝑓) |
94 | 93 | opeq2i 4344 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 〈0,
(#‘(1st ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))〉 =
〈0, (#‘𝑓)〉 |
95 | 92, 94 | oveq12i 6561 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((2nd ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) substr
〈0, (#‘(1st ‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))〉) =
((𝑤 ++ 〈“(𝑤‘0)”〉) substr
〈0, (#‘𝑓)〉) |
96 | 91, 95 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
((2nd ‘𝑐)
substr 〈0, (#‘(1st ‘𝑐))〉) = ((𝑤 ++ 〈“(𝑤‘0)”〉) substr 〈0,
(#‘𝑓)〉)) |
97 | 88, 96 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 → (𝐵 substr 〈0, (#‘𝐴)〉) = ((𝑤 ++ 〈“(𝑤‘0)”〉) substr 〈0,
(#‘𝑓)〉)) |
98 | 97, 4 | fvmptg 6189 |
. . . . . . . . . . . . . . . . . . 19
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ 𝐶 ∧ ((𝑤 ++ 〈“(𝑤‘0)”〉) substr
〈0, (#‘𝑓)〉)
∈ V) → (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) = ((𝑤 ++ 〈“(𝑤‘0)”〉) substr
〈0, (#‘𝑓)〉)) |
99 | 85, 86, 98 | sylancl 693 |
. . . . . . . . . . . . . . . . . 18
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) ∧ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸)) → (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) = ((𝑤 ++ 〈“(𝑤‘0)”〉) substr
〈0, (#‘𝑓)〉)) |
100 | 43 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) → (𝑤 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑤))) |
101 | 100 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) ∧ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸)) → (𝑤 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑤))) |
102 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑤 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑤)) → 𝑤 ∈ Word 𝑉) |
103 | | wrdsymb1 13197 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑤 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑤)) → (𝑤‘0) ∈ 𝑉) |
104 | 103 | s1cld 13236 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑤 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑤)) → 〈“(𝑤‘0)”〉 ∈ Word 𝑉) |
105 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑤 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑤)) → (#‘𝑤) = (#‘𝑤)) |
106 | | swrdccatid 13348 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑤 ∈ Word 𝑉 ∧ 〈“(𝑤‘0)”〉 ∈ Word 𝑉 ∧ (#‘𝑤) = (#‘𝑤)) → ((𝑤 ++ 〈“(𝑤‘0)”〉) substr 〈0,
(#‘𝑤)〉) = 𝑤) |
107 | 102, 104,
105, 106 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑤 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑤)) → ((𝑤 ++ 〈“(𝑤‘0)”〉) substr 〈0,
(#‘𝑤)〉) = 𝑤) |
108 | 107 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑤)) → 𝑤 = ((𝑤 ++ 〈“(𝑤‘0)”〉) substr 〈0,
(#‘𝑤)〉)) |
109 | 101, 108 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) ∧ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸)) → 𝑤 = ((𝑤 ++ 〈“(𝑤‘0)”〉) substr 〈0,
(#‘𝑤)〉)) |
110 | 71, 99, 109 | 3eqtr4rd 2655 |
. . . . . . . . . . . . . . . . 17
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) ∧ 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸)) → 𝑤 = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) |
111 | 110 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) → (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸) → 𝑤 = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))) |
112 | 111 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) ∧ 𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) →
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) → 𝑤 = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))) |
113 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 → (𝐹‘𝑐) = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)) |
114 | 113 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 → (𝑤 = (𝐹‘𝑐) ↔ 𝑤 = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉))) |
115 | 114 | imbi2d 329 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 →
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) → 𝑤 = (𝐹‘𝑐)) ↔ (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸) → 𝑤 = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)))) |
116 | 115 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) ∧ 𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) →
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) → 𝑤 = (𝐹‘𝑐)) ↔ (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸) → 𝑤 = (𝐹‘〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉)))) |
117 | 112, 116 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢
(((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) ∧ 𝑐 = 〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉) →
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) → 𝑤 = (𝐹‘𝑐))) |
118 | 66, 117 | rspcimedv 3284 |
. . . . . . . . . . . . 13
⊢
((〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) ∧ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁)) → (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
119 | 118 | ex 449 |
. . . . . . . . . . . 12
⊢
(〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉
∈ (𝑉 ClWalks 𝐸) → ((((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁) → (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐)))) |
120 | 119 | pm2.43b 53 |
. . . . . . . . . . 11
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁) → (〈𝑓, (𝑤 ++ 〈“(𝑤‘0)”〉)〉 ∈ (𝑉 ClWalks 𝐸) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
121 | 32, 120 | syl5bi 231 |
. . . . . . . . . 10
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁) → (𝑓(𝑉 ClWalks 𝐸)(𝑤 ++ 〈“(𝑤‘0)”〉) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
122 | 121 | exlimdv 1848 |
. . . . . . . . 9
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) ∧ (#‘𝑤) = 𝑁) → (∃𝑓 𝑓(𝑉 ClWalks 𝐸)(𝑤 ++ 〈“(𝑤‘0)”〉) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
123 | 122 | ex 449 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) → ((#‘𝑤) = 𝑁 → (∃𝑓 𝑓(𝑉 ClWalks 𝐸)(𝑤 ++ 〈“(𝑤‘0)”〉) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐)))) |
124 | 123 | com23 84 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) → (∃𝑓 𝑓(𝑉 ClWalks 𝐸)(𝑤 ++ 〈“(𝑤‘0)”〉) →
((#‘𝑤) = 𝑁 → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐)))) |
125 | 124 | impd 446 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) → ((∃𝑓 𝑓(𝑉 ClWalks 𝐸)(𝑤 ++ 〈“(𝑤‘0)”〉) ∧ (#‘𝑤) = 𝑁) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
126 | 31, 125 | sylbid 229 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁))) → (𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
127 | 126 | impancom 455 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑤 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑤) = 𝑁)) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
128 | 7, 127 | mpd 15 |
. . 3
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ 𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → ∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐)) |
129 | 128 | ralrimiva 2949 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → ∀𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐)) |
130 | | dffo3 6282 |
. 2
⊢ (𝐹:𝐶–onto→((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (𝐹:𝐶⟶((𝑉 ClWWalksN 𝐸)‘𝑁) ∧ ∀𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)∃𝑐 ∈ 𝐶 𝑤 = (𝐹‘𝑐))) |
131 | 5, 129, 130 | sylanbrc 695 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶–onto→((𝑉 ClWWalksN 𝐸)‘𝑁)) |