Metamath Proof Explorer

Theorem wlksoneq1eq2

Description: Two walks with identical sequences of vertices start and end at the same vertices. (Contributed by AV, 14-May-2021)

Ref Expression
Assertion wlksoneq1eq2 
|- ( ( F ( A ( WalksOn ` G ) B ) P /\ H ( C ( WalksOn ` G ) D ) P ) -> ( A = C /\ B = D ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 1 wlkonprop 
 |-  ( F ( A ( WalksOn ` G ) B ) P -> ( ( G e. _V /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
3 1 wlkonprop 
 |-  ( H ( C ( WalksOn ` G ) D ) P -> ( ( G e. _V /\ C e. ( Vtx ` G ) /\ D e. ( Vtx ` G ) ) /\ ( H e. _V /\ P e. _V ) /\ ( H ( Walks ` G ) P /\ ( P ` 0 ) = C /\ ( P ` ( # ` H ) ) = D ) ) )
4 simp2 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( P ` 0 ) = A )
5 4 eqcomd 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> A = ( P ` 0 ) )
6 simp2 
 |-  ( ( H ( Walks ` G ) P /\ ( P ` 0 ) = C /\ ( P ` ( # ` H ) ) = D ) -> ( P ` 0 ) = C )
7 5 6 sylan9eqr 
 |-  ( ( ( H ( Walks ` G ) P /\ ( P ` 0 ) = C /\ ( P ` ( # ` H ) ) = D ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> A = C )
8 simp3 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( P ` ( # ` F ) ) = B )
9 8 eqcomd 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> B = ( P ` ( # ` F ) ) )
10 9 adantl 
 |-  ( ( ( H ( Walks ` G ) P /\ ( P ` 0 ) = C /\ ( P ` ( # ` H ) ) = D ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> B = ( P ` ( # ` F ) ) )
11 wlklenvm1 
 |-  ( H ( Walks ` G ) P -> ( # ` H ) = ( ( # ` P ) - 1 ) )
12 wlklenvm1 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) = ( ( # ` P ) - 1 ) )
13 eqtr3 
 |-  ( ( ( # ` F ) = ( ( # ` P ) - 1 ) /\ ( # ` H ) = ( ( # ` P ) - 1 ) ) -> ( # ` F ) = ( # ` H ) )
14 13 fveq2d 
 |-  ( ( ( # ` F ) = ( ( # ` P ) - 1 ) /\ ( # ` H ) = ( ( # ` P ) - 1 ) ) -> ( P ` ( # ` F ) ) = ( P ` ( # ` H ) ) )
15 14 ex 
 |-  ( ( # ` F ) = ( ( # ` P ) - 1 ) -> ( ( # ` H ) = ( ( # ` P ) - 1 ) -> ( P ` ( # ` F ) ) = ( P ` ( # ` H ) ) ) )
16 12 15 syl 
 |-  ( F ( Walks ` G ) P -> ( ( # ` H ) = ( ( # ` P ) - 1 ) -> ( P ` ( # ` F ) ) = ( P ` ( # ` H ) ) ) )
17 16 3ad2ant1 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( ( # ` H ) = ( ( # ` P ) - 1 ) -> ( P ` ( # ` F ) ) = ( P ` ( # ` H ) ) ) )
18 17 com12 
 |-  ( ( # ` H ) = ( ( # ` P ) - 1 ) -> ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( P ` ( # ` F ) ) = ( P ` ( # ` H ) ) ) )
19 11 18 syl 
 |-  ( H ( Walks ` G ) P -> ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( P ` ( # ` F ) ) = ( P ` ( # ` H ) ) ) )
20 19 3ad2ant1 
 |-  ( ( H ( Walks ` G ) P /\ ( P ` 0 ) = C /\ ( P ` ( # ` H ) ) = D ) -> ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( P ` ( # ` F ) ) = ( P ` ( # ` H ) ) ) )
21 20 imp 
 |-  ( ( ( H ( Walks ` G ) P /\ ( P ` 0 ) = C /\ ( P ` ( # ` H ) ) = D ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( P ` ( # ` F ) ) = ( P ` ( # ` H ) ) )
22 simpl3 
 |-  ( ( ( H ( Walks ` G ) P /\ ( P ` 0 ) = C /\ ( P ` ( # ` H ) ) = D ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( P ` ( # ` H ) ) = D )
23 10 21 22 3eqtrd 
 |-  ( ( ( H ( Walks ` G ) P /\ ( P ` 0 ) = C /\ ( P ` ( # ` H ) ) = D ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> B = D )
24 7 23 jca 
 |-  ( ( ( H ( Walks ` G ) P /\ ( P ` 0 ) = C /\ ( P ` ( # ` H ) ) = D ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( A = C /\ B = D ) )
25 24 ex 
 |-  ( ( H ( Walks ` G ) P /\ ( P ` 0 ) = C /\ ( P ` ( # ` H ) ) = D ) -> ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( A = C /\ B = D ) ) )
26 25 3ad2ant3 
 |-  ( ( ( G e. _V /\ C e. ( Vtx ` G ) /\ D e. ( Vtx ` G ) ) /\ ( H e. _V /\ P e. _V ) /\ ( H ( Walks ` G ) P /\ ( P ` 0 ) = C /\ ( P ` ( # ` H ) ) = D ) ) -> ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( A = C /\ B = D ) ) )
27 26 com12 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( ( ( G e. _V /\ C e. ( Vtx ` G ) /\ D e. ( Vtx ` G ) ) /\ ( H e. _V /\ P e. _V ) /\ ( H ( Walks ` G ) P /\ ( P ` 0 ) = C /\ ( P ` ( # ` H ) ) = D ) ) -> ( A = C /\ B = D ) ) )
28 27 3ad2ant3 
 |-  ( ( ( G e. _V /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( ( ( G e. _V /\ C e. ( Vtx ` G ) /\ D e. ( Vtx ` G ) ) /\ ( H e. _V /\ P e. _V ) /\ ( H ( Walks ` G ) P /\ ( P ` 0 ) = C /\ ( P ` ( # ` H ) ) = D ) ) -> ( A = C /\ B = D ) ) )
29 28 imp 
 |-  ( ( ( ( G e. _V /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) /\ ( ( G e. _V /\ C e. ( Vtx ` G ) /\ D e. ( Vtx ` G ) ) /\ ( H e. _V /\ P e. _V ) /\ ( H ( Walks ` G ) P /\ ( P ` 0 ) = C /\ ( P ` ( # ` H ) ) = D ) ) ) -> ( A = C /\ B = D ) )
30 2 3 29 syl2an 
 |-  ( ( F ( A ( WalksOn ` G ) B ) P /\ H ( C ( WalksOn ` G ) D ) P ) -> ( A = C /\ B = D ) )