Theorem sseqfres

Description: The first elements in the strong recursive sequence are the sequence initializer. (Contributed by Thierry Arnoux, 23-Apr-2019)

	Ref	Expression
Hypotheses	sseqval.1	$$⊢\phi \to S\in \mathrm{V}$$
	sseqval.2	$$⊢\phi \to M\in \mathrm{Word}S$$
	sseqval.3	$$⊢W=\mathrm{Word}S\cap {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge \left|M\right|}\right]$$
	sseqval.4	$$⊢\phi \to F:W⟶S$$
Assertion	sseqfres	$$⊢\phi \to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^\left|M\right|\right)}=M$$

Proof

Step	Hyp	Ref	Expression
1		sseqval.1	$$⊢\phi \to S\in \mathrm{V}$$
2		sseqval.2	$$⊢\phi \to M\in \mathrm{Word}S$$
3		sseqval.3	$$⊢W=\mathrm{Word}S\cap {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge \left|M\right|}\right]$$
4		sseqval.4	$$⊢\phi \to F:W⟶S$$
5	1	adantr	$$⊢\left(\phi \wedge i\in \left(0..^\left|M\right|\right)\right)\to S\in \mathrm{V}$$
6	2	adantr	$$⊢\left(\phi \wedge i\in \left(0..^\left|M\right|\right)\right)\to M\in \mathrm{Word}S$$
7	4	adantr	$$⊢\left(\phi \wedge i\in \left(0..^\left|M\right|\right)\right)\to F:W⟶S$$
8		simpr	$$⊢\left(\phi \wedge i\in \left(0..^\left|M\right|\right)\right)\to i\in \left(0..^\left|M\right|\right)$$
9	5 6 3 7 8	sseqfv1	$$⊢\left(\phi \wedge i\in \left(0..^\left|M\right|\right)\right)\to \left(M{\mathrm{seq}}_{str}F\right)\left(i\right)=M\left(i\right)$$
10	9	ralrimiva	$$⊢\phi \to \forall i\in \left(0..^\left|M\right|\right)\left(M{\mathrm{seq}}_{str}F\right)\left(i\right)=M\left(i\right)$$
11	1 2 3 4	sseqfn	$$⊢\phi \to \left(M{\mathrm{seq}}_{str}F\right)Fn{\mathbb{N}}_0$$
12		wrdfn	$$⊢M\in \mathrm{Word}S\to MFn\left(0..^\left|M\right|\right)$$
13	2 12	syl	$$⊢\phi \to MFn\left(0..^\left|M\right|\right)$$
14		fzo0ssnn0	$$⊢\left(0..^\left|M\right|\right)\subseteq {\mathbb{N}}_0$$
15	14	a1i	$$⊢\phi \to \left(0..^\left|M\right|\right)\subseteq {\mathbb{N}}_0$$
16		fvreseq1	$$⊢\left(\left(\left(M{\mathrm{seq}}_{str}F\right)Fn{\mathbb{N}}_0\wedge MFn\left(0..^\left|M\right|\right)\right)\wedge \left(0..^\left|M\right|\right)\subseteq {\mathbb{N}}_0\right)\to \left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^\left|M\right|\right)}=M\leftrightarrow \forall i\in \left(0..^\left|M\right|\right)\left(M{\mathrm{seq}}_{str}F\right)\left(i\right)=M\left(i\right)\right)$$
17	11 13 15 16	syl21anc	$$⊢\phi \to \left({\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^\left|M\right|\right)}=M\leftrightarrow \forall i\in \left(0..^\left|M\right|\right)\left(M{\mathrm{seq}}_{str}F\right)\left(i\right)=M\left(i\right)\right)$$
18	10 17	mpbird	$$⊢\phi \to {\left(M{\mathrm{seq}}_{str}F\right)\upharpoonright }_{\left(0..^\left|M\right|\right)}=M$$