Theorem subiwrdlen

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

	Ref	Expression
Hypotheses	iwrdsplit.s	|- ( ph -> S e. _V )
	iwrdsplit.f	|- ( ph -> F : NN0 --> S )
	iwrdsplit.n	|- ( ph -> N e. NN0 )
Assertion	subiwrdlen	|- ( ph -> ( # ` ( F |` ( 0 ..^ N ) ) ) = N )

Proof

Step	Hyp	Ref	Expression
1		iwrdsplit.s	|- ( ph -> S e. _V )
2		iwrdsplit.f	|- ( ph -> F : NN0 --> S )
3		iwrdsplit.n	|- ( ph -> N e. NN0 )
4	2	ffnd	|- ( ph -> F Fn NN0 )
5		fzo0ssnn0	|- ( 0 ..^ N ) C_ NN0
6		fnssres	|- ( ( F Fn NN0 /\ ( 0 ..^ N ) C_ NN0 ) -> ( F |` ( 0 ..^ N ) ) Fn ( 0 ..^ N ) )
7	4 5 6	sylancl	|- ( ph -> ( F |` ( 0 ..^ N ) ) Fn ( 0 ..^ N ) )
8		hashfn	|- ( ( F |` ( 0 ..^ N ) ) Fn ( 0 ..^ N ) -> ( # ` ( F |` ( 0 ..^ N ) ) ) = ( # ` ( 0 ..^ N ) ) )
9	7 8	syl	|- ( ph -> ( # ` ( F |` ( 0 ..^ N ) ) ) = ( # ` ( 0 ..^ N ) ) )
10		hashfzo0	|- ( N e. NN0 -> ( # ` ( 0 ..^ N ) ) = N )
11	3 10	syl	|- ( ph -> ( # ` ( 0 ..^ N ) ) = N )
12	9 11	eqtrd	|- ( ph -> ( # ` ( F |` ( 0 ..^ N ) ) ) = N )