Proof of Theorem numclwwlk3lem
Step | Hyp | Ref
| Expression |
1 | | simp3 1056 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉) |
2 | | eluzge2nn0 11603 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈
ℕ0) |
3 | | numclwwlk.c |
. . . . . 6
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛)) |
4 | | numclwwlk.f |
. . . . . 6
⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝐶‘𝑛) ∣ (𝑤‘0) = 𝑣}) |
5 | 3, 4 | numclwwlkovf 26608 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑋𝐹𝑁) = {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑋}) |
6 | 1, 2, 5 | syl2an 493 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑋𝐹𝑁) = {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑋}) |
7 | 6 | fveq2d 6107 |
. . 3
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (#‘(𝑋𝐹𝑁)) = (#‘{𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑋})) |
8 | | pm4.42 995 |
. . . . . . . 8
⊢ ((𝑤‘0) = 𝑋 ↔ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ((𝑤‘0) = 𝑋 ∧ ¬ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)))) |
9 | | nne 2786 |
. . . . . . . . . 10
⊢ (¬
(𝑤‘(𝑁 − 2)) ≠ (𝑤‘0) ↔ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) |
10 | 9 | anbi2i 726 |
. . . . . . . . 9
⊢ (((𝑤‘0) = 𝑋 ∧ ¬ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ↔ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) |
11 | 10 | orbi2i 540 |
. . . . . . . 8
⊢ ((((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ((𝑤‘0) = 𝑋 ∧ ¬ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))) ↔ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))) |
12 | 8, 11 | bitri 263 |
. . . . . . 7
⊢ ((𝑤‘0) = 𝑋 ↔ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))) |
13 | 12 | a1i 11 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((𝑤‘0) = 𝑋 ↔ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))))) |
14 | 13 | rabbidv 3164 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑋} = {𝑤 ∈ (𝐶‘𝑁) ∣ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))}) |
15 | | unrab 3857 |
. . . . 5
⊢ ({𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∪ {𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) = {𝑤 ∈ (𝐶‘𝑁) ∣ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))} |
16 | 14, 15 | syl6eqr 2662 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑋} = ({𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∪ {𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))})) |
17 | 16 | fveq2d 6107 |
. . 3
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (#‘{𝑤 ∈
(𝐶‘𝑁) ∣ (𝑤‘0) = 𝑋}) = (#‘({𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∪ {𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}))) |
18 | 3 | numclwwlkfvc 26604 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝐶‘𝑁) = ((𝑉 ClWWalksN 𝐸)‘𝑁)) |
19 | 2, 18 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝐶‘𝑁) = ((𝑉 ClWWalksN 𝐸)‘𝑁)) |
20 | 19 | adantl 481 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝐶‘𝑁) = ((𝑉 ClWWalksN 𝐸)‘𝑁)) |
21 | | simpl2 1058 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ 𝑉 ∈
Fin) |
22 | | usgrav 25867 |
. . . . . . . . . 10
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
23 | 22 | simprd 478 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → 𝐸 ∈ V) |
24 | 23 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) → 𝐸 ∈ V) |
25 | 24 | adantr 480 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ 𝐸 ∈
V) |
26 | 2 | adantl 481 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ 𝑁 ∈
ℕ0) |
27 | | clwwlknfi 26306 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∈ Fin) |
28 | 21, 25, 26, 27 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∈ Fin) |
29 | 20, 28 | eqeltrd 2688 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝐶‘𝑁) ∈ Fin) |
30 | | rabfi 8070 |
. . . . 5
⊢ ((𝐶‘𝑁) ∈ Fin → {𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∈ Fin) |
31 | 29, 30 | syl 17 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ {𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∈ Fin) |
32 | | rabfi 8070 |
. . . . 5
⊢ ((𝐶‘𝑁) ∈ Fin → {𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))} ∈ Fin) |
33 | 29, 32 | syl 17 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ {𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))} ∈ Fin) |
34 | | inrab 3858 |
. . . . 5
⊢ ({𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∩ {𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) = {𝑤 ∈ (𝐶‘𝑁) ∣ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))} |
35 | | df-ne 2782 |
. . . . . . . . . . . . 13
⊢ ((𝑤‘(𝑁 − 2)) ≠ (𝑤‘0) ↔ ¬ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) |
36 | 35 | biimpi 205 |
. . . . . . . . . . . 12
⊢ ((𝑤‘(𝑁 − 2)) ≠ (𝑤‘0) → ¬ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) |
37 | 36 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) → ¬ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) |
38 | 37 | intnand 953 |
. . . . . . . . . 10
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) → ¬ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) |
39 | 38 | imori 428 |
. . . . . . . . 9
⊢ (¬
((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ¬ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) |
40 | | ianor 508 |
. . . . . . . . 9
⊢ (¬
(((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) ↔ (¬ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ¬ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))) |
41 | 39, 40 | mpbir 220 |
. . . . . . . 8
⊢ ¬
(((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) |
42 | 41 | a1i 11 |
. . . . . . 7
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
∧ 𝑤 ∈ (𝐶‘𝑁)) → ¬ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))) |
43 | 42 | ralrimiva 2949 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ ∀𝑤 ∈
(𝐶‘𝑁) ¬ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))) |
44 | | rabeq0 3911 |
. . . . . 6
⊢ ({𝑤 ∈ (𝐶‘𝑁) ∣ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))} = ∅ ↔ ∀𝑤 ∈ (𝐶‘𝑁) ¬ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))) |
45 | 43, 44 | sylibr 223 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ {𝑤 ∈ (𝐶‘𝑁) ∣ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))} = ∅) |
46 | 34, 45 | syl5eq 2656 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ ({𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∩ {𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) = ∅) |
47 | | hashun 13032 |
. . . 4
⊢ (({𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∈ Fin ∧ {𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))} ∈ Fin ∧ ({𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∩ {𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) = ∅) →
(#‘({𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∪ {𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))})) = ((#‘{𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))}) + (#‘{𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}))) |
48 | 31, 33, 46, 47 | syl3anc 1318 |
. . 3
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (#‘({𝑤 ∈
(𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∪ {𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))})) = ((#‘{𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))}) + (#‘{𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}))) |
49 | 7, 17, 48 | 3eqtrd 2648 |
. 2
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (#‘(𝑋𝐹𝑁)) = ((#‘{𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))}) + (#‘{𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}))) |
50 | | numclwwlk.g |
. . . . . 6
⊢ 𝐺 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝐶‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) = (𝑤‘0))}) |
51 | | numclwwlk.q |
. . . . . 6
⊢ 𝑄 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ ( lastS ‘𝑤) ≠ 𝑣)}) |
52 | | numclwwlk.h |
. . . . . 6
⊢ 𝐻 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝐶‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) ≠ (𝑤‘0))}) |
53 | 3, 4, 50, 51, 52 | numclwwlkovh 26628 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑋𝐻𝑁) = {𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))}) |
54 | 1, 2, 53 | syl2an 493 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑋𝐻𝑁) = {𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))}) |
55 | 54 | fveq2d 6107 |
. . 3
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (#‘(𝑋𝐻𝑁)) = (#‘{𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))})) |
56 | 3, 4, 50 | numclwwlkovg 26614 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑋𝐺𝑁) = {𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) |
57 | 1, 56 | sylan 487 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑋𝐺𝑁) = {𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) |
58 | 57 | fveq2d 6107 |
. . 3
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (#‘(𝑋𝐺𝑁)) = (#‘{𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))})) |
59 | 55, 58 | oveq12d 6567 |
. 2
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((#‘(𝑋𝐻𝑁)) + (#‘(𝑋𝐺𝑁))) = ((#‘{𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))}) + (#‘{𝑤 ∈ (𝐶‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}))) |
60 | 49, 59 | eqtr4d 2647 |
1
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (#‘(𝑋𝐹𝑁)) = ((#‘(𝑋𝐻𝑁)) + (#‘(𝑋𝐺𝑁)))) |