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