This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wlkiswwlks2lem1

Description: Lemma 1 for wlkiswwlks2 . (Contributed by Alexander van der Vekens, 20-Jul-2018)

Ref Expression
Hypothesis wlkiswwlks2lem.f ⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) )
Assertion wlkiswwlks2lem1 ( ( 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )

Proof

Step Hyp Ref Expression
1 wlkiswwlks2lem.f ⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) )
2 lencl ⊢ ( 𝑃 ∈ Word 𝑉 → ( ♯ ‘ 𝑃 ) ∈ ℕ0 )
3 elnnnn0c ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) )
4 3 biimpri ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝑃 ) ∈ ℕ )
5 2 4 sylan ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝑃 ) ∈ ℕ )
6 nnm1nn0 ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ0 )
7 5 6 syl ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ0 )
8 fvex ⊢ ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ∈ V
9 8 1 fnmpti ⊢ 𝐹 Fn ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) )
10 ffzo0hash ⊢ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ0 ∧ 𝐹 Fn ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )
11 7 9 10 sylancl ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )