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