Metamath Proof Explorer

Theorem eucrct2eupth1

Description: Removing one edge ( I( FN ) ) from a nonempty graph G with an Eulerian circuit <. F , P >. results in a graph S with an Eulerian path <. H , Q >. . This is the special case of eucrct2eupth (with J = ( N - 1 ) ) where the last segment/edge of the circuit is removed. (Contributed by AV, 11-Mar-2021) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022)

Ref Expression
Hypotheses eucrct2eupth1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
eucrct2eupth1.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
eucrct2eupth1.d ⊢ ( 𝜑 → 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 )
eucrct2eupth1.c ⊢ ( 𝜑 → 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 )
eucrct2eupth1.s ⊢ ( Vtx ‘ 𝑆 ) = 𝑉
eucrct2eupth1.g ⊢ ( 𝜑 → 0 < ( ♯ ‘ 𝐹 ) )
eucrct2eupth1.n ⊢ ( 𝜑 → 𝑁 = ( ( ♯ ‘ 𝐹 ) − 1 ) )
eucrct2eupth1.e ⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
eucrct2eupth1.h ⊢ 𝐻 = ( 𝐹 prefix 𝑁 )
eucrct2eupth1.q ⊢ 𝑄 = ( 𝑃 ↾ ( 0 ... 𝑁 ) )
Assertion eucrct2eupth1 ( 𝜑 → 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 )

Proof

Step Hyp Ref Expression
1 eucrct2eupth1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 eucrct2eupth1.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 eucrct2eupth1.d ⊢ ( 𝜑 → 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 )
4 eucrct2eupth1.c ⊢ ( 𝜑 → 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 )
5 eucrct2eupth1.s ⊢ ( Vtx ‘ 𝑆 ) = 𝑉
6 eucrct2eupth1.g ⊢ ( 𝜑 → 0 < ( ♯ ‘ 𝐹 ) )
7 eucrct2eupth1.n ⊢ ( 𝜑 → 𝑁 = ( ( ♯ ‘ 𝐹 ) − 1 ) )
8 eucrct2eupth1.e ⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
9 eucrct2eupth1.h ⊢ 𝐻 = ( 𝐹 prefix 𝑁 )
10 eucrct2eupth1.q ⊢ 𝑄 = ( 𝑃 ↾ ( 0 ... 𝑁 ) )
11 eupthiswlk ⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
12 wlkcl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
13 nn0z ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ℤ )
14 13 anim1i ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 0 < ( ♯ ‘ 𝐹 ) ) → ( ( ♯ ‘ 𝐹 ) ∈ ℤ ∧ 0 < ( ♯ ‘ 𝐹 ) ) )
15 elnnz ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝐹 ) ∈ ℤ ∧ 0 < ( ♯ ‘ 𝐹 ) ) )
16 14 15 sylibr ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 0 < ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐹 ) ∈ ℕ )
17 16 ex ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 0 < ( ♯ ‘ 𝐹 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ ) )
18 3 11 12 17 4syl ⊢ ( 𝜑 → ( 0 < ( ♯ ‘ 𝐹 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ ) )
19 6 18 mpd ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ℕ )
20 fzo0end ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
21 19 20 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
22 7 21 eqeltrd ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
23 1 2 3 22 8 9 10 5 eupthres ⊢ ( 𝜑 → 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 )