This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem repswsymball

Description: All the symbols of a "repeated symbol word" are the same. (Contributed by AV, 10-Nov-2018)

Ref Expression
Assertion repswsymball 
|- ( ( W e. Word V /\ S e. V ) -> ( W = ( S repeatS ( # ` W ) ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = S ) )

Proof

Step Hyp Ref Expression
1 df-3an 
 |-  ( ( W e. Word V /\ ( # ` W ) = ( # ` W ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = S ) <-> ( ( W e. Word V /\ ( # ` W ) = ( # ` W ) ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = S ) )
2 1 a1i 
 |-  ( ( W e. Word V /\ S e. V ) -> ( ( W e. Word V /\ ( # ` W ) = ( # ` W ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = S ) <-> ( ( W e. Word V /\ ( # ` W ) = ( # ` W ) ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = S ) ) )
3 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
4 3 anim1ci 
 |-  ( ( W e. Word V /\ S e. V ) -> ( S e. V /\ ( # ` W ) e. NN0 ) )
5 repsdf2 
 |-  ( ( S e. V /\ ( # ` W ) e. NN0 ) -> ( W = ( S repeatS ( # ` W ) ) <-> ( W e. Word V /\ ( # ` W ) = ( # ` W ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = S ) ) )
6 4 5 syl 
 |-  ( ( W e. Word V /\ S e. V ) -> ( W = ( S repeatS ( # ` W ) ) <-> ( W e. Word V /\ ( # ` W ) = ( # ` W ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = S ) ) )
7 simpl 
 |-  ( ( W e. Word V /\ S e. V ) -> W e. Word V )
8 eqidd 
 |-  ( ( W e. Word V /\ S e. V ) -> ( # ` W ) = ( # ` W ) )
9 7 8 jca 
 |-  ( ( W e. Word V /\ S e. V ) -> ( W e. Word V /\ ( # ` W ) = ( # ` W ) ) )
10 9 biantrurd 
 |-  ( ( W e. Word V /\ S e. V ) -> ( A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = S <-> ( ( W e. Word V /\ ( # ` W ) = ( # ` W ) ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = S ) ) )
11 2 6 10 3bitr4d 
 |-  ( ( W e. Word V /\ S e. V ) -> ( W = ( S repeatS ( # ` W ) ) <-> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = S ) )
12 11 biimpd 
 |-  ( ( W e. Word V /\ S e. V ) -> ( W = ( S repeatS ( # ` W ) ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = S ) )