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∈WordV→W=W⁡0repeatSW↔∀i∈0..^WW⁡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⁡0repeatS0=∅
6 4 5 ax-mp ⊢W⁡0repeatS0=∅
7 6 eqcomi ⊢∅=W⁡0repeatS0
8 simpr ⊢W=0∧W=∅→W=∅
9 oveq2 ⊢W=0→W⁡0repeatSW=W⁡0repeatS0
10 9 adantr ⊢W=0∧W=∅→W⁡0repeatSW=W⁡0repeatS0
11 7 8 10 3eqtr4a ⊢W=0∧W=∅→W=W⁡0repeatSW
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..^WW⁡i=W⁡0↔∀i∈∅W⁡i=W⁡0
17 12 16 mpbiri ⊢W=0→∀i∈0..^WW⁡i=W⁡0
18 17 adantr ⊢W=0∧W=∅→∀i∈0..^WW⁡i=W⁡0
19 11 18 2thd ⊢W=0∧W=∅→W=W⁡0repeatSW↔∀i∈0..^WW⁡i=W⁡0
20 3 19 mpancom ⊢W=∅→W=W⁡0repeatSW↔∀i∈0..^WW⁡i=W⁡0
21 20 a1d ⊢W=∅→W∈WordV→W=W⁡0repeatSW↔∀i∈0..^WW⁡i=W⁡0
22 df-3an ⊢W∈WordV∧W=W∧∀i∈0..^WW⁡i=W⁡0↔W∈WordV∧W=W∧∀i∈0..^WW⁡i=W⁡0
23 22 a1i ⊢W≠∅∧W∈WordV→W∈WordV∧W=W∧∀i∈0..^WW⁡i=W⁡0↔W∈WordV∧W=W∧∀i∈0..^WW⁡i=W⁡0
24 fstwrdne ⊢W∈WordV∧W≠∅→W⁡0∈V
25 24 ancoms ⊢W≠∅∧W∈WordV→W⁡0∈V
26 lencl ⊢W∈WordV→W∈ℕ0
27 26 adantl ⊢W≠∅∧W∈WordV→W∈ℕ0
28 repsdf2 ⊢W⁡0∈V∧W∈ℕ0→W=W⁡0repeatSW↔W∈WordV∧W=W∧∀i∈0..^WW⁡i=W⁡0
29 25 27 28 syl2anc ⊢W≠∅∧W∈WordV→W=W⁡0repeatSW↔W∈WordV∧W=W∧∀i∈0..^WW⁡i=W⁡0
30 simpr ⊢W≠∅∧W∈WordV→W∈WordV
31 eqidd ⊢W≠∅∧W∈WordV→W=W
32 30 31 jca ⊢W≠∅∧W∈WordV→W∈WordV∧W=W
33 32 biantrurd ⊢W≠∅∧W∈WordV→∀i∈0..^WW⁡i=W⁡0↔W∈WordV∧W=W∧∀i∈0..^WW⁡i=W⁡0
34 23 29 33 3bitr4d ⊢W≠∅∧W∈WordV→W=W⁡0repeatSW↔∀i∈0..^WW⁡i=W⁡0
35 34 ex ⊢W≠∅→W∈WordV→W=W⁡0repeatSW↔∀i∈0..^WW⁡i=W⁡0
36 21 35 pm2.61ine ⊢W∈WordV→W=W⁡0repeatSW↔∀i∈0..^WW⁡i=W⁡0