Step | Hyp | Ref
| Expression |
1 | | clwlksfclwwlk.1 |
. . 3
⊢ 𝐴 = (1st ‘𝑐) |
2 | | clwlksfclwwlk.2 |
. . 3
⊢ 𝐵 = (2nd ‘𝑐) |
3 | | clwlksfclwwlk.c |
. . 3
⊢ 𝐶 = {𝑐 ∈ (ClWalkS‘𝐺) ∣ (#‘𝐴) = 𝑁} |
4 | | clwlksfclwwlk.f |
. . 3
⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) |
5 | 1, 2, 3, 4 | clwlksfclwwlk 41269 |
. 2
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶⟶(𝑁 ClWWalkSN 𝐺)) |
6 | | simprl 790 |
. . . . . 6
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) → 𝑢 ∈ 𝐶) |
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
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) → (𝐹‘𝑢) = ((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
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) → (𝑤 ∈ 𝐶 ∧ ((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
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) → (𝐹‘𝑤) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉)) |
30 | 16, 29 | eqeq12d 2625 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) → ((𝐹‘𝑢) = (𝐹‘𝑤) ↔ ((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉))) |
31 | 1, 2, 3, 4 | clwlksfclwwlk1hashn 41266 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝐶 → (#‘(1st
‘𝑤)) = 𝑁) |
32 | 31 | eqcomd 2616 |
. . . . . . . 8
⊢ (𝑤 ∈ 𝐶 → 𝑁 = (#‘(1st ‘𝑤))) |
33 | 32 | adantl 481 |
. . . . . . 7
⊢ ((𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶) → 𝑁 = (#‘(1st ‘𝑤))) |
34 | 33 | ad2antlr 759 |
. . . . . 6
⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) ∧ ((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉)) → 𝑁 = (#‘(1st ‘𝑤))) |
35 | | prmnn 15226 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
ℕ) |
36 | 35 | ad2antlr 759 |
. . . . . . . 8
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) → 𝑁 ∈ ℕ) |
37 | 17 | adantl 481 |
. . . . . . . 8
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) → 𝑤 ∈ 𝐶) |
38 | 1, 2, 3, 4 | clwlksf1clwwlklem 41275 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶) → (((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉) → ∀𝑖 ∈ (0...𝑁)((2nd ‘𝑢)‘𝑖) = ((2nd ‘𝑤)‘𝑖))) |
39 | 36, 6, 37, 38 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) → (((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉) → ∀𝑖 ∈ (0...𝑁)((2nd ‘𝑢)‘𝑖) = ((2nd ‘𝑤)‘𝑖))) |
40 | 39 | imp 444 |
. . . . . 6
⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) ∧ ((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉)) → ∀𝑖 ∈ (0...𝑁)((2nd ‘𝑢)‘𝑖) = ((2nd ‘𝑤)‘𝑖)) |
41 | | fusgrusgr 40541 |
. . . . . . . . 9
⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph
) |
42 | | usgruspgr 40408 |
. . . . . . . . 9
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ USPGraph
) |
43 | 41, 42 | syl 17 |
. . . . . . . 8
⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈ USPGraph
) |
44 | 43 | ad3antrrr 762 |
. . . . . . 7
⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) ∧ ((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉)) → 𝐺 ∈ USPGraph ) |
45 | | elrabi 3328 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ {𝑐 ∈ (ClWalkS‘𝐺) ∣ (#‘𝐴) = 𝑁} → 𝑢 ∈ (ClWalkS‘𝐺)) |
46 | | clwlk1wlk 40982 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ (ClWalkS‘𝐺) → 𝑢 ∈ (1Walks‘𝐺)) |
47 | 45, 46 | syl 17 |
. . . . . . . . . 10
⊢ (𝑢 ∈ {𝑐 ∈ (ClWalkS‘𝐺) ∣ (#‘𝐴) = 𝑁} → 𝑢 ∈ (1Walks‘𝐺)) |
48 | 47, 3 | eleq2s 2706 |
. . . . . . . . 9
⊢ (𝑢 ∈ 𝐶 → 𝑢 ∈ (1Walks‘𝐺)) |
49 | | elrabi 3328 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ {𝑐 ∈ (ClWalkS‘𝐺) ∣ (#‘𝐴) = 𝑁} → 𝑤 ∈ (ClWalkS‘𝐺)) |
50 | | clwlk1wlk 40982 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ (ClWalkS‘𝐺) → 𝑤 ∈ (1Walks‘𝐺)) |
51 | 49, 50 | syl 17 |
. . . . . . . . . 10
⊢ (𝑤 ∈ {𝑐 ∈ (ClWalkS‘𝐺) ∣ (#‘𝐴) = 𝑁} → 𝑤 ∈ (1Walks‘𝐺)) |
52 | 51, 3 | eleq2s 2706 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝐶 → 𝑤 ∈ (1Walks‘𝐺)) |
53 | 48, 52 | anim12i 588 |
. . . . . . . 8
⊢ ((𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶) → (𝑢 ∈ (1Walks‘𝐺) ∧ 𝑤 ∈ (1Walks‘𝐺))) |
54 | 53 | ad2antlr 759 |
. . . . . . 7
⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) ∧ ((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉)) → (𝑢 ∈ (1Walks‘𝐺) ∧ 𝑤 ∈ (1Walks‘𝐺))) |
55 | 1, 2, 3, 4 | clwlksfclwwlk1hashn 41266 |
. . . . . . . . . 10
⊢ (𝑢 ∈ 𝐶 → (#‘(1st
‘𝑢)) = 𝑁) |
56 | 55 | eqcomd 2616 |
. . . . . . . . 9
⊢ (𝑢 ∈ 𝐶 → 𝑁 = (#‘(1st ‘𝑢))) |
57 | 56 | adantr 480 |
. . . . . . . 8
⊢ ((𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶) → 𝑁 = (#‘(1st ‘𝑢))) |
58 | 57 | ad2antlr 759 |
. . . . . . 7
⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) ∧ ((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉)) → 𝑁 = (#‘(1st ‘𝑢))) |
59 | | uspgr2wlkeq 40854 |
. . . . . . 7
⊢ ((𝐺 ∈ USPGraph ∧ (𝑢 ∈ (1Walks‘𝐺) ∧ 𝑤 ∈ (1Walks‘𝐺)) ∧ 𝑁 = (#‘(1st ‘𝑢))) → (𝑢 = 𝑤 ↔ (𝑁 = (#‘(1st ‘𝑤)) ∧ ∀𝑖 ∈ (0...𝑁)((2nd ‘𝑢)‘𝑖) = ((2nd ‘𝑤)‘𝑖)))) |
60 | 44, 54, 58, 59 | syl3anc 1318 |
. . . . . 6
⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) ∧ ((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉)) → (𝑢 = 𝑤 ↔ (𝑁 = (#‘(1st ‘𝑤)) ∧ ∀𝑖 ∈ (0...𝑁)((2nd ‘𝑢)‘𝑖) = ((2nd ‘𝑤)‘𝑖)))) |
61 | 34, 40, 60 | mpbir2and 959 |
. . . . 5
⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) ∧ ((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉)) → 𝑢 = 𝑤) |
62 | 61 | ex 449 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) → (((2nd ‘𝑢) substr 〈0,
(#‘(1st ‘𝑢))〉) = ((2nd ‘𝑤) substr 〈0,
(#‘(1st ‘𝑤))〉) → 𝑢 = 𝑤)) |
63 | 30, 62 | sylbid 229 |
. . 3
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ (𝑢 ∈ 𝐶 ∧ 𝑤 ∈ 𝐶)) → ((𝐹‘𝑢) = (𝐹‘𝑤) → 𝑢 = 𝑤)) |
64 | 63 | ralrimivva 2954 |
. 2
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) →
∀𝑢 ∈ 𝐶 ∀𝑤 ∈ 𝐶 ((𝐹‘𝑢) = (𝐹‘𝑤) → 𝑢 = 𝑤)) |
65 | | dff13 6416 |
. 2
⊢ (𝐹:𝐶–1-1→(𝑁 ClWWalkSN 𝐺) ↔ (𝐹:𝐶⟶(𝑁 ClWWalkSN 𝐺) ∧ ∀𝑢 ∈ 𝐶 ∀𝑤 ∈ 𝐶 ((𝐹‘𝑢) = (𝐹‘𝑤) → 𝑢 = 𝑤))) |
66 | 5, 64, 65 | sylanbrc 695 |
1
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶–1-1→(𝑁 ClWWalkSN 𝐺)) |