This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem repswsymball

Description: All the symbols of a "repeated symbol word" are the same. (Contributed by AV, 10-Nov-2018)

Ref Expression
Assertion repswsymball ⊢ W ∈ Word V ∧ S ∈ V → W = S repeatS W → ∀ i ∈ 0 ..^ W W ⁡ i = S

Proof

Step Hyp Ref Expression
1 df-3an ⊢ W ∈ Word V ∧ W = W ∧ ∀ i ∈ 0 ..^ W W ⁡ i = S ↔ W ∈ Word V ∧ W = W ∧ ∀ i ∈ 0 ..^ W W ⁡ i = S
2 1 a1i ⊢ W ∈ Word V ∧ S ∈ V → W ∈ Word V ∧ W = W ∧ ∀ i ∈ 0 ..^ W W ⁡ i = S ↔ W ∈ Word V ∧ W = W ∧ ∀ i ∈ 0 ..^ W W ⁡ i = S
3 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
4 3 anim1ci ⊢ W ∈ Word V ∧ S ∈ V → S ∈ V ∧ W ∈ ℕ 0
5 repsdf2 ⊢ S ∈ V ∧ W ∈ ℕ 0 → W = S repeatS W ↔ W ∈ Word V ∧ W = W ∧ ∀ i ∈ 0 ..^ W W ⁡ i = S
6 4 5 syl ⊢ W ∈ Word V ∧ S ∈ V → W = S repeatS W ↔ W ∈ Word V ∧ W = W ∧ ∀ i ∈ 0 ..^ W W ⁡ i = S
7 simpl ⊢ W ∈ Word V ∧ S ∈ V → W ∈ Word V
8 eqidd ⊢ W ∈ Word V ∧ S ∈ V → W = W
9 7 8 jca ⊢ W ∈ Word V ∧ S ∈ V → W ∈ Word V ∧ W = W
10 9 biantrurd ⊢ W ∈ Word V ∧ S ∈ V → ∀ i ∈ 0 ..^ W W ⁡ i = S ↔ W ∈ Word V ∧ W = W ∧ ∀ i ∈ 0 ..^ W W ⁡ i = S
11 2 6 10 3bitr4d ⊢ W ∈ Word V ∧ S ∈ V → W = S repeatS W ↔ ∀ i ∈ 0 ..^ W W ⁡ i = S
12 11 biimpd ⊢ W ∈ Word V ∧ S ∈ V → W = S repeatS W → ∀ i ∈ 0 ..^ W W ⁡ i = S