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 𝑆 → ( ♯ ‘ 𝐹 ) ∈ ℕ₀ )
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 ) ) ) ) ) ⟶ 𝑉 )