Step | Hyp | Ref
| Expression |
1 | | clwlksfclwwlk.c |
. . . . . 6
⊢ 𝐶 = {𝑐 ∈ (ClWalks‘𝐺) ∣ (♯‘𝐴) = 𝑁} |
2 | 1 | rabeq2i 3347 |
. . . . 5
⊢ (𝑐 ∈ 𝐶 ↔ (𝑐 ∈ (ClWalks‘𝐺) ∧ (♯‘𝐴) = 𝑁)) |
3 | | fusgrusgr 26437 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈
USGraph) |
4 | | usgrupgr 26299 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
UPGraph) |
5 | 3, 4 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈
UPGraph) |
6 | 5 | adantr 466 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐺 ∈
UPGraph) |
7 | | eqid 2771 |
. . . . . . . . . . 11
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
8 | | eqid 2771 |
. . . . . . . . . . 11
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
9 | | clwlksfclwwlk.1 |
. . . . . . . . . . 11
⊢ 𝐴 = (1st ‘𝑐) |
10 | | clwlksfclwwlk.2 |
. . . . . . . . . . 11
⊢ 𝐵 = (2nd ‘𝑐) |
11 | 7, 8, 9, 10 | upgrclwlkcompim 26912 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UPGraph ∧ 𝑐 ∈ (ClWalks‘𝐺)) → ((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) |
12 | 6, 11 | sylan 569 |
. . . . . . . . 9
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ (ClWalks‘𝐺)) → ((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) |
13 | | lencl 13520 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ Word dom
(iEdg‘𝐺) →
(♯‘𝐴) ∈
ℕ0) |
14 | | clwlksfclwwlk.f |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (♯‘𝐴)〉)) |
15 | 9, 10, 1, 14 | clwlksfclwwlk2wrdOLD 27239 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 ∈ 𝐶 → 𝐵 ∈ Word (Vtx‘𝐺)) |
16 | 15 | ad2antlr 706 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵 ∈ Word (Vtx‘𝐺)) |
17 | | swrdcl 13627 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐵 ∈ Word (Vtx‘𝐺) → (𝐵 substr 〈0, (♯‘𝐴)〉) ∈ Word
(Vtx‘𝐺)) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr 〈0, (♯‘𝐴)〉) ∈ Word
(Vtx‘𝐺)) |
19 | | ffz0iswrd 13528 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → 𝐵 ∈ Word (Vtx‘𝐺)) |
20 | 19 | 3ad2ant1 1127 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵 ∈ Word (Vtx‘𝐺)) |
21 | | prmnn 15595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
ℕ) |
22 | 21 | adantl 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ∈
ℕ) |
23 | 22 | 3ad2ant3 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝑁 ∈ ℕ) |
24 | | oveq2 6801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((♯‘𝐴) =
𝑁 →
(0...(♯‘𝐴)) =
(0...𝑁)) |
25 | 24 | feq2d 6171 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((♯‘𝐴) =
𝑁 → (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ↔ 𝐵:(0...𝑁)⟶(Vtx‘𝐺))) |
26 | 22 | nnnn0d 11553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ∈
ℕ0) |
27 | | ffz0hash 13433 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑁 ∈ ℕ0
∧ 𝐵:(0...𝑁)⟶(Vtx‘𝐺)) → (♯‘𝐵) = (𝑁 + 1)) |
28 | 26, 27 | sylan 569 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝐵:(0...𝑁)⟶(Vtx‘𝐺)) → (♯‘𝐵) = (𝑁 + 1)) |
29 | 28 | ex 397 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵:(0...𝑁)⟶(Vtx‘𝐺) → (♯‘𝐵) = (𝑁 + 1))) |
30 | 21 | nnred 11237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
ℝ) |
31 | 30 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑁 ∈ ℙ ∧
(♯‘𝐵) = (𝑁 + 1)) → 𝑁 ∈ ℝ) |
32 | 31 | lep1d 11157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑁 ∈ ℙ ∧
(♯‘𝐵) = (𝑁 + 1)) → 𝑁 ≤ (𝑁 + 1)) |
33 | | breq2 4790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((♯‘𝐵) =
(𝑁 + 1) → (𝑁 ≤ (♯‘𝐵) ↔ 𝑁 ≤ (𝑁 + 1))) |
34 | 33 | adantl 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑁 ∈ ℙ ∧
(♯‘𝐵) = (𝑁 + 1)) → (𝑁 ≤ (♯‘𝐵) ↔ 𝑁 ≤ (𝑁 + 1))) |
35 | 32, 34 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑁 ∈ ℙ ∧
(♯‘𝐵) = (𝑁 + 1)) → 𝑁 ≤ (♯‘𝐵)) |
36 | 35 | ex 397 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈ ℙ →
((♯‘𝐵) = (𝑁 + 1) → 𝑁 ≤ (♯‘𝐵))) |
37 | 36 | adantl 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) →
((♯‘𝐵) = (𝑁 + 1) → 𝑁 ≤ (♯‘𝐵))) |
38 | 29, 37 | syldc 48 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐵:(0...𝑁)⟶(Vtx‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ≤ (♯‘𝐵))) |
39 | 25, 38 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((♯‘𝐴) =
𝑁 → (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ≤ (♯‘𝐵)))) |
40 | 39 | 3imp21 1105 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝑁 ≤ (♯‘𝐵)) |
41 | | swrdn0 13639 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ (♯‘𝐵)) → (𝐵 substr 〈0, 𝑁〉) ≠ ∅) |
42 | 20, 23, 40, 41 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr 〈0, 𝑁〉) ≠ ∅) |
43 | | opeq2 4540 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((♯‘𝐴) =
𝑁 → 〈0,
(♯‘𝐴)〉 =
〈0, 𝑁〉) |
44 | 43 | oveq2d 6809 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((♯‘𝐴) =
𝑁 → (𝐵 substr 〈0, (♯‘𝐴)〉) = (𝐵 substr 〈0, 𝑁〉)) |
45 | 44 | neeq1d 3002 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((♯‘𝐴) =
𝑁 → ((𝐵 substr 〈0,
(♯‘𝐴)〉)
≠ ∅ ↔ (𝐵
substr 〈0, 𝑁〉)
≠ ∅)) |
46 | 45 | 3ad2ant2 1128 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr 〈0, (♯‘𝐴)〉) ≠ ∅ ↔
(𝐵 substr 〈0, 𝑁〉) ≠
∅)) |
47 | 42, 46 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ (♯‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr 〈0, (♯‘𝐴)〉) ≠
∅) |
48 | 47 | 3exp 1112 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → ((♯‘𝐴) = 𝑁 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (♯‘𝐴)〉) ≠
∅))) |
49 | 48 | ad2antlr 706 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) → ((♯‘𝐴) = 𝑁 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (♯‘𝐴)〉) ≠
∅))) |
50 | 49 | imp 393 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (♯‘𝐴)〉) ≠
∅)) |
51 | 50 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (♯‘𝐴)〉) ≠
∅)) |
52 | 51 | imp 393 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr 〈0, (♯‘𝐴)〉) ≠
∅) |
53 | 18, 52 | jca 501 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr 〈0, (♯‘𝐴)〉) ∈ Word
(Vtx‘𝐺) ∧ (𝐵 substr 〈0,
(♯‘𝐴)〉)
≠ ∅)) |
54 | | simp-5r 774 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → 𝐴 ∈ Word dom (iEdg‘𝐺)) |
55 | 3 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐺 ∈
USGraph) |
56 | 54, 55 | anim12ci 601 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom (iEdg‘𝐺))) |
57 | | simp-5r 774 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) |
58 | | prmuz2 15615 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
(ℤ≥‘2)) |
59 | | ffz0hash 13433 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) → (♯‘𝐵) = ((♯‘𝐴) + 1)) |
60 | 59 | adantlr 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((♯‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) → (♯‘𝐵) = ((♯‘𝐴) + 1)) |
61 | | eluz2 11894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((♯‘𝐴)
∈ (ℤ≥‘2) ↔ (2 ∈ ℤ ∧
(♯‘𝐴) ∈
ℤ ∧ 2 ≤ (♯‘𝐴))) |
62 | | 2re 11292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ 2 ∈
ℝ |
63 | 62 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((♯‘𝐴)
∈ ℤ → 2 ∈ ℝ) |
64 | | zre 11583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((♯‘𝐴)
∈ ℤ → (♯‘𝐴) ∈ ℝ) |
65 | | peano2re 10411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((♯‘𝐴)
∈ ℝ → ((♯‘𝐴) + 1) ∈ ℝ) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((♯‘𝐴)
∈ ℤ → ((♯‘𝐴) + 1) ∈ ℝ) |
67 | 63, 64, 66 | 3jca 1122 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((♯‘𝐴)
∈ ℤ → (2 ∈ ℝ ∧ (♯‘𝐴) ∈ ℝ ∧ ((♯‘𝐴) + 1) ∈
ℝ)) |
68 | 67 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((♯‘𝐴)
∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → (2 ∈ ℝ ∧
(♯‘𝐴) ∈
ℝ ∧ ((♯‘𝐴) + 1) ∈ ℝ)) |
69 | | simpr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((♯‘𝐴)
∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → 2 ≤ (♯‘𝐴)) |
70 | 64 | lep1d 11157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((♯‘𝐴)
∈ ℤ → (♯‘𝐴) ≤ ((♯‘𝐴) + 1)) |
71 | 70 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((♯‘𝐴)
∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → (♯‘𝐴) ≤ ((♯‘𝐴) + 1)) |
72 | | letr 10333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((2
∈ ℝ ∧ (♯‘𝐴) ∈ ℝ ∧ ((♯‘𝐴) + 1) ∈ ℝ) →
((2 ≤ (♯‘𝐴)
∧ (♯‘𝐴)
≤ ((♯‘𝐴) +
1)) → 2 ≤ ((♯‘𝐴) + 1))) |
73 | 72 | imp 393 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((2
∈ ℝ ∧ (♯‘𝐴) ∈ ℝ ∧ ((♯‘𝐴) + 1) ∈ ℝ) ∧ (2
≤ (♯‘𝐴)
∧ (♯‘𝐴)
≤ ((♯‘𝐴) +
1))) → 2 ≤ ((♯‘𝐴) + 1)) |
74 | 68, 69, 71, 73 | syl12anc 1474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((♯‘𝐴)
∈ ℤ ∧ 2 ≤ (♯‘𝐴)) → 2 ≤ ((♯‘𝐴) + 1)) |
75 | 74 | 3adant1 1124 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((2
∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 2 ≤
(♯‘𝐴)) → 2
≤ ((♯‘𝐴) +
1)) |
76 | 61, 75 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((♯‘𝐴)
∈ (ℤ≥‘2) → 2 ≤ ((♯‘𝐴) + 1)) |
77 | 76 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((♯‘𝐵)
= ((♯‘𝐴) + 1)
∧ (♯‘𝐴) =
𝑁) →
((♯‘𝐴) ∈
(ℤ≥‘2) → 2 ≤ ((♯‘𝐴) + 1))) |
78 | | eleq1 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 = (♯‘𝐴) → (𝑁 ∈ (ℤ≥‘2)
↔ (♯‘𝐴)
∈ (ℤ≥‘2))) |
79 | 78 | eqcoms 2779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((♯‘𝐴) =
𝑁 → (𝑁 ∈ (ℤ≥‘2)
↔ (♯‘𝐴)
∈ (ℤ≥‘2))) |
80 | 79 | adantl 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((♯‘𝐵)
= ((♯‘𝐴) + 1)
∧ (♯‘𝐴) =
𝑁) → (𝑁 ∈
(ℤ≥‘2) ↔ (♯‘𝐴) ∈
(ℤ≥‘2))) |
81 | | breq2 4790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((♯‘𝐵) =
((♯‘𝐴) + 1)
→ (2 ≤ (♯‘𝐵) ↔ 2 ≤ ((♯‘𝐴) + 1))) |
82 | 81 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((♯‘𝐵)
= ((♯‘𝐴) + 1)
∧ (♯‘𝐴) =
𝑁) → (2 ≤
(♯‘𝐵) ↔ 2
≤ ((♯‘𝐴) +
1))) |
83 | 77, 80, 82 | 3imtr4d 283 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((♯‘𝐵)
= ((♯‘𝐴) + 1)
∧ (♯‘𝐴) =
𝑁) → (𝑁 ∈
(ℤ≥‘2) → 2 ≤ (♯‘𝐵))) |
84 | 83 | ex 397 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((♯‘𝐵) =
((♯‘𝐴) + 1)
→ ((♯‘𝐴) =
𝑁 → (𝑁 ∈ (ℤ≥‘2)
→ 2 ≤ (♯‘𝐵)))) |
85 | 60, 84 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((♯‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) → ((♯‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ≥‘2)
→ 2 ≤ (♯‘𝐵)))) |
86 | 85 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) → ((♯‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ≥‘2)
→ 2 ≤ (♯‘𝐵)))) |
87 | 86 | imp 393 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ≥‘2)
→ 2 ≤ (♯‘𝐵))) |
88 | 87 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → (𝑁 ∈ (ℤ≥‘2)
→ 2 ≤ (♯‘𝐵))) |
89 | 58, 88 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℙ →
(((((((♯‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → 2 ≤ (♯‘𝐵))) |
90 | 89 | adantl 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) →
(((((((♯‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → 2 ≤ (♯‘𝐵))) |
91 | 90 | impcom 394 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 2 ≤
(♯‘𝐵)) |
92 | | simp-4r 770 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) |
93 | 7, 8 | usgrf 26272 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐺 ∈ USGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) =
2}) |
94 | 93 | anim1i 602 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) →
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) = 2}
∧ 𝐴 ∈ Word dom
(iEdg‘𝐺))) |
95 | | clwlkclwwlklem2 27150 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) = 2}
∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ 2 ≤ (♯‘𝐵)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) → ((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) ∧ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺))) |
96 | 94, 95 | syl3an1 1166 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ 2 ≤ (♯‘𝐵)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) → ((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) ∧ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺))) |
97 | | biid 251 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((lastS‘𝐵) =
(𝐵‘0) ↔
(lastS‘𝐵) = (𝐵‘0)) |
98 | | edgval 26162 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) |
99 | 98 | eleq2i 2842 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ({(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺)) |
100 | 99 | ralbii 3129 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∀𝑖 ∈
(0..^((♯‘𝐴)
− 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺)) |
101 | 98 | eleq2i 2842 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ({(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈
(Edg‘𝐺) ↔
{(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺)) |
102 | 97, 100, 101 | 3anbi123i 1158 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((lastS‘𝐵) =
(𝐵‘0) ∧
∀𝑖 ∈
(0..^((♯‘𝐴)
− 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺)) ↔ ((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) ∧ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺))) |
103 | 96, 102 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) ∧ 2 ≤ (♯‘𝐵)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) → ((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺))) |
104 | 56, 57, 91, 92, 103 | syl121anc 1481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺))) |
105 | 9, 10, 1, 14 | clwlksfclwwlk1hashOLD 27241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 ∈ 𝐶 → (♯‘𝐴) ∈ (0...(♯‘𝐵))) |
106 | | simp2 1131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((♯‘𝐴)
∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → 𝐵 ∈ Word (Vtx‘𝐺)) |
107 | | simp1 1130 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((♯‘𝐴)
∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) →
(♯‘𝐴) ∈
(0...(♯‘𝐵))) |
108 | | elfzelz 12549 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((♯‘𝐴)
∈ (0...(♯‘𝐵)) → (♯‘𝐴) ∈ ℤ) |
109 | | peano2zm 11622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((♯‘𝐴)
∈ ℤ → ((♯‘𝐴) − 1) ∈
ℤ) |
110 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((♯‘𝐴)
∈ ℤ → (♯‘𝐴) ∈ ℤ) |
111 | 64 | lem1d 11159 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((♯‘𝐴)
∈ ℤ → ((♯‘𝐴) − 1) ≤ (♯‘𝐴)) |
112 | | eluz2 11894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((♯‘𝐴)
∈ (ℤ≥‘((♯‘𝐴) − 1)) ↔ (((♯‘𝐴) − 1) ∈ ℤ
∧ (♯‘𝐴)
∈ ℤ ∧ ((♯‘𝐴) − 1) ≤ (♯‘𝐴))) |
113 | 109, 110,
111, 112 | syl3anbrc 1428 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((♯‘𝐴)
∈ ℤ → (♯‘𝐴) ∈
(ℤ≥‘((♯‘𝐴) − 1))) |
114 | | fzoss2 12704 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((♯‘𝐴)
∈ (ℤ≥‘((♯‘𝐴) − 1)) →
(0..^((♯‘𝐴)
− 1)) ⊆ (0..^(♯‘𝐴))) |
115 | 108, 113,
114 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((♯‘𝐴)
∈ (0...(♯‘𝐵)) → (0..^((♯‘𝐴) − 1)) ⊆
(0..^(♯‘𝐴))) |
116 | 115 | sselda 3752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((♯‘𝐴)
∈ (0...(♯‘𝐵)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → 𝑖 ∈
(0..^(♯‘𝐴))) |
117 | 116 | 3adant2 1125 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((♯‘𝐴)
∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → 𝑖 ∈
(0..^(♯‘𝐴))) |
118 | | swrd0fv 13648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈
(0...(♯‘𝐵))
∧ 𝑖 ∈
(0..^(♯‘𝐴)))
→ ((𝐵 substr 〈0,
(♯‘𝐴)〉)‘𝑖) = (𝐵‘𝑖)) |
119 | 106, 107,
117, 118 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((♯‘𝐴)
∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → ((𝐵 substr 〈0,
(♯‘𝐴)〉)‘𝑖) = (𝐵‘𝑖)) |
120 | 119 | eqcomd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((♯‘𝐴)
∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝐵‘𝑖) = ((𝐵 substr 〈0, (♯‘𝐴)〉)‘𝑖)) |
121 | | elfzom1elp1fzo 12743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((♯‘𝐴)
∈ ℤ ∧ 𝑖
∈ (0..^((♯‘𝐴) − 1))) → (𝑖 + 1) ∈ (0..^(♯‘𝐴))) |
122 | 108, 121 | sylan 569 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((♯‘𝐴)
∈ (0...(♯‘𝐵)) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝑖 + 1) ∈
(0..^(♯‘𝐴))) |
123 | 122 | 3adant2 1125 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((♯‘𝐴)
∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝑖 + 1) ∈
(0..^(♯‘𝐴))) |
124 | | swrd0fv 13648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈
(0...(♯‘𝐵))
∧ (𝑖 + 1) ∈
(0..^(♯‘𝐴)))
→ ((𝐵 substr 〈0,
(♯‘𝐴)〉)‘(𝑖 + 1)) = (𝐵‘(𝑖 + 1))) |
125 | 124 | eqcomd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈
(0...(♯‘𝐵))
∧ (𝑖 + 1) ∈
(0..^(♯‘𝐴)))
→ (𝐵‘(𝑖 + 1)) = ((𝐵 substr 〈0, (♯‘𝐴)〉)‘(𝑖 + 1))) |
126 | 106, 107,
123, 125 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((♯‘𝐴)
∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → (𝐵‘(𝑖 + 1)) = ((𝐵 substr 〈0, (♯‘𝐴)〉)‘(𝑖 + 1))) |
127 | 120, 126 | preq12d 4412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((♯‘𝐴)
∈ (0...(♯‘𝐵)) ∧ 𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr 〈0, (♯‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (♯‘𝐴)〉)‘(𝑖 + 1))}) |
128 | 127 | 3exp 1112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((♯‘𝐴)
∈ (0...(♯‘𝐵)) → (𝐵 ∈ Word (Vtx‘𝐺) → (𝑖 ∈ (0..^((♯‘𝐴) − 1)) → {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr 〈0, (♯‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (♯‘𝐴)〉)‘(𝑖 + 1))}))) |
129 | 105, 15, 128 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 ∈ 𝐶 → (𝑖 ∈ (0..^((♯‘𝐴) − 1)) → {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr 〈0, (♯‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (♯‘𝐴)〉)‘(𝑖 + 1))})) |
130 | 129 | imp 393 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑐 ∈ 𝐶 ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr 〈0, (♯‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (♯‘𝐴)〉)‘(𝑖 + 1))}) |
131 | 130 | eleq1d 2835 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑐 ∈ 𝐶 ∧ 𝑖 ∈ (0..^((♯‘𝐴) − 1))) → ({(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝐵 substr 〈0, (♯‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (♯‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
132 | 131 | ralbidva 3134 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑐 ∈ 𝐶 → (∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐵 substr 〈0,
(♯‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (♯‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
133 | 132 | ad2antlr 706 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈
(0..^((♯‘𝐴)
− 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘𝐴) − 1)){((𝐵 substr 〈0,
(♯‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (♯‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
134 | 9, 10, 1, 14 | clwlksfclwwlk2sswdOLD 27242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 ∈ 𝐶 → (♯‘𝐴) = (♯‘(𝐵 substr 〈0, (♯‘𝐴)〉))) |
135 | 134 | oveq1d 6808 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑐 ∈ 𝐶 → ((♯‘𝐴) − 1) = ((♯‘(𝐵 substr 〈0,
(♯‘𝐴)〉))
− 1)) |
136 | 135 | ad2antlr 706 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) →
((♯‘𝐴) −
1) = ((♯‘(𝐵
substr 〈0, (♯‘𝐴)〉)) − 1)) |
137 | 136 | oveq2d 6809 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) →
(0..^((♯‘𝐴)
− 1)) = (0..^((♯‘(𝐵 substr 〈0, (♯‘𝐴)〉)) −
1))) |
138 | 137 | raleqdv 3293 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈
(0..^((♯‘𝐴)
− 1)){((𝐵 substr
〈0, (♯‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (♯‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈
(0..^((♯‘(𝐵
substr 〈0, (♯‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (♯‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (♯‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
139 | 133, 138 | bitrd 268 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈
(0..^((♯‘𝐴)
− 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘(𝐵 substr 〈0,
(♯‘𝐴)〉))
− 1)){((𝐵 substr
〈0, (♯‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (♯‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
140 | | eleq1 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 = (♯‘𝐴) → (𝑁 ∈ ℙ ↔ (♯‘𝐴) ∈
ℙ)) |
141 | 140 | biimpd 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 = (♯‘𝐴) → (𝑁 ∈ ℙ → (♯‘𝐴) ∈
ℙ)) |
142 | 141 | eqcoms 2779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((♯‘𝐴) =
𝑁 → (𝑁 ∈ ℙ → (♯‘𝐴) ∈
ℙ)) |
143 | | prmnn 15595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((♯‘𝐴)
∈ ℙ → (♯‘𝐴) ∈ ℕ) |
144 | | elfz2nn0 12638 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((♯‘𝐴)
∈ (0...(♯‘𝐵)) ↔ ((♯‘𝐴) ∈ ℕ0 ∧
(♯‘𝐵) ∈
ℕ0 ∧ (♯‘𝐴) ≤ (♯‘𝐵))) |
145 | | 1zzd 11610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) → 1
∈ ℤ) |
146 | | nn0z 11602 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢
((♯‘𝐵)
∈ ℕ0 → (♯‘𝐵) ∈ ℤ) |
147 | 146 | adantl 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) →
(♯‘𝐵) ∈
ℤ) |
148 | | nn0z 11602 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢
((♯‘𝐴)
∈ ℕ0 → (♯‘𝐴) ∈ ℤ) |
149 | 148 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) →
(♯‘𝐴) ∈
ℤ) |
150 | 145, 147,
149 | 3jca 1122 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) → (1
∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈
ℤ)) |
151 | 150 | 3adant3 1126 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
(1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈
ℤ)) |
152 | 151 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((((♯‘𝐴)
∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧
(♯‘𝐴) ≤
(♯‘𝐵)) ∧
(♯‘𝐴) ∈
ℕ) → (1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈
ℤ)) |
153 | | simp3 1132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧
(♯‘𝐴) ≤
(♯‘𝐵)) →
(♯‘𝐴) ≤
(♯‘𝐵)) |
154 | | nnge1 11248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
((♯‘𝐴)
∈ ℕ → 1 ≤ (♯‘𝐴)) |
155 | 153, 154 | anim12ci 601 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((((♯‘𝐴)
∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧
(♯‘𝐴) ≤
(♯‘𝐵)) ∧
(♯‘𝐴) ∈
ℕ) → (1 ≤ (♯‘𝐴) ∧ (♯‘𝐴) ≤ (♯‘𝐵))) |
156 | 152, 155 | jca 501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((((♯‘𝐴)
∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧
(♯‘𝐴) ≤
(♯‘𝐵)) ∧
(♯‘𝐴) ∈
ℕ) → ((1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) ∧ (1 ≤
(♯‘𝐴) ∧
(♯‘𝐴) ≤
(♯‘𝐵)))) |
157 | 144, 156 | sylanb 570 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((♯‘𝐴)
∈ (0...(♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → ((1 ∈ ℤ
∧ (♯‘𝐵)
∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) ∧ (1 ≤
(♯‘𝐴) ∧
(♯‘𝐴) ≤
(♯‘𝐵)))) |
158 | | elfz2 12540 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((♯‘𝐴)
∈ (1...(♯‘𝐵)) ↔ ((1 ∈ ℤ ∧
(♯‘𝐵) ∈
ℤ ∧ (♯‘𝐴) ∈ ℤ) ∧ (1 ≤
(♯‘𝐴) ∧
(♯‘𝐴) ≤
(♯‘𝐵)))) |
159 | 157, 158 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((♯‘𝐴)
∈ (0...(♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) →
(♯‘𝐴) ∈
(1...(♯‘𝐵))) |
160 | | swrd0fvlsw 13652 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈
(1...(♯‘𝐵)))
→ (lastS‘(𝐵
substr 〈0, (♯‘𝐴)〉)) = (𝐵‘((♯‘𝐴) − 1))) |
161 | 160 | eqcomd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈
(1...(♯‘𝐵)))
→ (𝐵‘((♯‘𝐴) − 1)) = (lastS‘(𝐵 substr 〈0,
(♯‘𝐴)〉))) |
162 | | swrd0fv0 13649 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈
(1...(♯‘𝐵)))
→ ((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0) = (𝐵‘0)) |
163 | 162 | eqcomd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈
(1...(♯‘𝐵)))
→ (𝐵‘0) =
((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0)) |
164 | 161, 163 | preq12d 4412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝐴) ∈
(1...(♯‘𝐵)))
→ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr 〈0,
(♯‘𝐴)〉)),
((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0)}) |
165 | 164 | expcom 398 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((♯‘𝐴)
∈ (1...(♯‘𝐵)) → (𝐵 ∈ Word (Vtx‘𝐺) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr 〈0,
(♯‘𝐴)〉)),
((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0)})) |
166 | 159, 165 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((♯‘𝐴)
∈ (0...(♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ) → (𝐵 ∈ Word (Vtx‘𝐺) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr 〈0,
(♯‘𝐴)〉)),
((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0)})) |
167 | 166 | ex 397 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((♯‘𝐴)
∈ (0...(♯‘𝐵)) → ((♯‘𝐴) ∈ ℕ → (𝐵 ∈ Word (Vtx‘𝐺) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr 〈0,
(♯‘𝐴)〉)),
((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0)}))) |
168 | 167 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((♯‘𝐴)
∈ (0...(♯‘𝐵)) → (𝐵 ∈ Word (Vtx‘𝐺) → ((♯‘𝐴) ∈ ℕ → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr 〈0,
(♯‘𝐴)〉)),
((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0)}))) |
169 | 105, 15, 168 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑐 ∈ 𝐶 → ((♯‘𝐴) ∈ ℕ → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr 〈0,
(♯‘𝐴)〉)),
((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0)})) |
170 | 143, 169 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((♯‘𝐴)
∈ ℙ → (𝑐
∈ 𝐶 → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} =
{(lastS‘(𝐵 substr
〈0, (♯‘𝐴)〉)), ((𝐵 substr 〈0, (♯‘𝐴)〉)‘0)})) |
171 | 142, 170 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((♯‘𝐴) =
𝑁 → (𝑁 ∈ ℙ → (𝑐 ∈ 𝐶 → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr 〈0,
(♯‘𝐴)〉)),
((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0)}))) |
172 | 171 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((♯‘𝐴) =
𝑁 → (𝑐 ∈ 𝐶 → (𝑁 ∈ ℙ → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr 〈0,
(♯‘𝐴)〉)),
((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0)}))) |
173 | 172 | adantl 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → (𝑁 ∈ ℙ → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr 〈0,
(♯‘𝐴)〉)),
((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0)}))) |
174 | 173 | imp 393 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → (𝑁 ∈ ℙ → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr 〈0,
(♯‘𝐴)〉)),
((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0)})) |
175 | 174 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℙ →
(((((((♯‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr 〈0,
(♯‘𝐴)〉)),
((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0)})) |
176 | 175 | adantl 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) →
(((((((♯‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr 〈0,
(♯‘𝐴)〉)),
((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0)})) |
177 | 176 | impcom 394 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} = {(lastS‘(𝐵 substr 〈0,
(♯‘𝐴)〉)),
((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0)}) |
178 | 177 | eleq1d 2835 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ({(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈
(Edg‘𝐺) ↔
{(lastS‘(𝐵 substr
〈0, (♯‘𝐴)〉)), ((𝐵 substr 〈0, (♯‘𝐴)〉)‘0)} ∈
(Edg‘𝐺))) |
179 | 139, 178 | 3anbi23d 1550 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) →
(((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈
(0..^((♯‘𝐴)
− 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((♯‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺)) ↔ ((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘(𝐵 substr 〈0,
(♯‘𝐴)〉))
− 1)){((𝐵 substr
〈0, (♯‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (♯‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝐵 substr 〈0,
(♯‘𝐴)〉)),
((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0)} ∈ (Edg‘𝐺)))) |
180 | 104, 179 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((lastS‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((♯‘(𝐵 substr 〈0,
(♯‘𝐴)〉))
− 1)){((𝐵 substr
〈0, (♯‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (♯‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝐵 substr 〈0,
(♯‘𝐴)〉)),
((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0)} ∈ (Edg‘𝐺))) |
181 | | 3simpc 1146 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((lastS‘𝐵) =
(𝐵‘0) ∧
∀𝑖 ∈
(0..^((♯‘(𝐵
substr 〈0, (♯‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (♯‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (♯‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝐵 substr 〈0,
(♯‘𝐴)〉)),
((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0)} ∈ (Edg‘𝐺)) → (∀𝑖 ∈
(0..^((♯‘(𝐵
substr 〈0, (♯‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (♯‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (♯‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝐵 substr 〈0,
(♯‘𝐴)〉)),
((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0)} ∈ (Edg‘𝐺))) |
182 | 180, 181 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈
(0..^((♯‘(𝐵
substr 〈0, (♯‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (♯‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (♯‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝐵 substr 〈0,
(♯‘𝐴)〉)),
((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0)} ∈ (Edg‘𝐺))) |
183 | | 3anass 1080 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐵 substr 〈0,
(♯‘𝐴)〉)
∈ Word (Vtx‘𝐺)
∧ (𝐵 substr 〈0,
(♯‘𝐴)〉)
≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝐵 substr 〈0,
(♯‘𝐴)〉))
− 1)){((𝐵 substr
〈0, (♯‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (♯‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝐵 substr 〈0,
(♯‘𝐴)〉)),
((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0)} ∈ (Edg‘𝐺)) ↔ (((𝐵 substr 〈0, (♯‘𝐴)〉) ∈ Word
(Vtx‘𝐺) ∧ (𝐵 substr 〈0,
(♯‘𝐴)〉)
≠ ∅) ∧ (∀𝑖 ∈ (0..^((♯‘(𝐵 substr 〈0,
(♯‘𝐴)〉))
− 1)){((𝐵 substr
〈0, (♯‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (♯‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝐵 substr 〈0,
(♯‘𝐴)〉)),
((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0)} ∈ (Edg‘𝐺)))) |
184 | 53, 182, 183 | sylanbrc 572 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (((𝐵 substr 〈0,
(♯‘𝐴)〉)
∈ Word (Vtx‘𝐺)
∧ (𝐵 substr 〈0,
(♯‘𝐴)〉)
≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝐵 substr 〈0,
(♯‘𝐴)〉))
− 1)){((𝐵 substr
〈0, (♯‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (♯‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝐵 substr 〈0,
(♯‘𝐴)〉)),
((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0)} ∈ (Edg‘𝐺))) |
185 | | eqid 2771 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
186 | 7, 185 | isclwwlk 27134 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 substr 〈0,
(♯‘𝐴)〉)
∈ (ClWWalks‘𝐺)
↔ (((𝐵 substr 〈0,
(♯‘𝐴)〉)
∈ Word (Vtx‘𝐺)
∧ (𝐵 substr 〈0,
(♯‘𝐴)〉)
≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝐵 substr 〈0,
(♯‘𝐴)〉))
− 1)){((𝐵 substr
〈0, (♯‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (♯‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝐵 substr 〈0,
(♯‘𝐴)〉)),
((𝐵 substr 〈0,
(♯‘𝐴)〉)‘0)} ∈ (Edg‘𝐺))) |
187 | 184, 186 | sylibr 224 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr 〈0, (♯‘𝐴)〉) ∈
(ClWWalks‘𝐺)) |
188 | 134 | eqeq1d 2773 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑐 ∈ 𝐶 → ((♯‘𝐴) = 𝑁 ↔ (♯‘(𝐵 substr 〈0, (♯‘𝐴)〉)) = 𝑁)) |
189 | 188 | biimpcd 239 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝐴) =
𝑁 → (𝑐 ∈ 𝐶 → (♯‘(𝐵 substr 〈0, (♯‘𝐴)〉)) = 𝑁)) |
190 | 189 | adantl 467 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → (♯‘(𝐵 substr 〈0, (♯‘𝐴)〉)) = 𝑁)) |
191 | 190 | imp 393 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → (♯‘(𝐵 substr 〈0, (♯‘𝐴)〉)) = 𝑁) |
192 | 191 | adantr 466 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) →
(♯‘(𝐵 substr
〈0, (♯‘𝐴)〉)) = 𝑁) |
193 | | isclwwlkn 27180 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 substr 〈0,
(♯‘𝐴)〉)
∈ (𝑁 ClWWalksN 𝐺) ↔ ((𝐵 substr 〈0, (♯‘𝐴)〉) ∈
(ClWWalks‘𝐺) ∧
(♯‘(𝐵 substr
〈0, (♯‘𝐴)〉)) = 𝑁)) |
194 | 187, 192,
193 | sylanbrc 572 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr 〈0, (♯‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺)) |
195 | 194 | exp31 406 |
. . . . . . . . . . . . . . . 16
⊢
((((((♯‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴)))) ∧ (♯‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (♯‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺)))) |
196 | 195 | exp41 421 |
. . . . . . . . . . . . . . 15
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) → (𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → ((∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → ((♯‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (♯‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺))))))) |
197 | 13, 196 | mpancom 668 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ Word dom
(iEdg‘𝐺) →
(𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺) → ((∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → ((♯‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (♯‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺))))))) |
198 | 197 | imp 393 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Word dom
(iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) → ((∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → ((♯‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (♯‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺)))))) |
199 | 198 | 3impib 1108 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Word dom
(iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → ((♯‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (♯‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺))))) |
200 | 199 | com12 32 |
. . . . . . . . . . 11
⊢
((♯‘𝐴) =
𝑁 → (((𝐴 ∈ Word dom
(iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (♯‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺))))) |
201 | 200 | com14 96 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (((𝐴 ∈ Word dom
(iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈
(0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → (𝑐 ∈ 𝐶 → ((♯‘𝐴) = 𝑁 → (𝐵 substr 〈0, (♯‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺))))) |
202 | 201 | adantr 466 |
. . . . . . . . 9
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ (ClWalks‘𝐺)) → (((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(♯‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(♯‘𝐴))) → (𝑐 ∈ 𝐶 → ((♯‘𝐴) = 𝑁 → (𝐵 substr 〈0, (♯‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺))))) |
203 | 12, 202 | mpd 15 |
. . . . . . . 8
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ (ClWalks‘𝐺)) → (𝑐 ∈ 𝐶 → ((♯‘𝐴) = 𝑁 → (𝐵 substr 〈0, (♯‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺)))) |
204 | 203 | expcom 398 |
. . . . . . 7
⊢ (𝑐 ∈ (ClWalks‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝑐 ∈ 𝐶 → ((♯‘𝐴) = 𝑁 → (𝐵 substr 〈0, (♯‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺))))) |
205 | 204 | com24 95 |
. . . . . 6
⊢ (𝑐 ∈ (ClWalks‘𝐺) → ((♯‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (♯‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺))))) |
206 | 205 | imp 393 |
. . . . 5
⊢ ((𝑐 ∈ (ClWalks‘𝐺) ∧ (♯‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (♯‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺)))) |
207 | 2, 206 | sylbi 207 |
. . . 4
⊢ (𝑐 ∈ 𝐶 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (♯‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺)))) |
208 | 207 | pm2.43i 52 |
. . 3
⊢ (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (♯‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺))) |
209 | 208 | impcom 394 |
. 2
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ 𝐶) → (𝐵 substr 〈0, (♯‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺)) |
210 | 209, 14 | fmptd 6527 |
1
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶⟶(𝑁 ClWWalksN 𝐺)) |