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 ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) = ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 iswrd ⊢ ( 𝑊 ∈ Word 𝑉 ↔ ∃ 𝑙 ∈ ℕ0 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑉 )
2 ffn ⊢ ( 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑉 → 𝑊 Fn ( 0 ..^ 𝑙 ) )
3 2 reximi ⊢ ( ∃ 𝑙 ∈ ℕ0 𝑊 : ( 0 ..^ 𝑙 ) ⟶ 𝑉 → ∃ 𝑙 ∈ ℕ0 𝑊 Fn ( 0 ..^ 𝑙 ) )
4 1 3 sylbi ⊢ ( 𝑊 ∈ Word 𝑉 → ∃ 𝑙 ∈ ℕ0 𝑊 Fn ( 0 ..^ 𝑙 ) )
5 fneq1 ⊢ ( 𝑤 = 𝑊 → ( 𝑤 Fn ( 0 ..^ 𝑙 ) ↔ 𝑊 Fn ( 0 ..^ 𝑙 ) ) )
6 5 rexbidv ⊢ ( 𝑤 = 𝑊 → ( ∃ 𝑙 ∈ ℕ0 𝑤 Fn ( 0 ..^ 𝑙 ) ↔ ∃ 𝑙 ∈ ℕ0 𝑊 Fn ( 0 ..^ 𝑙 ) ) )
7 6 elabg ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 ∈ { 𝑤 ∣ ∃ 𝑙 ∈ ℕ0 𝑤 Fn ( 0 ..^ 𝑙 ) } ↔ ∃ 𝑙 ∈ ℕ0 𝑊 Fn ( 0 ..^ 𝑙 ) ) )
8 4 7 mpbird ⊢ ( 𝑊 ∈ Word 𝑉 → 𝑊 ∈ { 𝑤 ∣ ∃ 𝑙 ∈ ℕ0 𝑤 Fn ( 0 ..^ 𝑙 ) } )
9 cshfn ⊢ ( ( 𝑊 ∈ { 𝑤 ∣ ∃ 𝑙 ∈ ℕ0 𝑤 Fn ( 0 ..^ 𝑙 ) } ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) = if ( 𝑊 = ∅ , ∅ , ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
10 8 9 sylan ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) = if ( 𝑊 = ∅ , ∅ , ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
11 iftrue ⊢ ( 𝑊 = ∅ → if ( 𝑊 = ∅ , ∅ , ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) = ∅ )
12 11 adantr ⊢ ( ( 𝑊 = ∅ ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ) → if ( 𝑊 = ∅ , ∅ , ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) = ∅ )
13 oveq1 ⊢ ( 𝑊 = ∅ → ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ( ∅ substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) )
14 swrd0 ⊢ ( ∅ substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ∅
15 13 14 eqtrdi ⊢ ( 𝑊 = ∅ → ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ∅ )
16 oveq1 ⊢ ( 𝑊 = ∅ → ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) = ( ∅ prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )
17 pfx0 ⊢ ( ∅ prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) = ∅
18 16 17 eqtrdi ⊢ ( 𝑊 = ∅ → ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) = ∅ )
19 15 18 oveq12d ⊢ ( 𝑊 = ∅ → ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) = ( ∅ ++ ∅ ) )
20 19 adantr ⊢ ( ( 𝑊 = ∅ ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) = ( ∅ ++ ∅ ) )
21 ccatidid ⊢ ( ∅ ++ ∅ ) = ∅
22 20 21 eqtr2di ⊢ ( ( 𝑊 = ∅ ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ) → ∅ = ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
23 12 22 eqtrd ⊢ ( ( 𝑊 = ∅ ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ) → if ( 𝑊 = ∅ , ∅ , ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) = ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
24 iffalse ⊢ ( ¬ 𝑊 = ∅ → if ( 𝑊 = ∅ , ∅ , ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) = ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
25 24 adantr ⊢ ( ( ¬ 𝑊 = ∅ ∧ ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) ) → if ( 𝑊 = ∅ , ∅ , ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) = ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
26 23 25 pm2.61ian ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → if ( 𝑊 = ∅ , ∅ , ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) = ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
27 10 26 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) = ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )