2cshwcshw - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > 2cshwcshw		Structured version Visualization version GIF version

Theorem 2cshwcshw 13422

Description: If a word is a cyclically shifted word, and a second word is the result of cyclically shifting the same word, then the second word is the result of cyclically shifting the first word. (Contributed by AV, 11-May-2018.) (Revised by AV, 12-Jun-2018.) (Proof shortened by AV, 3-Nov-2018.)

**Assertion**
Ref	Expression
2cshwcshw	⊢ ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → ((𝐾 ∈ (0...𝑁) ∧ 𝑋 = (𝑌 cyclShift 𝐾) ∧ ∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))

Distinct variable groups: 𝑚,𝑛,𝐾 𝑚,𝑁,𝑛 𝑚,𝑉,𝑛 𝑚,𝑋,𝑛 𝑚,𝑌,𝑛 𝑚,𝑍,𝑛

**Proof of Theorem 2cshwcshw**
Step	Hyp	Ref	Expression
1		difelfznle 12322	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ (0...𝑁) ∧ 𝑚 ∈ (0...𝑁) ∧ ¬ 𝐾 ≤ 𝑚) → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁))
2	1	3exp 1256	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → (¬ 𝐾 ≤ 𝑚 → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁))))
3	2	ad2antrr 758	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑚 ∈ (0...𝑁) → (¬ 𝐾 ≤ 𝑚 → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁))))
4	3	imp 444	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) → (¬ 𝐾 ≤ 𝑚 → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁)))
5	4	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → (¬ 𝐾 ≤ 𝑚 → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁)))
6	5	com12 32	. . . . . . . . . . . . . 14 ⊢ (¬ 𝐾 ≤ 𝑚 → (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁)))
7	6	adantl 481	. . . . . . . . . . . . 13 ⊢ ((¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚) → (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁)))
8	7	imp 444	. . . . . . . . . . . 12 ⊢ (((¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚) ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁))
9		simprl 790	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → 𝑌 ∈ Word 𝑉)
10	9	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → 𝑌 ∈ Word 𝑉)
11		elfzelz 12213	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℤ)
12	11	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → 𝐾 ∈ ℤ)
13	12	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → 𝐾 ∈ ℤ)
14		elfz2 12204	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐾 ∈ (0...𝑁) ↔ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
15		elfzelz 12213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℤ)
16		zaddcl 11294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑚 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑚 + 𝑁) ∈ ℤ)
17	16	adantrr 749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑚 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝑚 + 𝑁) ∈ ℤ)
18		simprr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑚 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → 𝐾 ∈ ℤ)
19	17, 18	zsubcld 11363	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑚 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ)
20	19	ex 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
21	15, 20	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑚 ∈ (0...𝑁) → ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
22	21	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ (0...𝑁) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
23	22	3adant1 1072	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ (0...𝑁) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
24	23	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) → (𝑚 ∈ (0...𝑁) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
25	14, 24	sylbi 206	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
26	25	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) → (𝑚 ∈ (0...𝑁) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
27	26	imp 444	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ)
28		2cshw 13410	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑌 ∈ Word 𝑉 ∧ 𝐾 ∈ ℤ ∧ ((𝑚 + 𝑁) − 𝐾) ∈ ℤ) → ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)) = (𝑌 cyclShift (𝐾 + ((𝑚 + 𝑁) − 𝐾))))
29	10, 13, 27, 28	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)) = (𝑌 cyclShift (𝐾 + ((𝑚 + 𝑁) − 𝐾))))
30	18, 19	zaddcld 11362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑚 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ)
31	30	ex 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
32	15, 31	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑚 ∈ (0...𝑁) → ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
33	32	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ (0...𝑁) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
34	33	3adant1 1072	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ (0...𝑁) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
35	34	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) → (𝑚 ∈ (0...𝑁) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
36	14, 35	sylbi 206	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
37	36	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) → (𝑚 ∈ (0...𝑁) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
38	37	imp 444	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ)
39		cshwsublen 13393	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑌 ∈ Word 𝑉 ∧ (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ) → (𝑌 cyclShift (𝐾 + ((𝑚 + 𝑁) − 𝐾))) = (𝑌 cyclShift ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌))))
40	10, 38, 39	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → (𝑌 cyclShift (𝐾 + ((𝑚 + 𝑁) − 𝐾))) = (𝑌 cyclShift ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌))))
41	29, 40	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)) = (𝑌 cyclShift ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌))))
42		elfz2nn0 12300	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝐾 ≤ 𝑁))
43		elfznn0 12302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℕ₀)
44		nn0cn 11179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 ∈ ℕ₀ → 𝑚 ∈ ℂ)
45		nn0cn 11179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝐾 ∈ ℕ₀ → 𝐾 ∈ ℂ)
46		nn0cn 11179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℂ)
47	45, 46	anim12i 588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ))
48		simprl 790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → 𝐾 ∈ ℂ)
49		addcl 9897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑚 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑚 + 𝑁) ∈ ℂ)
50	49	adantrl 748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → (𝑚 + 𝑁) ∈ ℂ)
51	48, 50	pncan3d 10274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) = (𝑚 + 𝑁))
52	51	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = ((𝑚 + 𝑁) − 𝑁))
53		pncan 10166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑚 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑚 + 𝑁) − 𝑁) = 𝑚)
54	53	adantrl 748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → ((𝑚 + 𝑁) − 𝑁) = 𝑚)
55	52, 54	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚)
56	44, 47, 55	syl2an 493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑚 ∈ ℕ₀ ∧ (𝐾 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀)) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚)
57	56	ex 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 ∈ ℕ₀ → ((𝐾 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
58	43, 57	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑚 ∈ (0...𝑁) → ((𝐾 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
59	58	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
60	59	3adant3 1074	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝐾 ≤ 𝑁) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
61	42, 60	sylbi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
62	61	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
63		oveq2 6557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((#‘𝑌) = 𝑁 → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁))
64	63	eqeq1d 2612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((#‘𝑌) = 𝑁 → (((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = 𝑚 ↔ ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
65	64	imbi2d 329	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((#‘𝑌) = 𝑁 → ((𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = 𝑚) ↔ (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚)))
66	65	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → ((𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = 𝑚) ↔ (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚)))
67	66	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → ((𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = 𝑚) ↔ (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚)))
68	62, 67	mpbird 246	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = 𝑚))
69	68	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = 𝑚))
70	69	imp 444	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = 𝑚)
71	70	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → (𝑌 cyclShift ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌))) = (𝑌 cyclShift 𝑚))
72	41, 71	eqtr2d 2645	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)))
73	72	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)))
74		oveq1 6556	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 = (𝑌 cyclShift 𝐾) → (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)) = ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)))
75	74	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)) = ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)))
76	73, 75	eqtr4d 2647	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑌 cyclShift 𝑚) = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)))
77	76	exp41 636	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → ((¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚) → (𝑚 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑌 cyclShift 𝑚) = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))))))
78	77	com24 93	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑚 ∈ (0...𝑁) → ((¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚) → (𝑌 cyclShift 𝑚) = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))))))
79	78	imp41 617	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) → (𝑌 cyclShift 𝑚) = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)))
80	79	eqeq2d 2620	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) → (𝑍 = (𝑌 cyclShift 𝑚) ↔ 𝑍 = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))))
81	80	biimpd 218	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) → (𝑍 = (𝑌 cyclShift 𝑚) → 𝑍 = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))))
82	81	impancom 455	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ((¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚) → 𝑍 = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))))
83	82	impcom 445	. . . . . . . . . . . 12 ⊢ (((¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚) ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → 𝑍 = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)))
84		oveq2 6557	. . . . . . . . . . . . . 14 ⊢ (𝑛 = ((𝑚 + 𝑁) − 𝐾) → (𝑋 cyclShift 𝑛) = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)))
85	84	eqeq2d 2620	. . . . . . . . . . . . 13 ⊢ (𝑛 = ((𝑚 + 𝑁) − 𝐾) → (𝑍 = (𝑋 cyclShift 𝑛) ↔ 𝑍 = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))))
86	85	rspcev 3282	. . . . . . . . . . . 12 ⊢ ((((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁) ∧ 𝑍 = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
87	8, 83, 86	syl2anc 691	. . . . . . . . . . 11 ⊢ (((¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚) ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
88	87	exp31 628	. . . . . . . . . 10 ⊢ (¬ 𝑚 = 0 → (¬ 𝐾 ≤ 𝑚 → (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))
89		oveq2 6557	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 0 → (𝑌 cyclShift 𝑚) = (𝑌 cyclShift 0))
90	89	eqeq2d 2620	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 0 → (𝑍 = (𝑌 cyclShift 𝑚) ↔ 𝑍 = (𝑌 cyclShift 0)))
91		cshw0 13391	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑌 ∈ Word 𝑉 → (𝑌 cyclShift 0) = 𝑌)
92	91	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → (𝑌 cyclShift 0) = 𝑌)
93	92	eqeq2d 2620	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → (𝑍 = (𝑌 cyclShift 0) ↔ 𝑍 = 𝑌))
94		fznn0sub2 12315	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐾 ∈ (0...𝑁) → (𝑁 − 𝐾) ∈ (0...𝑁))
95	94	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ∈ (0...𝑁))
96		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((#‘𝑌) = 𝑁 → ((#‘𝑌) − 𝐾) = (𝑁 − 𝐾))
97	96	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((#‘𝑌) = 𝑁 → (((#‘𝑌) − 𝐾) ∈ (0...𝑁) ↔ (𝑁 − 𝐾) ∈ (0...𝑁)))
98	97	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) → (((#‘𝑌) − 𝐾) ∈ (0...𝑁) ↔ (𝑁 − 𝐾) ∈ (0...𝑁)))
99	95, 98	mpbird 246	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) → ((#‘𝑌) − 𝐾) ∈ (0...𝑁))
100	99	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → ((#‘𝑌) − 𝐾) ∈ (0...𝑁))
101		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑋 = (𝑌 cyclShift 𝐾) → (𝑋 cyclShift ((#‘𝑌) − 𝐾)) = ((𝑌 cyclShift 𝐾) cyclShift ((#‘𝑌) − 𝐾)))
102		simpl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → 𝑌 ∈ Word 𝑉)
103		2cshwid 13411	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑌 ∈ Word 𝑉 ∧ 𝐾 ∈ ℤ) → ((𝑌 cyclShift 𝐾) cyclShift ((#‘𝑌) − 𝐾)) = 𝑌)
104	102, 11, 103	syl2an 493	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) → ((𝑌 cyclShift 𝐾) cyclShift ((#‘𝑌) − 𝐾)) = 𝑌)
105	101, 104	sylan9eqr 2666	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑋 cyclShift ((#‘𝑌) − 𝐾)) = 𝑌)
106	105	eqcomd 2616	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → 𝑌 = (𝑋 cyclShift ((#‘𝑌) − 𝐾)))
107		oveq2 6557	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = ((#‘𝑌) − 𝐾) → (𝑋 cyclShift 𝑛) = (𝑋 cyclShift ((#‘𝑌) − 𝐾)))
108	107	eqeq2d 2620	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = ((#‘𝑌) − 𝐾) → (𝑌 = (𝑋 cyclShift 𝑛) ↔ 𝑌 = (𝑋 cyclShift ((#‘𝑌) − 𝐾))))
109	108	rspcev 3282	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((#‘𝑌) − 𝐾) ∈ (0...𝑁) ∧ 𝑌 = (𝑋 cyclShift ((#‘𝑌) − 𝐾))) → ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛))
110	100, 106, 109	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛))
111	110	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑍 = 𝑌) → ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛))
112		eqeq1 2614	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑍 = 𝑌 → (𝑍 = (𝑋 cyclShift 𝑛) ↔ 𝑌 = (𝑋 cyclShift 𝑛)))
113	112	rexbidv 3034	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑍 = 𝑌 → (∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛) ↔ ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛)))
114	113	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑍 = 𝑌) → (∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛) ↔ ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛)))
115	111, 114	mpbird 246	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑍 = 𝑌) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
116	115	exp41 636	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → (𝐾 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑍 = 𝑌 → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
117	116	com24 93	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → (𝑍 = 𝑌 → (𝑋 = (𝑌 cyclShift 𝐾) → (𝐾 ∈ (0...𝑁) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
118	93, 117	sylbid 229	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → (𝑍 = (𝑌 cyclShift 0) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝐾 ∈ (0...𝑁) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
119	118	com24 93	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → (𝐾 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑍 = (𝑌 cyclShift 0) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
120	119	impcom 445	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑍 = (𝑌 cyclShift 0) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))
121	120	com13 86	. . . . . . . . . . . . . . . 16 ⊢ (𝑍 = (𝑌 cyclShift 0) → (𝑋 = (𝑌 cyclShift 𝐾) → ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))
122	121	a1d 25	. . . . . . . . . . . . . . 15 ⊢ (𝑍 = (𝑌 cyclShift 0) → (𝑚 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
123	90, 122	syl6bi 242	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 0 → (𝑍 = (𝑌 cyclShift 𝑚) → (𝑚 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))))
124	123	com24 93	. . . . . . . . . . . . 13 ⊢ (𝑚 = 0 → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑚 ∈ (0...𝑁) → (𝑍 = (𝑌 cyclShift 𝑚) → ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))))
125	124	com15 99	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑚 ∈ (0...𝑁) → (𝑍 = (𝑌 cyclShift 𝑚) → (𝑚 = 0 → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))))
126	125	imp41 617	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → (𝑚 = 0 → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
127	126	com12 32	. . . . . . . . . 10 ⊢ (𝑚 = 0 → (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
128		difelfzle 12321	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ (0...𝑁) ∧ 𝑚 ∈ (0...𝑁) ∧ 𝐾 ≤ 𝑚) → (𝑚 − 𝐾) ∈ (0...𝑁))
129	128	3exp 1256	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → (𝐾 ≤ 𝑚 → (𝑚 − 𝐾) ∈ (0...𝑁))))
130	129	ad2antrr 758	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑚 ∈ (0...𝑁) → (𝐾 ≤ 𝑚 → (𝑚 − 𝐾) ∈ (0...𝑁))))
131	130	imp 444	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) → (𝐾 ≤ 𝑚 → (𝑚 − 𝐾) ∈ (0...𝑁)))
132	131	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → (𝐾 ≤ 𝑚 → (𝑚 − 𝐾) ∈ (0...𝑁)))
133	132	impcom 445	. . . . . . . . . . . 12 ⊢ ((𝐾 ≤ 𝑚 ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → (𝑚 − 𝐾) ∈ (0...𝑁))
134	9	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) → 𝑌 ∈ Word 𝑉)
135	12	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) → 𝐾 ∈ ℤ)
136		zsubcl 11296	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 − 𝐾) ∈ ℤ)
137	136	ex 449	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 ∈ ℤ → (𝐾 ∈ ℤ → (𝑚 − 𝐾) ∈ ℤ))
138	15, 11, 137	syl2imc 40	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → (𝑚 − 𝐾) ∈ ℤ))
139	138	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) → (𝑚 ∈ (0...𝑁) → (𝑚 − 𝐾) ∈ ℤ))
140	139	imp 444	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) → (𝑚 − 𝐾) ∈ ℤ)
141		2cshw 13410	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑌 ∈ Word 𝑉 ∧ 𝐾 ∈ ℤ ∧ (𝑚 − 𝐾) ∈ ℤ) → ((𝑌 cyclShift 𝐾) cyclShift (𝑚 − 𝐾)) = (𝑌 cyclShift (𝐾 + (𝑚 − 𝐾))))
142	134, 135, 140, 141	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑌 cyclShift 𝐾) cyclShift (𝑚 − 𝐾)) = (𝑌 cyclShift (𝐾 + (𝑚 − 𝐾))))
143		zcn 11259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐾 ∈ ℤ → 𝐾 ∈ ℂ)
144	15	zcnd 11359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℂ)
145		pncan3 10168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐾 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (𝐾 + (𝑚 − 𝐾)) = 𝑚)
146	143, 144, 145	syl2anr 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑚 ∈ (0...𝑁) ∧ 𝐾 ∈ ℤ) → (𝐾 + (𝑚 − 𝐾)) = 𝑚)
147	146	ex 449	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 ∈ (0...𝑁) → (𝐾 ∈ ℤ → (𝐾 + (𝑚 − 𝐾)) = 𝑚))
148	11, 147	syl5com 31	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → (𝐾 + (𝑚 − 𝐾)) = 𝑚))
149	148	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) → (𝑚 ∈ (0...𝑁) → (𝐾 + (𝑚 − 𝐾)) = 𝑚))
150	149	imp 444	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) → (𝐾 + (𝑚 − 𝐾)) = 𝑚)
151	150	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) → (𝑌 cyclShift (𝐾 + (𝑚 − 𝐾))) = (𝑌 cyclShift 𝑚))
152	142, 151	eqtr2d 2645	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) → (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift (𝑚 − 𝐾)))
153	152	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift (𝑚 − 𝐾)))
154		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑋 = (𝑌 cyclShift 𝐾) → (𝑋 cyclShift (𝑚 − 𝐾)) = ((𝑌 cyclShift 𝐾) cyclShift (𝑚 − 𝐾)))
155	154	eqeq2d 2620	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑋 = (𝑌 cyclShift 𝐾) → ((𝑌 cyclShift 𝑚) = (𝑋 cyclShift (𝑚 − 𝐾)) ↔ (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift (𝑚 − 𝐾))))
156	155	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → ((𝑌 cyclShift 𝑚) = (𝑋 cyclShift (𝑚 − 𝐾)) ↔ (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift (𝑚 − 𝐾))))
157	153, 156	mpbird 246	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑌 cyclShift 𝑚) = (𝑋 cyclShift (𝑚 − 𝐾)))
158	157	eqeq2d 2620	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑍 = (𝑌 cyclShift 𝑚) ↔ 𝑍 = (𝑋 cyclShift (𝑚 − 𝐾))))
159	158	biimpd 218	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑍 = (𝑌 cyclShift 𝑚) → 𝑍 = (𝑋 cyclShift (𝑚 − 𝐾))))
160	159	exp41 636	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝐾 ≤ 𝑚 → (𝑚 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑍 = (𝑌 cyclShift 𝑚) → 𝑍 = (𝑋 cyclShift (𝑚 − 𝐾)))))))
161	160	com24 93	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑚 ∈ (0...𝑁) → (𝐾 ≤ 𝑚 → (𝑍 = (𝑌 cyclShift 𝑚) → 𝑍 = (𝑋 cyclShift (𝑚 − 𝐾)))))))
162	161	imp31 447	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) → (𝐾 ≤ 𝑚 → (𝑍 = (𝑌 cyclShift 𝑚) → 𝑍 = (𝑋 cyclShift (𝑚 − 𝐾)))))
163	162	com23 84	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) → (𝑍 = (𝑌 cyclShift 𝑚) → (𝐾 ≤ 𝑚 → 𝑍 = (𝑋 cyclShift (𝑚 − 𝐾)))))
164	163	imp 444	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → (𝐾 ≤ 𝑚 → 𝑍 = (𝑋 cyclShift (𝑚 − 𝐾))))
165	164	impcom 445	. . . . . . . . . . . 12 ⊢ ((𝐾 ≤ 𝑚 ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → 𝑍 = (𝑋 cyclShift (𝑚 − 𝐾)))
166		oveq2 6557	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑚 − 𝐾) → (𝑋 cyclShift 𝑛) = (𝑋 cyclShift (𝑚 − 𝐾)))
167	166	eqeq2d 2620	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑚 − 𝐾) → (𝑍 = (𝑋 cyclShift 𝑛) ↔ 𝑍 = (𝑋 cyclShift (𝑚 − 𝐾))))
168	167	rspcev 3282	. . . . . . . . . . . 12 ⊢ (((𝑚 − 𝐾) ∈ (0...𝑁) ∧ 𝑍 = (𝑋 cyclShift (𝑚 − 𝐾))) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
169	133, 165, 168	syl2anc 691	. . . . . . . . . . 11 ⊢ ((𝐾 ≤ 𝑚 ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
170	169	ex 449	. . . . . . . . . 10 ⊢ (𝐾 ≤ 𝑚 → (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
171	88, 127, 170	pm2.61ii 176	. . . . . . . . 9 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
172	171	ex 449	. . . . . . . 8 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) → (𝑍 = (𝑌 cyclShift 𝑚) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
173	172	rexlimdva 3013	. . . . . . 7 ⊢ (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
174	173	ex 449	. . . . . 6 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝑋 = (𝑌 cyclShift 𝐾) → (∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))
175	174	com23 84	. . . . 5 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚) → (𝑋 = (𝑌 cyclShift 𝐾) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))
176	175	ex 449	. . . 4 ⊢ (𝐾 ∈ (0...𝑁) → ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → (∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚) → (𝑋 = (𝑌 cyclShift 𝐾) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
177	176	com24 93	. . 3 ⊢ (𝐾 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → (∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚) → ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
178	177	3imp 1249	. 2 ⊢ ((𝐾 ∈ (0...𝑁) ∧ 𝑋 = (𝑌 cyclShift 𝐾) ∧ ∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚)) → ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
179	178	com12 32	1 ⊢ ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → ((𝐾 ∈ (0...𝑁) ∧ 𝑋 = (𝑌 cyclShift 𝐾) ∧ ∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ∃wrex 2897 class class class wbr 4583 ‘cfv 5804 (class class class)co 6549 ℂcc 9813 0cc0 9815 + caddc 9818 ≤ cle 9954 − cmin 10145 ℕ₀cn0 11169 ℤcz 11254 ...cfz 12197 #chash 12979 Word cword 13146 cyclShift ccsh 13385

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-sup 8231 df-inf 8232 df-card 8648 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-n0 11170 df-z 11255 df-uz 11564 df-rp 11709 df-fz 12198 df-fzo 12335 df-fl 12455 df-mod 12531 df-hash 12980 df-word 13154 df-concat 13156 df-substr 13158 df-csh 13386

This theorem is referenced by: eleclclwwlknlem1 26345 eleclclwwlksnlem1 41245

W3C validator