Theorem cshw1

Description: If cyclically shifting a word by 1 position results in the word itself, the word is build of identical symbols. Remark: also "valid" for an empty word! (Contributed by AV, 13-May-2018) (Revised by AV, 7-Jun-2018) (Proof shortened by AV, 1-Nov-2018)

	Ref	Expression
Assertion	cshw1	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 cyclShift 1 ) = 𝑊 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) )

Proof

Step	Hyp	Ref	Expression
1		ral0	⊢ ∀ 𝑖 ∈ ∅ ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 )
2		oveq2	⊢ ( ( ♯ ‘ 𝑊 ) = 0 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ 0 ) )
3		fzo0	⊢ ( 0 ..^ 0 ) = ∅
4	2 3	eqtrdi	⊢ ( ( ♯ ‘ 𝑊 ) = 0 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ∅ )
5	4	raleqdv	⊢ ( ( ♯ ‘ 𝑊 ) = 0 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ↔ ∀ 𝑖 ∈ ∅ ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ) )
6	1 5	mpbiri	⊢ ( ( ♯ ‘ 𝑊 ) = 0 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) )
7	6	a1d	⊢ ( ( ♯ ‘ 𝑊 ) = 0 → ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 cyclShift 1 ) = 𝑊 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ) )
8		simprl	⊢ ( ( ( ¬ ( ♯ ‘ 𝑊 ) = 0 ∧ ¬ ( ♯ ‘ 𝑊 ) = 1 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 cyclShift 1 ) = 𝑊 ) ) → 𝑊 ∈ Word 𝑉 )
9		lencl	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
10		1nn0	⊢ 1 ∈ ℕ0
11	10	a1i	⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ¬ ( ♯ ‘ 𝑊 ) = 0 ∧ ¬ ( ♯ ‘ 𝑊 ) = 1 ) ) → 1 ∈ ℕ0 )
12		df-ne	⊢ ( ( ♯ ‘ 𝑊 ) ≠ 0 ↔ ¬ ( ♯ ‘ 𝑊 ) = 0 )
13		elnnne0	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) )
14	13	simplbi2com	⊢ ( ( ♯ ‘ 𝑊 ) ≠ 0 → ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
15	12 14	sylbir	⊢ ( ¬ ( ♯ ‘ 𝑊 ) = 0 → ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
16	15	adantr	⊢ ( ( ¬ ( ♯ ‘ 𝑊 ) = 0 ∧ ¬ ( ♯ ‘ 𝑊 ) = 1 ) → ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
17	16	impcom	⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ¬ ( ♯ ‘ 𝑊 ) = 0 ∧ ¬ ( ♯ ‘ 𝑊 ) = 1 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
18		neqne	⊢ ( ¬ ( ♯ ‘ 𝑊 ) = 1 → ( ♯ ‘ 𝑊 ) ≠ 1 )
19	18	ad2antll	⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ¬ ( ♯ ‘ 𝑊 ) = 0 ∧ ¬ ( ♯ ‘ 𝑊 ) = 1 ) ) → ( ♯ ‘ 𝑊 ) ≠ 1 )
20		nngt1ne1	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( 1 < ( ♯ ‘ 𝑊 ) ↔ ( ♯ ‘ 𝑊 ) ≠ 1 ) )
21	17 20	syl	⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ¬ ( ♯ ‘ 𝑊 ) = 0 ∧ ¬ ( ♯ ‘ 𝑊 ) = 1 ) ) → ( 1 < ( ♯ ‘ 𝑊 ) ↔ ( ♯ ‘ 𝑊 ) ≠ 1 ) )
22	19 21	mpbird	⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ¬ ( ♯ ‘ 𝑊 ) = 0 ∧ ¬ ( ♯ ‘ 𝑊 ) = 1 ) ) → 1 < ( ♯ ‘ 𝑊 ) )
23		elfzo0	⊢ ( 1 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 1 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 1 < ( ♯ ‘ 𝑊 ) ) )
24	11 17 22 23	syl3anbrc	⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ¬ ( ♯ ‘ 𝑊 ) = 0 ∧ ¬ ( ♯ ‘ 𝑊 ) = 1 ) ) → 1 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
25	24	ex	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ( ¬ ( ♯ ‘ 𝑊 ) = 0 ∧ ¬ ( ♯ ‘ 𝑊 ) = 1 ) → 1 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
26	9 25	syl	⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ¬ ( ♯ ‘ 𝑊 ) = 0 ∧ ¬ ( ♯ ‘ 𝑊 ) = 1 ) → 1 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
27	26	adantr	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 cyclShift 1 ) = 𝑊 ) → ( ( ¬ ( ♯ ‘ 𝑊 ) = 0 ∧ ¬ ( ♯ ‘ 𝑊 ) = 1 ) → 1 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
28	27	impcom	⊢ ( ( ( ¬ ( ♯ ‘ 𝑊 ) = 0 ∧ ¬ ( ♯ ‘ 𝑊 ) = 1 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 cyclShift 1 ) = 𝑊 ) ) → 1 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
29		simprr	⊢ ( ( ( ¬ ( ♯ ‘ 𝑊 ) = 0 ∧ ¬ ( ♯ ‘ 𝑊 ) = 1 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 cyclShift 1 ) = 𝑊 ) ) → ( 𝑊 cyclShift 1 ) = 𝑊 )
30		lbfzo0	⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ )
31	30 13	sylbbr	⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
32	31	ex	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) ≠ 0 → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
33	12 32	biimtrrid	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ¬ ( ♯ ‘ 𝑊 ) = 0 → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
34	9 33	syl	⊢ ( 𝑊 ∈ Word 𝑉 → ( ¬ ( ♯ ‘ 𝑊 ) = 0 → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
35	34	adantr	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 cyclShift 1 ) = 𝑊 ) → ( ¬ ( ♯ ‘ 𝑊 ) = 0 → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
36	35	com12	⊢ ( ¬ ( ♯ ‘ 𝑊 ) = 0 → ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 cyclShift 1 ) = 𝑊 ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
37	36	adantr	⊢ ( ( ¬ ( ♯ ‘ 𝑊 ) = 0 ∧ ¬ ( ♯ ‘ 𝑊 ) = 1 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 cyclShift 1 ) = 𝑊 ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
38	37	imp	⊢ ( ( ( ¬ ( ♯ ‘ 𝑊 ) = 0 ∧ ¬ ( ♯ ‘ 𝑊 ) = 1 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 cyclShift 1 ) = 𝑊 ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
39		elfzoelz	⊢ ( 1 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 1 ∈ ℤ )
40		cshweqrep	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 1 ∈ ℤ ) → ( ( ( 𝑊 cyclShift 1 ) = 𝑊 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ∀ 𝑖 ∈ ℕ0 ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ ( ( 0 + ( 𝑖 · 1 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
41	39 40	sylan2	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 1 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( 𝑊 cyclShift 1 ) = 𝑊 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ∀ 𝑖 ∈ ℕ0 ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ ( ( 0 + ( 𝑖 · 1 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
42	41	imp	⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 1 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( ( 𝑊 cyclShift 1 ) = 𝑊 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ∀ 𝑖 ∈ ℕ0 ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ ( ( 0 + ( 𝑖 · 1 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
43	8 28 29 38 42	syl22anc	⊢ ( ( ( ¬ ( ♯ ‘ 𝑊 ) = 0 ∧ ¬ ( ♯ ‘ 𝑊 ) = 1 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 cyclShift 1 ) = 𝑊 ) ) → ∀ 𝑖 ∈ ℕ0 ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ ( ( 0 + ( 𝑖 · 1 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
44		0nn0	⊢ 0 ∈ ℕ0
45		fzossnn0	⊢ ( 0 ∈ ℕ0 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⊆ ℕ0 )
46		ssralv	⊢ ( ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⊆ ℕ0 → ( ∀ 𝑖 ∈ ℕ0 ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ ( ( 0 + ( 𝑖 · 1 ) ) mod ( ♯ ‘ 𝑊 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ ( ( 0 + ( 𝑖 · 1 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
47	44 45 46	mp2b	⊢ ( ∀ 𝑖 ∈ ℕ0 ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ ( ( 0 + ( 𝑖 · 1 ) ) mod ( ♯ ‘ 𝑊 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ ( ( 0 + ( 𝑖 · 1 ) ) mod ( ♯ ‘ 𝑊 ) ) ) )
48		eqcom	⊢ ( ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ ( ( 0 + ( 𝑖 · 1 ) ) mod ( ♯ ‘ 𝑊 ) ) ) ↔ ( 𝑊 ‘ ( ( 0 + ( 𝑖 · 1 ) ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ 0 ) )
49		elfzoelz	⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝑖 ∈ ℤ )
50		zre	⊢ ( 𝑖 ∈ ℤ → 𝑖 ∈ ℝ )
51		ax-1rid	⊢ ( 𝑖 ∈ ℝ → ( 𝑖 · 1 ) = 𝑖 )
52	50 51	syl	⊢ ( 𝑖 ∈ ℤ → ( 𝑖 · 1 ) = 𝑖 )
53	52	oveq2d	⊢ ( 𝑖 ∈ ℤ → ( 0 + ( 𝑖 · 1 ) ) = ( 0 + 𝑖 ) )
54		zcn	⊢ ( 𝑖 ∈ ℤ → 𝑖 ∈ ℂ )
55	54	addlidd	⊢ ( 𝑖 ∈ ℤ → ( 0 + 𝑖 ) = 𝑖 )
56	53 55	eqtrd	⊢ ( 𝑖 ∈ ℤ → ( 0 + ( 𝑖 · 1 ) ) = 𝑖 )
57	49 56	syl	⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 0 + ( 𝑖 · 1 ) ) = 𝑖 )
58	57	oveq1d	⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 0 + ( 𝑖 · 1 ) ) mod ( ♯ ‘ 𝑊 ) ) = ( 𝑖 mod ( ♯ ‘ 𝑊 ) ) )
59		zmodidfzoimp	⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝑖 mod ( ♯ ‘ 𝑊 ) ) = 𝑖 )
60	58 59	eqtrd	⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 0 + ( 𝑖 · 1 ) ) mod ( ♯ ‘ 𝑊 ) ) = 𝑖 )
61	60	fveqeq2d	⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ‘ ( ( 0 + ( 𝑖 · 1 ) ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ 0 ) ↔ ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ) )
62	61	biimpd	⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ‘ ( ( 0 + ( 𝑖 · 1 ) ) mod ( ♯ ‘ 𝑊 ) ) ) = ( 𝑊 ‘ 0 ) → ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ) )
63	48 62	biimtrid	⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ ( ( 0 + ( 𝑖 · 1 ) ) mod ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ) )
64	63	ralimia	⊢ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ ( ( 0 + ( 𝑖 · 1 ) ) mod ( ♯ ‘ 𝑊 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) )
65	47 64	syl	⊢ ( ∀ 𝑖 ∈ ℕ0 ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ ( ( 0 + ( 𝑖 · 1 ) ) mod ( ♯ ‘ 𝑊 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) )
66	43 65	syl	⊢ ( ( ( ¬ ( ♯ ‘ 𝑊 ) = 0 ∧ ¬ ( ♯ ‘ 𝑊 ) = 1 ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 cyclShift 1 ) = 𝑊 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) )
67	66	ex	⊢ ( ( ¬ ( ♯ ‘ 𝑊 ) = 0 ∧ ¬ ( ♯ ‘ 𝑊 ) = 1 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 cyclShift 1 ) = 𝑊 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ) )
68	67	impancom	⊢ ( ( ¬ ( ♯ ‘ 𝑊 ) = 0 ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 cyclShift 1 ) = 𝑊 ) ) → ( ¬ ( ♯ ‘ 𝑊 ) = 1 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ) )
69		eqid	⊢ ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 )
70		c0ex	⊢ 0 ∈ V
71		fveqeq2	⊢ ( 𝑖 = 0 → ( ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ↔ ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) ) )
72	70 71	ralsn	⊢ ( ∀ 𝑖 ∈ { 0 } ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ↔ ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) )
73	69 72	mpbir	⊢ ∀ 𝑖 ∈ { 0 } ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 )
74		oveq2	⊢ ( ( ♯ ‘ 𝑊 ) = 1 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ 1 ) )
75		fzo01	⊢ ( 0 ..^ 1 ) = { 0 }
76	74 75	eqtrdi	⊢ ( ( ♯ ‘ 𝑊 ) = 1 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = { 0 } )
77	76	raleqdv	⊢ ( ( ♯ ‘ 𝑊 ) = 1 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ↔ ∀ 𝑖 ∈ { 0 } ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ) )
78	73 77	mpbiri	⊢ ( ( ♯ ‘ 𝑊 ) = 1 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) )
79	68 78	pm2.61d2	⊢ ( ( ¬ ( ♯ ‘ 𝑊 ) = 0 ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 cyclShift 1 ) = 𝑊 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) )
80	79	ex	⊢ ( ¬ ( ♯ ‘ 𝑊 ) = 0 → ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 cyclShift 1 ) = 𝑊 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) ) )
81	7 80	pm2.61i	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑊 cyclShift 1 ) = 𝑊 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) )