Metamath Proof Explorer

Theorem cshword

Description: Perform a cyclical shift for a word. (Contributed by Alexander van der Vekens, 20-May-2018) (Revised by AV, 12-Oct-2022)

Ref Expression
Assertion cshword ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to {W}\mathrm{cyclShift}{N}=\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)$

Proof

Step Hyp Ref Expression
1 iswrd ${⊢}{W}\in \mathrm{Word}{V}↔\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{W}:\left(0..^{l}\right)⟶{V}$
2 ffn ${⊢}{W}:\left(0..^{l}\right)⟶{V}\to {W}Fn\left(0..^{l}\right)$
3 2 reximi ${⊢}\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{W}:\left(0..^{l}\right)⟶{V}\to \exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{W}Fn\left(0..^{l}\right)$
4 1 3 sylbi ${⊢}{W}\in \mathrm{Word}{V}\to \exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{W}Fn\left(0..^{l}\right)$
5 fneq1 ${⊢}{w}={W}\to \left({w}Fn\left(0..^{l}\right)↔{W}Fn\left(0..^{l}\right)\right)$
6 5 rexbidv ${⊢}{w}={W}\to \left(\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{w}Fn\left(0..^{l}\right)↔\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{W}Fn\left(0..^{l}\right)\right)$
7 6 elabg ${⊢}{W}\in \mathrm{Word}{V}\to \left({W}\in \left\{{w}|\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{w}Fn\left(0..^{l}\right)\right\}↔\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{W}Fn\left(0..^{l}\right)\right)$
8 4 7 mpbird ${⊢}{W}\in \mathrm{Word}{V}\to {W}\in \left\{{w}|\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{w}Fn\left(0..^{l}\right)\right\}$
9 cshfn ${⊢}\left({W}\in \left\{{w}|\exists {l}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{w}Fn\left(0..^{l}\right)\right\}\wedge {N}\in ℤ\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)$
10 8 9 sylan ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\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)$
11 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$
12 11 adantr ${⊢}\left({W}=\varnothing \wedge \left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\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$
13 oveq1 ${⊢}{W}=\varnothing \to {W}\mathrm{substr}⟨{N}\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩=\varnothing \mathrm{substr}⟨{N}\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩$
14 swrd0 ${⊢}\varnothing \mathrm{substr}⟨{N}\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩=\varnothing$
15 13 14 eqtrdi ${⊢}{W}=\varnothing \to {W}\mathrm{substr}⟨{N}\mathrm{mod}\left|{W}\right|,\left|{W}\right|⟩=\varnothing$
16 oveq1 ${⊢}{W}=\varnothing \to {W}\mathrm{prefix}\left({N}\mathrm{mod}\left|{W}\right|\right)=\varnothing \mathrm{prefix}\left({N}\mathrm{mod}\left|{W}\right|\right)$
17 pfx0 ${⊢}\varnothing \mathrm{prefix}\left({N}\mathrm{mod}\left|{W}\right|\right)=\varnothing$
18 16 17 eqtrdi ${⊢}{W}=\varnothing \to {W}\mathrm{prefix}\left({N}\mathrm{mod}\left|{W}\right|\right)=\varnothing$
19 15 18 oveq12d ${⊢}{W}=\varnothing \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)=\varnothing \mathrm{++}\varnothing$
20 19 adantr ${⊢}\left({W}=\varnothing \wedge \left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\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)=\varnothing \mathrm{++}\varnothing$
21 ccatidid ${⊢}\varnothing \mathrm{++}\varnothing =\varnothing$
22 20 21 eqtr2di ${⊢}\left({W}=\varnothing \wedge \left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\right)\to \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)$
23 12 22 eqtrd ${⊢}\left({W}=\varnothing \wedge \left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\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)=\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)$
24 iffalse ${⊢}¬{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)=\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)$
25 24 adantr ${⊢}\left(¬{W}=\varnothing \wedge \left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\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)=\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)$
26 23 25 pm2.61ian ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\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)=\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)$
27 10 26 eqtrd ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {N}\in ℤ\right)\to {W}\mathrm{cyclShift}{N}=\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)$