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 ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N = W substr N mod W W ++ W prefix N mod W

Proof

Step Hyp Ref Expression
1 iswrd ⊢ W ∈ Word V ↔ ∃ l ∈ ℕ 0 W : 0 ..^ l ⟶ V
2 ffn ⊢ W : 0 ..^ l ⟶ V → W Fn 0 ..^ l
3 2 reximi ⊢ ∃ l ∈ ℕ 0 W : 0 ..^ l ⟶ V → ∃ l ∈ ℕ 0 W Fn 0 ..^ l
4 1 3 sylbi ⊢ W ∈ Word V → ∃ l ∈ ℕ 0 W Fn 0 ..^ l
5 fneq1 ⊢ w = W → w Fn 0 ..^ l ↔ W Fn 0 ..^ l
6 5 rexbidv ⊢ w = W → ∃ l ∈ ℕ 0 w Fn 0 ..^ l ↔ ∃ l ∈ ℕ 0 W Fn 0 ..^ l
7 6 elabg ⊢ W ∈ Word V → W ∈ w | ∃ l ∈ ℕ 0 w Fn 0 ..^ l ↔ ∃ l ∈ ℕ 0 W Fn 0 ..^ l
8 4 7 mpbird ⊢ W ∈ Word V → W ∈ w | ∃ l ∈ ℕ 0 w Fn 0 ..^ l
9 cshfn ⊢ W ∈ w | ∃ l ∈ ℕ 0 w Fn 0 ..^ l ∧ N ∈ ℤ → W cyclShift N = if W = ∅ ∅ W substr N mod W W ++ W prefix N mod W
10 8 9 sylan ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N = if W = ∅ ∅ W substr N mod W W ++ W prefix N mod W
11 iftrue ⊢ W = ∅ → if W = ∅ ∅ W substr N mod W W ++ W prefix N mod W = ∅
12 11 adantr ⊢ W = ∅ ∧ W ∈ Word V ∧ N ∈ ℤ → if W = ∅ ∅ W substr N mod W W ++ W prefix N mod W = ∅
13 oveq1 ⊢ W = ∅ → W substr N mod W W = ∅ substr N mod W W
14 swrd0 ⊢ ∅ substr N mod W W = ∅
15 13 14 eqtrdi ⊢ W = ∅ → W substr N mod W W = ∅
16 oveq1 ⊢ W = ∅ → W prefix N mod W = ∅ prefix N mod W
17 pfx0 ⊢ ∅ prefix N mod W = ∅
18 16 17 eqtrdi ⊢ W = ∅ → W prefix N mod W = ∅
19 15 18 oveq12d ⊢ W = ∅ → W substr N mod W W ++ W prefix N mod W = ∅ ++ ∅
20 19 adantr ⊢ W = ∅ ∧ W ∈ Word V ∧ N ∈ ℤ → W substr N mod W W ++ W prefix N mod W = ∅ ++ ∅
21 ccatidid ⊢ ∅ ++ ∅ = ∅
22 20 21 eqtr2di ⊢ W = ∅ ∧ W ∈ Word V ∧ N ∈ ℤ → ∅ = W substr N mod W W ++ W prefix N mod W
23 12 22 eqtrd ⊢ W = ∅ ∧ W ∈ Word V ∧ N ∈ ℤ → if W = ∅ ∅ W substr N mod W W ++ W prefix N mod W = W substr N mod W W ++ W prefix N mod W
24 iffalse ⊢ ¬ W = ∅ → if W = ∅ ∅ W substr N mod W W ++ W prefix N mod W = W substr N mod W W ++ W prefix N mod W
25 24 adantr ⊢ ¬ W = ∅ ∧ W ∈ Word V ∧ N ∈ ℤ → if W = ∅ ∅ W substr N mod W W ++ W prefix N mod W = W substr N mod W W ++ W prefix N mod W
26 23 25 pm2.61ian ⊢ W ∈ Word V ∧ N ∈ ℤ → if W = ∅ ∅ W substr N mod W W ++ W prefix N mod W = W substr N mod W W ++ W prefix N mod W
27 10 26 eqtrd ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N = W substr N mod W W ++ W prefix N mod W