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

Metamath Proof Explorer

Theorem redwlklem

Description: Lemma for redwlk . (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 29-Jan-2021)

Ref Expression
Assertion redwlklem ( ( 𝐹 ∈ Word 𝑆 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) → ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 0 ... ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) ⟶ 𝑉 )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
2 fzossfz ⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐹 ) )
3 fssres ⊢ ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
4 1 2 3 sylancl ⊢ ( ( ( 𝐹 ∈ Word 𝑆 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) → ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
5 4 ex ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) )
6 lencl ⊢ ( 𝐹 ∈ Word 𝑆 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
7 6 nn0zd ⊢ ( 𝐹 ∈ Word 𝑆 → ( ♯ ‘ 𝐹 ) ∈ ℤ )
8 fzoval ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℤ → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
9 7 8 syl ⊢ ( 𝐹 ∈ Word 𝑆 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
10 9 adantr ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
11 wrdred1hash ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) = ( ( ♯ ‘ 𝐹 ) − 1 ) )
12 oveq2 ⊢ ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) = ( ( ♯ ‘ 𝐹 ) − 1 ) → ( 0 ... ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) = ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
13 12 eqeq2d ⊢ ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) = ( ( ♯ ‘ 𝐹 ) − 1 ) → ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ... ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) ↔ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
14 11 13 syl ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) → ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ... ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) ↔ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
15 10 14 mpbird ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ... ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) )
16 15 feq2d ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) → ( ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ↔ ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 0 ... ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) ⟶ 𝑉 ) )
17 5 16 sylibd ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 0 ... ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) ⟶ 𝑉 ) )
18 17 3impia ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 1 ≤ ( ♯ ‘ 𝐹 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) → ( 𝑃 ↾ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) : ( 0 ... ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ) ⟶ 𝑉 )