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 ⊢FAWalksOn⁡GBP∧HCWalksOn⁡GDP→A=C∧B=D

Proof

Step Hyp Ref Expression
1 eqid ⊢Vtx⁡G=Vtx⁡G
2 1 wlkonprop ⊢FAWalksOn⁡GBP→G∈V∧A∈Vtx⁡G∧B∈Vtx⁡G∧F∈V∧P∈V∧FWalks⁡GP∧P⁡0=A∧P⁡F=B
3 1 wlkonprop ⊢HCWalksOn⁡GDP→G∈V∧C∈Vtx⁡G∧D∈Vtx⁡G∧H∈V∧P∈V∧HWalks⁡GP∧P⁡0=C∧P⁡H=D
4 simp2 ⊢FWalks⁡GP∧P⁡0=A∧P⁡F=B→P⁡0=A
5 4 eqcomd ⊢FWalks⁡GP∧P⁡0=A∧P⁡F=B→A=P⁡0
6 simp2 ⊢HWalks⁡GP∧P⁡0=C∧P⁡H=D→P⁡0=C
7 5 6 sylan9eqr ⊢HWalks⁡GP∧P⁡0=C∧P⁡H=D∧FWalks⁡GP∧P⁡0=A∧P⁡F=B→A=C
8 simp3 ⊢FWalks⁡GP∧P⁡0=A∧P⁡F=B→P⁡F=B
9 8 eqcomd ⊢FWalks⁡GP∧P⁡0=A∧P⁡F=B→B=P⁡F
10 9 adantl ⊢HWalks⁡GP∧P⁡0=C∧P⁡H=D∧FWalks⁡GP∧P⁡0=A∧P⁡F=B→B=P⁡F
11 wlklenvm1 ⊢HWalks⁡GP→H=P−1
12 wlklenvm1 ⊢FWalks⁡GP→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 ⊢FWalks⁡GP→H=P−1→P⁡F=P⁡H
17 16 3ad2ant1 ⊢FWalks⁡GP∧P⁡0=A∧P⁡F=B→H=P−1→P⁡F=P⁡H
18 17 com12 ⊢H=P−1→FWalks⁡GP∧P⁡0=A∧P⁡F=B→P⁡F=P⁡H
19 11 18 syl ⊢HWalks⁡GP→FWalks⁡GP∧P⁡0=A∧P⁡F=B→P⁡F=P⁡H
20 19 3ad2ant1 ⊢HWalks⁡GP∧P⁡0=C∧P⁡H=D→FWalks⁡GP∧P⁡0=A∧P⁡F=B→P⁡F=P⁡H
21 20 imp ⊢HWalks⁡GP∧P⁡0=C∧P⁡H=D∧FWalks⁡GP∧P⁡0=A∧P⁡F=B→P⁡F=P⁡H
22 simpl3 ⊢HWalks⁡GP∧P⁡0=C∧P⁡H=D∧FWalks⁡GP∧P⁡0=A∧P⁡F=B→P⁡H=D
23 10 21 22 3eqtrd ⊢HWalks⁡GP∧P⁡0=C∧P⁡H=D∧FWalks⁡GP∧P⁡0=A∧P⁡F=B→B=D
24 7 23 jca ⊢HWalks⁡GP∧P⁡0=C∧P⁡H=D∧FWalks⁡GP∧P⁡0=A∧P⁡F=B→A=C∧B=D
25 24 ex ⊢HWalks⁡GP∧P⁡0=C∧P⁡H=D→FWalks⁡GP∧P⁡0=A∧P⁡F=B→A=C∧B=D
26 25 3ad2ant3 ⊢G∈V∧C∈Vtx⁡G∧D∈Vtx⁡G∧H∈V∧P∈V∧HWalks⁡GP∧P⁡0=C∧P⁡H=D→FWalks⁡GP∧P⁡0=A∧P⁡F=B→A=C∧B=D
27 26 com12 ⊢FWalks⁡GP∧P⁡0=A∧P⁡F=B→G∈V∧C∈Vtx⁡G∧D∈Vtx⁡G∧H∈V∧P∈V∧HWalks⁡GP∧P⁡0=C∧P⁡H=D→A=C∧B=D
28 27 3ad2ant3 ⊢G∈V∧A∈Vtx⁡G∧B∈Vtx⁡G∧F∈V∧P∈V∧FWalks⁡GP∧P⁡0=A∧P⁡F=B→G∈V∧C∈Vtx⁡G∧D∈Vtx⁡G∧H∈V∧P∈V∧HWalks⁡GP∧P⁡0=C∧P⁡H=D→A=C∧B=D
29 28 imp ⊢G∈V∧A∈Vtx⁡G∧B∈Vtx⁡G∧F∈V∧P∈V∧FWalks⁡GP∧P⁡0=A∧P⁡F=B∧G∈V∧C∈Vtx⁡G∧D∈Vtx⁡G∧H∈V∧P∈V∧HWalks⁡GP∧P⁡0=C∧P⁡H=D→A=C∧B=D
30 2 3 29 syl2an ⊢FAWalksOn⁡GBP∧HCWalksOn⁡GDP→A=C∧B=D