Step | Hyp | Ref
| Expression |
1 | | extwwlkfab.v |
. . 3
β’ π = (VtxβπΊ) |
2 | | extwwlkfab.c |
. . 3
β’ πΆ = (π£ β π, π β (β€β₯β2)
β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£}) |
3 | | extwwlkfab.f |
. . 3
β’ πΉ = (π(ClWWalksNOnβπΊ)(π β 2)) |
4 | | numclwwlk.t |
. . 3
β’ π = (π’ β (ππΆπ) β¦ β¨(π’ prefix (π β 2)), (π’β(π β 1))β©) |
5 | 1, 2, 3, 4 | numclwwlk1lem2f 29341 |
. 2
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β π:(ππΆπ)βΆ(πΉ Γ (πΊ NeighbVtx π))) |
6 | | elxp 5661 |
. . . . 5
β’ (π β (πΉ Γ (πΊ NeighbVtx π)) β βπβπ(π = β¨π, πβ© β§ (π β πΉ β§ π β (πΊ NeighbVtx π)))) |
7 | 1, 2, 3 | numclwwlk1lem2foa 29340 |
. . . . . . . . . . 11
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β ((π β πΉ β§ π β (πΊ NeighbVtx π)) β ((π ++ β¨βπββ©) ++ β¨βπββ©) β (ππΆπ))) |
8 | 7 | com12 32 |
. . . . . . . . . 10
β’ ((π β πΉ β§ π β (πΊ NeighbVtx π)) β ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β ((π ++
β¨βπββ©) ++ β¨βπββ©) β (ππΆπ))) |
9 | 8 | adantl 483 |
. . . . . . . . 9
β’ ((π = β¨π, πβ© β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β ((π ++
β¨βπββ©) ++ β¨βπββ©) β (ππΆπ))) |
10 | 9 | imp 408 |
. . . . . . . 8
β’ (((π = β¨π, πβ© β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β§ (πΊ β USGraph β§ π β π β§ π β (β€β₯β3)))
β ((π ++
β¨βπββ©) ++ β¨βπββ©) β (ππΆπ)) |
11 | | simpl 484 |
. . . . . . . . 9
β’ ((((π ++ β¨βπββ©) ++
β¨βπββ©) β (ππΆπ) β§ ((π = β¨π, πβ© β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β§ (πΊ β USGraph β§ π β π β§ π β (β€β₯β3))))
β ((π ++
β¨βπββ©) ++ β¨βπββ©) β (ππΆπ)) |
12 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π₯ = ((π ++ β¨βπββ©) ++ β¨βπββ©) β (πβπ₯) = (πβ((π ++ β¨βπββ©) ++ β¨βπββ©))) |
13 | 12 | eqeq2d 2748 |
. . . . . . . . . 10
β’ (π₯ = ((π ++ β¨βπββ©) ++ β¨βπββ©) β (π = (πβπ₯) β π = (πβ((π ++ β¨βπββ©) ++ β¨βπββ©)))) |
14 | 1, 2, 3, 4 | numclwwlk1lem2fv 29342 |
. . . . . . . . . . . 12
β’ (((π ++ β¨βπββ©) ++
β¨βπββ©) β (ππΆπ) β (πβ((π ++ β¨βπββ©) ++ β¨βπββ©)) = β¨(((π ++ β¨βπββ©) ++
β¨βπββ©) prefix (π β 2)), (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β
1))β©) |
15 | 14 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π ++ β¨βπββ©) ++
β¨βπββ©) β (ππΆπ) β§ ((π = β¨π, πβ© β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β§ (πΊ β USGraph β§ π β π β§ π β (β€β₯β3))))
β (πβ((π ++ β¨βπββ©) ++
β¨βπββ©)) = β¨(((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β(π β 1))β©) |
16 | 15 | eqeq2d 2748 |
. . . . . . . . . 10
β’ ((((π ++ β¨βπββ©) ++
β¨βπββ©) β (ππΆπ) β§ ((π = β¨π, πβ© β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β§ (πΊ β USGraph β§ π β π β§ π β (β€β₯β3))))
β (π = (πβ((π ++ β¨βπββ©) ++ β¨βπββ©)) β π = β¨(((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β(π β 1))β©)) |
17 | 13, 16 | sylan9bbr 512 |
. . . . . . . . 9
β’
(((((π ++
β¨βπββ©) ++ β¨βπββ©) β (ππΆπ) β§ ((π = β¨π, πβ© β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β§ (πΊ β USGraph β§ π β π β§ π β (β€β₯β3))))
β§ π₯ = ((π ++ β¨βπββ©) ++
β¨βπββ©)) β (π = (πβπ₯) β π = β¨(((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β(π β 1))β©)) |
18 | | simprll 778 |
. . . . . . . . . 10
β’ ((((π ++ β¨βπββ©) ++
β¨βπββ©) β (ππΆπ) β§ ((π = β¨π, πβ© β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β§ (πΊ β USGraph β§ π β π β§ π β (β€β₯β3))))
β π = β¨π, πβ©) |
19 | 1 | nbgrisvtx 28331 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΊ NeighbVtx π) β π β π) |
20 | 3 | eleq2i 2830 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β πΉ β π β (π(ClWWalksNOnβπΊ)(π β 2))) |
21 | | uz3m2nn 12823 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β
(β€β₯β3) β (π β 2) β β) |
22 | 21 | nnne0d 12210 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β
(β€β₯β3) β (π β 2) β 0) |
23 | 22 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β (π β 2) β
0) |
24 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(EdgβπΊ) =
(EdgβπΊ) |
25 | 1, 24 | clwwlknonel 29081 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β 2) β 0 β (π β (π(ClWWalksNOnβπΊ)(π β 2)) β ((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = (π β 2) β§ (πβ0) = π))) |
26 | 23, 25 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β (π β (π(ClWWalksNOnβπΊ)(π β 2)) β ((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = (π β 2) β§ (πβ0) = π))) |
27 | 20, 26 | bitrid 283 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β (π β πΉ β ((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = (π β 2) β§ (πβ0) = π))) |
28 | | df-3an 1090 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = (π β 2) β§ (πβ0) = π) β (((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = (π β 2)) β§ (πβ0) = π)) |
29 | 27, 28 | bitrdi 287 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β (π β πΉ β (((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = (π β 2)) β§ (πβ0) = π))) |
30 | | simplll 774 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β (β€β₯β3)))
β§ π β π) β π β Word π) |
31 | | s1cl 14497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β π β β¨βπββ© β Word π) |
32 | 31 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β π β§ π β (β€β₯β3))
β β¨βπββ© β Word π) |
33 | 32 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β (β€β₯β3)))
β β¨βπββ© β Word π) |
34 | 33 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β (β€β₯β3)))
β§ π β π) β β¨βπββ© β Word π) |
35 | | s1cl 14497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β π β β¨βπββ© β Word π) |
36 | 35 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β (β€β₯β3)))
β§ π β π) β β¨βπββ© β Word π) |
37 | | ccatass 14483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β Word π β§ β¨βπββ© β Word π β§ β¨βπββ© β Word π) β ((π ++ β¨βπββ©) ++ β¨βπββ©) = (π ++ (β¨βπββ© ++
β¨βπββ©))) |
38 | 37 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β Word π β§ β¨βπββ© β Word π β§ β¨βπββ© β Word π) β (((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)) = ((π ++ (β¨βπββ© ++
β¨βπββ©)) prefix (π β 2))) |
39 | 30, 34, 36, 38 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β (β€β₯β3)))
β§ π β π) β (((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)) = ((π ++ (β¨βπββ© ++
β¨βπββ©)) prefix (π β 2))) |
40 | | ccatcl 14469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((β¨βπββ© β Word π β§ β¨βπββ© β Word π) β (β¨βπββ© ++ β¨βπββ©) β Word π) |
41 | 33, 35, 40 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β (β€β₯β3)))
β§ π β π) β (β¨βπββ© ++
β¨βπββ©) β Word π) |
42 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β Word π β§ (β―βπ) = (π β 2)) β (β―βπ) = (π β 2)) |
43 | 42 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β Word π β§ (β―βπ) = (π β 2)) β (π β 2) = (β―βπ)) |
44 | 43 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β (β€β₯β3)))
β (π β 2) =
(β―βπ)) |
45 | 44 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β (β€β₯β3)))
β§ π β π) β (π β 2) = (β―βπ)) |
46 | | pfxccatid 14636 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β Word π β§ (β¨βπββ© ++ β¨βπββ©) β Word π β§ (π β 2) = (β―βπ)) β ((π ++ (β¨βπββ© ++ β¨βπββ©)) prefix (π β 2)) = π) |
47 | 30, 41, 45, 46 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β (β€β₯β3)))
β§ π β π) β ((π ++ (β¨βπββ© ++ β¨βπββ©)) prefix (π β 2)) = π) |
48 | 39, 47 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β (β€β₯β3)))
β§ π β π) β π = (((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2))) |
49 | | 1e2m1 12287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ 1 = (2
β 1) |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β
(β€β₯β3) β 1 = (2 β 1)) |
51 | 50 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β
(β€β₯β3) β (π β 1) = (π β (2 β 1))) |
52 | | eluzelcn 12782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β
(β€β₯β3) β π β β) |
53 | | 2cnd 12238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β
(β€β₯β3) β 2 β β) |
54 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β
(β€β₯β3) β 1 β β) |
55 | 52, 53, 54 | subsubd 11547 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β
(β€β₯β3) β (π β (2 β 1)) = ((π β 2) +
1)) |
56 | 51, 55 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β
(β€β₯β3) β (π β 1) = ((π β 2) + 1)) |
57 | 56 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β π β§ π β (β€β₯β3))
β (π β 1) =
((π β 2) +
1)) |
58 | 57 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β (β€β₯β3)))
β (π β 1) =
((π β 2) +
1)) |
59 | 58 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β (β€β₯β3)))
β§ π β π) β (π β 1) = ((π β 2) + 1)) |
60 | 59 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β (β€β₯β3)))
β§ π β π) β (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 1)) = (((π ++ β¨βπββ©) ++
β¨βπββ©)β((π β 2) + 1))) |
61 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β (β€β₯β3)))
β§ π β π) β (π β Word π β§ (β―βπ) = (π β 2))) |
62 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β (β€β₯β3)))
β π β π) |
63 | 62 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β (β€β₯β3)))
β§ π β π) β (π β π β§ π β π)) |
64 | | ccatw2s1p2 14532 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β π)) β (((π ++ β¨βπββ©) ++ β¨βπββ©)β((π β 2) + 1)) = π) |
65 | 61, 63, 64 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β (β€β₯β3)))
β§ π β π) β (((π ++ β¨βπββ©) ++ β¨βπββ©)β((π β 2) + 1)) = π) |
66 | 60, 65 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β (β€β₯β3)))
β§ π β π) β π = (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 1))) |
67 | 48, 66 | opeq12d 4843 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β (β€β₯β3)))
β§ π β π) β β¨π, πβ© = β¨(((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β(π β 1))β©) |
68 | 67 | exp31 421 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β Word π β§ (β―βπ) = (π β 2)) β ((π β π β§ π β (β€β₯β3))
β (π β π β β¨π, πβ© = β¨(((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β(π β 1))β©))) |
69 | 68 | 3ad2antl1 1186 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = (π β 2)) β ((π β π β§ π β (β€β₯β3))
β (π β π β β¨π, πβ© = β¨(((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β(π β 1))β©))) |
70 | 69 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = (π β 2)) β§ (πβ0) = π) β ((π β π β§ π β (β€β₯β3))
β (π β π β β¨π, πβ© = β¨(((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β(π β 1))β©))) |
71 | 70 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β π β§ π β (β€β₯β3))
β ((((π β Word
π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = (π β 2)) β§ (πβ0) = π) β (π β π β β¨π, πβ© = β¨(((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β(π β 1))β©))) |
72 | 71 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β ((((π β Word
π β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = (π β 2)) β§ (πβ0) = π) β (π β π β β¨π, πβ© = β¨(((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β(π β 1))β©))) |
73 | 29, 72 | sylbid 239 |
. . . . . . . . . . . . . . . . 17
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β (π β πΉ β (π β π β β¨π, πβ© = β¨(((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β(π β 1))β©))) |
74 | 73 | com23 86 |
. . . . . . . . . . . . . . . 16
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β (π β π β (π β πΉ β β¨π, πβ© = β¨(((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β(π β 1))β©))) |
75 | 19, 74 | syl5 34 |
. . . . . . . . . . . . . . 15
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β (π β (πΊ NeighbVtx π) β (π β πΉ β β¨π, πβ© = β¨(((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)), (((π ++ β¨βπββ©) ++
β¨βπββ©)β(π β 1))β©))) |
76 | 75 | com13 88 |
. . . . . . . . . . . . . 14
β’ (π β πΉ β (π β (πΊ NeighbVtx π) β ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β β¨π, πβ© = β¨(((π ++ β¨βπββ©) ++
β¨βπββ©) prefix (π β 2)), (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β
1))β©))) |
77 | 76 | imp 408 |
. . . . . . . . . . . . 13
β’ ((π β πΉ β§ π β (πΊ NeighbVtx π)) β ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β β¨π, πβ© = β¨(((π ++ β¨βπββ©) ++
β¨βπββ©) prefix (π β 2)), (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β
1))β©)) |
78 | 77 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π = β¨π, πβ© β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β β¨π, πβ© = β¨(((π ++ β¨βπββ©) ++
β¨βπββ©) prefix (π β 2)), (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β
1))β©)) |
79 | 78 | imp 408 |
. . . . . . . . . . 11
β’ (((π = β¨π, πβ© β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β§ (πΊ β USGraph β§ π β π β§ π β (β€β₯β3)))
β β¨π, πβ© = β¨(((π ++ β¨βπββ©) ++
β¨βπββ©) prefix (π β 2)), (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β
1))β©) |
80 | 79 | adantl 483 |
. . . . . . . . . 10
β’ ((((π ++ β¨βπββ©) ++
β¨βπββ©) β (ππΆπ) β§ ((π = β¨π, πβ© β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β§ (πΊ β USGraph β§ π β π β§ π β (β€β₯β3))))
β β¨π, πβ© = β¨(((π ++ β¨βπββ©) ++
β¨βπββ©) prefix (π β 2)), (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β
1))β©) |
81 | 18, 80 | eqtrd 2777 |
. . . . . . . . 9
β’ ((((π ++ β¨βπββ©) ++
β¨βπββ©) β (ππΆπ) β§ ((π = β¨π, πβ© β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β§ (πΊ β USGraph β§ π β π β§ π β (β€β₯β3))))
β π = β¨(((π ++ β¨βπββ©) ++
β¨βπββ©) prefix (π β 2)), (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β
1))β©) |
82 | 11, 17, 81 | rspcedvd 3586 |
. . . . . . . 8
β’ ((((π ++ β¨βπββ©) ++
β¨βπββ©) β (ππΆπ) β§ ((π = β¨π, πβ© β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β§ (πΊ β USGraph β§ π β π β§ π β (β€β₯β3))))
β βπ₯ β
(ππΆπ)π = (πβπ₯)) |
83 | 10, 82 | mpancom 687 |
. . . . . . 7
β’ (((π = β¨π, πβ© β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β§ (πΊ β USGraph β§ π β π β§ π β (β€β₯β3)))
β βπ₯ β
(ππΆπ)π = (πβπ₯)) |
84 | 83 | ex 414 |
. . . . . 6
β’ ((π = β¨π, πβ© β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β βπ₯ β
(ππΆπ)π = (πβπ₯))) |
85 | 84 | exlimivv 1936 |
. . . . 5
β’
(βπβπ(π = β¨π, πβ© β§ (π β πΉ β§ π β (πΊ NeighbVtx π))) β ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β βπ₯ β
(ππΆπ)π = (πβπ₯))) |
86 | 6, 85 | sylbi 216 |
. . . 4
β’ (π β (πΉ Γ (πΊ NeighbVtx π)) β ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β βπ₯ β
(ππΆπ)π = (πβπ₯))) |
87 | 86 | impcom 409 |
. . 3
β’ (((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β§ π β (πΉ Γ (πΊ NeighbVtx π))) β βπ₯ β (ππΆπ)π = (πβπ₯)) |
88 | 87 | ralrimiva 3144 |
. 2
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β βπ β
(πΉ Γ (πΊ NeighbVtx π))βπ₯ β (ππΆπ)π = (πβπ₯)) |
89 | | dffo3 7057 |
. 2
β’ (π:(ππΆπ)βontoβ(πΉ Γ (πΊ NeighbVtx π)) β (π:(ππΆπ)βΆ(πΉ Γ (πΊ NeighbVtx π)) β§ βπ β (πΉ Γ (πΊ NeighbVtx π))βπ₯ β (ππΆπ)π = (πβπ₯))) |
90 | 5, 88, 89 | sylanbrc 584 |
1
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β π:(ππΆπ)βontoβ(πΉ Γ (πΊ NeighbVtx π))) |