Metamath Proof Explorer

Theorem cshw0

Description: A word cyclically shifted by 0 is the word itself. (Contributed by AV, 16-May-2018) (Revised by AV, 20-May-2018) (Revised by AV, 26-Oct-2018)

Ref Expression
Assertion cshw0 ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift 0 ) = 𝑊 )

Proof

Step Hyp Ref Expression
1 0csh0 ⊢ ( ∅ cyclShift 0 ) = ∅
2 oveq1 ⊢ ( ∅ = 𝑊 → ( ∅ cyclShift 0 ) = ( 𝑊 cyclShift 0 ) )
3 id ⊢ ( ∅ = 𝑊 → ∅ = 𝑊 )
4 1 2 3 3eqtr3a ⊢ ( ∅ = 𝑊 → ( 𝑊 cyclShift 0 ) = 𝑊 )
5 4 a1d ⊢ ( ∅ = 𝑊 → ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift 0 ) = 𝑊 ) )
6 0z ⊢ 0 ∈ ℤ
7 cshword ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 0 ∈ ℤ ) → ( 𝑊 cyclShift 0 ) = ( ( 𝑊 substr ⟨ ( 0 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 0 mod ( ♯ ‘ 𝑊 ) ) ) ) )
8 6 7 mpan2 ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift 0 ) = ( ( 𝑊 substr ⟨ ( 0 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 0 mod ( ♯ ‘ 𝑊 ) ) ) ) )
9 8 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ∅ ≠ 𝑊 ) → ( 𝑊 cyclShift 0 ) = ( ( 𝑊 substr ⟨ ( 0 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 0 mod ( ♯ ‘ 𝑊 ) ) ) ) )
10 necom ⊢ ( ∅ ≠ 𝑊 ↔ 𝑊 ≠ ∅ )
11 lennncl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
12 nnrp ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ♯ ‘ 𝑊 ) ∈ ℝ+ )
13 0mod ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℝ+ → ( 0 mod ( ♯ ‘ 𝑊 ) ) = 0 )
14 13 opeq1d ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℝ+ → ⟨ ( 0 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ = ⟨ 0 , ( ♯ ‘ 𝑊 ) ⟩ )
15 14 oveq2d ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℝ+ → ( 𝑊 substr ⟨ ( 0 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ( 𝑊 substr ⟨ 0 , ( ♯ ‘ 𝑊 ) ⟩ ) )
16 13 oveq2d ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℝ+ → ( 𝑊 prefix ( 0 mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 prefix 0 ) )
17 15 16 oveq12d ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℝ+ → ( ( 𝑊 substr ⟨ ( 0 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 0 mod ( ♯ ‘ 𝑊 ) ) ) ) = ( ( 𝑊 substr ⟨ 0 , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix 0 ) ) )
18 11 12 17 3syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 substr ⟨ ( 0 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 0 mod ( ♯ ‘ 𝑊 ) ) ) ) = ( ( 𝑊 substr ⟨ 0 , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix 0 ) ) )
19 10 18 sylan2b ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ∅ ≠ 𝑊 ) → ( ( 𝑊 substr ⟨ ( 0 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 0 mod ( ♯ ‘ 𝑊 ) ) ) ) = ( ( 𝑊 substr ⟨ 0 , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix 0 ) ) )
20 9 19 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ∅ ≠ 𝑊 ) → ( 𝑊 cyclShift 0 ) = ( ( 𝑊 substr ⟨ 0 , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix 0 ) ) )
21 lencl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
22 pfxval ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) → ( 𝑊 prefix ( ♯ ‘ 𝑊 ) ) = ( 𝑊 substr ⟨ 0 , ( ♯ ‘ 𝑊 ) ⟩ ) )
23 21 22 mpdan ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 prefix ( ♯ ‘ 𝑊 ) ) = ( 𝑊 substr ⟨ 0 , ( ♯ ‘ 𝑊 ) ⟩ ) )
24 pfxid ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 prefix ( ♯ ‘ 𝑊 ) ) = 𝑊 )
25 23 24 eqtr3d ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 substr ⟨ 0 , ( ♯ ‘ 𝑊 ) ⟩ ) = 𝑊 )
26 25 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ∅ ≠ 𝑊 ) → ( 𝑊 substr ⟨ 0 , ( ♯ ‘ 𝑊 ) ⟩ ) = 𝑊 )
27 pfx00 ⊢ ( 𝑊 prefix 0 ) = ∅
28 27 a1i ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ∅ ≠ 𝑊 ) → ( 𝑊 prefix 0 ) = ∅ )
29 26 28 oveq12d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ∅ ≠ 𝑊 ) → ( ( 𝑊 substr ⟨ 0 , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix 0 ) ) = ( 𝑊 ++ ∅ ) )
30 ccatrid ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 ++ ∅ ) = 𝑊 )
31 30 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ∅ ≠ 𝑊 ) → ( 𝑊 ++ ∅ ) = 𝑊 )
32 20 29 31 3eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ∅ ≠ 𝑊 ) → ( 𝑊 cyclShift 0 ) = 𝑊 )
33 32 expcom ⊢ ( ∅ ≠ 𝑊 → ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift 0 ) = 𝑊 ) )
34 5 33 pm2.61ine ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift 0 ) = 𝑊 )