Theorem iswlkon

Description: Properties of a pair of functions to be a walk between two given vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 2-Nov-2017) (Revised by AV, 31-Dec-2020) (Revised by AV, 22-Mar-2021)

	Ref	Expression
Hypothesis	wlkson.v	|- V = ( Vtx ` G )
Assertion	iswlkon	|- ( ( ( A e. V /\ B e. V ) /\ ( F e. U /\ P e. Z ) ) -> ( F ( A ( WalksOn ` G ) B ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )

Proof

Step	Hyp	Ref	Expression
1		wlkson.v	|- V = ( Vtx ` G )
2	1	wlkson	|- ( ( A e. V /\ B e. V ) -> ( A ( WalksOn ` G ) B ) = { <. f , p >. | ( f ( Walks ` G ) p /\ ( p ` 0 ) = A /\ ( p ` ( # ` f ) ) = B ) } )
3		fveq1	|- ( p = P -> ( p ` 0 ) = ( P ` 0 ) )
4	3	adantl	|- ( ( f = F /\ p = P ) -> ( p ` 0 ) = ( P ` 0 ) )
5	4	eqeq1d	|- ( ( f = F /\ p = P ) -> ( ( p ` 0 ) = A <-> ( P ` 0 ) = A ) )
6		simpr	|- ( ( f = F /\ p = P ) -> p = P )
7		fveq2	|- ( f = F -> ( # ` f ) = ( # ` F ) )
8	7	adantr	|- ( ( f = F /\ p = P ) -> ( # ` f ) = ( # ` F ) )
9	6 8	fveq12d	|- ( ( f = F /\ p = P ) -> ( p ` ( # ` f ) ) = ( P ` ( # ` F ) ) )
10	9	eqeq1d	|- ( ( f = F /\ p = P ) -> ( ( p ` ( # ` f ) ) = B <-> ( P ` ( # ` F ) ) = B ) )
11	2 5 10	2rbropap	|- ( ( ( A e. V /\ B e. V ) /\ F e. U /\ P e. Z ) -> ( F ( A ( WalksOn ` G ) B ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
12	11	3expb	|- ( ( ( A e. V /\ B e. V ) /\ ( F e. U /\ P e. Z ) ) -> ( F ( A ( WalksOn ` G ) B ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )