Metamath Proof Explorer


Theorem eupthseg

Description: The N -th edge in an eulerian path is the edge having P ( N ) and P ( N + 1 ) as endpoints . (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 18-Feb-2021)

Ref Expression
Hypothesis eupths.i I=iEdgG
Assertion eupthseg FEulerPathsGPN0..^FPNPN+1IFN

Proof

Step Hyp Ref Expression
1 eupths.i I=iEdgG
2 1 eupthi FEulerPathsGPFWalksGPF:0..^F1-1 ontodomI
3 2 simpld FEulerPathsGPFWalksGP
4 1 wlkvtxeledg FWalksGPk0..^FPkPk+1IFk
5 fveq2 k=NPk=PN
6 fvoveq1 k=NPk+1=PN+1
7 5 6 preq12d k=NPkPk+1=PNPN+1
8 2fveq3 k=NIFk=IFN
9 7 8 sseq12d k=NPkPk+1IFkPNPN+1IFN
10 9 rspccv k0..^FPkPk+1IFkN0..^FPNPN+1IFN
11 3 4 10 3syl FEulerPathsGPN0..^FPNPN+1IFN
12 11 imp FEulerPathsGPN0..^FPNPN+1IFN