Theorem cshfn

Description: Perform a cyclical shift for a function over a half-open range of nonnegative integers. (Contributed by AV, 20-May-2018) (Revised by AV, 17-Nov-2018) (Revised by AV, 4-Nov-2022)

	Ref	Expression
Assertion	cshfn	$$⊢\left(W\in \left\{f|\exists l\in {\mathbb{N}}_{0}fFn\left(0..^l\right)\right\}\wedge N\in \mathbb{Z}\right)\to W\mathrm{cyclShift}N=if\left(W=\varnothing ,\varnothing ,\left(W\mathrm{substr}⟨N\mathrm{mod}\left|W\right|,\left|W\right|⟩\right)\mathrm{++}\left(W\mathrm{prefix}\left(N\mathrm{mod}\left|W\right|\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$$⊢w=W\to \left(w=\varnothing \leftrightarrow W=\varnothing \right)$$
2	1	adantr	$$⊢\left(w=W\wedge n=N\right)\to \left(w=\varnothing \leftrightarrow W=\varnothing \right)$$
3		simpl	$$⊢\left(w=W\wedge n=N\right)\to w=W$$
4		simpr	$$⊢\left(w=W\wedge n=N\right)\to n=N$$
5		fveq2	$$⊢w=W\to \left|w\right|=\left|W\right|$$
6	5	adantr	$$⊢\left(w=W\wedge n=N\right)\to \left|w\right|=\left|W\right|$$
7	4 6	oveq12d	$$⊢\left(w=W\wedge n=N\right)\to n\mathrm{mod}\left|w\right|=N\mathrm{mod}\left|W\right|$$
8	7 6	opeq12d	$$⊢\left(w=W\wedge n=N\right)\to ⟨n\mathrm{mod}\left|w\right|,\left|w\right|⟩=⟨N\mathrm{mod}\left|W\right|,\left|W\right|⟩$$
9	3 8	oveq12d	$$⊢\left(w=W\wedge n=N\right)\to w\mathrm{substr}⟨n\mathrm{mod}\left|w\right|,\left|w\right|⟩=W\mathrm{substr}⟨N\mathrm{mod}\left|W\right|,\left|W\right|⟩$$
10	3 7	oveq12d	$$⊢\left(w=W\wedge n=N\right)\to w\mathrm{prefix}\left(n\mathrm{mod}\left|w\right|\right)=W\mathrm{prefix}\left(N\mathrm{mod}\left|W\right|\right)$$
11	9 10	oveq12d	$$⊢\left(w=W\wedge n=N\right)\to \left(w\mathrm{substr}⟨n\mathrm{mod}\left|w\right|,\left|w\right|⟩\right)\mathrm{++}\left(w\mathrm{prefix}\left(n\mathrm{mod}\left|w\right|\right)\right)=\left(W\mathrm{substr}⟨N\mathrm{mod}\left|W\right|,\left|W\right|⟩\right)\mathrm{++}\left(W\mathrm{prefix}\left(N\mathrm{mod}\left|W\right|\right)\right)$$
12	2 11	ifbieq2d	$$⊢\left(w=W\wedge n=N\right)\to if\left(w=\varnothing ,\varnothing ,\left(w\mathrm{substr}⟨n\mathrm{mod}\left|w\right|,\left|w\right|⟩\right)\mathrm{++}\left(w\mathrm{prefix}\left(n\mathrm{mod}\left|w\right|\right)\right)\right)=if\left(W=\varnothing ,\varnothing ,\left(W\mathrm{substr}⟨N\mathrm{mod}\left|W\right|,\left|W\right|⟩\right)\mathrm{++}\left(W\mathrm{prefix}\left(N\mathrm{mod}\left|W\right|\right)\right)\right)$$
13		df-csh	$$⊢\mathrm{cyclShift}=\left(w\in \left\{f|\exists l\in {\mathbb{N}}_{0}fFn\left(0..^l\right)\right\},n\in \mathbb{Z}⟼if\left(w=\varnothing ,\varnothing ,\left(w\mathrm{substr}⟨n\mathrm{mod}\left|w\right|,\left|w\right|⟩\right)\mathrm{++}\left(w\mathrm{prefix}\left(n\mathrm{mod}\left|w\right|\right)\right)\right)\right)$$
14		0ex	$$⊢\varnothing \in \mathrm{V}$$
15		ovex	$$⊢\left(W\mathrm{substr}⟨N\mathrm{mod}\left|W\right|,\left|W\right|⟩\right)\mathrm{++}\left(W\mathrm{prefix}\left(N\mathrm{mod}\left|W\right|\right)\right)\in \mathrm{V}$$
16	14 15	ifex	$$⊢if\left(W=\varnothing ,\varnothing ,\left(W\mathrm{substr}⟨N\mathrm{mod}\left|W\right|,\left|W\right|⟩\right)\mathrm{++}\left(W\mathrm{prefix}\left(N\mathrm{mod}\left|W\right|\right)\right)\right)\in \mathrm{V}$$
17	12 13 16	ovmpoa	$$⊢\left(W\in \left\{f|\exists l\in {\mathbb{N}}_{0}fFn\left(0..^l\right)\right\}\wedge N\in \mathbb{Z}\right)\to W\mathrm{cyclShift}N=if\left(W=\varnothing ,\varnothing ,\left(W\mathrm{substr}⟨N\mathrm{mod}\left|W\right|,\left|W\right|⟩\right)\mathrm{++}\left(W\mathrm{prefix}\left(N\mathrm{mod}\left|W\right|\right)\right)\right)$$