Description: Construction of a 3-cycle from three given edges in a graph, containing an endpoint of one of these edges. (Contributed by Alexander van der Vekens, 17-Nov-2017) (Revised by AV, 10-Feb-2021) (Revised by AV, 24-Mar-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 3wlkd.p | |- P = <" A B C D "> |
|
3wlkd.f | |- F = <" J K L "> |
||
3wlkd.s | |- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) ) |
||
3wlkd.n | |- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) |
||
3wlkd.e | |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) ) |
||
3wlkd.v | |- V = ( Vtx ` G ) |
||
3wlkd.i | |- I = ( iEdg ` G ) |
||
3trld.n | |- ( ph -> ( J =/= K /\ J =/= L /\ K =/= L ) ) |
||
3cycld.e | |- ( ph -> A = D ) |
||
Assertion | 3cyclpd | |- ( ph -> ( F ( Cycles ` G ) P /\ ( # ` F ) = 3 /\ ( P ` 0 ) = A ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3wlkd.p | |- P = <" A B C D "> |
|
2 | 3wlkd.f | |- F = <" J K L "> |
|
3 | 3wlkd.s | |- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) ) |
|
4 | 3wlkd.n | |- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) ) |
|
5 | 3wlkd.e | |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) ) |
|
6 | 3wlkd.v | |- V = ( Vtx ` G ) |
|
7 | 3wlkd.i | |- I = ( iEdg ` G ) |
|
8 | 3trld.n | |- ( ph -> ( J =/= K /\ J =/= L /\ K =/= L ) ) |
|
9 | 3cycld.e | |- ( ph -> A = D ) |
|
10 | 1 2 3 4 5 6 7 8 9 | 3cycld | |- ( ph -> F ( Cycles ` G ) P ) |
11 | 2 | fveq2i | |- ( # ` F ) = ( # ` <" J K L "> ) |
12 | s3len | |- ( # ` <" J K L "> ) = 3 |
|
13 | 11 12 | eqtri | |- ( # ` F ) = 3 |
14 | 13 | a1i | |- ( ph -> ( # ` F ) = 3 ) |
15 | 1 | fveq1i | |- ( P ` 0 ) = ( <" A B C D "> ` 0 ) |
16 | s4fv0 | |- ( A e. V -> ( <" A B C D "> ` 0 ) = A ) |
|
17 | 15 16 | eqtrid | |- ( A e. V -> ( P ` 0 ) = A ) |
18 | 17 | ad2antrr | |- ( ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( P ` 0 ) = A ) |
19 | 3 18 | syl | |- ( ph -> ( P ` 0 ) = A ) |
20 | 10 14 19 | 3jca | |- ( ph -> ( F ( Cycles ` G ) P /\ ( # ` F ) = 3 /\ ( P ` 0 ) = A ) ) |