Theorem 0csh0

Description: Cyclically shifting an empty set/word always results in the empty word/set. (Contributed by AV, 25-Oct-2018) (Revised by AV, 17-Nov-2018)

	Ref	Expression
Assertion	0csh0	$$⊢\varnothing \mathrm{cyclShift}N=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		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)$$
2	1	a1i	$$⊢N\in \mathbb{Z}\to \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)$$
3		iftrue	$$⊢w=\varnothing \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)=\varnothing$$
4	3	ad2antrl	$$⊢\left(N\in \mathbb{Z}\wedge \left(w=\varnothing \wedge n=N\right)\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)=\varnothing$$
5		0nn0	$$⊢0\in {\mathbb{N}}_0$$
6		f0	$$⊢\varnothing :\varnothing ⟶\mathrm{V}$$
7		ffn	$$⊢\varnothing :\varnothing ⟶\mathrm{V}\to \varnothing Fn\varnothing$$
8		fzo0	$$⊢\left(0..^0\right)=\varnothing$$
9	8	eqcomi	$$⊢\varnothing =\left(0..^0\right)$$
10	9	fneq2i	$$⊢\varnothing Fn\varnothing \leftrightarrow \varnothing Fn\left(0..^0\right)$$
11	7 10	sylib	$$⊢\varnothing :\varnothing ⟶\mathrm{V}\to \varnothing Fn\left(0..^0\right)$$
12	6 11	ax-mp	$$⊢\varnothing Fn\left(0..^0\right)$$
13		id	$$⊢0\in {\mathbb{N}}_0\to 0\in {\mathbb{N}}_0$$
14		oveq2	$$⊢l=0\to \left(0..^l\right)=\left(0..^0\right)$$
15	14	fneq2d	$$⊢l=0\to \left(\varnothing Fn\left(0..^l\right)\leftrightarrow \varnothing Fn\left(0..^0\right)\right)$$
16	15	adantl	$$⊢\left(0\in {\mathbb{N}}_0\wedge l=0\right)\to \left(\varnothing Fn\left(0..^l\right)\leftrightarrow \varnothing Fn\left(0..^0\right)\right)$$
17	13 16	rspcedv	$$⊢0\in {\mathbb{N}}_0\to \left(\varnothing Fn\left(0..^0\right)\to \exists l\in {\mathbb{N}}_0\varnothing Fn\left(0..^l\right)\right)$$
18	5 12 17	mp2	$$⊢\exists l\in {\mathbb{N}}_0\varnothing Fn\left(0..^l\right)$$
19		0ex	$$⊢\varnothing \in \mathrm{V}$$
20		fneq1	$$⊢f=\varnothing \to \left(fFn\left(0..^l\right)\leftrightarrow \varnothing Fn\left(0..^l\right)\right)$$
21	20	rexbidv	$$⊢f=\varnothing \to \left(\exists l\in {\mathbb{N}}_{0}fFn\left(0..^l\right)\leftrightarrow \exists l\in {\mathbb{N}}_0\varnothing Fn\left(0..^l\right)\right)$$
22	19 21	elab	$$⊢\varnothing \in \left\{f|\exists l\in {\mathbb{N}}_{0}fFn\left(0..^l\right)\right\}\leftrightarrow \exists l\in {\mathbb{N}}_0\varnothing Fn\left(0..^l\right)$$
23	18 22	mpbir	$$⊢\varnothing \in \left\{f|\exists l\in {\mathbb{N}}_{0}fFn\left(0..^l\right)\right\}$$
24	23	a1i	$$⊢N\in \mathbb{Z}\to \varnothing \in \left\{f|\exists l\in {\mathbb{N}}_{0}fFn\left(0..^l\right)\right\}$$
25		id	$$⊢N\in \mathbb{Z}\to N\in \mathbb{Z}$$
26	19	a1i	$$⊢N\in \mathbb{Z}\to \varnothing \in \mathrm{V}$$
27	2 4 24 25 26	ovmpod	$$⊢N\in \mathbb{Z}\to \varnothing \mathrm{cyclShift}N=\varnothing$$
28		cshnz	$$⊢\neg N\in \mathbb{Z}\to \varnothing \mathrm{cyclShift}N=\varnothing$$
29	27 28	pm2.61i	$$⊢\varnothing \mathrm{cyclShift}N=\varnothing$$