Metamath Proof Explorer

Theorem repswccat

Description: The concatenation of two "repeated symbol words" with the same symbol is again a "repeated symbol word". (Contributed by AV, 4-Nov-2018)

Ref Expression
Assertion repswccat 
|- ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) -> ( ( S repeatS N ) ++ ( S repeatS M ) ) = ( S repeatS ( N + M ) ) )

Proof

Step Hyp Ref Expression
1 repswlen 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( # ` ( S repeatS N ) ) = N )
2 1 3adant3 
 |-  ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) -> ( # ` ( S repeatS N ) ) = N )
3 repswlen 
 |-  ( ( S e. V /\ M e. NN0 ) -> ( # ` ( S repeatS M ) ) = M )
4 3 3adant2 
 |-  ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) -> ( # ` ( S repeatS M ) ) = M )
5 2 4 oveq12d 
 |-  ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) -> ( ( # ` ( S repeatS N ) ) + ( # ` ( S repeatS M ) ) ) = ( N + M ) )
6 5 oveq2d 
 |-  ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) -> ( 0 ..^ ( ( # ` ( S repeatS N ) ) + ( # ` ( S repeatS M ) ) ) ) = ( 0 ..^ ( N + M ) ) )
7 simp1 
 |-  ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) -> S e. V )
8 7 adantr 
 |-  ( ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) /\ x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) ) -> S e. V )
9 simpl2 
 |-  ( ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) /\ x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) ) -> N e. NN0 )
10 2 oveq2d 
 |-  ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) -> ( 0 ..^ ( # ` ( S repeatS N ) ) ) = ( 0 ..^ N ) )
11 10 eleq2d 
 |-  ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) -> ( x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) <-> x e. ( 0 ..^ N ) ) )
12 11 biimpa 
 |-  ( ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) /\ x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) ) -> x e. ( 0 ..^ N ) )
13 8 9 12 3jca 
 |-  ( ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) /\ x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) ) -> ( S e. V /\ N e. NN0 /\ x e. ( 0 ..^ N ) ) )
14 13 adantlr 
 |-  ( ( ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) /\ x e. ( 0 ..^ ( ( # ` ( S repeatS N ) ) + ( # ` ( S repeatS M ) ) ) ) ) /\ x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) ) -> ( S e. V /\ N e. NN0 /\ x e. ( 0 ..^ N ) ) )
15 repswsymb 
 |-  ( ( S e. V /\ N e. NN0 /\ x e. ( 0 ..^ N ) ) -> ( ( S repeatS N ) ` x ) = S )
16 14 15 syl 
 |-  ( ( ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) /\ x e. ( 0 ..^ ( ( # ` ( S repeatS N ) ) + ( # ` ( S repeatS M ) ) ) ) ) /\ x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) ) -> ( ( S repeatS N ) ` x ) = S )
17 7 ad2antrr 
 |-  ( ( ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) /\ x e. ( 0 ..^ ( ( # ` ( S repeatS N ) ) + ( # ` ( S repeatS M ) ) ) ) ) /\ -. x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) ) -> S e. V )
18 simpll3 
 |-  ( ( ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) /\ x e. ( 0 ..^ ( ( # ` ( S repeatS N ) ) + ( # ` ( S repeatS M ) ) ) ) ) /\ -. x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) ) -> M e. NN0 )
19 2 4 jca 
 |-  ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) -> ( ( # ` ( S repeatS N ) ) = N /\ ( # ` ( S repeatS M ) ) = M ) )
20 simpr 
 |-  ( ( ( N e. NN0 /\ M e. NN0 ) /\ x e. ( 0 ..^ ( N + M ) ) ) -> x e. ( 0 ..^ ( N + M ) ) )
21 20 anim1i 
 |-  ( ( ( ( N e. NN0 /\ M e. NN0 ) /\ x e. ( 0 ..^ ( N + M ) ) ) /\ -. x e. ( 0 ..^ N ) ) -> ( x e. ( 0 ..^ ( N + M ) ) /\ -. x e. ( 0 ..^ N ) ) )
22 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
23 nn0z 
 |-  ( M e. NN0 -> M e. ZZ )
24 22 23 anim12i 
 |-  ( ( N e. NN0 /\ M e. NN0 ) -> ( N e. ZZ /\ M e. ZZ ) )
25 24 ad2antrr 
 |-  ( ( ( ( N e. NN0 /\ M e. NN0 ) /\ x e. ( 0 ..^ ( N + M ) ) ) /\ -. x e. ( 0 ..^ N ) ) -> ( N e. ZZ /\ M e. ZZ ) )
26 fzocatel 
 |-  ( ( ( x e. ( 0 ..^ ( N + M ) ) /\ -. x e. ( 0 ..^ N ) ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( x - N ) e. ( 0 ..^ M ) )
27 21 25 26 syl2anc 
 |-  ( ( ( ( N e. NN0 /\ M e. NN0 ) /\ x e. ( 0 ..^ ( N + M ) ) ) /\ -. x e. ( 0 ..^ N ) ) -> ( x - N ) e. ( 0 ..^ M ) )
28 27 exp31 
 |-  ( ( N e. NN0 /\ M e. NN0 ) -> ( x e. ( 0 ..^ ( N + M ) ) -> ( -. x e. ( 0 ..^ N ) -> ( x - N ) e. ( 0 ..^ M ) ) ) )
29 28 3adant1 
 |-  ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) -> ( x e. ( 0 ..^ ( N + M ) ) -> ( -. x e. ( 0 ..^ N ) -> ( x - N ) e. ( 0 ..^ M ) ) ) )
30 oveq12 
 |-  ( ( ( # ` ( S repeatS N ) ) = N /\ ( # ` ( S repeatS M ) ) = M ) -> ( ( # ` ( S repeatS N ) ) + ( # ` ( S repeatS M ) ) ) = ( N + M ) )
31 30 oveq2d 
 |-  ( ( ( # ` ( S repeatS N ) ) = N /\ ( # ` ( S repeatS M ) ) = M ) -> ( 0 ..^ ( ( # ` ( S repeatS N ) ) + ( # ` ( S repeatS M ) ) ) ) = ( 0 ..^ ( N + M ) ) )
32 31 eleq2d 
 |-  ( ( ( # ` ( S repeatS N ) ) = N /\ ( # ` ( S repeatS M ) ) = M ) -> ( x e. ( 0 ..^ ( ( # ` ( S repeatS N ) ) + ( # ` ( S repeatS M ) ) ) ) <-> x e. ( 0 ..^ ( N + M ) ) ) )
33 oveq2 
 |-  ( ( # ` ( S repeatS N ) ) = N -> ( 0 ..^ ( # ` ( S repeatS N ) ) ) = ( 0 ..^ N ) )
34 33 eleq2d 
 |-  ( ( # ` ( S repeatS N ) ) = N -> ( x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) <-> x e. ( 0 ..^ N ) ) )
35 34 notbid 
 |-  ( ( # ` ( S repeatS N ) ) = N -> ( -. x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) <-> -. x e. ( 0 ..^ N ) ) )
36 35 adantr 
 |-  ( ( ( # ` ( S repeatS N ) ) = N /\ ( # ` ( S repeatS M ) ) = M ) -> ( -. x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) <-> -. x e. ( 0 ..^ N ) ) )
37 oveq2 
 |-  ( ( # ` ( S repeatS N ) ) = N -> ( x - ( # ` ( S repeatS N ) ) ) = ( x - N ) )
38 37 eleq1d 
 |-  ( ( # ` ( S repeatS N ) ) = N -> ( ( x - ( # ` ( S repeatS N ) ) ) e. ( 0 ..^ M ) <-> ( x - N ) e. ( 0 ..^ M ) ) )
39 38 adantr 
 |-  ( ( ( # ` ( S repeatS N ) ) = N /\ ( # ` ( S repeatS M ) ) = M ) -> ( ( x - ( # ` ( S repeatS N ) ) ) e. ( 0 ..^ M ) <-> ( x - N ) e. ( 0 ..^ M ) ) )
40 36 39 imbi12d 
 |-  ( ( ( # ` ( S repeatS N ) ) = N /\ ( # ` ( S repeatS M ) ) = M ) -> ( ( -. x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) -> ( x - ( # ` ( S repeatS N ) ) ) e. ( 0 ..^ M ) ) <-> ( -. x e. ( 0 ..^ N ) -> ( x - N ) e. ( 0 ..^ M ) ) ) )
41 32 40 imbi12d 
 |-  ( ( ( # ` ( S repeatS N ) ) = N /\ ( # ` ( S repeatS M ) ) = M ) -> ( ( x e. ( 0 ..^ ( ( # ` ( S repeatS N ) ) + ( # ` ( S repeatS M ) ) ) ) -> ( -. x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) -> ( x - ( # ` ( S repeatS N ) ) ) e. ( 0 ..^ M ) ) ) <-> ( x e. ( 0 ..^ ( N + M ) ) -> ( -. x e. ( 0 ..^ N ) -> ( x - N ) e. ( 0 ..^ M ) ) ) ) )
42 29 41 syl5ibr 
 |-  ( ( ( # ` ( S repeatS N ) ) = N /\ ( # ` ( S repeatS M ) ) = M ) -> ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) -> ( x e. ( 0 ..^ ( ( # ` ( S repeatS N ) ) + ( # ` ( S repeatS M ) ) ) ) -> ( -. x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) -> ( x - ( # ` ( S repeatS N ) ) ) e. ( 0 ..^ M ) ) ) ) )
43 19 42 mpcom 
 |-  ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) -> ( x e. ( 0 ..^ ( ( # ` ( S repeatS N ) ) + ( # ` ( S repeatS M ) ) ) ) -> ( -. x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) -> ( x - ( # ` ( S repeatS N ) ) ) e. ( 0 ..^ M ) ) ) )
44 43 imp31 
 |-  ( ( ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) /\ x e. ( 0 ..^ ( ( # ` ( S repeatS N ) ) + ( # ` ( S repeatS M ) ) ) ) ) /\ -. x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) ) -> ( x - ( # ` ( S repeatS N ) ) ) e. ( 0 ..^ M ) )
45 repswsymb 
 |-  ( ( S e. V /\ M e. NN0 /\ ( x - ( # ` ( S repeatS N ) ) ) e. ( 0 ..^ M ) ) -> ( ( S repeatS M ) ` ( x - ( # ` ( S repeatS N ) ) ) ) = S )
46 17 18 44 45 syl3anc 
 |-  ( ( ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) /\ x e. ( 0 ..^ ( ( # ` ( S repeatS N ) ) + ( # ` ( S repeatS M ) ) ) ) ) /\ -. x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) ) -> ( ( S repeatS M ) ` ( x - ( # ` ( S repeatS N ) ) ) ) = S )
47 16 46 ifeqda 
 |-  ( ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) /\ x e. ( 0 ..^ ( ( # ` ( S repeatS N ) ) + ( # ` ( S repeatS M ) ) ) ) ) -> if ( x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) , ( ( S repeatS N ) ` x ) , ( ( S repeatS M ) ` ( x - ( # ` ( S repeatS N ) ) ) ) ) = S )
48 6 47 mpteq12dva 
 |-  ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) -> ( x e. ( 0 ..^ ( ( # ` ( S repeatS N ) ) + ( # ` ( S repeatS M ) ) ) ) |-> if ( x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) , ( ( S repeatS N ) ` x ) , ( ( S repeatS M ) ` ( x - ( # ` ( S repeatS N ) ) ) ) ) ) = ( x e. ( 0 ..^ ( N + M ) ) |-> S ) )
49 ovex 
 |-  ( S repeatS N ) e. _V
50 ovex 
 |-  ( S repeatS M ) e. _V
51 49 50 pm3.2i 
 |-  ( ( S repeatS N ) e. _V /\ ( S repeatS M ) e. _V )
52 ccatfval 
 |-  ( ( ( S repeatS N ) e. _V /\ ( S repeatS M ) e. _V ) -> ( ( S repeatS N ) ++ ( S repeatS M ) ) = ( x e. ( 0 ..^ ( ( # ` ( S repeatS N ) ) + ( # ` ( S repeatS M ) ) ) ) |-> if ( x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) , ( ( S repeatS N ) ` x ) , ( ( S repeatS M ) ` ( x - ( # ` ( S repeatS N ) ) ) ) ) ) )
53 51 52 mp1i 
 |-  ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) -> ( ( S repeatS N ) ++ ( S repeatS M ) ) = ( x e. ( 0 ..^ ( ( # ` ( S repeatS N ) ) + ( # ` ( S repeatS M ) ) ) ) |-> if ( x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) , ( ( S repeatS N ) ` x ) , ( ( S repeatS M ) ` ( x - ( # ` ( S repeatS N ) ) ) ) ) ) )
54 nn0addcl 
 |-  ( ( N e. NN0 /\ M e. NN0 ) -> ( N + M ) e. NN0 )
55 54 3adant1 
 |-  ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) -> ( N + M ) e. NN0 )
56 reps 
 |-  ( ( S e. V /\ ( N + M ) e. NN0 ) -> ( S repeatS ( N + M ) ) = ( x e. ( 0 ..^ ( N + M ) ) |-> S ) )
57 7 55 56 syl2anc 
 |-  ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) -> ( S repeatS ( N + M ) ) = ( x e. ( 0 ..^ ( N + M ) ) |-> S ) )
58 48 53 57 3eqtr4d 
 |-  ( ( S e. V /\ N e. NN0 /\ M e. NN0 ) -> ( ( S repeatS N ) ++ ( S repeatS M ) ) = ( S repeatS ( N + M ) ) )