Step |
Hyp |
Ref |
Expression |
1 |
|
2cycld.1 |
|- P = <" A B C "> |
2 |
|
2cycld.2 |
|- F = <" J K "> |
3 |
|
2cycld.3 |
|- ( ph -> ( A e. V /\ B e. V /\ C e. V ) ) |
4 |
|
2cycld.4 |
|- ( ph -> ( A =/= B /\ B =/= C ) ) |
5 |
|
2cycld.5 |
|- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) ) |
6 |
|
2cycld.6 |
|- V = ( Vtx ` G ) |
7 |
|
2cycld.7 |
|- I = ( iEdg ` G ) |
8 |
|
2cycld.8 |
|- ( ph -> J =/= K ) |
9 |
|
2cycld.9 |
|- ( ph -> A = C ) |
10 |
1 2 3 4 5 6 7 8
|
2pthd |
|- ( ph -> F ( Paths ` G ) P ) |
11 |
1
|
fveq1i |
|- ( P ` 0 ) = ( <" A B C "> ` 0 ) |
12 |
|
s3fv0 |
|- ( A e. V -> ( <" A B C "> ` 0 ) = A ) |
13 |
11 12
|
syl5eq |
|- ( A e. V -> ( P ` 0 ) = A ) |
14 |
13
|
3ad2ant1 |
|- ( ( A e. V /\ B e. V /\ C e. V ) -> ( P ` 0 ) = A ) |
15 |
14
|
adantr |
|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ A = C ) -> ( P ` 0 ) = A ) |
16 |
|
simpr |
|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ A = C ) -> A = C ) |
17 |
2
|
fveq2i |
|- ( # ` F ) = ( # ` <" J K "> ) |
18 |
|
s2len |
|- ( # ` <" J K "> ) = 2 |
19 |
17 18
|
eqtri |
|- ( # ` F ) = 2 |
20 |
1 19
|
fveq12i |
|- ( P ` ( # ` F ) ) = ( <" A B C "> ` 2 ) |
21 |
|
s3fv2 |
|- ( C e. V -> ( <" A B C "> ` 2 ) = C ) |
22 |
20 21
|
eqtr2id |
|- ( C e. V -> C = ( P ` ( # ` F ) ) ) |
23 |
22
|
3ad2ant3 |
|- ( ( A e. V /\ B e. V /\ C e. V ) -> C = ( P ` ( # ` F ) ) ) |
24 |
23
|
adantr |
|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ A = C ) -> C = ( P ` ( # ` F ) ) ) |
25 |
15 16 24
|
3eqtrd |
|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ A = C ) -> ( P ` 0 ) = ( P ` ( # ` F ) ) ) |
26 |
3 9 25
|
syl2anc |
|- ( ph -> ( P ` 0 ) = ( P ` ( # ` F ) ) ) |
27 |
|
iscycl |
|- ( F ( Cycles ` G ) P <-> ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) |
28 |
10 26 27
|
sylanbrc |
|- ( ph -> F ( Cycles ` G ) P ) |