This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cshwcl

Description: A cyclically shifted word is a word over the same set as for the original word. (Contributed by AV, 16-May-2018) (Revised by AV, 21-May-2018) (Revised by AV, 27-Oct-2018)

Ref Expression
Assertion cshwcl ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift 𝑁 ) ∈ Word 𝑉 )

Proof

Step Hyp Ref Expression
1 cshword ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) = ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
2 swrdcl ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝑉 )
3 pfxcl ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ∈ Word 𝑉 )
4 ccatcl ⊢ ( ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝑉 ∧ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ∈ Word 𝑉 ) → ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ Word 𝑉 )
5 2 3 4 syl2anc ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ Word 𝑉 )
6 5 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ Word 𝑉 )
7 1 6 eqeltrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) ∈ Word 𝑉 )
8 7 expcom ⊢ ( 𝑁 ∈ ℤ → ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift 𝑁 ) ∈ Word 𝑉 ) )
9 cshnz ⊢ ( ¬ 𝑁 ∈ ℤ → ( 𝑊 cyclShift 𝑁 ) = ∅ )
10 wrd0 ⊢ ∅ ∈ Word 𝑉
11 9 10 eqeltrdi ⊢ ( ¬ 𝑁 ∈ ℤ → ( 𝑊 cyclShift 𝑁 ) ∈ Word 𝑉 )
12 11 a1d ⊢ ( ¬ 𝑁 ∈ ℤ → ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift 𝑁 ) ∈ Word 𝑉 ) )
13 8 12 pm2.61i ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift 𝑁 ) ∈ Word 𝑉 )