Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . 4
β’
(VtxβπΊ) =
(VtxβπΊ) |
2 | | eqid 2733 |
. . . 4
β’
(EdgβπΊ) =
(EdgβπΊ) |
3 | 1, 2 | clwwlknp 29023 |
. . 3
β’ (π β (π ClWWalksN πΊ) β ((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) |
4 | | simpr 486 |
. . . . 5
β’
(((((π β Word
(VtxβπΊ) β§
(β―βπ) = π) β§ βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ π β (β€β₯β2))
β§ πΊ β UMGraph)
β πΊ β
UMGraph) |
5 | | uz2m1nn 12853 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β2) β (π β 1) β β) |
6 | | lbfzo0 13618 |
. . . . . . . . . . 11
β’ (0 β
(0..^(π β 1)) β
(π β 1) β
β) |
7 | 5, 6 | sylibr 233 |
. . . . . . . . . 10
β’ (π β
(β€β₯β2) β 0 β (0..^(π β 1))) |
8 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ (π = 0 β (πβπ) = (πβ0)) |
9 | 8 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β
(β€β₯β2) β§ π = 0) β (πβπ) = (πβ0)) |
10 | | oveq1 7365 |
. . . . . . . . . . . . . . 15
β’ (π = 0 β (π + 1) = (0 + 1)) |
11 | 10 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β
(β€β₯β2) β§ π = 0) β (π + 1) = (0 + 1)) |
12 | | 0p1e1 12280 |
. . . . . . . . . . . . . 14
β’ (0 + 1) =
1 |
13 | 11, 12 | eqtrdi 2789 |
. . . . . . . . . . . . 13
β’ ((π β
(β€β₯β2) β§ π = 0) β (π + 1) = 1) |
14 | 13 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ ((π β
(β€β₯β2) β§ π = 0) β (πβ(π + 1)) = (πβ1)) |
15 | 9, 14 | preq12d 4703 |
. . . . . . . . . . 11
β’ ((π β
(β€β₯β2) β§ π = 0) β {(πβπ), (πβ(π + 1))} = {(πβ0), (πβ1)}) |
16 | 15 | eleq1d 2819 |
. . . . . . . . . 10
β’ ((π β
(β€β₯β2) β§ π = 0) β ({(πβπ), (πβ(π + 1))} β (EdgβπΊ) β {(πβ0), (πβ1)} β (EdgβπΊ))) |
17 | 7, 16 | rspcdv 3572 |
. . . . . . . . 9
β’ (π β
(β€β₯β2) β (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β {(πβ0), (πβ1)} β (EdgβπΊ))) |
18 | 17 | com12 32 |
. . . . . . . 8
β’
(βπ β
(0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β (π β (β€β₯β2)
β {(πβ0), (πβ1)} β
(EdgβπΊ))) |
19 | 18 | 3ad2ant2 1135 |
. . . . . . 7
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β (π β (β€β₯β2)
β {(πβ0), (πβ1)} β
(EdgβπΊ))) |
20 | 19 | imp 408 |
. . . . . 6
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ π β (β€β₯β2))
β {(πβ0), (πβ1)} β
(EdgβπΊ)) |
21 | 20 | adantr 482 |
. . . . 5
β’
(((((π β Word
(VtxβπΊ) β§
(β―βπ) = π) β§ βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ π β (β€β₯β2))
β§ πΊ β UMGraph)
β {(πβ0), (πβ1)} β
(EdgβπΊ)) |
22 | 2 | umgredgne 28138 |
. . . . . 6
β’ ((πΊ β UMGraph β§ {(πβ0), (πβ1)} β (EdgβπΊ)) β (πβ0) β (πβ1)) |
23 | 22 | necomd 2996 |
. . . . 5
β’ ((πΊ β UMGraph β§ {(πβ0), (πβ1)} β (EdgβπΊ)) β (πβ1) β (πβ0)) |
24 | 4, 21, 23 | syl2anc 585 |
. . . 4
β’
(((((π β Word
(VtxβπΊ) β§
(β―βπ) = π) β§ βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ π β (β€β₯β2))
β§ πΊ β UMGraph)
β (πβ1) β
(πβ0)) |
25 | 24 | exp31 421 |
. . 3
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β (π β (β€β₯β2)
β (πΊ β UMGraph
β (πβ1) β
(πβ0)))) |
26 | 3, 25 | syl 17 |
. 2
β’ (π β (π ClWWalksN πΊ) β (π β (β€β₯β2)
β (πΊ β UMGraph
β (πβ1) β
(πβ0)))) |
27 | 26 | 3imp31 1113 |
1
β’ ((πΊ β UMGraph β§ π β
(β€β₯β2) β§ π β (π ClWWalksN πΊ)) β (πβ1) β (πβ0)) |