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 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) = 𝑆 ) )