# Metamath Proof Explorer

## 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 {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{f}Fn\left(0..^{l}\right)\right\},{n}\in ℤ⟼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 ℤ\to \mathrm{cyclShift}=\left({w}\in \left\{{f}|\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{f}Fn\left(0..^{l}\right)\right\},{n}\in ℤ⟼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 ℤ\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 {ℕ}_{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 ↔\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 {ℕ}_{0}\to 0\in {ℕ}_{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)↔\varnothing Fn\left(0..^0\right)\right)$
16 15 adantl ${⊢}\left(0\in {ℕ}_{0}\wedge {l}=0\right)\to \left(\varnothing Fn\left(0..^{l}\right)↔\varnothing Fn\left(0..^0\right)\right)$
17 13 16 rspcedv ${⊢}0\in {ℕ}_{0}\to \left(\varnothing Fn\left(0..^0\right)\to \exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\varnothing Fn\left(0..^{l}\right)\right)$
18 5 12 17 mp2 ${⊢}\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\varnothing Fn\left(0..^{l}\right)$
19 0ex ${⊢}\varnothing \in \mathrm{V}$
20 fneq1 ${⊢}{f}=\varnothing \to \left({f}Fn\left(0..^{l}\right)↔\varnothing Fn\left(0..^{l}\right)\right)$
21 20 rexbidv ${⊢}{f}=\varnothing \to \left(\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{f}Fn\left(0..^{l}\right)↔\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\varnothing Fn\left(0..^{l}\right)\right)$
22 19 21 elab ${⊢}\varnothing \in \left\{{f}|\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{f}Fn\left(0..^{l}\right)\right\}↔\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\varnothing Fn\left(0..^{l}\right)$
23 18 22 mpbir ${⊢}\varnothing \in \left\{{f}|\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{f}Fn\left(0..^{l}\right)\right\}$
24 23 a1i ${⊢}{N}\in ℤ\to \varnothing \in \left\{{f}|\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{f}Fn\left(0..^{l}\right)\right\}$
25 id ${⊢}{N}\in ℤ\to {N}\in ℤ$
26 19 a1i ${⊢}{N}\in ℤ\to \varnothing \in \mathrm{V}$
27 2 4 24 25 26 ovmpod ${⊢}{N}\in ℤ\to \varnothing \mathrm{cyclShift}{N}=\varnothing$
28 cshnz ${⊢}¬{N}\in ℤ\to \varnothing \mathrm{cyclShift}{N}=\varnothing$
29 27 28 pm2.61i ${⊢}\varnothing \mathrm{cyclShift}{N}=\varnothing$