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