Theorem subiwrdlen

Description: Length of a subword of an infinite word. (Contributed by Thierry Arnoux, 25-Apr-2019)

	Ref	Expression
Hypotheses	iwrdsplit.s	⊢ ( 𝜑 → 𝑆 ∈ V )
	iwrdsplit.f	⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ 𝑆 )
	iwrdsplit.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	subiwrdlen	⊢ ( 𝜑 → ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) = 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		iwrdsplit.s	⊢ ( 𝜑 → 𝑆 ∈ V )
2		iwrdsplit.f	⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ 𝑆 )
3		iwrdsplit.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4	2	ffnd	⊢ ( 𝜑 → 𝐹 Fn ℕ0 )
5		fzo0ssnn0	⊢ ( 0 ..^ 𝑁 ) ⊆ ℕ0
6		fnssres	⊢ ( ( 𝐹 Fn ℕ0 ∧ ( 0 ..^ 𝑁 ) ⊆ ℕ0 ) → ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) Fn ( 0 ..^ 𝑁 ) )
7	4 5 6	sylancl	⊢ ( 𝜑 → ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) Fn ( 0 ..^ 𝑁 ) )
8		hashfn	⊢ ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) Fn ( 0 ..^ 𝑁 ) → ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) = ( ♯ ‘ ( 0 ..^ 𝑁 ) ) )
9	7 8	syl	⊢ ( 𝜑 → ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) = ( ♯ ‘ ( 0 ..^ 𝑁 ) ) )
10		hashfzo0	⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
11	3 10	syl	⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
12	9 11	eqtrd	⊢ ( 𝜑 → ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) = 𝑁 )