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 𝑉 )