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 ) ) )