| Step | Hyp | Ref
| Expression |
| 1 | | rusgrusgr 29582 |
. . . . . 6
⊢ (𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USGraph) |
| 2 | | usgruspgr 29197 |
. . . . . 6
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
USPGraph) |
| 3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USPGraph) |
| 4 | 3 | ad2antlr 727 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝐺 ∈
USPGraph) |
| 5 | | simpl 482 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑋 ∈ 𝑉) |
| 6 | 5 | adantl 481 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝑋 ∈ 𝑉) |
| 7 | | uzuzle23 12931 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈
(ℤ≥‘2)) |
| 8 | 7 | ad2antll 729 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝑁 ∈
(ℤ≥‘2)) |
| 9 | | numclwlk1.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
| 10 | | numclwlk1.c |
. . . . 5
⊢ 𝐶 = {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑋 ∧ ((2nd
‘𝑤)‘(𝑁 − 2)) = 𝑋)} |
| 11 | | eqid 2737 |
. . . . 5
⊢ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋} = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋} |
| 12 | 9, 10, 11 | dlwwlknondlwlknonen 30385 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ 𝐶 ≈ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋}) |
| 13 | 4, 6, 8, 12 | syl3anc 1373 |
. . 3
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝐶 ≈ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋}) |
| 14 | 1 | anim2i 617 |
. . . . . . . . 9
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) → (𝑉 ∈ Fin ∧ 𝐺 ∈ USGraph)) |
| 15 | 14 | ancomd 461 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) → (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin)) |
| 16 | 9 | isfusgr 29335 |
. . . . . . . 8
⊢ (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin)) |
| 17 | 15, 16 | sylibr 234 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) → 𝐺 ∈ FinUSGraph) |
| 18 | | eluzge3nn 12932 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℕ) |
| 19 | 18 | nnnn0d 12587 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈
ℕ0) |
| 20 | 19 | adantl 481 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑁 ∈
ℕ0) |
| 21 | | wlksnfi 29927 |
. . . . . . 7
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℕ0)
→ {𝑤 ∈
(Walks‘𝐺) ∣
(♯‘(1st ‘𝑤)) = 𝑁} ∈ Fin) |
| 22 | 17, 20, 21 | syl2an 596 |
. . . . . 6
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ {𝑤 ∈
(Walks‘𝐺) ∣
(♯‘(1st ‘𝑤)) = 𝑁} ∈ Fin) |
| 23 | | clwlkswks 29796 |
. . . . . . . 8
⊢
(ClWalks‘𝐺)
⊆ (Walks‘𝐺) |
| 24 | 23 | a1i 11 |
. . . . . . 7
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (ClWalks‘𝐺)
⊆ (Walks‘𝐺)) |
| 25 | | simp21 1207 |
. . . . . . 7
⊢ ((((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ ((♯‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑋 ∧ ((2nd ‘𝑤)‘(𝑁 − 2)) = 𝑋) ∧ 𝑤 ∈ (ClWalks‘𝐺)) → (♯‘(1st
‘𝑤)) = 𝑁) |
| 26 | 24, 25 | rabssrabd 4083 |
. . . . . 6
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ {𝑤 ∈
(ClWalks‘𝐺) ∣
((♯‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑋 ∧ ((2nd ‘𝑤)‘(𝑁 − 2)) = 𝑋)} ⊆ {𝑤 ∈ (Walks‘𝐺) ∣ (♯‘(1st
‘𝑤)) = 𝑁}) |
| 27 | 22, 26 | ssfid 9301 |
. . . . 5
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ {𝑤 ∈
(ClWalks‘𝐺) ∣
((♯‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑋 ∧ ((2nd ‘𝑤)‘(𝑁 − 2)) = 𝑋)} ∈ Fin) |
| 28 | 10, 27 | eqeltrid 2845 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝐶 ∈
Fin) |
| 29 | 9 | clwwlknonfin 30113 |
. . . . . 6
⊢ (𝑉 ∈ Fin → (𝑋(ClWWalksNOn‘𝐺)𝑁) ∈ Fin) |
| 30 | 29 | ad2antrr 726 |
. . . . 5
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∈ Fin) |
| 31 | | ssrab2 4080 |
. . . . . 6
⊢ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋} ⊆ (𝑋(ClWWalksNOn‘𝐺)𝑁) |
| 32 | 31 | a1i 11 |
. . . . 5
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋} ⊆ (𝑋(ClWWalksNOn‘𝐺)𝑁)) |
| 33 | 30, 32 | ssfid 9301 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋} ∈ Fin) |
| 34 | | hashen 14386 |
. . . 4
⊢ ((𝐶 ∈ Fin ∧ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋} ∈ Fin) → ((♯‘𝐶) = (♯‘{𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋}) ↔ 𝐶 ≈ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋})) |
| 35 | 28, 33, 34 | syl2anc 584 |
. . 3
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ ((♯‘𝐶) =
(♯‘{𝑤 ∈
(𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋}) ↔ 𝐶 ≈ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋})) |
| 36 | 13, 35 | mpbird 257 |
. 2
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (♯‘𝐶) =
(♯‘{𝑤 ∈
(𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋})) |
| 37 | | eqidd 2738 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣}) = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})) |
| 38 | | oveq12 7440 |
. . . . . 6
⊢ ((𝑣 = 𝑋 ∧ 𝑛 = 𝑁) → (𝑣(ClWWalksNOn‘𝐺)𝑛) = (𝑋(ClWWalksNOn‘𝐺)𝑁)) |
| 39 | | fvoveq1 7454 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (𝑤‘(𝑛 − 2)) = (𝑤‘(𝑁 − 2))) |
| 40 | 39 | adantl 481 |
. . . . . . 7
⊢ ((𝑣 = 𝑋 ∧ 𝑛 = 𝑁) → (𝑤‘(𝑛 − 2)) = (𝑤‘(𝑁 − 2))) |
| 41 | | simpl 482 |
. . . . . . 7
⊢ ((𝑣 = 𝑋 ∧ 𝑛 = 𝑁) → 𝑣 = 𝑋) |
| 42 | 40, 41 | eqeq12d 2753 |
. . . . . 6
⊢ ((𝑣 = 𝑋 ∧ 𝑛 = 𝑁) → ((𝑤‘(𝑛 − 2)) = 𝑣 ↔ (𝑤‘(𝑁 − 2)) = 𝑋)) |
| 43 | 38, 42 | rabeqbidv 3455 |
. . . . 5
⊢ ((𝑣 = 𝑋 ∧ 𝑛 = 𝑁) → {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣} = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋}) |
| 44 | 43 | adantl 481 |
. . . 4
⊢ ((((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ (𝑣 = 𝑋 ∧ 𝑛 = 𝑁)) → {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣} = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋}) |
| 45 | | ovex 7464 |
. . . . . 6
⊢ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∈ V |
| 46 | 45 | rabex 5339 |
. . . . 5
⊢ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋} ∈ V |
| 47 | 46 | a1i 11 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋} ∈ V) |
| 48 | 37, 44, 6, 8, 47 | ovmpod 7585 |
. . 3
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑋(𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})𝑁) = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋}) |
| 49 | 48 | fveq2d 6910 |
. 2
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (♯‘(𝑋(𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})𝑁)) = (♯‘{𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋})) |
| 50 | | eqid 2737 |
. . . 4
⊢ (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣}) = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣}) |
| 51 | | eqid 2737 |
. . . 4
⊢ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) = (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) |
| 52 | 9, 50, 51 | numclwwlk1 30380 |
. . 3
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (♯‘(𝑋(𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})𝑁)) = (𝐾 · (♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))))) |
| 53 | | numclwlk1.f |
. . . . . . 7
⊢ 𝐹 = {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = (𝑁 − 2) ∧
((2nd ‘𝑤)‘0) = 𝑋)} |
| 54 | 5, 9 | eleqtrdi 2851 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑋 ∈
(Vtx‘𝐺)) |
| 55 | 54 | adantl 481 |
. . . . . . . 8
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝑋 ∈
(Vtx‘𝐺)) |
| 56 | | uz3m2nn 12933 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ ℕ) |
| 57 | 56 | ad2antll 729 |
. . . . . . . 8
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑁 − 2) ∈
ℕ) |
| 58 | | clwwlknonclwlknonen 30382 |
. . . . . . . 8
⊢ ((𝐺 ∈ USPGraph ∧ 𝑋 ∈ (Vtx‘𝐺) ∧ (𝑁 − 2) ∈ ℕ) → {𝑤 ∈ (ClWalks‘𝐺) ∣
((♯‘(1st ‘𝑤)) = (𝑁 − 2) ∧ ((2nd
‘𝑤)‘0) = 𝑋)} ≈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))) |
| 59 | 4, 55, 57, 58 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ {𝑤 ∈
(ClWalks‘𝐺) ∣
((♯‘(1st ‘𝑤)) = (𝑁 − 2) ∧ ((2nd
‘𝑤)‘0) = 𝑋)} ≈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))) |
| 60 | 53, 59 | eqbrtrid 5178 |
. . . . . 6
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝐹 ≈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))) |
| 61 | | uznn0sub 12917 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 2) ∈
ℕ0) |
| 62 | 7, 61 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈
ℕ0) |
| 63 | 62 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 2) ∈
ℕ0) |
| 64 | | wlksnfi 29927 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ FinUSGraph ∧ (𝑁 − 2) ∈
ℕ0) → {𝑤 ∈ (Walks‘𝐺) ∣ (♯‘(1st
‘𝑤)) = (𝑁 − 2)} ∈
Fin) |
| 65 | 17, 63, 64 | syl2an 596 |
. . . . . . . . 9
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ {𝑤 ∈
(Walks‘𝐺) ∣
(♯‘(1st ‘𝑤)) = (𝑁 − 2)} ∈ Fin) |
| 66 | | simp2l 1200 |
. . . . . . . . . 10
⊢ ((((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ ((♯‘(1st ‘𝑤)) = (𝑁 − 2) ∧ ((2nd
‘𝑤)‘0) = 𝑋) ∧ 𝑤 ∈ (ClWalks‘𝐺)) → (♯‘(1st
‘𝑤)) = (𝑁 − 2)) |
| 67 | 24, 66 | rabssrabd 4083 |
. . . . . . . . 9
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ {𝑤 ∈
(ClWalks‘𝐺) ∣
((♯‘(1st ‘𝑤)) = (𝑁 − 2) ∧ ((2nd
‘𝑤)‘0) = 𝑋)} ⊆ {𝑤 ∈ (Walks‘𝐺) ∣ (♯‘(1st
‘𝑤)) = (𝑁 − 2)}) |
| 68 | 65, 67 | ssfid 9301 |
. . . . . . . 8
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ {𝑤 ∈
(ClWalks‘𝐺) ∣
((♯‘(1st ‘𝑤)) = (𝑁 − 2) ∧ ((2nd
‘𝑤)‘0) = 𝑋)} ∈ Fin) |
| 69 | 53, 68 | eqeltrid 2845 |
. . . . . . 7
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝐹 ∈
Fin) |
| 70 | 9 | clwwlknonfin 30113 |
. . . . . . . 8
⊢ (𝑉 ∈ Fin → (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) ∈ Fin) |
| 71 | 70 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) ∈ Fin) |
| 72 | | hashen 14386 |
. . . . . . 7
⊢ ((𝐹 ∈ Fin ∧ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) ∈ Fin) →
((♯‘𝐹) =
(♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))) ↔ 𝐹 ≈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)))) |
| 73 | 69, 71, 72 | syl2anc 584 |
. . . . . 6
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ ((♯‘𝐹) =
(♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))) ↔ 𝐹 ≈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)))) |
| 74 | 60, 73 | mpbird 257 |
. . . . 5
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (♯‘𝐹) =
(♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)))) |
| 75 | 74 | eqcomd 2743 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))) = (♯‘𝐹)) |
| 76 | 75 | oveq2d 7447 |
. . 3
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝐾 ·
(♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)))) = (𝐾 · (♯‘𝐹))) |
| 77 | 52, 76 | eqtrd 2777 |
. 2
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (♯‘(𝑋(𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})𝑁)) = (𝐾 · (♯‘𝐹))) |
| 78 | 36, 49, 77 | 3eqtr2d 2783 |
1
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (♯‘𝐶) =
(𝐾 ·
(♯‘𝐹))) |