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 ⊢ W ∈ Word V → W = W ⁡ 0 repeatS W ↔ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0

Proof

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