Step | Hyp | Ref
| Expression |
1 | | 3anass 1095 |
. . . . . . 7
β’
(((β―β(1st βπ€)) = 2 β§ ((2nd βπ€)β0) = π β§ ((2nd βπ€)β0) = π) β ((β―β(1st
βπ€)) = 2 β§
(((2nd βπ€)β0) = π β§ ((2nd βπ€)β0) = π))) |
2 | | anidm 565 |
. . . . . . . 8
β’
((((2nd βπ€)β0) = π β§ ((2nd βπ€)β0) = π) β ((2nd βπ€)β0) = π) |
3 | 2 | anbi2i 623 |
. . . . . . 7
β’
(((β―β(1st βπ€)) = 2 β§ (((2nd βπ€)β0) = π β§ ((2nd βπ€)β0) = π)) β ((β―β(1st
βπ€)) = 2 β§
((2nd βπ€)β0) = π)) |
4 | 1, 3 | bitri 274 |
. . . . . 6
β’
(((β―β(1st βπ€)) = 2 β§ ((2nd βπ€)β0) = π β§ ((2nd βπ€)β0) = π) β ((β―β(1st
βπ€)) = 2 β§
((2nd βπ€)β0) = π)) |
5 | 4 | rabbii 3413 |
. . . . 5
β’ {π€ β (ClWalksβπΊ) β£
((β―β(1st βπ€)) = 2 β§ ((2nd βπ€)β0) = π β§ ((2nd βπ€)β0) = π)} = {π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = 2 β§
((2nd βπ€)β0) = π)} |
6 | 5 | fveq2i 6845 |
. . . 4
β’
(β―β{π€
β (ClWalksβπΊ)
β£ ((β―β(1st βπ€)) = 2 β§ ((2nd βπ€)β0) = π β§ ((2nd βπ€)β0) = π)}) = (β―β{π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = 2 β§
((2nd βπ€)β0) = π)}) |
7 | | simpl 483 |
. . . . 5
β’ ((π β Fin β§ πΊ RegUSGraph πΎ) β π β Fin) |
8 | | simpr 485 |
. . . . 5
β’ ((π β Fin β§ πΊ RegUSGraph πΎ) β πΊ RegUSGraph πΎ) |
9 | | simpl 483 |
. . . . 5
β’ ((π β π β§ π = 2) β π β π) |
10 | | numclwlk1.v |
. . . . . 6
β’ π = (VtxβπΊ) |
11 | 10 | clwlknon2num 29312 |
. . . . 5
β’ ((π β Fin β§ πΊ RegUSGraph πΎ β§ π β π) β (β―β{π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = 2 β§
((2nd βπ€)β0) = π)}) = πΎ) |
12 | 7, 8, 9, 11 | syl2an3an 1422 |
. . . 4
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π = 2)) β (β―β{π€ β (ClWalksβπΊ) β£
((β―β(1st βπ€)) = 2 β§ ((2nd βπ€)β0) = π)}) = πΎ) |
13 | 6, 12 | eqtrid 2788 |
. . 3
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π = 2)) β (β―β{π€ β (ClWalksβπΊ) β£
((β―β(1st βπ€)) = 2 β§ ((2nd βπ€)β0) = π β§ ((2nd βπ€)β0) = π)}) = πΎ) |
14 | | rusgrusgr 28512 |
. . . . . . . . 9
β’ (πΊ RegUSGraph πΎ β πΊ β USGraph) |
15 | 14 | anim2i 617 |
. . . . . . . 8
β’ ((π β Fin β§ πΊ RegUSGraph πΎ) β (π β Fin β§ πΊ β USGraph)) |
16 | 15 | ancomd 462 |
. . . . . . 7
β’ ((π β Fin β§ πΊ RegUSGraph πΎ) β (πΊ β USGraph β§ π β Fin)) |
17 | 10 | isfusgr 28266 |
. . . . . . 7
β’ (πΊ β FinUSGraph β (πΊ β USGraph β§ π β Fin)) |
18 | 16, 17 | sylibr 233 |
. . . . . 6
β’ ((π β Fin β§ πΊ RegUSGraph πΎ) β πΊ β FinUSGraph) |
19 | | ne0i 4294 |
. . . . . . 7
β’ (π β π β π β β
) |
20 | 19 | adantr 481 |
. . . . . 6
β’ ((π β π β§ π = 2) β π β β
) |
21 | 10 | frusgrnn0 28519 |
. . . . . 6
β’ ((πΊ β FinUSGraph β§ πΊ RegUSGraph πΎ β§ π β β
) β πΎ β
β0) |
22 | 18, 8, 20, 21 | syl2an3an 1422 |
. . . . 5
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π = 2)) β πΎ β
β0) |
23 | 22 | nn0red 12474 |
. . . 4
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π = 2)) β πΎ β β) |
24 | | ax-1rid 11121 |
. . . 4
β’ (πΎ β β β (πΎ Β· 1) = πΎ) |
25 | 23, 24 | syl 17 |
. . 3
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π = 2)) β (πΎ Β· 1) = πΎ) |
26 | 10 | wlkl0 29311 |
. . . . . . 7
β’ (π β π β {π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)} = {β¨β
, {β¨0, πβ©}β©}) |
27 | 26 | ad2antrl 726 |
. . . . . 6
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π = 2)) β {π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)} = {β¨β
, {β¨0, πβ©}β©}) |
28 | 27 | fveq2d 6846 |
. . . . 5
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π = 2)) β (β―β{π€ β (ClWalksβπΊ) β£
((β―β(1st βπ€)) = 0 β§ ((2nd βπ€)β0) = π)}) = (β―β{β¨β
,
{β¨0, πβ©}β©})) |
29 | | opex 5421 |
. . . . . 6
β’
β¨β
, {β¨0, πβ©}β© β V |
30 | | hashsng 14269 |
. . . . . 6
β’
(β¨β
, {β¨0, πβ©}β© β V β
(β―β{β¨β
, {β¨0, πβ©}β©}) = 1) |
31 | 29, 30 | ax-mp 5 |
. . . . 5
β’
(β―β{β¨β
, {β¨0, πβ©}β©}) = 1 |
32 | 28, 31 | eqtr2di 2793 |
. . . 4
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π = 2)) β 1 = (β―β{π€ β (ClWalksβπΊ) β£
((β―β(1st βπ€)) = 0 β§ ((2nd βπ€)β0) = π)})) |
33 | 32 | oveq2d 7373 |
. . 3
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π = 2)) β (πΎ Β· 1) = (πΎ Β· (β―β{π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)}))) |
34 | 13, 25, 33 | 3eqtr2d 2782 |
. 2
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π = 2)) β (β―β{π€ β (ClWalksβπΊ) β£
((β―β(1st βπ€)) = 2 β§ ((2nd βπ€)β0) = π β§ ((2nd βπ€)β0) = π)}) = (πΎ Β· (β―β{π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)}))) |
35 | | numclwlk1.c |
. . . . . 6
β’ πΆ = {π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = π β§ ((2nd
βπ€)β0) = π β§ ((2nd
βπ€)β(π β 2)) = π)} |
36 | | eqeq2 2748 |
. . . . . . . 8
β’ (π = 2 β
((β―β(1st βπ€)) = π β (β―β(1st
βπ€)) =
2)) |
37 | | oveq1 7364 |
. . . . . . . . . 10
β’ (π = 2 β (π β 2) = (2 β
2)) |
38 | | 2cn 12228 |
. . . . . . . . . . 11
β’ 2 β
β |
39 | 38 | subidi 11472 |
. . . . . . . . . 10
β’ (2
β 2) = 0 |
40 | 37, 39 | eqtrdi 2792 |
. . . . . . . . 9
β’ (π = 2 β (π β 2) = 0) |
41 | 40 | fveqeq2d 6850 |
. . . . . . . 8
β’ (π = 2 β (((2nd
βπ€)β(π β 2)) = π β ((2nd βπ€)β0) = π)) |
42 | 36, 41 | 3anbi13d 1438 |
. . . . . . 7
β’ (π = 2 β
(((β―β(1st βπ€)) = π β§ ((2nd βπ€)β0) = π β§ ((2nd βπ€)β(π β 2)) = π) β ((β―β(1st
βπ€)) = 2 β§
((2nd βπ€)β0) = π β§ ((2nd βπ€)β0) = π))) |
43 | 42 | rabbidv 3415 |
. . . . . 6
β’ (π = 2 β {π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = π β§ ((2nd
βπ€)β0) = π β§ ((2nd
βπ€)β(π β 2)) = π)} = {π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = 2 β§
((2nd βπ€)β0) = π β§ ((2nd βπ€)β0) = π)}) |
44 | 35, 43 | eqtrid 2788 |
. . . . 5
β’ (π = 2 β πΆ = {π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = 2 β§
((2nd βπ€)β0) = π β§ ((2nd βπ€)β0) = π)}) |
45 | 44 | fveq2d 6846 |
. . . 4
β’ (π = 2 β (β―βπΆ) = (β―β{π€ β (ClWalksβπΊ) β£
((β―β(1st βπ€)) = 2 β§ ((2nd βπ€)β0) = π β§ ((2nd βπ€)β0) = π)})) |
46 | | numclwlk1.f |
. . . . . . 7
β’ πΉ = {π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = (π β 2) β§
((2nd βπ€)β0) = π)} |
47 | 40 | eqeq2d 2747 |
. . . . . . . . 9
β’ (π = 2 β
((β―β(1st βπ€)) = (π β 2) β
(β―β(1st βπ€)) = 0)) |
48 | 47 | anbi1d 630 |
. . . . . . . 8
β’ (π = 2 β
(((β―β(1st βπ€)) = (π β 2) β§ ((2nd
βπ€)β0) = π) β
((β―β(1st βπ€)) = 0 β§ ((2nd βπ€)β0) = π))) |
49 | 48 | rabbidv 3415 |
. . . . . . 7
β’ (π = 2 β {π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = (π β 2) β§
((2nd βπ€)β0) = π)} = {π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)}) |
50 | 46, 49 | eqtrid 2788 |
. . . . . 6
β’ (π = 2 β πΉ = {π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)}) |
51 | 50 | fveq2d 6846 |
. . . . 5
β’ (π = 2 β (β―βπΉ) = (β―β{π€ β (ClWalksβπΊ) β£
((β―β(1st βπ€)) = 0 β§ ((2nd βπ€)β0) = π)})) |
52 | 51 | oveq2d 7373 |
. . . 4
β’ (π = 2 β (πΎ Β· (β―βπΉ)) = (πΎ Β· (β―β{π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)}))) |
53 | 45, 52 | eqeq12d 2752 |
. . 3
β’ (π = 2 β
((β―βπΆ) = (πΎ Β· (β―βπΉ)) β (β―β{π€ β (ClWalksβπΊ) β£
((β―β(1st βπ€)) = 2 β§ ((2nd βπ€)β0) = π β§ ((2nd βπ€)β0) = π)}) = (πΎ Β· (β―β{π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)})))) |
54 | 53 | ad2antll 727 |
. 2
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π = 2)) β ((β―βπΆ) = (πΎ Β· (β―βπΉ)) β (β―β{π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = 2 β§
((2nd βπ€)β0) = π β§ ((2nd βπ€)β0) = π)}) = (πΎ Β· (β―β{π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)})))) |
55 | 34, 54 | mpbird 256 |
1
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π = 2)) β (β―βπΆ) = (πΎ Β· (β―βπΉ))) |