Step | Hyp | Ref
| Expression |
1 | | df-br 5107 |
. . 3
β’ (πΉ(UPWalksβπΊ)π β β¨πΉ, πβ© β (UPWalksβπΊ)) |
2 | | upwlksfval.v |
. . . . . 6
β’ π = (VtxβπΊ) |
3 | | upwlksfval.i |
. . . . . 6
β’ πΌ = (iEdgβπΊ) |
4 | 2, 3 | upwlksfval 46123 |
. . . . 5
β’ (πΊ β π β (UPWalksβπΊ) = {β¨π, πβ© β£ (π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))})}) |
5 | 4 | 3ad2ant1 1134 |
. . . 4
β’ ((πΊ β π β§ πΉ β π β§ π β π) β (UPWalksβπΊ) = {β¨π, πβ© β£ (π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))})}) |
6 | 5 | eleq2d 2820 |
. . 3
β’ ((πΊ β π β§ πΉ β π β§ π β π) β (β¨πΉ, πβ© β (UPWalksβπΊ) β β¨πΉ, πβ© β {β¨π, πβ© β£ (π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))})})) |
7 | 1, 6 | bitrid 283 |
. 2
β’ ((πΊ β π β§ πΉ β π β§ π β π) β (πΉ(UPWalksβπΊ)π β β¨πΉ, πβ© β {β¨π, πβ© β£ (π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))})})) |
8 | | eleq1 2822 |
. . . . . 6
β’ (π = πΉ β (π β Word dom πΌ β πΉ β Word dom πΌ)) |
9 | 8 | adantr 482 |
. . . . 5
β’ ((π = πΉ β§ π = π) β (π β Word dom πΌ β πΉ β Word dom πΌ)) |
10 | | simpr 486 |
. . . . . 6
β’ ((π = πΉ β§ π = π) β π = π) |
11 | | fveq2 6843 |
. . . . . . . 8
β’ (π = πΉ β (β―βπ) = (β―βπΉ)) |
12 | 11 | oveq2d 7374 |
. . . . . . 7
β’ (π = πΉ β (0...(β―βπ)) = (0...(β―βπΉ))) |
13 | 12 | adantr 482 |
. . . . . 6
β’ ((π = πΉ β§ π = π) β (0...(β―βπ)) = (0...(β―βπΉ))) |
14 | 10, 13 | feq12d 6657 |
. . . . 5
β’ ((π = πΉ β§ π = π) β (π:(0...(β―βπ))βΆπ β π:(0...(β―βπΉ))βΆπ)) |
15 | 11 | oveq2d 7374 |
. . . . . . 7
β’ (π = πΉ β (0..^(β―βπ)) = (0..^(β―βπΉ))) |
16 | 15 | adantr 482 |
. . . . . 6
β’ ((π = πΉ β§ π = π) β (0..^(β―βπ)) = (0..^(β―βπΉ))) |
17 | | fveq1 6842 |
. . . . . . . 8
β’ (π = πΉ β (πβπ) = (πΉβπ)) |
18 | 17 | fveq2d 6847 |
. . . . . . 7
β’ (π = πΉ β (πΌβ(πβπ)) = (πΌβ(πΉβπ))) |
19 | | fveq1 6842 |
. . . . . . . 8
β’ (π = π β (πβπ) = (πβπ)) |
20 | | fveq1 6842 |
. . . . . . . 8
β’ (π = π β (πβ(π + 1)) = (πβ(π + 1))) |
21 | 19, 20 | preq12d 4703 |
. . . . . . 7
β’ (π = π β {(πβπ), (πβ(π + 1))} = {(πβπ), (πβ(π + 1))}) |
22 | 18, 21 | eqeqan12d 2747 |
. . . . . 6
β’ ((π = πΉ β§ π = π) β ((πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
23 | 16, 22 | raleqbidv 3318 |
. . . . 5
β’ ((π = πΉ β§ π = π) β (βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))} β βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
24 | 9, 14, 23 | 3anbi123d 1437 |
. . . 4
β’ ((π = πΉ β§ π = π) β ((π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β (πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) |
25 | 24 | opelopabga 5491 |
. . 3
β’ ((πΉ β π β§ π β π) β (β¨πΉ, πβ© β {β¨π, πβ© β£ (π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))})} β (πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) |
26 | 25 | 3adant1 1131 |
. 2
β’ ((πΊ β π β§ πΉ β π β§ π β π) β (β¨πΉ, πβ© β {β¨π, πβ© β£ (π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))})} β (πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) |
27 | 7, 26 | bitrd 279 |
1
β’ ((πΊ β π β§ πΉ β π β§ π β π) β (πΉ(UPWalksβπΊ)π β (πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) |