Step | Hyp | Ref
| Expression |
1 | | eleq1 2822 |
. . . . . . . . . 10
β’
((β―βπ) =
π β
((β―βπ) β
β β π β
β)) |
2 | | len0nnbi 14448 |
. . . . . . . . . . 11
β’ (π β Word π β (π β β
β (β―βπ) β
β)) |
3 | 2 | biimprcd 250 |
. . . . . . . . . 10
β’
((β―βπ)
β β β (π
β Word π β π β β
)) |
4 | 1, 3 | syl6bir 254 |
. . . . . . . . 9
β’
((β―βπ) =
π β (π β β β (π β Word π β π β β
))) |
5 | 4 | impcom 409 |
. . . . . . . 8
β’ ((π β β β§
(β―βπ) = π) β (π β Word π β π β β
)) |
6 | 5 | imp 408 |
. . . . . . 7
β’ (((π β β β§
(β―βπ) = π) β§ π β Word π) β π β β
) |
7 | 6 | biantrurd 534 |
. . . . . 6
β’ (((π β β β§
(β―βπ) = π) β§ π β Word π) β ((βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β (π β β
β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)))) |
8 | 7 | bicomd 222 |
. . . . 5
β’ (((π β β β§
(β―βπ) = π) β§ π β Word π) β ((π β β
β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) β (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ))) |
9 | 8 | pm5.32da 580 |
. . . 4
β’ ((π β β β§
(β―βπ) = π) β ((π β Word π β§ (π β β
β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ))) β (π β Word π β§ (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)))) |
10 | 9 | ex 414 |
. . 3
β’ (π β β β
((β―βπ) = π β ((π β Word π β§ (π β β
β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ))) β (π β Word π β§ (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ))))) |
11 | 10 | pm5.32rd 579 |
. 2
β’ (π β β β (((π β Word π β§ (π β β
β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ))) β§ (β―βπ) = π) β ((π β Word π β§ (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) β§ (β―βπ) = π))) |
12 | | isclwwlkn 29020 |
. . 3
β’ (π β (π ClWWalksN πΊ) β (π β (ClWWalksβπΊ) β§ (β―βπ) = π)) |
13 | | isclwwlknx.v |
. . . . . 6
β’ π = (VtxβπΊ) |
14 | | isclwwlknx.e |
. . . . . 6
β’ πΈ = (EdgβπΊ) |
15 | 13, 14 | isclwwlk 28977 |
. . . . 5
β’ (π β (ClWWalksβπΊ) β ((π β Word π β§ π β β
) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) |
16 | | 3anass 1096 |
. . . . . 6
β’ (((π β Word π β§ π β β
) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β ((π β Word π β§ π β β
) β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ))) |
17 | | anass 470 |
. . . . . 6
β’ (((π β Word π β§ π β β
) β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) β (π β Word π β§ (π β β
β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)))) |
18 | 16, 17 | bitri 275 |
. . . . 5
β’ (((π β Word π β§ π β β
) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β (π β Word π β§ (π β β
β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)))) |
19 | 15, 18 | bitri 275 |
. . . 4
β’ (π β (ClWWalksβπΊ) β (π β Word π β§ (π β β
β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)))) |
20 | 19 | anbi1i 625 |
. . 3
β’ ((π β (ClWWalksβπΊ) β§ (β―βπ) = π) β ((π β Word π β§ (π β β
β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ))) β§ (β―βπ) = π)) |
21 | 12, 20 | bitri 275 |
. 2
β’ (π β (π ClWWalksN πΊ) β ((π β Word π β§ (π β β
β§ (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ))) β§ (β―βπ) = π)) |
22 | | 3anass 1096 |
. . 3
β’ ((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β (π β Word π β§ (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ))) |
23 | 22 | anbi1i 625 |
. 2
β’ (((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = π) β ((π β Word π β§ (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) β§ (β―βπ) = π)) |
24 | 11, 21, 23 | 3bitr4g 314 |
1
β’ (π β β β (π β (π ClWWalksN πΊ) β ((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = π))) |