Step | Hyp | Ref
| Expression |
1 | | upgr2wlk.v |
. . . 4
β’ π = (VtxβπΊ) |
2 | | upgr2wlk.i |
. . . 4
β’ πΌ = (iEdgβπΊ) |
3 | 1, 2 | upgriswlk 28936 |
. . 3
β’ (πΊ β UPGraph β (πΉ(WalksβπΊ)π β (πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) |
4 | 3 | anbi1d 630 |
. 2
β’ (πΊ β UPGraph β ((πΉ(WalksβπΊ)π β§ (β―βπΉ) = 2) β ((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) β§ (β―βπΉ) = 2))) |
5 | | iswrdb 14472 |
. . . . . . . . 9
β’ (πΉ β Word dom πΌ β πΉ:(0..^(β―βπΉ))βΆdom πΌ) |
6 | | oveq2 7419 |
. . . . . . . . . 10
β’
((β―βπΉ) =
2 β (0..^(β―βπΉ)) = (0..^2)) |
7 | 6 | feq2d 6703 |
. . . . . . . . 9
β’
((β―βπΉ) =
2 β (πΉ:(0..^(β―βπΉ))βΆdom πΌ β πΉ:(0..^2)βΆdom πΌ)) |
8 | 5, 7 | bitrid 282 |
. . . . . . . 8
β’
((β―βπΉ) =
2 β (πΉ β Word dom
πΌ β πΉ:(0..^2)βΆdom πΌ)) |
9 | | oveq2 7419 |
. . . . . . . . 9
β’
((β―βπΉ) =
2 β (0...(β―βπΉ)) = (0...2)) |
10 | 9 | feq2d 6703 |
. . . . . . . 8
β’
((β―βπΉ) =
2 β (π:(0...(β―βπΉ))βΆπ β π:(0...2)βΆπ)) |
11 | | fzo0to2pr 13719 |
. . . . . . . . . . 11
β’ (0..^2) =
{0, 1} |
12 | 6, 11 | eqtrdi 2788 |
. . . . . . . . . 10
β’
((β―βπΉ) =
2 β (0..^(β―βπΉ)) = {0, 1}) |
13 | 12 | raleqdv 3325 |
. . . . . . . . 9
β’
((β―βπΉ) =
2 β (βπ β
(0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β βπ β {0, 1} (πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
14 | | 2wlklem 28962 |
. . . . . . . . 9
β’
(βπ β
{0, 1} (πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) |
15 | 13, 14 | bitrdi 286 |
. . . . . . . 8
β’
((β―βπΉ) =
2 β (βπ β
(0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}))) |
16 | 8, 10, 15 | 3anbi123d 1436 |
. . . . . . 7
β’
((β―βπΉ) =
2 β ((πΉ β Word
dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) β (πΉ:(0..^2)βΆdom πΌ β§ π:(0...2)βΆπ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})))) |
17 | 16 | adantl 482 |
. . . . . 6
β’ ((πΊ β UPGraph β§
(β―βπΉ) = 2)
β ((πΉ β Word dom
πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) β (πΉ:(0..^2)βΆdom πΌ β§ π:(0...2)βΆπ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})))) |
18 | | 3anass 1095 |
. . . . . 6
β’ ((πΉ:(0..^2)βΆdom πΌ β§ π:(0...2)βΆπ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β (πΉ:(0..^2)βΆdom πΌ β§ (π:(0...2)βΆπ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})))) |
19 | 17, 18 | bitrdi 286 |
. . . . 5
β’ ((πΊ β UPGraph β§
(β―βπΉ) = 2)
β ((πΉ β Word dom
πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) β (πΉ:(0..^2)βΆdom πΌ β§ (π:(0...2)βΆπ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}))))) |
20 | 19 | ex 413 |
. . . 4
β’ (πΊ β UPGraph β
((β―βπΉ) = 2
β ((πΉ β Word dom
πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) β (πΉ:(0..^2)βΆdom πΌ β§ (π:(0...2)βΆπ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})))))) |
21 | 20 | pm5.32rd 578 |
. . 3
β’ (πΊ β UPGraph β (((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) β§ (β―βπΉ) = 2) β ((πΉ:(0..^2)βΆdom πΌ β§ (π:(0...2)βΆπ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}))) β§ (β―βπΉ) = 2))) |
22 | | 3anass 1095 |
. . . 4
β’ (((πΉ:(0..^2)βΆdom πΌ β§ (β―βπΉ) = 2) β§ π:(0...2)βΆπ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β ((πΉ:(0..^2)βΆdom πΌ β§ (β―βπΉ) = 2) β§ (π:(0...2)βΆπ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})))) |
23 | | an32 644 |
. . . 4
β’ (((πΉ:(0..^2)βΆdom πΌ β§ (β―βπΉ) = 2) β§ (π:(0...2)βΆπ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}))) β ((πΉ:(0..^2)βΆdom πΌ β§ (π:(0...2)βΆπ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}))) β§ (β―βπΉ) = 2)) |
24 | 22, 23 | bitri 274 |
. . 3
β’ (((πΉ:(0..^2)βΆdom πΌ β§ (β―βπΉ) = 2) β§ π:(0...2)βΆπ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β ((πΉ:(0..^2)βΆdom πΌ β§ (π:(0...2)βΆπ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)}))) β§ (β―βπΉ) = 2)) |
25 | 21, 24 | bitr4di 288 |
. 2
β’ (πΊ β UPGraph β (((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) β§ (β―βπΉ) = 2) β ((πΉ:(0..^2)βΆdom πΌ β§ (β―βπΉ) = 2) β§ π:(0...2)βΆπ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})))) |
26 | | 2nn0 12491 |
. . . . . . 7
β’ 2 β
β0 |
27 | | fnfzo0hash 14411 |
. . . . . . 7
β’ ((2
β β0 β§ πΉ:(0..^2)βΆdom πΌ) β (β―βπΉ) = 2) |
28 | 26, 27 | mpan 688 |
. . . . . 6
β’ (πΉ:(0..^2)βΆdom πΌ β (β―βπΉ) = 2) |
29 | 28 | pm4.71i 560 |
. . . . 5
β’ (πΉ:(0..^2)βΆdom πΌ β (πΉ:(0..^2)βΆdom πΌ β§ (β―βπΉ) = 2)) |
30 | 29 | bicomi 223 |
. . . 4
β’ ((πΉ:(0..^2)βΆdom πΌ β§ (β―βπΉ) = 2) β πΉ:(0..^2)βΆdom πΌ) |
31 | 30 | a1i 11 |
. . 3
β’ (πΊ β UPGraph β ((πΉ:(0..^2)βΆdom πΌ β§ (β―βπΉ) = 2) β πΉ:(0..^2)βΆdom πΌ)) |
32 | 31 | 3anbi1d 1440 |
. 2
β’ (πΊ β UPGraph β (((πΉ:(0..^2)βΆdom πΌ β§ (β―βπΉ) = 2) β§ π:(0...2)βΆπ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})) β (πΉ:(0..^2)βΆdom πΌ β§ π:(0...2)βΆπ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})))) |
33 | 4, 25, 32 | 3bitrd 304 |
1
β’ (πΊ β UPGraph β ((πΉ(WalksβπΊ)π β§ (β―βπΉ) = 2) β (πΉ:(0..^2)βΆdom πΌ β§ π:(0...2)βΆπ β§ ((πΌβ(πΉβ0)) = {(πβ0), (πβ1)} β§ (πΌβ(πΉβ1)) = {(πβ1), (πβ2)})))) |