Step | Hyp | Ref
| Expression |
1 | | df-br 5150 |
. . 3
β’ (πΉ(WalksβπΊ)π β β¨πΉ, πβ© β (WalksβπΊ)) |
2 | | wksfval.v |
. . . . . 6
β’ π = (VtxβπΊ) |
3 | | wksfval.i |
. . . . . 6
β’ πΌ = (iEdgβπΊ) |
4 | 2, 3 | wksfval 28866 |
. . . . 5
β’ (πΊ β π β (WalksβπΊ) = {β¨π, πβ© β£ (π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πβπ))))}) |
5 | 4 | 3ad2ant1 1134 |
. . . 4
β’ ((πΊ β π β§ πΉ β π β§ π β π) β (WalksβπΊ) = {β¨π, πβ© β£ (π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πβπ))))}) |
6 | 5 | eleq2d 2820 |
. . 3
β’ ((πΊ β π β§ πΉ β π β§ π β π) β (β¨πΉ, πβ© β (WalksβπΊ) β β¨πΉ, πβ© β {β¨π, πβ© β£ (π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πβπ))))})) |
7 | 1, 6 | bitrid 283 |
. 2
β’ ((πΊ β π β§ πΉ β π β§ π β π) β (πΉ(WalksβπΊ)π β β¨πΉ, πβ© β {β¨π, πβ© β£ (π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πβπ))))})) |
8 | | eleq1 2822 |
. . . . . 6
β’ (π = πΉ β (π β Word dom πΌ β πΉ β Word dom πΌ)) |
9 | 8 | adantr 482 |
. . . . 5
β’ ((π = πΉ β§ π = π) β (π β Word dom πΌ β πΉ β Word dom πΌ)) |
10 | | simpr 486 |
. . . . . 6
β’ ((π = πΉ β§ π = π) β π = π) |
11 | | fveq2 6892 |
. . . . . . . 8
β’ (π = πΉ β (β―βπ) = (β―βπΉ)) |
12 | 11 | oveq2d 7425 |
. . . . . . 7
β’ (π = πΉ β (0...(β―βπ)) = (0...(β―βπΉ))) |
13 | 12 | adantr 482 |
. . . . . 6
β’ ((π = πΉ β§ π = π) β (0...(β―βπ)) = (0...(β―βπΉ))) |
14 | 10, 13 | feq12d 6706 |
. . . . 5
β’ ((π = πΉ β§ π = π) β (π:(0...(β―βπ))βΆπ β π:(0...(β―βπΉ))βΆπ)) |
15 | 11 | oveq2d 7425 |
. . . . . . 7
β’ (π = πΉ β (0..^(β―βπ)) = (0..^(β―βπΉ))) |
16 | 15 | adantr 482 |
. . . . . 6
β’ ((π = πΉ β§ π = π) β (0..^(β―βπ)) = (0..^(β―βπΉ))) |
17 | | fveq1 6891 |
. . . . . . . . 9
β’ (π = π β (πβπ) = (πβπ)) |
18 | | fveq1 6891 |
. . . . . . . . 9
β’ (π = π β (πβ(π + 1)) = (πβ(π + 1))) |
19 | 17, 18 | eqeq12d 2749 |
. . . . . . . 8
β’ (π = π β ((πβπ) = (πβ(π + 1)) β (πβπ) = (πβ(π + 1)))) |
20 | 19 | adantl 483 |
. . . . . . 7
β’ ((π = πΉ β§ π = π) β ((πβπ) = (πβ(π + 1)) β (πβπ) = (πβ(π + 1)))) |
21 | | fveq1 6891 |
. . . . . . . . 9
β’ (π = πΉ β (πβπ) = (πΉβπ)) |
22 | 21 | fveq2d 6896 |
. . . . . . . 8
β’ (π = πΉ β (πΌβ(πβπ)) = (πΌβ(πΉβπ))) |
23 | 17 | sneqd 4641 |
. . . . . . . 8
β’ (π = π β {(πβπ)} = {(πβπ)}) |
24 | 22, 23 | eqeqan12d 2747 |
. . . . . . 7
β’ ((π = πΉ β§ π = π) β ((πΌβ(πβπ)) = {(πβπ)} β (πΌβ(πΉβπ)) = {(πβπ)})) |
25 | 17, 18 | preq12d 4746 |
. . . . . . . . 9
β’ (π = π β {(πβπ), (πβ(π + 1))} = {(πβπ), (πβ(π + 1))}) |
26 | 25 | adantl 483 |
. . . . . . . 8
β’ ((π = πΉ β§ π = π) β {(πβπ), (πβ(π + 1))} = {(πβπ), (πβ(π + 1))}) |
27 | 22 | adantr 482 |
. . . . . . . 8
β’ ((π = πΉ β§ π = π) β (πΌβ(πβπ)) = (πΌβ(πΉβπ))) |
28 | 26, 27 | sseq12d 4016 |
. . . . . . 7
β’ ((π = πΉ β§ π = π) β ({(πβπ), (πβ(π + 1))} β (πΌβ(πβπ)) β {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) |
29 | 20, 24, 28 | ifpbi123d 1079 |
. . . . . 6
β’ ((π = πΉ β§ π = π) β (if-((πβπ) = (πβ(π + 1)), (πΌβ(πβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πβπ))) β if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))))) |
30 | 16, 29 | raleqbidv 3343 |
. . . . 5
β’ ((π = πΉ β§ π = π) β (βπ β (0..^(β―βπ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πβπ))) β βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))))) |
31 | 9, 14, 30 | 3anbi123d 1437 |
. . . 4
β’ ((π = πΉ β§ π = π) β ((π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πβπ)))) β (πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))))) |
32 | 31 | opelopabga 5534 |
. . 3
β’ ((πΉ β π β§ π β π) β (β¨πΉ, πβ© β {β¨π, πβ© β£ (π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πβπ))))} β (πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))))) |
33 | 32 | 3adant1 1131 |
. 2
β’ ((πΊ β π β§ πΉ β π β§ π β π) β (β¨πΉ, πβ© β {β¨π, πβ© β£ (π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πβπ))))} β (πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))))) |
34 | 7, 33 | bitrd 279 |
1
β’ ((πΊ β π β§ πΉ β π β§ π β π) β (πΉ(WalksβπΊ)π β (πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))))) |