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