Step |
Hyp |
Ref |
Expression |
1 |
|
2wlkd.p |
|- P = <" A B C "> |
2 |
|
2wlkd.f |
|- F = <" J K "> |
3 |
|
2wlkd.s |
|- ( ph -> ( A e. V /\ B e. V /\ C e. V ) ) |
4 |
|
2wlkd.n |
|- ( ph -> ( A =/= B /\ B =/= C ) ) |
5 |
|
2wlkd.e |
|- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) ) |
6 |
|
2wlkd.v |
|- V = ( Vtx ` G ) |
7 |
|
2wlkd.i |
|- I = ( iEdg ` G ) |
8 |
1 2 3 4 5 6 7
|
2wlkd |
|- ( ph -> F ( Walks ` G ) P ) |
9 |
3
|
simp1d |
|- ( ph -> A e. V ) |
10 |
1
|
fveq1i |
|- ( P ` 0 ) = ( <" A B C "> ` 0 ) |
11 |
|
s3fv0 |
|- ( A e. V -> ( <" A B C "> ` 0 ) = A ) |
12 |
10 11
|
eqtrid |
|- ( A e. V -> ( P ` 0 ) = A ) |
13 |
9 12
|
syl |
|- ( ph -> ( P ` 0 ) = A ) |
14 |
2
|
fveq2i |
|- ( # ` F ) = ( # ` <" J K "> ) |
15 |
|
s2len |
|- ( # ` <" J K "> ) = 2 |
16 |
14 15
|
eqtri |
|- ( # ` F ) = 2 |
17 |
1 16
|
fveq12i |
|- ( P ` ( # ` F ) ) = ( <" A B C "> ` 2 ) |
18 |
3
|
simp3d |
|- ( ph -> C e. V ) |
19 |
|
s3fv2 |
|- ( C e. V -> ( <" A B C "> ` 2 ) = C ) |
20 |
18 19
|
syl |
|- ( ph -> ( <" A B C "> ` 2 ) = C ) |
21 |
17 20
|
eqtrid |
|- ( ph -> ( P ` ( # ` F ) ) = C ) |
22 |
|
3simpb |
|- ( ( A e. V /\ B e. V /\ C e. V ) -> ( A e. V /\ C e. V ) ) |
23 |
3 22
|
syl |
|- ( ph -> ( A e. V /\ C e. V ) ) |
24 |
|
s2cli |
|- <" J K "> e. Word _V |
25 |
2 24
|
eqeltri |
|- F e. Word _V |
26 |
|
s3cli |
|- <" A B C "> e. Word _V |
27 |
1 26
|
eqeltri |
|- P e. Word _V |
28 |
25 27
|
pm3.2i |
|- ( F e. Word _V /\ P e. Word _V ) |
29 |
6
|
iswlkon |
|- ( ( ( A e. V /\ C e. V ) /\ ( F e. Word _V /\ P e. Word _V ) ) -> ( F ( A ( WalksOn ` G ) C ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = C ) ) ) |
30 |
23 28 29
|
sylancl |
|- ( ph -> ( F ( A ( WalksOn ` G ) C ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = C ) ) ) |
31 |
8 13 21 30
|
mpbir3and |
|- ( ph -> F ( A ( WalksOn ` G ) C ) P ) |