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 ) )`
` |-  ( ( ( # ` 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 ) )`
` |-  ( ( ( # ` 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 )`
` |-  ( ( 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 ) ) )`