Step | Hyp | Ref
| Expression |
1 | | wlkiswwlks2lem.f |
. . . 4
β’ πΉ = (π₯ β (0..^((β―βπ) β 1)) β¦ (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))})) |
2 | 1 | wlkiswwlks2lem1 29123 |
. . 3
β’ ((π β Word π β§ 1 β€ (β―βπ)) β (β―βπΉ) = ((β―βπ) β 1)) |
3 | 2 | 3adant1 1131 |
. 2
β’ ((πΊ β USPGraph β§ π β Word π β§ 1 β€ (β―βπ)) β (β―βπΉ) = ((β―βπ) β 1)) |
4 | | lencl 14483 |
. . . . . . . . . 10
β’ (π β Word π β (β―βπ) β
β0) |
5 | 4 | 3ad2ant2 1135 |
. . . . . . . . 9
β’ ((πΊ β USPGraph β§ π β Word π β§ 1 β€ (β―βπ)) β (β―βπ) β
β0) |
6 | 1 | wlkiswwlks2lem2 29124 |
. . . . . . . . 9
β’
(((β―βπ)
β β0 β§ π β (0..^((β―βπ) β 1))) β (πΉβπ) = (β‘πΈβ{(πβπ), (πβ(π + 1))})) |
7 | 5, 6 | sylan 581 |
. . . . . . . 8
β’ (((πΊ β USPGraph β§ π β Word π β§ 1 β€ (β―βπ)) β§ π β (0..^((β―βπ) β 1))) β (πΉβπ) = (β‘πΈβ{(πβπ), (πβ(π + 1))})) |
8 | 7 | adantr 482 |
. . . . . . 7
β’ ((((πΊ β USPGraph β§ π β Word π β§ 1 β€ (β―βπ)) β§ π β (0..^((β―βπ) β 1))) β§ {(πβπ), (πβ(π + 1))} β ran πΈ) β (πΉβπ) = (β‘πΈβ{(πβπ), (πβ(π + 1))})) |
9 | 8 | fveq2d 6896 |
. . . . . 6
β’ ((((πΊ β USPGraph β§ π β Word π β§ 1 β€ (β―βπ)) β§ π β (0..^((β―βπ) β 1))) β§ {(πβπ), (πβ(π + 1))} β ran πΈ) β (πΈβ(πΉβπ)) = (πΈβ(β‘πΈβ{(πβπ), (πβ(π + 1))}))) |
10 | | wlkiswwlks2lem.e |
. . . . . . . . . . 11
β’ πΈ = (iEdgβπΊ) |
11 | 10 | uspgrf1oedg 28433 |
. . . . . . . . . 10
β’ (πΊ β USPGraph β πΈ:dom πΈβ1-1-ontoβ(EdgβπΊ)) |
12 | 10 | rneqi 5937 |
. . . . . . . . . . . 12
β’ ran πΈ = ran (iEdgβπΊ) |
13 | | edgval 28309 |
. . . . . . . . . . . 12
β’
(EdgβπΊ) = ran
(iEdgβπΊ) |
14 | 12, 13 | eqtr4i 2764 |
. . . . . . . . . . 11
β’ ran πΈ = (EdgβπΊ) |
15 | | f1oeq3 6824 |
. . . . . . . . . . 11
β’ (ran
πΈ = (EdgβπΊ) β (πΈ:dom πΈβ1-1-ontoβran
πΈ β πΈ:dom πΈβ1-1-ontoβ(EdgβπΊ))) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . 10
β’ (πΈ:dom πΈβ1-1-ontoβran
πΈ β πΈ:dom πΈβ1-1-ontoβ(EdgβπΊ)) |
17 | 11, 16 | sylibr 233 |
. . . . . . . . 9
β’ (πΊ β USPGraph β πΈ:dom πΈβ1-1-ontoβran
πΈ) |
18 | 17 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((πΊ β USPGraph β§ π β Word π β§ 1 β€ (β―βπ)) β πΈ:dom πΈβ1-1-ontoβran
πΈ) |
19 | 18 | adantr 482 |
. . . . . . 7
β’ (((πΊ β USPGraph β§ π β Word π β§ 1 β€ (β―βπ)) β§ π β (0..^((β―βπ) β 1))) β πΈ:dom πΈβ1-1-ontoβran
πΈ) |
20 | | f1ocnvfv2 7275 |
. . . . . . 7
β’ ((πΈ:dom πΈβ1-1-ontoβran
πΈ β§ {(πβπ), (πβ(π + 1))} β ran πΈ) β (πΈβ(β‘πΈβ{(πβπ), (πβ(π + 1))})) = {(πβπ), (πβ(π + 1))}) |
21 | 19, 20 | sylan 581 |
. . . . . 6
β’ ((((πΊ β USPGraph β§ π β Word π β§ 1 β€ (β―βπ)) β§ π β (0..^((β―βπ) β 1))) β§ {(πβπ), (πβ(π + 1))} β ran πΈ) β (πΈβ(β‘πΈβ{(πβπ), (πβ(π + 1))})) = {(πβπ), (πβ(π + 1))}) |
22 | 9, 21 | eqtrd 2773 |
. . . . 5
β’ ((((πΊ β USPGraph β§ π β Word π β§ 1 β€ (β―βπ)) β§ π β (0..^((β―βπ) β 1))) β§ {(πβπ), (πβ(π + 1))} β ran πΈ) β (πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) |
23 | 22 | ex 414 |
. . . 4
β’ (((πΊ β USPGraph β§ π β Word π β§ 1 β€ (β―βπ)) β§ π β (0..^((β―βπ) β 1))) β ({(πβπ), (πβ(π + 1))} β ran πΈ β (πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
24 | 23 | ralimdva 3168 |
. . 3
β’ ((πΊ β USPGraph β§ π β Word π β§ 1 β€ (β―βπ)) β (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β βπ β (0..^((β―βπ) β 1))(πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
25 | | oveq2 7417 |
. . . . 5
β’
((β―βπΉ) =
((β―βπ) β
1) β (0..^(β―βπΉ)) = (0..^((β―βπ) β 1))) |
26 | 25 | raleqdv 3326 |
. . . 4
β’
((β―βπΉ) =
((β―βπ) β
1) β (βπ β
(0..^(β―βπΉ))(πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β βπ β (0..^((β―βπ) β 1))(πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
27 | 26 | imbi2d 341 |
. . 3
β’
((β―βπΉ) =
((β―βπ) β
1) β ((βπ
β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β βπ β (0..^(β―βπΉ))(πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) β (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β βπ β (0..^((β―βπ) β 1))(πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) |
28 | 24, 27 | imbitrrid 245 |
. 2
β’
((β―βπΉ) =
((β―βπ) β
1) β ((πΊ β
USPGraph β§ π β
Word π β§ 1 β€
(β―βπ)) β
(βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β βπ β (0..^(β―βπΉ))(πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) |
29 | 3, 28 | mpcom 38 |
1
β’ ((πΊ β USPGraph β§ π β Word π β§ 1 β€ (β―βπ)) β (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β βπ β (0..^(β―βπΉ))(πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |