Metamath Proof Explorer

Theorem uspgr2wlkeq2

Description: Conditions for two walks within the same simple pseudograph to be identical. It is sufficient that the vertices (in the same order) are identical. (Contributed by Alexander van der Vekens, 25-Aug-2018) (Revised by AV, 14-Apr-2021)

Ref Expression
Assertion uspgr2wlkeq2 
|- ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) -> ( ( 2nd ` A ) = ( 2nd ` B ) -> A = B ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) -> ( # ` ( 1st ` B ) ) = N )
2 1 eqcomd 
 |-  ( ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) -> N = ( # ` ( 1st ` B ) ) )
3 2 3ad2ant3 
 |-  ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) -> N = ( # ` ( 1st ` B ) ) )
4 3 adantr 
 |-  ( ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) -> N = ( # ` ( 1st ` B ) ) )
5 fveq1 
 |-  ( ( 2nd ` A ) = ( 2nd ` B ) -> ( ( 2nd ` A ) ` i ) = ( ( 2nd ` B ) ` i ) )
6 5 adantl 
 |-  ( ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) -> ( ( 2nd ` A ) ` i ) = ( ( 2nd ` B ) ` i ) )
7 6 ralrimivw 
 |-  ( ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) -> A. i e. ( 0 ... N ) ( ( 2nd ` A ) ` i ) = ( ( 2nd ` B ) ` i ) )
8 simpl1l 
 |-  ( ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) -> G e. USPGraph )
9 simpl 
 |-  ( ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) -> A e. ( Walks ` G ) )
10 simpl 
 |-  ( ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) -> B e. ( Walks ` G ) )
11 9 10 anim12i 
 |-  ( ( ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) -> ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) )
12 11 3adant1 
 |-  ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) -> ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) )
13 12 adantr 
 |-  ( ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) -> ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) )
14 simpr 
 |-  ( ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) -> ( # ` ( 1st ` A ) ) = N )
15 14 eqcomd 
 |-  ( ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) -> N = ( # ` ( 1st ` A ) ) )
16 15 3ad2ant2 
 |-  ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) -> N = ( # ` ( 1st ` A ) ) )
17 16 adantr 
 |-  ( ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) -> N = ( # ` ( 1st ` A ) ) )
18 uspgr2wlkeq 
 |-  ( ( G e. USPGraph /\ ( A e. ( Walks ` G ) /\ B e. ( Walks ` G ) ) /\ N = ( # ` ( 1st ` A ) ) ) -> ( A = B <-> ( N = ( # ` ( 1st ` B ) ) /\ A. i e. ( 0 ... N ) ( ( 2nd ` A ) ` i ) = ( ( 2nd ` B ) ` i ) ) ) )
19 8 13 17 18 syl3anc 
 |-  ( ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) -> ( A = B <-> ( N = ( # ` ( 1st ` B ) ) /\ A. i e. ( 0 ... N ) ( ( 2nd ` A ) ` i ) = ( ( 2nd ` B ) ` i ) ) ) )
20 4 7 19 mpbir2and 
 |-  ( ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) -> A = B )
21 20 ex 
 |-  ( ( ( G e. USPGraph /\ N e. NN0 ) /\ ( A e. ( Walks ` G ) /\ ( # ` ( 1st ` A ) ) = N ) /\ ( B e. ( Walks ` G ) /\ ( # ` ( 1st ` B ) ) = N ) ) -> ( ( 2nd ` A ) = ( 2nd ` B ) -> A = B ) )