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 ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ) → ( 𝑊 = ( 𝑆 repeatS ( ♯ ‘ 𝑊 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = 𝑆 ) )

Proof

Step Hyp Ref Expression
1 df-3an ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = 𝑆 ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = 𝑆 ) )
2 1 a1i ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = 𝑆 ) ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = 𝑆 ) ) )
3 lencl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
4 3 anim1ci ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ) → ( 𝑆 ∈ 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) )
5 repsdf2 ⊢ ( ( 𝑆 ∈ 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) → ( 𝑊 = ( 𝑆 repeatS ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = 𝑆 ) ) )
6 4 5 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ) → ( 𝑊 = ( 𝑆 repeatS ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = 𝑆 ) ) )
7 simpl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ) → 𝑊 ∈ Word 𝑉 )
8 eqidd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) )
9 7 8 jca ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ) → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ) )
10 9 biantrurd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = 𝑆 ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑊 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = 𝑆 ) ) )
11 2 6 10 3bitr4d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ) → ( 𝑊 = ( 𝑆 repeatS ( ♯ ‘ 𝑊 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = 𝑆 ) )
12 11 biimpd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ) → ( 𝑊 = ( 𝑆 repeatS ( ♯ ‘ 𝑊 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = 𝑆 ) )