Step | Hyp | Ref
| Expression |
1 | | df-clwwlk 28975 |
. . 3
β’ ClWWalks
= (π β V β¦
{π€ β Word
(Vtxβπ) β£
(π€ β β
β§
βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β (Edgβπ) β§ {(lastSβπ€), (π€β0)} β (Edgβπ))}) |
2 | | fveq2 6846 |
. . . . . 6
β’ (π = πΊ β (Vtxβπ) = (VtxβπΊ)) |
3 | | clwwlk.v |
. . . . . 6
β’ π = (VtxβπΊ) |
4 | 2, 3 | eqtr4di 2791 |
. . . . 5
β’ (π = πΊ β (Vtxβπ) = π) |
5 | | wrdeq 14433 |
. . . . 5
β’
((Vtxβπ) =
π β Word
(Vtxβπ) = Word π) |
6 | 4, 5 | syl 17 |
. . . 4
β’ (π = πΊ β Word (Vtxβπ) = Word π) |
7 | | fveq2 6846 |
. . . . . . . 8
β’ (π = πΊ β (Edgβπ) = (EdgβπΊ)) |
8 | | clwwlk.e |
. . . . . . . 8
β’ πΈ = (EdgβπΊ) |
9 | 7, 8 | eqtr4di 2791 |
. . . . . . 7
β’ (π = πΊ β (Edgβπ) = πΈ) |
10 | 9 | eleq2d 2820 |
. . . . . 6
β’ (π = πΊ β ({(π€βπ), (π€β(π + 1))} β (Edgβπ) β {(π€βπ), (π€β(π + 1))} β πΈ)) |
11 | 10 | ralbidv 3171 |
. . . . 5
β’ (π = πΊ β (βπ β (0..^((β―βπ€) β 1)){(π€βπ), (π€β(π + 1))} β (Edgβπ) β βπ β (0..^((β―βπ€) β 1)){(π€βπ), (π€β(π + 1))} β πΈ)) |
12 | 9 | eleq2d 2820 |
. . . . 5
β’ (π = πΊ β ({(lastSβπ€), (π€β0)} β (Edgβπ) β {(lastSβπ€), (π€β0)} β πΈ)) |
13 | 11, 12 | 3anbi23d 1440 |
. . . 4
β’ (π = πΊ β ((π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β (Edgβπ) β§ {(lastSβπ€), (π€β0)} β (Edgβπ)) β (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ β§ {(lastSβπ€), (π€β0)} β πΈ))) |
14 | 6, 13 | rabeqbidv 3423 |
. . 3
β’ (π = πΊ β {π€ β Word (Vtxβπ) β£ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β (Edgβπ) β§ {(lastSβπ€), (π€β0)} β (Edgβπ))} = {π€ β Word π β£ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ β§ {(lastSβπ€), (π€β0)} β πΈ)}) |
15 | | id 22 |
. . 3
β’ (πΊ β V β πΊ β V) |
16 | 3 | fvexi 6860 |
. . . . 5
β’ π β V |
17 | 16 | a1i 11 |
. . . 4
β’ (πΊ β V β π β V) |
18 | | wrdexg 14421 |
. . . 4
β’ (π β V β Word π β V) |
19 | | rabexg 5292 |
. . . 4
β’ (Word
π β V β {π€ β Word π β£ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ β§ {(lastSβπ€), (π€β0)} β πΈ)} β V) |
20 | 17, 18, 19 | 3syl 18 |
. . 3
β’ (πΊ β V β {π€ β Word π β£ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ β§ {(lastSβπ€), (π€β0)} β πΈ)} β V) |
21 | 1, 14, 15, 20 | fvmptd3 6975 |
. 2
β’ (πΊ β V β
(ClWWalksβπΊ) = {π€ β Word π β£ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ β§ {(lastSβπ€), (π€β0)} β πΈ)}) |
22 | | fvprc 6838 |
. . 3
β’ (Β¬
πΊ β V β
(ClWWalksβπΊ) =
β
) |
23 | | noel 4294 |
. . . . . . . 8
β’ Β¬
{(lastSβπ€), (π€β0)} β
β
|
24 | | fvprc 6838 |
. . . . . . . . . 10
β’ (Β¬
πΊ β V β
(EdgβπΊ) =
β
) |
25 | 8, 24 | eqtrid 2785 |
. . . . . . . . 9
β’ (Β¬
πΊ β V β πΈ = β
) |
26 | 25 | eleq2d 2820 |
. . . . . . . 8
β’ (Β¬
πΊ β V β
({(lastSβπ€), (π€β0)} β πΈ β {(lastSβπ€), (π€β0)} β β
)) |
27 | 23, 26 | mtbiri 327 |
. . . . . . 7
β’ (Β¬
πΊ β V β Β¬
{(lastSβπ€), (π€β0)} β πΈ) |
28 | 27 | adantr 482 |
. . . . . 6
β’ ((Β¬
πΊ β V β§ π€ β Word π) β Β¬ {(lastSβπ€), (π€β0)} β πΈ) |
29 | 28 | intn3an3d 1482 |
. . . . 5
β’ ((Β¬
πΊ β V β§ π€ β Word π) β Β¬ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ β§ {(lastSβπ€), (π€β0)} β πΈ)) |
30 | 29 | ralrimiva 3140 |
. . . 4
β’ (Β¬
πΊ β V β
βπ€ β Word π Β¬ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ β§ {(lastSβπ€), (π€β0)} β πΈ)) |
31 | | rabeq0 4348 |
. . . 4
β’ ({π€ β Word π β£ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ β§ {(lastSβπ€), (π€β0)} β πΈ)} = β
β βπ€ β Word π Β¬ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ β§ {(lastSβπ€), (π€β0)} β πΈ)) |
32 | 30, 31 | sylibr 233 |
. . 3
β’ (Β¬
πΊ β V β {π€ β Word π β£ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ β§ {(lastSβπ€), (π€β0)} β πΈ)} = β
) |
33 | 22, 32 | eqtr4d 2776 |
. 2
β’ (Β¬
πΊ β V β
(ClWWalksβπΊ) = {π€ β Word π β£ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ β§ {(lastSβπ€), (π€β0)} β πΈ)}) |
34 | 21, 33 | pm2.61i 182 |
1
β’
(ClWWalksβπΊ) =
{π€ β Word π β£ (π€ β β
β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β πΈ β§ {(lastSβπ€), (π€β0)} β πΈ)} |