Metamath Proof Explorer

Theorem 2cycld

Description: Construction of a 2-cycle from two given edges in a graph. (Contributed by BTernaryTau, 16-Oct-2023)

Ref Expression
Hypotheses 2cycld.1 
|- P = <" A B C ">
2cycld.2 
|- F = <" J K ">
2cycld.3 
|- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )
2cycld.4 
|- ( ph -> ( A =/= B /\ B =/= C ) )
2cycld.5 
|- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) )
2cycld.6 
|- V = ( Vtx ` G )
2cycld.7 
|- I = ( iEdg ` G )
2cycld.8 
|- ( ph -> J =/= K )
2cycld.9 
|- ( ph -> A = C )
Assertion 2cycld 
|- ( ph -> F ( Cycles ` G ) P )

Proof

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 eqtrid 
 |-  ( 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 )