Metamath Proof Explorer


Theorem repswsymballbi

Description: A word is a "repeated symbol word" iff each of its symbols equals the first symbol of the word. (Contributed by AV, 10-Nov-2018)

Ref Expression
Assertion repswsymballbi ( 𝑊 ∈ Word 𝑉 → ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 ( 𝑊 = ∅ → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ∅ ) )
2 hash0 ( ♯ ‘ ∅ ) = 0
3 1 2 syl6eq ( 𝑊 = ∅ → ( ♯ ‘ 𝑊 ) = 0 )
4 fvex ( 𝑊 ‘ 0 ) ∈ V
5 repsw0 ( ( 𝑊 ‘ 0 ) ∈ V → ( ( 𝑊 ‘ 0 ) repeatS 0 ) = ∅ )
6 4 5 ax-mp ( ( 𝑊 ‘ 0 ) repeatS 0 ) = ∅
7 6 eqcomi ∅ = ( ( 𝑊 ‘ 0 ) repeatS 0 )
8 simpr ( ( ( ♯ ‘ 𝑊 ) = 0 ∧ 𝑊 = ∅ ) → 𝑊 = ∅ )
9 oveq2 ( ( ♯ ‘ 𝑊 ) = 0 → ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) = ( ( 𝑊 ‘ 0 ) repeatS 0 ) )
10 9 adantr ( ( ( ♯ ‘ 𝑊 ) = 0 ∧ 𝑊 = ∅ ) → ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) = ( ( 𝑊 ‘ 0 ) repeatS 0 ) )
11 7 8 10 3eqtr4a ( ( ( ♯ ‘ 𝑊 ) = 0 ∧ 𝑊 = ∅ ) → 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) )
12 ral0 𝑖 ∈ ∅ ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 )
13 oveq2 ( ( ♯ ‘ 𝑊 ) = 0 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ 0 ) )
14 fzo0 ( 0 ..^ 0 ) = ∅
15 13 14 syl6eq ( ( ♯ ‘ 𝑊 ) = 0 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ∅ )
16 15 raleqdv ( ( ♯ ‘ 𝑊 ) = 0 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ↔ ∀ 𝑖 ∈ ∅ ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
17 12 16 mpbiri ( ( ♯ ‘ 𝑊 ) = 0 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) )
18 17 adantr ( ( ( ♯ ‘ 𝑊 ) = 0 ∧ 𝑊 = ∅ ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) )
19 11 18 2thd ( ( ( ♯ ‘ 𝑊 ) = 0 ∧ 𝑊 = ∅ ) → ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
20 3 19 mpancom ( 𝑊 = ∅ → ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
21 20 a1d ( 𝑊 = ∅ → ( 𝑊 ∈ Word 𝑉 → ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) ) )
22 df-3an ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
23 22 a1i ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) ) )
24 fstwrdne ( ( 𝑊 ∈ Word 𝑉𝑊 ≠ ∅ ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 )
25 24 ancoms ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 )
26 lencl ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
27 26 adantl ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
28 repsdf2 ( ( ( 𝑊 ‘ 0 ) ∈ 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) → ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) ) )
29 25 27 28 syl2anc ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ) → ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) ) )
30 simpr ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ) → 𝑊 ∈ Word 𝑉 )
31 eqidd ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) )
32 30 31 jca ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ) → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ) )
33 32 biantrurd ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) ) )
34 23 29 33 3bitr4d ( ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ) → ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )
35 34 ex ( 𝑊 ≠ ∅ → ( 𝑊 ∈ Word 𝑉 → ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) ) )
36 21 35 pm2.61ine ( 𝑊 ∈ Word 𝑉 → ( 𝑊 = ( ( 𝑊 ‘ 0 ) repeatS ( ♯ ‘ 𝑊 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑖 ) = ( 𝑊 ‘ 0 ) ) )