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 | | simprl 790 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) → 𝑢 ∈ 𝐶) |
7 | | ovex 6577 |
. . . . . 6
⊢
((2nd ‘𝑢) substr 〈0, (#‘(1st
‘𝑢))〉) ∈
V |
8 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑐 = 𝑢 → (2nd ‘𝑐) = (2nd ‘𝑢)) |
9 | 2, 8 | syl5eq 2656 |
. . . . . . . 8
⊢ (𝑐 = 𝑢 → 𝐵 = (2nd ‘𝑢)) |
10 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑢 → (1st ‘𝑐) = (1st ‘𝑢)) |
11 | 1, 10 | syl5eq 2656 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑢 → 𝐴 = (1st ‘𝑢)) |
12 | 11 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑐 = 𝑢 → (#‘𝐴) = (#‘(1st ‘𝑢))) |
13 | 12 | opeq2d 4347 |
. . . . . . . 8
⊢ (𝑐 = 𝑢 → 〈0, (#‘𝐴)〉 = 〈0, (#‘(1st
‘𝑢))〉) |
14 | 9, 13 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑐 = 𝑢 → (𝐵 substr 〈0, (#‘𝐴)〉) = ((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉)) |
15 | 14, 4 | fvmptg 6189 |
. . . . . 6
⊢ ((𝑢 ∈ 𝐶 ∧ ((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉) ∈ V) → (𝐹‘𝑢) = ((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉)) |
16 | 6, 7, 15 | sylancl 693 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) → (𝐹‘𝑢) = ((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉)) |
17 | | simpr 476 |
. . . . . . . 8
⊢ ((𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶) → 𝑤 ∈ 𝐶) |
18 | | ovex 6577 |
. . . . . . . 8
⊢
((2nd ‘𝑤) substr 〈0, (#‘(1st
‘𝑤))〉) ∈
V |
19 | 17, 18 | jctir 559 |
. . . . . . 7
⊢ ((𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶) → (𝑤 ∈ 𝐶 ∧ ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉) ∈ V)) |
20 | 19 | adantl 481 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) → (𝑤 ∈ 𝐶 ∧ ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉) ∈ V)) |
21 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑐 = 𝑤 → (2nd ‘𝑐) = (2nd ‘𝑤)) |
22 | 2, 21 | syl5eq 2656 |
. . . . . . . 8
⊢ (𝑐 = 𝑤 → 𝐵 = (2nd ‘𝑤)) |
23 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑤 → (1st ‘𝑐) = (1st ‘𝑤)) |
24 | 1, 23 | syl5eq 2656 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑤 → 𝐴 = (1st ‘𝑤)) |
25 | 24 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑐 = 𝑤 → (#‘𝐴) = (#‘(1st ‘𝑤))) |
26 | 25 | opeq2d 4347 |
. . . . . . . 8
⊢ (𝑐 = 𝑤 → 〈0, (#‘𝐴)〉 = 〈0, (#‘(1st
‘𝑤))〉) |
27 | 22, 26 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑐 = 𝑤 → (𝐵 substr 〈0, (#‘𝐴)〉) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉)) |
28 | 27, 4 | fvmptg 6189 |
. . . . . 6
⊢ ((𝑤 ∈ 𝐶 ∧ ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉) ∈ V) → (𝐹‘𝑤) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉)) |
29 | 20, 28 | syl 17 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) → (𝐹‘𝑤) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉)) |
30 | 16, 29 | eqeq12d 2625 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) → ((𝐹‘𝑢) = (𝐹‘𝑤) ↔ ((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉))) |
31 | 1, 2, 3, 4 | clwlkfclwwlk1hashn 26368 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝐶 → (#‘(1st
‘𝑤)) = 𝑁) |
32 | 31 | eqcomd 2616 |
. . . . . . . 8
⊢ (𝑤 ∈ 𝐶 → 𝑁 = (#‘(1st ‘𝑤))) |
33 | 32 | adantl 481 |
. . . . . . 7
⊢ ((𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶) → 𝑁 = (#‘(1st ‘𝑤))) |
34 | 33 | ad2antlr 759 |
. . . . . 6
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) ∧ ((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉)) → 𝑁 = (#‘(1st ‘𝑤))) |
35 | | prmnn 15226 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
ℕ) |
36 | 35 | 3ad2ant3 1077 |
. . . . . . . . 9
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → 𝑁 ∈ ℕ) |
37 | 36 | adantr 480 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) → 𝑁 ∈ ℕ) |
38 | 17 | adantl 481 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) → 𝑤 ∈ 𝐶) |
39 | 1, 2, 3, 4 | clwlkf1clwwlklem 26376 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶) → (((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉) → ∀𝑖 ∈ (0...𝑁)((2nd ‘𝑢)‘𝑖) = ((2nd ‘𝑤)‘𝑖))) |
40 | 37, 6, 38, 39 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) → (((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉) → ∀𝑖 ∈ (0...𝑁)((2nd ‘𝑢)‘𝑖) = ((2nd ‘𝑤)‘𝑖))) |
41 | 40 | imp 444 |
. . . . . 6
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) ∧ ((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉)) → ∀𝑖 ∈ (0...𝑁)((2nd ‘𝑢)‘𝑖) = ((2nd ‘𝑤)‘𝑖)) |
42 | | simpll1 1093 |
. . . . . . 7
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) ∧ ((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉)) → 𝑉 USGrph 𝐸) |
43 | | elrabi 3328 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ {𝑐 ∈ (𝑉 ClWalks 𝐸) ∣ (#‘𝐴) = 𝑁} → 𝑢 ∈ (𝑉 ClWalks 𝐸)) |
44 | | clwlkswlks 26286 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (𝑉 ClWalks 𝐸) → 𝑢 ∈ (𝑉 Walks 𝐸)) |
45 | 43, 44 | syl 17 |
. . . . . . . . . 10
⊢ (𝑢 ∈ {𝑐 ∈ (𝑉 ClWalks 𝐸) ∣ (#‘𝐴) = 𝑁} → 𝑢 ∈ (𝑉 Walks 𝐸)) |
46 | 45, 3 | eleq2s 2706 |
. . . . . . . . 9
⊢ (𝑢 ∈ 𝐶 → 𝑢 ∈ (𝑉 Walks 𝐸)) |
47 | | elrabi 3328 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ {𝑐 ∈ (𝑉 ClWalks 𝐸) ∣ (#‘𝐴) = 𝑁} → 𝑤 ∈ (𝑉 ClWalks 𝐸)) |
48 | | clwlkswlks 26286 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ (𝑉 ClWalks 𝐸) → 𝑤 ∈ (𝑉 Walks 𝐸)) |
49 | 47, 48 | syl 17 |
. . . . . . . . . 10
⊢ (𝑤 ∈ {𝑐 ∈ (𝑉 ClWalks 𝐸) ∣ (#‘𝐴) = 𝑁} → 𝑤 ∈ (𝑉 Walks 𝐸)) |
50 | 49, 3 | eleq2s 2706 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝐶 → 𝑤 ∈ (𝑉 Walks 𝐸)) |
51 | 46, 50 | anim12i 588 |
. . . . . . . 8
⊢ ((𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶) → (𝑢 ∈ (𝑉 Walks 𝐸) ∧ 𝑤 ∈ (𝑉 Walks 𝐸))) |
52 | 51 | ad2antlr 759 |
. . . . . . 7
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) ∧ ((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉)) → (𝑢 ∈ (𝑉 Walks 𝐸) ∧ 𝑤 ∈ (𝑉 Walks 𝐸))) |
53 | 1, 2, 3, 4 | clwlkfclwwlk1hashn 26368 |
. . . . . . . . . 10
⊢ (𝑢 ∈ 𝐶 → (#‘(1st
‘𝑢)) = 𝑁) |
54 | 53 | eqcomd 2616 |
. . . . . . . . 9
⊢ (𝑢 ∈ 𝐶 → 𝑁 = (#‘(1st ‘𝑢))) |
55 | 54 | adantr 480 |
. . . . . . . 8
⊢ ((𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶) → 𝑁 = (#‘(1st ‘𝑢))) |
56 | 55 | ad2antlr 759 |
. . . . . . 7
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) ∧ ((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉)) → 𝑁 = (#‘(1st ‘𝑢))) |
57 | | usg2wlkeq 26236 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ (𝑢 ∈ (𝑉 Walks 𝐸) ∧ 𝑤 ∈ (𝑉 Walks 𝐸)) ∧ 𝑁 = (#‘(1st ‘𝑢))) → (𝑢 = 𝑤 ↔ (𝑁 = (#‘(1st ‘𝑤)) ∧ ∀𝑖 ∈ (0...𝑁)((2nd ‘𝑢)‘𝑖) = ((2nd ‘𝑤)‘𝑖)))) |
58 | 42, 52, 56, 57 | syl3anc 1318 |
. . . . . 6
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) ∧ ((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉)) → (𝑢 = 𝑤 ↔ (𝑁 = (#‘(1st ‘𝑤)) ∧ ∀𝑖 ∈ (0...𝑁)((2nd ‘𝑢)‘𝑖) = ((2nd ‘𝑤)‘𝑖)))) |
59 | 34, 41, 58 | mpbir2and 959 |
. . . . 5
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) ∧ ((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉)) → 𝑢 = 𝑤) |
60 | 59 | ex 449 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) → (((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉) → 𝑢 = 𝑤)) |
61 | 30, 60 | sylbid 229 |
. . 3
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) → ((𝐹‘𝑢) = (𝐹‘𝑤) → 𝑢 = 𝑤)) |
62 | 61 | ralrimivva 2954 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → ∀𝑢 ∈ 𝐶 ∀𝑤 ∈ 𝐶 ((𝐹‘𝑢) = (𝐹‘𝑤) → 𝑢 = 𝑤)) |
63 | | dff13 6416 |
. 2
⊢ (𝐹:𝐶–1-1→((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (𝐹:𝐶⟶((𝑉 ClWWalksN 𝐸)‘𝑁) ∧ ∀𝑢 ∈ 𝐶 ∀𝑤 ∈ 𝐶 ((𝐹‘𝑢) = (𝐹‘𝑤) → 𝑢 = 𝑤))) |
64 | 5, 62, 63 | sylanbrc 695 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶–1-1→((𝑉 ClWWalksN 𝐸)‘𝑁)) |