Proof of Theorem av-numclwwlk3lem
Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . . . 5
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉) |
2 | | eluz2nn 11602 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℕ) |
3 | | av-numclwwlk.f |
. . . . . 6
⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑣}) |
4 | 3 | av-numclwwlkovf 41511 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋𝐹𝑁) = {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋}) |
5 | 1, 2, 4 | syl2an 493 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑋𝐹𝑁) = {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋}) |
6 | 5 | fveq2d 6107 |
. . 3
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (#‘(𝑋𝐹𝑁)) = (#‘{𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋})) |
7 | | pm4.42 995 |
. . . . . . . 8
⊢ ((𝑤‘0) = 𝑋 ↔ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ((𝑤‘0) = 𝑋 ∧ ¬ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)))) |
8 | | nne 2786 |
. . . . . . . . . 10
⊢ (¬
(𝑤‘(𝑁 − 2)) ≠ (𝑤‘0) ↔ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) |
9 | 8 | anbi2i 726 |
. . . . . . . . 9
⊢ (((𝑤‘0) = 𝑋 ∧ ¬ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ↔ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) |
10 | 9 | orbi2i 540 |
. . . . . . . 8
⊢ ((((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ((𝑤‘0) = 𝑋 ∧ ¬ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))) ↔ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))) |
11 | 7, 10 | bitri 263 |
. . . . . . 7
⊢ ((𝑤‘0) = 𝑋 ↔ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))) |
12 | 11 | a1i 11 |
. . . . . 6
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((𝑤‘0) = 𝑋 ↔ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))))) |
13 | 12 | rabbidv 3164 |
. . . . 5
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋} = {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))}) |
14 | | unrab 3857 |
. . . . 5
⊢ ({𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∪ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) = {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))} |
15 | 13, 14 | syl6eqr 2662 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋} = ({𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∪ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))})) |
16 | 15 | fveq2d 6107 |
. . 3
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (#‘{𝑤 ∈
(𝑁 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑋}) = (#‘({𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∪ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}))) |
17 | | av-numclwwlk.v |
. . . . . . 7
⊢ 𝑉 = (Vtx‘𝐺) |
18 | 17 | fusgrvtxfi 40538 |
. . . . . . . 8
⊢ (𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin) |
19 | 18 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ 𝑉 ∈
Fin) |
20 | 17, 19 | syl5eqelr 2693 |
. . . . . 6
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (Vtx‘𝐺) ∈
Fin) |
21 | | clwwlksnfi 41220 |
. . . . . 6
⊢
((Vtx‘𝐺)
∈ Fin → (𝑁
ClWWalkSN 𝐺) ∈
Fin) |
22 | 20, 21 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑁 ClWWalkSN 𝐺) ∈ Fin) |
23 | | rabfi 8070 |
. . . . 5
⊢ ((𝑁 ClWWalkSN 𝐺) ∈ Fin → {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∈ Fin) |
24 | 22, 23 | syl 17 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∈ Fin) |
25 | | rabfi 8070 |
. . . . 5
⊢ ((𝑁 ClWWalkSN 𝐺) ∈ Fin → {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))} ∈ Fin) |
26 | 22, 25 | syl 17 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))} ∈ Fin) |
27 | | inrab 3858 |
. . . . 5
⊢ ({𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∩ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) = {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))} |
28 | | neneq 2788 |
. . . . . . . . . . . 12
⊢ ((𝑤‘(𝑁 − 2)) ≠ (𝑤‘0) → ¬ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) |
29 | 28 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) → ¬ (𝑤‘(𝑁 − 2)) = (𝑤‘0)) |
30 | 29 | intnand 953 |
. . . . . . . . . 10
⊢ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) → ¬ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) |
31 | 30 | imori 428 |
. . . . . . . . 9
⊢ (¬
((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ¬ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) |
32 | | ianor 508 |
. . . . . . . . 9
⊢ (¬
(((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) ↔ (¬ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∨ ¬ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))) |
33 | 31, 32 | mpbir 220 |
. . . . . . . 8
⊢ ¬
(((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))) |
34 | 33 | a1i 11 |
. . . . . . 7
⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
∧ 𝑤 ∈ (𝑁 ClWWalkSN 𝐺)) → ¬ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))) |
35 | 34 | ralrimiva 2949 |
. . . . . 6
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ ∀𝑤 ∈
(𝑁 ClWWalkSN 𝐺) ¬ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))) |
36 | | rabeq0 3911 |
. . . . . 6
⊢ ({𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))} = ∅ ↔ ∀𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ¬ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))) |
37 | 35, 36 | sylibr 223 |
. . . . 5
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ (((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0)) ∧ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0)))} = ∅) |
38 | 27, 37 | syl5eq 2656 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ ({𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∩ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) = ∅) |
39 | | hashun 13032 |
. . . 4
⊢ (({𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∈ Fin ∧ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))} ∈ Fin ∧ ({𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∩ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) = ∅) →
(#‘({𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∪ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))})) = ((#‘{𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))}) + (#‘{𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}))) |
40 | 24, 26, 38, 39 | syl3anc 1318 |
. . 3
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (#‘({𝑤 ∈
(𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))} ∪ {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))})) = ((#‘{𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))}) + (#‘{𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}))) |
41 | 6, 16, 40 | 3eqtrd 2648 |
. 2
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (#‘(𝑋𝐹𝑁)) = ((#‘{𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))}) + (#‘{𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}))) |
42 | | av-numclwwlk.q |
. . . . . 6
⊢ 𝑄 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ ( lastS ‘𝑤) ≠ 𝑣)}) |
43 | | av-numclwwlk.h |
. . . . . 6
⊢ 𝐻 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) ≠ (𝑤‘0))}) |
44 | 17, 42, 3, 43 | av-numclwwlkovh 41531 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋𝐻𝑁) = {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))}) |
45 | 1, 2, 44 | syl2an 493 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑋𝐻𝑁) = {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))}) |
46 | 45 | fveq2d 6107 |
. . 3
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (#‘(𝑋𝐻𝑁)) = (#‘{𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))})) |
47 | | av-numclwwlk.c |
. . . . . 6
⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑛 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) = (𝑤‘0))}) |
48 | 47 | av-numclwwlkovg 41518 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑋𝐶𝑁) = {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) |
49 | 48 | adantll 746 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑋𝐶𝑁) = {𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}) |
50 | 49 | fveq2d 6107 |
. . 3
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (#‘(𝑋𝐶𝑁)) = (#‘{𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))})) |
51 | 46, 50 | oveq12d 6567 |
. 2
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((#‘(𝑋𝐻𝑁)) + (#‘(𝑋𝐶𝑁))) = ((#‘{𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))}) + (#‘{𝑤 ∈ (𝑁 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) = (𝑤‘0))}))) |
52 | 41, 51 | eqtr4d 2647 |
1
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (#‘(𝑋𝐹𝑁)) = ((#‘(𝑋𝐻𝑁)) + (#‘(𝑋𝐶𝑁)))) |