3cyclpd

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

Proof

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	syl5eq	\|- ( 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 ) )

Metamath Proof Explorer

Theorem 3cyclpd

Proof