Step | Hyp | Ref
| Expression |
1 | | clwwlknnn 29026 |
. 2
β’ (π β (π ClWWalksN πΊ) β π β β) |
2 | | idd 24 |
. . . . . . . . . 10
β’ (π β β β (π β Word (VtxβπΊ) β π β Word (VtxβπΊ))) |
3 | | idd 24 |
. . . . . . . . . 10
β’ (π β β β
(βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
4 | | nncn 12169 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β) |
5 | | npcan1 11588 |
. . . . . . . . . . . . . 14
β’ (π β β β ((π β 1) + 1) = π) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β β β ((π β 1) + 1) = π) |
7 | 6 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ (π β β β π = ((π β 1) + 1)) |
8 | 7 | eqeq2d 2744 |
. . . . . . . . . . 11
β’ (π β β β
((β―βπ) = π β (β―βπ) = ((π β 1) + 1))) |
9 | 8 | biimpd 228 |
. . . . . . . . . 10
β’ (π β β β
((β―βπ) = π β (β―βπ) = ((π β 1) + 1))) |
10 | 2, 3, 9 | 3anim123d 1444 |
. . . . . . . . 9
β’ (π β β β ((π β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ (β―βπ) = π) β (π β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ (β―βπ) = ((π β 1) + 1)))) |
11 | 10 | com12 32 |
. . . . . . . 8
β’ ((π β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ (β―βπ) = π) β (π β β β (π β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ (β―βπ) = ((π β 1) + 1)))) |
12 | 11 | 3exp 1120 |
. . . . . . 7
β’ (π β Word (VtxβπΊ) β (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β ((β―βπ) = π β (π β β β (π β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ (β―βπ) = ((π β 1) + 1)))))) |
13 | 12 | a1dd 50 |
. . . . . 6
β’ (π β Word (VtxβπΊ) β (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β ({(lastSβπ), (πβ0)} β (EdgβπΊ) β ((β―βπ) = π β (π β β β (π β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ (β―βπ) = ((π β 1) + 1))))))) |
14 | 13 | adantr 482 |
. . . . 5
β’ ((π β Word (VtxβπΊ) β§ π β β
) β (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β ({(lastSβπ), (πβ0)} β (EdgβπΊ) β ((β―βπ) = π β (π β β β (π β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ (β―βπ) = ((π β 1) + 1))))))) |
15 | 14 | 3imp1 1348 |
. . . 4
β’ ((((π β Word (VtxβπΊ) β§ π β β
) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = π) β (π β β β (π β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ (β―βπ) = ((π β 1) + 1)))) |
16 | 15 | com12 32 |
. . 3
β’ (π β β β ((((π β Word (VtxβπΊ) β§ π β β
) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = π) β (π β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ (β―βπ) = ((π β 1) + 1)))) |
17 | | isclwwlkn 29020 |
. . . . 5
β’ (π β (π ClWWalksN πΊ) β (π β (ClWWalksβπΊ) β§ (β―βπ) = π)) |
18 | 17 | a1i 11 |
. . . 4
β’ (π β β β (π β (π ClWWalksN πΊ) β (π β (ClWWalksβπΊ) β§ (β―βπ) = π))) |
19 | | eqid 2733 |
. . . . . 6
β’
(VtxβπΊ) =
(VtxβπΊ) |
20 | | eqid 2733 |
. . . . . 6
β’
(EdgβπΊ) =
(EdgβπΊ) |
21 | 19, 20 | isclwwlk 28977 |
. . . . 5
β’ (π β (ClWWalksβπΊ) β ((π β Word (VtxβπΊ) β§ π β β
) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) |
22 | 21 | anbi1i 625 |
. . . 4
β’ ((π β (ClWWalksβπΊ) β§ (β―βπ) = π) β (((π β Word (VtxβπΊ) β§ π β β
) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = π)) |
23 | 18, 22 | bitrdi 287 |
. . 3
β’ (π β β β (π β (π ClWWalksN πΊ) β (((π β Word (VtxβπΊ) β§ π β β
) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = π))) |
24 | | nnm1nn0 12462 |
. . . 4
β’ (π β β β (π β 1) β
β0) |
25 | 19, 20 | iswwlksnx 28834 |
. . . 4
β’ ((π β 1) β
β0 β (π β ((π β 1) WWalksN πΊ) β (π β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ (β―βπ) = ((π β 1) + 1)))) |
26 | 24, 25 | syl 17 |
. . 3
β’ (π β β β (π β ((π β 1) WWalksN πΊ) β (π β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ (β―βπ) = ((π β 1) + 1)))) |
27 | 16, 23, 26 | 3imtr4d 294 |
. 2
β’ (π β β β (π β (π ClWWalksN πΊ) β π β ((π β 1) WWalksN πΊ))) |
28 | 1, 27 | mpcom 38 |
1
β’ (π β (π ClWWalksN πΊ) β π β ((π β 1) WWalksN πΊ)) |