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

Metamath Proof Explorer

Theorem wlkiswwlks2lem3

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

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

Proof

Step Hyp Ref Expression
1 wlkiswwlks2lem.f ⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) )
2 1 wlkiswwlks2lem1 ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )
3 wrdf ⊢ ( 𝑃 ∈ Word 𝑉 → 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ 𝑉 )
4 lencl ⊢ ( 𝑃 ∈ Word 𝑉 → ( ♯ ‘ 𝑃 ) ∈ ℕ0 )
5 nn0z ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ♯ ‘ 𝑃 ) ∈ ℤ )
6 fzoval ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℤ → ( 0 ..^ ( ♯ ‘ 𝑃 ) ) = ( 0 ... ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
7 5 6 syl ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( 0 ..^ ( ♯ ‘ 𝑃 ) ) = ( 0 ... ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
8 oveq2 ⊢ ( ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ♯ ‘ 𝐹 ) → ( 0 ... ( ( ♯ ‘ 𝑃 ) − 1 ) ) = ( 0 ... ( ♯ ‘ 𝐹 ) ) )
9 8 eqcoms ⊢ ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) → ( 0 ... ( ( ♯ ‘ 𝑃 ) − 1 ) ) = ( 0 ... ( ♯ ‘ 𝐹 ) ) )
10 7 9 sylan9eq ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( 0 ..^ ( ♯ ‘ 𝑃 ) ) = ( 0 ... ( ♯ ‘ 𝐹 ) ) )
11 10 feq2d ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ 𝑉 ↔ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) )
12 11 biimpcd ⊢ ( 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ 𝑉 → ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) )
13 12 expd ⊢ ( 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ 𝑉 → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) ) )
14 3 4 13 sylc ⊢ ( 𝑃 ∈ Word 𝑉 → ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) )
15 14 adantr ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) )
16 2 15 mpd ⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )