Metamath Proof Explorer

Theorem upgreupthseg

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

Ref Expression
Hypothesis upgreupthseg.i ⊢ I = iEdg ⁡ G
Assertion upgreupthseg ⊢ G ∈ UPGraph ∧ F EulerPaths ⁡ G P ∧ N ∈ 0 ..^ F → I ⁡ F ⁡ N = P ⁡ N P ⁡ N + 1

Proof

Step Hyp Ref Expression
1 upgreupthseg.i ⊢ I = iEdg ⁡ G
2 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
3 1 2 upgreupthi ⊢ G ∈ UPGraph ∧ F EulerPaths ⁡ G P → F : 0 ..^ F ⟶ 1-1 onto dom ⁡ I ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ ∀ n ∈ 0 ..^ F I ⁡ F ⁡ n = P ⁡ n P ⁡ n + 1
4 2fveq3 ⊢ n = N → I ⁡ F ⁡ n = I ⁡ F ⁡ N
5 fveq2 ⊢ n = N → P ⁡ n = P ⁡ N
6 fvoveq1 ⊢ n = N → P ⁡ n + 1 = P ⁡ N + 1
7 5 6 preq12d ⊢ n = N → P ⁡ n P ⁡ n + 1 = P ⁡ N P ⁡ N + 1
8 4 7 eqeq12d ⊢ n = N → I ⁡ F ⁡ n = P ⁡ n P ⁡ n + 1 ↔ I ⁡ F ⁡ N = P ⁡ N P ⁡ N + 1
9 8 rspccv ⊢ ∀ n ∈ 0 ..^ F I ⁡ F ⁡ n = P ⁡ n P ⁡ n + 1 → N ∈ 0 ..^ F → I ⁡ F ⁡ N = P ⁡ N P ⁡ N + 1
10 9 3ad2ant3 ⊢ F : 0 ..^ F ⟶ 1-1 onto dom ⁡ I ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ ∀ n ∈ 0 ..^ F I ⁡ F ⁡ n = P ⁡ n P ⁡ n + 1 → N ∈ 0 ..^ F → I ⁡ F ⁡ N = P ⁡ N P ⁡ N + 1
11 3 10 syl ⊢ G ∈ UPGraph ∧ F EulerPaths ⁡ G P → N ∈ 0 ..^ F → I ⁡ F ⁡ N = P ⁡ N P ⁡ N + 1
12 11 3impia ⊢ G ∈ UPGraph ∧ F EulerPaths ⁡ G P ∧ N ∈ 0 ..^ F → I ⁡ F ⁡ N = P ⁡ N P ⁡ N + 1