Step | Hyp | Ref
| Expression |
1 | | wwlknon 28844 |
. . . . . . 7
β’ (π€ β (π΄(2 WWalksNOn πΊ)π΅) β (π€ β (2 WWalksN πΊ) β§ (π€β0) = π΄ β§ (π€β2) = π΅)) |
2 | 1 | a1i 11 |
. . . . . 6
β’ ((πΊ β USGraph β§ π΄ β π΅) β (π€ β (π΄(2 WWalksNOn πΊ)π΅) β (π€ β (2 WWalksN πΊ) β§ (π€β0) = π΄ β§ (π€β2) = π΅))) |
3 | 2 | anbi1d 631 |
. . . . 5
β’ ((πΊ β USGraph β§ π΄ β π΅) β ((π€ β (π΄(2 WWalksNOn πΊ)π΅) β§ βπ π(π΄(SPathsOnβπΊ)π΅)π€) β ((π€ β (2 WWalksN πΊ) β§ (π€β0) = π΄ β§ (π€β2) = π΅) β§ βπ π(π΄(SPathsOnβπΊ)π΅)π€))) |
4 | | 3anass 1096 |
. . . . . . 7
β’ ((π€ β (2 WWalksN πΊ) β§ (π€β0) = π΄ β§ (π€β2) = π΅) β (π€ β (2 WWalksN πΊ) β§ ((π€β0) = π΄ β§ (π€β2) = π΅))) |
5 | 4 | anbi1i 625 |
. . . . . 6
β’ (((π€ β (2 WWalksN πΊ) β§ (π€β0) = π΄ β§ (π€β2) = π΅) β§ βπ π(π΄(SPathsOnβπΊ)π΅)π€) β ((π€ β (2 WWalksN πΊ) β§ ((π€β0) = π΄ β§ (π€β2) = π΅)) β§ βπ π(π΄(SPathsOnβπΊ)π΅)π€)) |
6 | | anass 470 |
. . . . . 6
β’ (((π€ β (2 WWalksN πΊ) β§ ((π€β0) = π΄ β§ (π€β2) = π΅)) β§ βπ π(π΄(SPathsOnβπΊ)π΅)π€) β (π€ β (2 WWalksN πΊ) β§ (((π€β0) = π΄ β§ (π€β2) = π΅) β§ βπ π(π΄(SPathsOnβπΊ)π΅)π€))) |
7 | 5, 6 | bitri 275 |
. . . . 5
β’ (((π€ β (2 WWalksN πΊ) β§ (π€β0) = π΄ β§ (π€β2) = π΅) β§ βπ π(π΄(SPathsOnβπΊ)π΅)π€) β (π€ β (2 WWalksN πΊ) β§ (((π€β0) = π΄ β§ (π€β2) = π΅) β§ βπ π(π΄(SPathsOnβπΊ)π΅)π€))) |
8 | 3, 7 | bitrdi 287 |
. . . 4
β’ ((πΊ β USGraph β§ π΄ β π΅) β ((π€ β (π΄(2 WWalksNOn πΊ)π΅) β§ βπ π(π΄(SPathsOnβπΊ)π΅)π€) β (π€ β (2 WWalksN πΊ) β§ (((π€β0) = π΄ β§ (π€β2) = π΅) β§ βπ π(π΄(SPathsOnβπΊ)π΅)π€)))) |
9 | 8 | rabbidva2 3412 |
. . 3
β’ ((πΊ β USGraph β§ π΄ β π΅) β {π€ β (π΄(2 WWalksNOn πΊ)π΅) β£ βπ π(π΄(SPathsOnβπΊ)π΅)π€} = {π€ β (2 WWalksN πΊ) β£ (((π€β0) = π΄ β§ (π€β2) = π΅) β§ βπ π(π΄(SPathsOnβπΊ)π΅)π€)}) |
10 | | usgrupgr 28175 |
. . . . . . . . . . 11
β’ (πΊ β USGraph β πΊ β
UPGraph) |
11 | | wlklnwwlknupgr 28873 |
. . . . . . . . . . 11
β’ (πΊ β UPGraph β
(βπ(π(WalksβπΊ)π€ β§ (β―βπ) = 2) β π€ β (2 WWalksN πΊ))) |
12 | 10, 11 | syl 17 |
. . . . . . . . . 10
β’ (πΊ β USGraph β
(βπ(π(WalksβπΊ)π€ β§ (β―βπ) = 2) β π€ β (2 WWalksN πΊ))) |
13 | 12 | bicomd 222 |
. . . . . . . . 9
β’ (πΊ β USGraph β (π€ β (2 WWalksN πΊ) β βπ(π(WalksβπΊ)π€ β§ (β―βπ) = 2))) |
14 | 13 | adantr 482 |
. . . . . . . 8
β’ ((πΊ β USGraph β§ π΄ β π΅) β (π€ β (2 WWalksN πΊ) β βπ(π(WalksβπΊ)π€ β§ (β―βπ) = 2))) |
15 | | simprl 770 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β USGraph β§ π΄ β π΅) β§ ((π€β0) = π΄ β§ (π€β2) = π΅)) β§ (π(WalksβπΊ)π€ β§ (β―βπ) = 2)) β π(WalksβπΊ)π€) |
16 | | simprl 770 |
. . . . . . . . . . . . . . 15
β’ (((πΊ β USGraph β§ π΄ β π΅) β§ ((π€β0) = π΄ β§ (π€β2) = π΅)) β (π€β0) = π΄) |
17 | 16 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β USGraph β§ π΄ β π΅) β§ ((π€β0) = π΄ β§ (π€β2) = π΅)) β§ (π(WalksβπΊ)π€ β§ (β―βπ) = 2)) β (π€β0) = π΄) |
18 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
β’
((β―βπ) =
2 β (π€β(β―βπ)) = (π€β2)) |
19 | 18 | ad2antll 728 |
. . . . . . . . . . . . . . 15
β’ ((((πΊ β USGraph β§ π΄ β π΅) β§ ((π€β0) = π΄ β§ (π€β2) = π΅)) β§ (π(WalksβπΊ)π€ β§ (β―βπ) = 2)) β (π€β(β―βπ)) = (π€β2)) |
20 | | simprr 772 |
. . . . . . . . . . . . . . . 16
β’ (((πΊ β USGraph β§ π΄ β π΅) β§ ((π€β0) = π΄ β§ (π€β2) = π΅)) β (π€β2) = π΅) |
21 | 20 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((πΊ β USGraph β§ π΄ β π΅) β§ ((π€β0) = π΄ β§ (π€β2) = π΅)) β§ (π(WalksβπΊ)π€ β§ (β―βπ) = 2)) β (π€β2) = π΅) |
22 | 19, 21 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β USGraph β§ π΄ β π΅) β§ ((π€β0) = π΄ β§ (π€β2) = π΅)) β§ (π(WalksβπΊ)π€ β§ (β―βπ) = 2)) β (π€β(β―βπ)) = π΅) |
23 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(VtxβπΊ) =
(VtxβπΊ) |
24 | 23 | wlkp 28606 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π(WalksβπΊ)π€ β π€:(0...(β―βπ))βΆ(VtxβπΊ)) |
25 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((β―βπ) =
2 β (0...(β―βπ)) = (0...2)) |
26 | 25 | feq2d 6659 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((β―βπ) =
2 β (π€:(0...(β―βπ))βΆ(VtxβπΊ) β π€:(0...2)βΆ(VtxβπΊ))) |
27 | 24, 26 | syl5ibcom 244 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π(WalksβπΊ)π€ β ((β―βπ) = 2 β π€:(0...2)βΆ(VtxβπΊ))) |
28 | 27 | imp 408 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π(WalksβπΊ)π€ β§ (β―βπ) = 2) β π€:(0...2)βΆ(VtxβπΊ)) |
29 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€:(0...2)βΆ(VtxβπΊ) β π€:(0...2)βΆ(VtxβπΊ)) |
30 | | 2nn0 12437 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 2 β
β0 |
31 | | 0elfz 13545 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (2 β
β0 β 0 β (0...2)) |
32 | 30, 31 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€:(0...2)βΆ(VtxβπΊ) β 0 β
(0...2)) |
33 | 29, 32 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€:(0...2)βΆ(VtxβπΊ) β (π€β0) β (VtxβπΊ)) |
34 | | nn0fz0 13546 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (2 β
β0 β 2 β (0...2)) |
35 | 30, 34 | mpbi 229 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 2 β
(0...2) |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€:(0...2)βΆ(VtxβπΊ) β 2 β
(0...2)) |
37 | 29, 36 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€:(0...2)βΆ(VtxβπΊ) β (π€β2) β (VtxβπΊ)) |
38 | 33, 37 | jca 513 |
. . . . . . . . . . . . . . . . . . 19
β’ (π€:(0...2)βΆ(VtxβπΊ) β ((π€β0) β (VtxβπΊ) β§ (π€β2) β (VtxβπΊ))) |
39 | 28, 38 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π(WalksβπΊ)π€ β§ (β―βπ) = 2) β ((π€β0) β (VtxβπΊ) β§ (π€β2) β (VtxβπΊ))) |
40 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π€β0) = π΄ β ((π€β0) β (VtxβπΊ) β π΄ β (VtxβπΊ))) |
41 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π€β2) = π΅ β ((π€β2) β (VtxβπΊ) β π΅ β (VtxβπΊ))) |
42 | 40, 41 | bi2anan9 638 |
. . . . . . . . . . . . . . . . . 18
β’ (((π€β0) = π΄ β§ (π€β2) = π΅) β (((π€β0) β (VtxβπΊ) β§ (π€β2) β (VtxβπΊ)) β (π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)))) |
43 | 39, 42 | imbitrid 243 |
. . . . . . . . . . . . . . . . 17
β’ (((π€β0) = π΄ β§ (π€β2) = π΅) β ((π(WalksβπΊ)π€ β§ (β―βπ) = 2) β (π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)))) |
44 | 43 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((πΊ β USGraph β§ π΄ β π΅) β§ ((π€β0) = π΄ β§ (π€β2) = π΅)) β ((π(WalksβπΊ)π€ β§ (β―βπ) = 2) β (π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)))) |
45 | 44 | imp 408 |
. . . . . . . . . . . . . . 15
β’ ((((πΊ β USGraph β§ π΄ β π΅) β§ ((π€β0) = π΄ β§ (π€β2) = π΅)) β§ (π(WalksβπΊ)π€ β§ (β―βπ) = 2)) β (π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ))) |
46 | | vex 3452 |
. . . . . . . . . . . . . . . 16
β’ π β V |
47 | | vex 3452 |
. . . . . . . . . . . . . . . 16
β’ π€ β V |
48 | 46, 47 | pm3.2i 472 |
. . . . . . . . . . . . . . 15
β’ (π β V β§ π€ β V) |
49 | 23 | iswlkon 28647 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (π β V β§ π€ β V)) β (π(π΄(WalksOnβπΊ)π΅)π€ β (π(WalksβπΊ)π€ β§ (π€β0) = π΄ β§ (π€β(β―βπ)) = π΅))) |
50 | 45, 48, 49 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β USGraph β§ π΄ β π΅) β§ ((π€β0) = π΄ β§ (π€β2) = π΅)) β§ (π(WalksβπΊ)π€ β§ (β―βπ) = 2)) β (π(π΄(WalksOnβπΊ)π΅)π€ β (π(WalksβπΊ)π€ β§ (π€β0) = π΄ β§ (π€β(β―βπ)) = π΅))) |
51 | 15, 17, 22, 50 | mpbir3and 1343 |
. . . . . . . . . . . . 13
β’ ((((πΊ β USGraph β§ π΄ β π΅) β§ ((π€β0) = π΄ β§ (π€β2) = π΅)) β§ (π(WalksβπΊ)π€ β§ (β―βπ) = 2)) β π(π΄(WalksOnβπΊ)π΅)π€) |
52 | | simplll 774 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β USGraph β§ π΄ β π΅) β§ ((π€β0) = π΄ β§ (π€β2) = π΅)) β§ (π(WalksβπΊ)π€ β§ (β―βπ) = 2)) β πΊ β USGraph) |
53 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β USGraph β§ π΄ β π΅) β§ ((π€β0) = π΄ β§ (π€β2) = π΅)) β§ (π(WalksβπΊ)π€ β§ (β―βπ) = 2)) β (β―βπ) = 2) |
54 | | simpllr 775 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β USGraph β§ π΄ β π΅) β§ ((π€β0) = π΄ β§ (π€β2) = π΅)) β§ (π(WalksβπΊ)π€ β§ (β―βπ) = 2)) β π΄ β π΅) |
55 | | usgr2wlkspth 28749 |
. . . . . . . . . . . . . 14
β’ ((πΊ β USGraph β§
(β―βπ) = 2 β§
π΄ β π΅) β (π(π΄(WalksOnβπΊ)π΅)π€ β π(π΄(SPathsOnβπΊ)π΅)π€)) |
56 | 52, 53, 54, 55 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((((πΊ β USGraph β§ π΄ β π΅) β§ ((π€β0) = π΄ β§ (π€β2) = π΅)) β§ (π(WalksβπΊ)π€ β§ (β―βπ) = 2)) β (π(π΄(WalksOnβπΊ)π΅)π€ β π(π΄(SPathsOnβπΊ)π΅)π€)) |
57 | 51, 56 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((((πΊ β USGraph β§ π΄ β π΅) β§ ((π€β0) = π΄ β§ (π€β2) = π΅)) β§ (π(WalksβπΊ)π€ β§ (β―βπ) = 2)) β π(π΄(SPathsOnβπΊ)π΅)π€) |
58 | 57 | ex 414 |
. . . . . . . . . . 11
β’ (((πΊ β USGraph β§ π΄ β π΅) β§ ((π€β0) = π΄ β§ (π€β2) = π΅)) β ((π(WalksβπΊ)π€ β§ (β―βπ) = 2) β π(π΄(SPathsOnβπΊ)π΅)π€)) |
59 | 58 | eximdv 1921 |
. . . . . . . . . 10
β’ (((πΊ β USGraph β§ π΄ β π΅) β§ ((π€β0) = π΄ β§ (π€β2) = π΅)) β (βπ(π(WalksβπΊ)π€ β§ (β―βπ) = 2) β βπ π(π΄(SPathsOnβπΊ)π΅)π€)) |
60 | 59 | ex 414 |
. . . . . . . . 9
β’ ((πΊ β USGraph β§ π΄ β π΅) β (((π€β0) = π΄ β§ (π€β2) = π΅) β (βπ(π(WalksβπΊ)π€ β§ (β―βπ) = 2) β βπ π(π΄(SPathsOnβπΊ)π΅)π€))) |
61 | 60 | com23 86 |
. . . . . . . 8
β’ ((πΊ β USGraph β§ π΄ β π΅) β (βπ(π(WalksβπΊ)π€ β§ (β―βπ) = 2) β (((π€β0) = π΄ β§ (π€β2) = π΅) β βπ π(π΄(SPathsOnβπΊ)π΅)π€))) |
62 | 14, 61 | sylbid 239 |
. . . . . . 7
β’ ((πΊ β USGraph β§ π΄ β π΅) β (π€ β (2 WWalksN πΊ) β (((π€β0) = π΄ β§ (π€β2) = π΅) β βπ π(π΄(SPathsOnβπΊ)π΅)π€))) |
63 | 62 | imp 408 |
. . . . . 6
β’ (((πΊ β USGraph β§ π΄ β π΅) β§ π€ β (2 WWalksN πΊ)) β (((π€β0) = π΄ β§ (π€β2) = π΅) β βπ π(π΄(SPathsOnβπΊ)π΅)π€)) |
64 | 63 | pm4.71d 563 |
. . . . 5
β’ (((πΊ β USGraph β§ π΄ β π΅) β§ π€ β (2 WWalksN πΊ)) β (((π€β0) = π΄ β§ (π€β2) = π΅) β (((π€β0) = π΄ β§ (π€β2) = π΅) β§ βπ π(π΄(SPathsOnβπΊ)π΅)π€))) |
65 | 64 | bicomd 222 |
. . . 4
β’ (((πΊ β USGraph β§ π΄ β π΅) β§ π€ β (2 WWalksN πΊ)) β ((((π€β0) = π΄ β§ (π€β2) = π΅) β§ βπ π(π΄(SPathsOnβπΊ)π΅)π€) β ((π€β0) = π΄ β§ (π€β2) = π΅))) |
66 | 65 | rabbidva 3417 |
. . 3
β’ ((πΊ β USGraph β§ π΄ β π΅) β {π€ β (2 WWalksN πΊ) β£ (((π€β0) = π΄ β§ (π€β2) = π΅) β§ βπ π(π΄(SPathsOnβπΊ)π΅)π€)} = {π€ β (2 WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€β2) = π΅)}) |
67 | 9, 66 | eqtrd 2777 |
. 2
β’ ((πΊ β USGraph β§ π΄ β π΅) β {π€ β (π΄(2 WWalksNOn πΊ)π΅) β£ βπ π(π΄(SPathsOnβπΊ)π΅)π€} = {π€ β (2 WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€β2) = π΅)}) |
68 | 23 | iswspthsnon 28843 |
. 2
β’ (π΄(2 WSPathsNOn πΊ)π΅) = {π€ β (π΄(2 WWalksNOn πΊ)π΅) β£ βπ π(π΄(SPathsOnβπΊ)π΅)π€} |
69 | 23 | iswwlksnon 28840 |
. 2
β’ (π΄(2 WWalksNOn πΊ)π΅) = {π€ β (2 WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€β2) = π΅)} |
70 | 67, 68, 69 | 3eqtr4g 2802 |
1
β’ ((πΊ β USGraph β§ π΄ β π΅) β (π΄(2 WSPathsNOn πΊ)π΅) = (π΄(2 WWalksNOn πΊ)π΅)) |