2wlkd

Description: Construction of a walk from two given edges in a graph. (Contributed by Alexander van der Vekens, 5-Feb-2018) (Revised by AV, 23-Jan-2021) (Proof shortened by AV, 14-Feb-2021) (Revised by AV, 24-Mar-2021)

	Ref	Expression
Hypotheses	2wlkd.p	\|- P = <" A B C ">
	2wlkd.f	\|- F = <" J K ">
	2wlkd.s	\|- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )
	2wlkd.n	\|- ( ph -> ( A =/= B /\ B =/= C ) )
	2wlkd.e	\|- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) )
	2wlkd.v	\|- V = ( Vtx ` G )
	2wlkd.i	\|- I = ( iEdg ` G )
Assertion	2wlkd	\|- ( ph -> F ( Walks ` G ) P )

Proof

Step	Hyp	Ref	Expression
1		2wlkd.p	\|- P = <" A B C ">
2		2wlkd.f	\|- F = <" J K ">
3		2wlkd.s	\|- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )
4		2wlkd.n	\|- ( ph -> ( A =/= B /\ B =/= C ) )
5		2wlkd.e	\|- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) )
6		2wlkd.v	\|- V = ( Vtx ` G )
7		2wlkd.i	\|- I = ( iEdg ` G )
8		s3cli	\|- <" A B C "> e. Word _V
9	1 8	eqeltri	\|- P e. Word _V
10	9	a1i	\|- ( ph -> P e. Word _V )
11		s2cli	\|- <" J K "> e. Word _V
12	2 11	eqeltri	\|- F e. Word _V
13	12	a1i	\|- ( ph -> F e. Word _V )
14	1 2	2wlkdlem1	\|- ( # ` P ) = ( ( # ` F ) + 1 )
15	14	a1i	\|- ( ph -> ( # ` P ) = ( ( # ` F ) + 1 ) )
16	1 2 3 4 5	2wlkdlem10	\|- ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )
17	1 2 3 4	2wlkdlem5	\|- ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) )
18	6	1vgrex	\|- ( A e. V -> G e. _V )
19	18	3ad2ant1	\|- ( ( A e. V /\ B e. V /\ C e. V ) -> G e. _V )
20	3 19	syl	\|- ( ph -> G e. _V )
21	1 2 3	2wlkdlem4	\|- ( ph -> A. k e. ( 0 ... ( # ` F ) ) ( P ` k ) e. V )
22	10 13 15 16 17 20 6 7 21	wlkd	\|- ( ph -> F ( Walks ` G ) P )

Metamath Proof Explorer

Theorem 2wlkd

Proof