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