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 eqtrdi ⊢ ( 𝑊 = ∅ → ( ♯ ‘ 𝑊 ) = 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 eqtrdi ⊢ ( ( ♯ ‘ 𝑊 ) = 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 ) ) )