Step | Hyp | Ref
| Expression |
1 | | isclwwlknx.v |
. . . 4
β’ π = (VtxβπΊ) |
2 | 1 | clwwlknbp 29021 |
. . 3
β’ (π β (π ClWWalksN πΊ) β (π β Word π β§ (β―βπ) = π)) |
3 | | simpr 486 |
. . . 4
β’ ((π β (π ClWWalksN πΊ) β§ (π β Word π β§ (β―βπ) = π)) β (π β Word π β§ (β―βπ) = π)) |
4 | | clwwlknnn 29019 |
. . . . . . 7
β’ (π β (π ClWWalksN πΊ) β π β β) |
5 | | isclwwlknx.e |
. . . . . . . . 9
β’ πΈ = (EdgβπΊ) |
6 | 1, 5 | isclwwlknx 29022 |
. . . . . . . 8
β’ (π β β β (π β (π ClWWalksN πΊ) β ((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = π))) |
7 | | 3simpc 1151 |
. . . . . . . . 9
β’ ((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) |
8 | 7 | adantr 482 |
. . . . . . . 8
β’ (((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = π) β (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) |
9 | 6, 8 | syl6bi 253 |
. . . . . . 7
β’ (π β β β (π β (π ClWWalksN πΊ) β (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ))) |
10 | 4, 9 | mpcom 38 |
. . . . . 6
β’ (π β (π ClWWalksN πΊ) β (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) |
11 | 10 | adantr 482 |
. . . . 5
β’ ((π β (π ClWWalksN πΊ) β§ (π β Word π β§ (β―βπ) = π)) β (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) |
12 | | oveq1 7369 |
. . . . . . . . 9
β’
((β―βπ) =
π β
((β―βπ) β
1) = (π β
1)) |
13 | 12 | oveq2d 7378 |
. . . . . . . 8
β’
((β―βπ) =
π β
(0..^((β―βπ)
β 1)) = (0..^(π
β 1))) |
14 | 13 | raleqdv 3316 |
. . . . . . 7
β’
((β―βπ) =
π β (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β πΈ)) |
15 | 14 | anbi1d 631 |
. . . . . 6
β’
((β―βπ) =
π β ((βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ))) |
16 | 15 | ad2antll 728 |
. . . . 5
β’ ((π β (π ClWWalksN πΊ) β§ (π β Word π β§ (β―βπ) = π)) β ((βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ))) |
17 | 11, 16 | mpbid 231 |
. . . 4
β’ ((π β (π ClWWalksN πΊ) β§ (π β Word π β§ (β―βπ) = π)) β (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) |
18 | 3, 17 | jca 513 |
. . 3
β’ ((π β (π ClWWalksN πΊ) β§ (π β Word π β§ (β―βπ) = π)) β ((π β Word π β§ (β―βπ) = π) β§ (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ))) |
19 | 2, 18 | mpdan 686 |
. 2
β’ (π β (π ClWWalksN πΊ) β ((π β Word π β§ (β―βπ) = π) β§ (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ))) |
20 | | 3anass 1096 |
. 2
β’ (((π β Word π β§ (β―βπ) = π) β§ βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β ((π β Word π β§ (β―βπ) = π) β§ (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ))) |
21 | 19, 20 | sylibr 233 |
1
β’ (π β (π ClWWalksN πΊ) β ((π β Word π β§ (β―βπ) = π) β§ βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) |