Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . 4
β’ ((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph ) β πΊ RegUSGraph πΎ) |
2 | | simp1 1137 |
. . . 4
β’ ((π β Fin β§ π β π β§ π β (β€β₯β3))
β π β
Fin) |
3 | | numclwwlk3.v |
. . . . 5
β’ π = (VtxβπΊ) |
4 | 3 | finrusgrfusgr 28555 |
. . . 4
β’ ((πΊ RegUSGraph πΎ β§ π β Fin) β πΊ β FinUSGraph) |
5 | 1, 2, 4 | syl2an 597 |
. . 3
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph ) β§ (π β Fin β§ π β π β§ π β (β€β₯β3)))
β πΊ β
FinUSGraph) |
6 | | simpr2 1196 |
. . 3
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph ) β§ (π β Fin β§ π β π β§ π β (β€β₯β3)))
β π β π) |
7 | | uzuzle23 12821 |
. . . . 5
β’ (π β
(β€β₯β3) β π β
(β€β₯β2)) |
8 | 7 | 3ad2ant3 1136 |
. . . 4
β’ ((π β Fin β§ π β π β§ π β (β€β₯β3))
β π β
(β€β₯β2)) |
9 | 8 | adantl 483 |
. . 3
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph ) β§ (π β Fin β§ π β π β§ π β (β€β₯β3)))
β π β
(β€β₯β2)) |
10 | | eqid 2737 |
. . . 4
β’ (π£ β π, π β (β€β₯β2)
β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£}) = (π£ β π, π β (β€β₯β2)
β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£}) |
11 | | eqid 2737 |
. . . 4
β’ (π£ β π, π β (β€β₯β2)
β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π£}) = (π£ β π, π β (β€β₯β2)
β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π£}) |
12 | 10, 11 | numclwwlk3lem2 29370 |
. . 3
β’ (((πΊ β FinUSGraph β§ π β π) β§ π β (β€β₯β2))
β (β―β(π(ClWWalksNOnβπΊ)π)) = ((β―β(π(π£ β π, π β (β€β₯β2)
β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π£})π)) + (β―β(π(π£ β π, π β (β€β₯β2)
β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£})π)))) |
13 | 5, 6, 9, 12 | syl21anc 837 |
. 2
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph ) β§ (π β Fin β§ π β π β§ π β (β€β₯β3)))
β (β―β(π(ClWWalksNOnβπΊ)π)) = ((β―β(π(π£ β π, π β (β€β₯β2)
β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π£})π)) + (β―β(π(π£ β π, π β (β€β₯β2)
β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£})π)))) |
14 | | eqid 2737 |
. . . 4
β’ (π£ β π, π β β β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π£ β§ (lastSβπ€) β π£)}) = (π£ β π, π β β β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π£ β§ (lastSβπ€) β π£)}) |
15 | 3, 14, 11 | numclwwlk2 29367 |
. . 3
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph ) β§ (π β Fin β§ π β π β§ π β (β€β₯β3)))
β (β―β(π(π£ β π, π β (β€β₯β2)
β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π£})π)) = ((πΎβ(π β 2)) β (β―β(π(ClWWalksNOnβπΊ)(π β 2))))) |
16 | 1, 2 | anim12ci 615 |
. . . 4
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph ) β§ (π β Fin β§ π β π β§ π β (β€β₯β3)))
β (π β Fin β§
πΊ RegUSGraph πΎ)) |
17 | | 3simpc 1151 |
. . . . 5
β’ ((π β Fin β§ π β π β§ π β (β€β₯β3))
β (π β π β§ π β
(β€β₯β3))) |
18 | 17 | adantl 483 |
. . . 4
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph ) β§ (π β Fin β§ π β π β§ π β (β€β₯β3)))
β (π β π β§ π β
(β€β₯β3))) |
19 | | eqid 2737 |
. . . . 5
β’ (π(ClWWalksNOnβπΊ)(π β 2)) = (π(ClWWalksNOnβπΊ)(π β 2)) |
20 | 3, 10, 19 | numclwwlk1 29347 |
. . . 4
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β3)))
β (β―β(π(π£ β π, π β (β€β₯β2)
β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£})π)) = (πΎ Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2))))) |
21 | 16, 18, 20 | syl2anc 585 |
. . 3
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph ) β§ (π β Fin β§ π β π β§ π β (β€β₯β3)))
β (β―β(π(π£ β π, π β (β€β₯β2)
β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£})π)) = (πΎ Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2))))) |
22 | 15, 21 | oveq12d 7380 |
. 2
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph ) β§ (π β Fin β§ π β π β§ π β (β€β₯β3)))
β ((β―β(π(π£ β π, π β (β€β₯β2)
β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π£})π)) + (β―β(π(π£ β π, π β (β€β₯β2)
β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£})π))) = (((πΎβ(π β 2)) β (β―β(π(ClWWalksNOnβπΊ)(π β 2)))) + (πΎ Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2)))))) |
23 | | simpll 766 |
. . . . 5
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph ) β§ (π β Fin β§ π β π β§ π β (β€β₯β3)))
β πΊ RegUSGraph πΎ) |
24 | | ne0i 4299 |
. . . . . . 7
β’ (π β π β π β β
) |
25 | 24 | 3ad2ant2 1135 |
. . . . . 6
β’ ((π β Fin β§ π β π β§ π β (β€β₯β3))
β π β
β
) |
26 | 25 | adantl 483 |
. . . . 5
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph ) β§ (π β Fin β§ π β π β§ π β (β€β₯β3)))
β π β
β
) |
27 | 3 | frusgrnn0 28561 |
. . . . 5
β’ ((πΊ β FinUSGraph β§ πΊ RegUSGraph πΎ β§ π β β
) β πΎ β
β0) |
28 | 5, 23, 26, 27 | syl3anc 1372 |
. . . 4
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph ) β§ (π β Fin β§ π β π β§ π β (β€β₯β3)))
β πΎ β
β0) |
29 | 28 | nn0cnd 12482 |
. . 3
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph ) β§ (π β Fin β§ π β π β§ π β (β€β₯β3)))
β πΎ β
β) |
30 | | uz3m2nn 12823 |
. . . . . 6
β’ (π β
(β€β₯β3) β (π β 2) β β) |
31 | 30 | 3anim3i 1155 |
. . . . 5
β’ ((π β Fin β§ π β π β§ π β (β€β₯β3))
β (π β Fin β§
π β π β§ (π β 2) β
β)) |
32 | 31 | adantl 483 |
. . . 4
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph ) β§ (π β Fin β§ π β π β§ π β (β€β₯β3)))
β (π β Fin β§
π β π β§ (π β 2) β
β)) |
33 | 3 | clwwlknonfin 29080 |
. . . . 5
β’ (π β Fin β (π(ClWWalksNOnβπΊ)(π β 2)) β Fin) |
34 | 33 | 3ad2ant1 1134 |
. . . 4
β’ ((π β Fin β§ π β π β§ (π β 2) β β) β (π(ClWWalksNOnβπΊ)(π β 2)) β Fin) |
35 | | hashcl 14263 |
. . . . 5
β’ ((π(ClWWalksNOnβπΊ)(π β 2)) β Fin β
(β―β(π(ClWWalksNOnβπΊ)(π β 2))) β
β0) |
36 | 35 | nn0cnd 12482 |
. . . 4
β’ ((π(ClWWalksNOnβπΊ)(π β 2)) β Fin β
(β―β(π(ClWWalksNOnβπΊ)(π β 2))) β
β) |
37 | 32, 34, 36 | 3syl 18 |
. . 3
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph ) β§ (π β Fin β§ π β π β§ π β (β€β₯β3)))
β (β―β(π(ClWWalksNOnβπΊ)(π β 2))) β
β) |
38 | | numclwwlk3lem1 29368 |
. . 3
β’ ((πΎ β β β§
(β―β(π(ClWWalksNOnβπΊ)(π β 2))) β β β§ π β
(β€β₯β2)) β (((πΎβ(π β 2)) β (β―β(π(ClWWalksNOnβπΊ)(π β 2)))) + (πΎ Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2))))) = (((πΎ β 1) Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2)))) + (πΎβ(π β 2)))) |
39 | 29, 37, 9, 38 | syl3anc 1372 |
. 2
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph ) β§ (π β Fin β§ π β π β§ π β (β€β₯β3)))
β (((πΎβ(π β 2)) β
(β―β(π(ClWWalksNOnβπΊ)(π β 2)))) + (πΎ Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2))))) = (((πΎ β 1) Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2)))) + (πΎβ(π β 2)))) |
40 | 13, 22, 39 | 3eqtrd 2781 |
1
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph ) β§ (π β Fin β§ π β π β§ π β (β€β₯β3)))
β (β―β(π(ClWWalksNOnβπΊ)π)) = (((πΎ β 1) Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2)))) + (πΎβ(π β 2)))) |