Metamath Proof Explorer

Theorem repsdf2

Description: Alternative definition of a "repeated symbol word". (Contributed by AV, 7-Nov-2018)

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

Proof

Step Hyp Ref Expression
1 repsconst 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) = ( ( 0 ..^ N ) X. { S } ) )
2 1 eqeq2d 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( W = ( S repeatS N ) <-> W = ( ( 0 ..^ N ) X. { S } ) ) )
3 fconst2g 
 |-  ( S e. V -> ( W : ( 0 ..^ N ) --> { S } <-> W = ( ( 0 ..^ N ) X. { S } ) ) )
4 3 adantr 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( W : ( 0 ..^ N ) --> { S } <-> W = ( ( 0 ..^ N ) X. { S } ) ) )
5 fconstfv 
 |-  ( W : ( 0 ..^ N ) --> { S } <-> ( W Fn ( 0 ..^ N ) /\ A. i e. ( 0 ..^ N ) ( W ` i ) = S ) )
6 snssi 
 |-  ( S e. V -> { S } C_ V )
7 6 adantr 
 |-  ( ( S e. V /\ N e. NN0 ) -> { S } C_ V )
8 7 anim1ci 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ W : ( 0 ..^ N ) --> { S } ) -> ( W : ( 0 ..^ N ) --> { S } /\ { S } C_ V ) )
9 fss 
 |-  ( ( W : ( 0 ..^ N ) --> { S } /\ { S } C_ V ) -> W : ( 0 ..^ N ) --> V )
10 iswrdi 
 |-  ( W : ( 0 ..^ N ) --> V -> W e. Word V )
11 8 9 10 3syl 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ W : ( 0 ..^ N ) --> { S } ) -> W e. Word V )
12 ffzo0hash 
 |-  ( ( N e. NN0 /\ W Fn ( 0 ..^ N ) ) -> ( # ` W ) = N )
13 12 expcom 
 |-  ( W Fn ( 0 ..^ N ) -> ( N e. NN0 -> ( # ` W ) = N ) )
14 ffn 
 |-  ( W : ( 0 ..^ N ) --> { S } -> W Fn ( 0 ..^ N ) )
15 13 14 syl11 
 |-  ( N e. NN0 -> ( W : ( 0 ..^ N ) --> { S } -> ( # ` W ) = N ) )
16 15 adantl 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( W : ( 0 ..^ N ) --> { S } -> ( # ` W ) = N ) )
17 16 imp 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ W : ( 0 ..^ N ) --> { S } ) -> ( # ` W ) = N )
18 11 17 jca 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ W : ( 0 ..^ N ) --> { S } ) -> ( W e. Word V /\ ( # ` W ) = N ) )
19 18 ex 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( W : ( 0 ..^ N ) --> { S } -> ( W e. Word V /\ ( # ` W ) = N ) ) )
20 5 19 syl5bir 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( ( W Fn ( 0 ..^ N ) /\ A. i e. ( 0 ..^ N ) ( W ` i ) = S ) -> ( W e. Word V /\ ( # ` W ) = N ) ) )
21 20 expcomd 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( A. i e. ( 0 ..^ N ) ( W ` i ) = S -> ( W Fn ( 0 ..^ N ) -> ( W e. Word V /\ ( # ` W ) = N ) ) ) )
22 21 imp 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ A. i e. ( 0 ..^ N ) ( W ` i ) = S ) -> ( W Fn ( 0 ..^ N ) -> ( W e. Word V /\ ( # ` W ) = N ) ) )
23 wrdf 
 |-  ( W e. Word V -> W : ( 0 ..^ ( # ` W ) ) --> V )
24 ffn 
 |-  ( W : ( 0 ..^ ( # ` W ) ) --> V -> W Fn ( 0 ..^ ( # ` W ) ) )
25 oveq2 
 |-  ( ( # ` W ) = N -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ N ) )
26 25 fneq2d 
 |-  ( ( # ` W ) = N -> ( W Fn ( 0 ..^ ( # ` W ) ) <-> W Fn ( 0 ..^ N ) ) )
27 26 biimpd 
 |-  ( ( # ` W ) = N -> ( W Fn ( 0 ..^ ( # ` W ) ) -> W Fn ( 0 ..^ N ) ) )
28 27 a1d 
 |-  ( ( # ` W ) = N -> ( ( S e. V /\ N e. NN0 ) -> ( W Fn ( 0 ..^ ( # ` W ) ) -> W Fn ( 0 ..^ N ) ) ) )
29 28 com13 
 |-  ( W Fn ( 0 ..^ ( # ` W ) ) -> ( ( S e. V /\ N e. NN0 ) -> ( ( # ` W ) = N -> W Fn ( 0 ..^ N ) ) ) )
30 23 24 29 3syl 
 |-  ( W e. Word V -> ( ( S e. V /\ N e. NN0 ) -> ( ( # ` W ) = N -> W Fn ( 0 ..^ N ) ) ) )
31 30 com12 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( W e. Word V -> ( ( # ` W ) = N -> W Fn ( 0 ..^ N ) ) ) )
32 31 impd 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( ( W e. Word V /\ ( # ` W ) = N ) -> W Fn ( 0 ..^ N ) ) )
33 32 adantr 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ A. i e. ( 0 ..^ N ) ( W ` i ) = S ) -> ( ( W e. Word V /\ ( # ` W ) = N ) -> W Fn ( 0 ..^ N ) ) )
34 22 33 impbid 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ A. i e. ( 0 ..^ N ) ( W ` i ) = S ) -> ( W Fn ( 0 ..^ N ) <-> ( W e. Word V /\ ( # ` W ) = N ) ) )
35 34 ex 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( A. i e. ( 0 ..^ N ) ( W ` i ) = S -> ( W Fn ( 0 ..^ N ) <-> ( W e. Word V /\ ( # ` W ) = N ) ) ) )
36 35 pm5.32rd 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( ( W Fn ( 0 ..^ N ) /\ A. i e. ( 0 ..^ N ) ( W ` i ) = S ) <-> ( ( W e. Word V /\ ( # ` W ) = N ) /\ A. i e. ( 0 ..^ N ) ( W ` i ) = S ) ) )
37 df-3an 
 |-  ( ( W e. Word V /\ ( # ` W ) = N /\ A. i e. ( 0 ..^ N ) ( W ` i ) = S ) <-> ( ( W e. Word V /\ ( # ` W ) = N ) /\ A. i e. ( 0 ..^ N ) ( W ` i ) = S ) )
38 36 5 37 3bitr4g 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( W : ( 0 ..^ N ) --> { S } <-> ( W e. Word V /\ ( # ` W ) = N /\ A. i e. ( 0 ..^ N ) ( W ` i ) = S ) ) )
39 2 4 38 3bitr2d 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( W = ( S repeatS N ) <-> ( W e. Word V /\ ( # ` W ) = N /\ A. i e. ( 0 ..^ N ) ( W ` i ) = S ) ) )