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∈WordV∧S∈V→W=SrepeatSW→∀i∈0..^WW⁡i=S

Proof

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