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 e. Word V -> ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) <-> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )

Proof

Step Hyp Ref Expression
1 fveq2
 |-  ( W = (/) -> ( # ` W ) = ( # ` (/) ) )
2 hash0
 |-  ( # ` (/) ) = 0
3 1 2 syl6eq
 |-  ( W = (/) -> ( # ` W ) = 0 )
4 fvex
 |-  ( W ` 0 ) e. _V
5 repsw0
 |-  ( ( W ` 0 ) e. _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
 |-  A. i e. (/) ( W ` i ) = ( W ` 0 )
13 oveq2
 |-  ( ( # ` W ) = 0 -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ 0 ) )
14 fzo0
 |-  ( 0 ..^ 0 ) = (/)
15 13 14 syl6eq
 |-  ( ( # ` W ) = 0 -> ( 0 ..^ ( # ` W ) ) = (/) )
16 15 raleqdv
 |-  ( ( # ` W ) = 0 -> ( A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) <-> A. i e. (/) ( W ` i ) = ( W ` 0 ) ) )
17 12 16 mpbiri
 |-  ( ( # ` W ) = 0 -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) )
18 17 adantr
 |-  ( ( ( # ` W ) = 0 /\ W = (/) ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) )
19 11 18 2thd
 |-  ( ( ( # ` W ) = 0 /\ W = (/) ) -> ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) <-> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )
20 3 19 mpancom
 |-  ( W = (/) -> ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) <-> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )
21 20 a1d
 |-  ( W = (/) -> ( W e. Word V -> ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) <-> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) ) )
22 df-3an
 |-  ( ( W e. Word V /\ ( # ` W ) = ( # ` W ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) <-> ( ( W e. Word V /\ ( # ` W ) = ( # ` W ) ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )
23 22 a1i
 |-  ( ( W =/= (/) /\ W e. Word V ) -> ( ( W e. Word V /\ ( # ` W ) = ( # ` W ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) <-> ( ( W e. Word V /\ ( # ` W ) = ( # ` W ) ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) ) )
24 fstwrdne
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( W ` 0 ) e. V )
25 24 ancoms
 |-  ( ( W =/= (/) /\ W e. Word V ) -> ( W ` 0 ) e. V )
26 lencl
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
27 26 adantl
 |-  ( ( W =/= (/) /\ W e. Word V ) -> ( # ` W ) e. NN0 )
28 repsdf2
 |-  ( ( ( W ` 0 ) e. V /\ ( # ` W ) e. NN0 ) -> ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) <-> ( W e. Word V /\ ( # ` W ) = ( # ` W ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) ) )
29 25 27 28 syl2anc
 |-  ( ( W =/= (/) /\ W e. Word V ) -> ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) <-> ( W e. Word V /\ ( # ` W ) = ( # ` W ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) ) )
30 simpr
 |-  ( ( W =/= (/) /\ W e. Word V ) -> W e. Word V )
31 eqidd
 |-  ( ( W =/= (/) /\ W e. Word V ) -> ( # ` W ) = ( # ` W ) )
32 30 31 jca
 |-  ( ( W =/= (/) /\ W e. Word V ) -> ( W e. Word V /\ ( # ` W ) = ( # ` W ) ) )
33 32 biantrurd
 |-  ( ( W =/= (/) /\ W e. Word V ) -> ( A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) <-> ( ( W e. Word V /\ ( # ` W ) = ( # ` W ) ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) ) )
34 23 29 33 3bitr4d
 |-  ( ( W =/= (/) /\ W e. Word V ) -> ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) <-> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )
35 34 ex
 |-  ( W =/= (/) -> ( W e. Word V -> ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) <-> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) ) )
36 21 35 pm2.61ine
 |-  ( W e. Word V -> ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) <-> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )