Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ccatmulgnn0dir Structured version   Visualization version   Unicode version

Theorem ccatmulgnn0dir 29440
Description: Concatenation of words follow the rule mulgnn0dir 16793 (although applying mulgnn0dir 16793 would require  S to be a set). In this case  A is  <" K "> to the power  M in the free monoid. (Contributed by Thierry Arnoux, 5-Oct-2018.)
Hypotheses
Ref Expression
ccatmulgnn0dir.a  |-  A  =  ( ( 0..^ M )  X.  { K } )
ccatmulgnn0dir.b  |-  B  =  ( ( 0..^ N )  X.  { K } )
ccatmulgnn0dir.c  |-  C  =  ( ( 0..^ ( M  +  N ) )  X.  { K } )
ccatmulgnn0dir.k  |-  ( ph  ->  K  e.  S )
ccatmulgnn0dir.m  |-  ( ph  ->  M  e.  NN0 )
ccatmulgnn0dir.n  |-  ( ph  ->  N  e.  NN0 )
Assertion
Ref Expression
ccatmulgnn0dir  |-  ( ph  ->  ( A ++  B )  =  C )

Proof of Theorem ccatmulgnn0dir
Dummy variable  i is distinct from all other variables.
StepHypRef Expression
1 ccatmulgnn0dir.a . . . . . . . . 9  |-  A  =  ( ( 0..^ M )  X.  { K } )
21fveq2i 5873 . . . . . . . 8  |-  ( # `  A )  =  (
# `  ( (
0..^ M )  X. 
{ K } ) )
3 fzofi 12194 . . . . . . . . 9  |-  ( 0..^ M )  e.  Fin
4 snfi 7655 . . . . . . . . 9  |-  { K }  e.  Fin
5 hashxp 12613 . . . . . . . . 9  |-  ( ( ( 0..^ M )  e.  Fin  /\  { K }  e.  Fin )  ->  ( # `  (
( 0..^ M )  X.  { K }
) )  =  ( ( # `  (
0..^ M ) )  x.  ( # `  { K } ) ) )
63, 4, 5mp2an 679 . . . . . . . 8  |-  ( # `  ( ( 0..^ M )  X.  { K } ) )  =  ( ( # `  (
0..^ M ) )  x.  ( # `  { K } ) )
72, 6eqtri 2475 . . . . . . 7  |-  ( # `  A )  =  ( ( # `  (
0..^ M ) )  x.  ( # `  { K } ) )
8 ccatmulgnn0dir.m . . . . . . . . 9  |-  ( ph  ->  M  e.  NN0 )
9 hashfzo0 12609 . . . . . . . . 9  |-  ( M  e.  NN0  ->  ( # `  ( 0..^ M ) )  =  M )
108, 9syl 17 . . . . . . . 8  |-  ( ph  ->  ( # `  (
0..^ M ) )  =  M )
11 ccatmulgnn0dir.k . . . . . . . . 9  |-  ( ph  ->  K  e.  S )
12 hashsng 12556 . . . . . . . . 9  |-  ( K  e.  S  ->  ( # `
 { K }
)  =  1 )
1311, 12syl 17 . . . . . . . 8  |-  ( ph  ->  ( # `  { K } )  =  1 )
1410, 13oveq12d 6313 . . . . . . 7  |-  ( ph  ->  ( ( # `  (
0..^ M ) )  x.  ( # `  { K } ) )  =  ( M  x.  1 ) )
157, 14syl5eq 2499 . . . . . 6  |-  ( ph  ->  ( # `  A
)  =  ( M  x.  1 ) )
168nn0cnd 10934 . . . . . . 7  |-  ( ph  ->  M  e.  CC )
1716mulid1d 9665 . . . . . 6  |-  ( ph  ->  ( M  x.  1 )  =  M )
1815, 17eqtrd 2487 . . . . 5  |-  ( ph  ->  ( # `  A
)  =  M )
19 ccatmulgnn0dir.b . . . . . . . . 9  |-  B  =  ( ( 0..^ N )  X.  { K } )
2019fveq2i 5873 . . . . . . . 8  |-  ( # `  B )  =  (
# `  ( (
0..^ N )  X. 
{ K } ) )
21 fzofi 12194 . . . . . . . . 9  |-  ( 0..^ N )  e.  Fin
22 hashxp 12613 . . . . . . . . 9  |-  ( ( ( 0..^ N )  e.  Fin  /\  { K }  e.  Fin )  ->  ( # `  (
( 0..^ N )  X.  { K }
) )  =  ( ( # `  (
0..^ N ) )  x.  ( # `  { K } ) ) )
2321, 4, 22mp2an 679 . . . . . . . 8  |-  ( # `  ( ( 0..^ N )  X.  { K } ) )  =  ( ( # `  (
0..^ N ) )  x.  ( # `  { K } ) )
2420, 23eqtri 2475 . . . . . . 7  |-  ( # `  B )  =  ( ( # `  (
0..^ N ) )  x.  ( # `  { K } ) )
25 ccatmulgnn0dir.n . . . . . . . . 9  |-  ( ph  ->  N  e.  NN0 )
26 hashfzo0 12609 . . . . . . . . 9  |-  ( N  e.  NN0  ->  ( # `  ( 0..^ N ) )  =  N )
2725, 26syl 17 . . . . . . . 8  |-  ( ph  ->  ( # `  (
0..^ N ) )  =  N )
2827, 13oveq12d 6313 . . . . . . 7  |-  ( ph  ->  ( ( # `  (
0..^ N ) )  x.  ( # `  { K } ) )  =  ( N  x.  1 ) )
2924, 28syl5eq 2499 . . . . . 6  |-  ( ph  ->  ( # `  B
)  =  ( N  x.  1 ) )
3025nn0cnd 10934 . . . . . . 7  |-  ( ph  ->  N  e.  CC )
3130mulid1d 9665 . . . . . 6  |-  ( ph  ->  ( N  x.  1 )  =  N )
3229, 31eqtrd 2487 . . . . 5  |-  ( ph  ->  ( # `  B
)  =  N )
3318, 32oveq12d 6313 . . . 4  |-  ( ph  ->  ( ( # `  A
)  +  ( # `  B ) )  =  ( M  +  N
) )
3433oveq2d 6311 . . 3  |-  ( ph  ->  ( 0..^ ( (
# `  A )  +  ( # `  B
) ) )  =  ( 0..^ ( M  +  N ) ) )
35 simpll 761 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ ( (
# `  A )  +  ( # `  B
) ) ) )  /\  i  e.  ( 0..^ ( # `  A
) ) )  ->  ph )
36 simpr 463 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ ( (
# `  A )  +  ( # `  B
) ) ) )  /\  i  e.  ( 0..^ ( # `  A
) ) )  -> 
i  e.  ( 0..^ ( # `  A
) ) )
3718oveq2d 6311 . . . . . . 7  |-  ( ph  ->  ( 0..^ ( # `  A ) )  =  ( 0..^ M ) )
3835, 37syl 17 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ ( (
# `  A )  +  ( # `  B
) ) ) )  /\  i  e.  ( 0..^ ( # `  A
) ) )  -> 
( 0..^ ( # `  A ) )  =  ( 0..^ M ) )
3936, 38eleqtrd 2533 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ ( (
# `  A )  +  ( # `  B
) ) ) )  /\  i  e.  ( 0..^ ( # `  A
) ) )  -> 
i  e.  ( 0..^ M ) )
40 fconstg 5775 . . . . . . . 8  |-  ( K  e.  S  ->  (
( 0..^ M )  X.  { K }
) : ( 0..^ M ) --> { K } )
4111, 40syl 17 . . . . . . 7  |-  ( ph  ->  ( ( 0..^ M )  X.  { K } ) : ( 0..^ M ) --> { K } )
421a1i 11 . . . . . . . 8  |-  ( ph  ->  A  =  ( ( 0..^ M )  X. 
{ K } ) )
4342feq1d 5719 . . . . . . 7  |-  ( ph  ->  ( A : ( 0..^ M ) --> { K }  <->  ( (
0..^ M )  X. 
{ K } ) : ( 0..^ M ) --> { K }
) )
4441, 43mpbird 236 . . . . . 6  |-  ( ph  ->  A : ( 0..^ M ) --> { K } )
45 fvconst 6087 . . . . . 6  |-  ( ( A : ( 0..^ M ) --> { K }  /\  i  e.  ( 0..^ M ) )  ->  ( A `  i )  =  K )
4644, 45sylan 474 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( A `  i )  =  K )
4735, 39, 46syl2anc 667 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ ( (
# `  A )  +  ( # `  B
) ) ) )  /\  i  e.  ( 0..^ ( # `  A
) ) )  -> 
( A `  i
)  =  K )
48 simpll 761 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ ( (
# `  A )  +  ( # `  B
) ) ) )  /\  -.  i  e.  ( 0..^ ( # `  A ) ) )  ->  ph )
49 simplr 763 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ ( (
# `  A )  +  ( # `  B
) ) ) )  /\  -.  i  e.  ( 0..^ ( # `  A ) ) )  ->  i  e.  ( 0..^ ( ( # `  A )  +  (
# `  B )
) ) )
50 simpr 463 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ ( (
# `  A )  +  ( # `  B
) ) ) )  /\  -.  i  e.  ( 0..^ ( # `  A ) ) )  ->  -.  i  e.  ( 0..^ ( # `  A
) ) )
5118, 8eqeltrd 2531 . . . . . . . . 9  |-  ( ph  ->  ( # `  A
)  e.  NN0 )
5248, 51syl 17 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ ( (
# `  A )  +  ( # `  B
) ) ) )  /\  -.  i  e.  ( 0..^ ( # `  A ) ) )  ->  ( # `  A
)  e.  NN0 )
5352nn0zd 11045 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ ( (
# `  A )  +  ( # `  B
) ) ) )  /\  -.  i  e.  ( 0..^ ( # `  A ) ) )  ->  ( # `  A
)  e.  ZZ )
5432, 25eqeltrd 2531 . . . . . . . . 9  |-  ( ph  ->  ( # `  B
)  e.  NN0 )
5548, 54syl 17 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ ( (
# `  A )  +  ( # `  B
) ) ) )  /\  -.  i  e.  ( 0..^ ( # `  A ) ) )  ->  ( # `  B
)  e.  NN0 )
5655nn0zd 11045 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ ( (
# `  A )  +  ( # `  B
) ) ) )  /\  -.  i  e.  ( 0..^ ( # `  A ) ) )  ->  ( # `  B
)  e.  ZZ )
57 fzocatel 11985 . . . . . . 7  |-  ( ( ( i  e.  ( 0..^ ( ( # `  A )  +  (
# `  B )
) )  /\  -.  i  e.  ( 0..^ ( # `  A
) ) )  /\  ( ( # `  A
)  e.  ZZ  /\  ( # `  B )  e.  ZZ ) )  ->  ( i  -  ( # `  A ) )  e.  ( 0..^ ( # `  B
) ) )
5849, 50, 53, 56, 57syl22anc 1270 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ ( (
# `  A )  +  ( # `  B
) ) ) )  /\  -.  i  e.  ( 0..^ ( # `  A ) ) )  ->  ( i  -  ( # `  A ) )  e.  ( 0..^ ( # `  B
) ) )
5932oveq2d 6311 . . . . . . 7  |-  ( ph  ->  ( 0..^ ( # `  B ) )  =  ( 0..^ N ) )
6048, 59syl 17 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ ( (
# `  A )  +  ( # `  B
) ) ) )  /\  -.  i  e.  ( 0..^ ( # `  A ) ) )  ->  ( 0..^ (
# `  B )
)  =  ( 0..^ N ) )
6158, 60eleqtrd 2533 . . . . 5  |-  ( ( ( ph  /\  i  e.  ( 0..^ ( (
# `  A )  +  ( # `  B
) ) ) )  /\  -.  i  e.  ( 0..^ ( # `  A ) ) )  ->  ( i  -  ( # `  A ) )  e.  ( 0..^ N ) )
62 fconstg 5775 . . . . . . . 8  |-  ( K  e.  S  ->  (
( 0..^ N )  X.  { K }
) : ( 0..^ N ) --> { K } )
6311, 62syl 17 . . . . . . 7  |-  ( ph  ->  ( ( 0..^ N )  X.  { K } ) : ( 0..^ N ) --> { K } )
6419a1i 11 . . . . . . . 8  |-  ( ph  ->  B  =  ( ( 0..^ N )  X. 
{ K } ) )
6564feq1d 5719 . . . . . . 7  |-  ( ph  ->  ( B : ( 0..^ N ) --> { K }  <->  ( (
0..^ N )  X. 
{ K } ) : ( 0..^ N ) --> { K }
) )
6663, 65mpbird 236 . . . . . 6  |-  ( ph  ->  B : ( 0..^ N ) --> { K } )
67 fvconst 6087 . . . . . 6  |-  ( ( B : ( 0..^ N ) --> { K }  /\  ( i  -  ( # `  A ) )  e.  ( 0..^ N ) )  -> 
( B `  (
i  -  ( # `  A ) ) )  =  K )
6866, 67sylan 474 . . . . 5  |-  ( (
ph  /\  ( i  -  ( # `  A
) )  e.  ( 0..^ N ) )  ->  ( B `  ( i  -  ( # `
 A ) ) )  =  K )
6948, 61, 68syl2anc 667 . . . 4  |-  ( ( ( ph  /\  i  e.  ( 0..^ ( (
# `  A )  +  ( # `  B
) ) ) )  /\  -.  i  e.  ( 0..^ ( # `  A ) ) )  ->  ( B `  ( i  -  ( # `
 A ) ) )  =  K )
7047, 69ifeqda 3916 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ ( ( # `  A )  +  (
# `  B )
) ) )  ->  if ( i  e.  ( 0..^ ( # `  A
) ) ,  ( A `  i ) ,  ( B `  ( i  -  ( # `
 A ) ) ) )  =  K )
7134, 70mpteq12dva 4483 . 2  |-  ( ph  ->  ( i  e.  ( 0..^ ( ( # `  A )  +  (
# `  B )
) )  |->  if ( i  e.  ( 0..^ ( # `  A
) ) ,  ( A `  i ) ,  ( B `  ( i  -  ( # `
 A ) ) ) ) )  =  ( i  e.  ( 0..^ ( M  +  N ) )  |->  K ) )
72 ovex 6323 . . . . 5  |-  ( 0..^ M )  e.  _V
73 snex 4644 . . . . 5  |-  { K }  e.  _V
7472, 73xpex 6600 . . . 4  |-  ( ( 0..^ M )  X. 
{ K } )  e.  _V
751, 74eqeltri 2527 . . 3  |-  A  e. 
_V
76 ovex 6323 . . . . 5  |-  ( 0..^ N )  e.  _V
7776, 73xpex 6600 . . . 4  |-  ( ( 0..^ N )  X. 
{ K } )  e.  _V
7819, 77eqeltri 2527 . . 3  |-  B  e. 
_V
79 ccatfval 12726 . . 3  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A ++  B )  =  ( i  e.  ( 0..^ ( (
# `  A )  +  ( # `  B
) ) )  |->  if ( i  e.  ( 0..^ ( # `  A
) ) ,  ( A `  i ) ,  ( B `  ( i  -  ( # `
 A ) ) ) ) ) )
8075, 78, 79mp2an 679 . 2  |-  ( A ++  B )  =  ( i  e.  ( 0..^ ( ( # `  A
)  +  ( # `  B ) ) ) 
|->  if ( i  e.  ( 0..^ ( # `  A ) ) ,  ( A `  i
) ,  ( B `
 ( i  -  ( # `  A ) ) ) ) )
81 ccatmulgnn0dir.c . . 3  |-  C  =  ( ( 0..^ ( M  +  N ) )  X.  { K } )
82 fconstmpt 4881 . . 3  |-  ( ( 0..^ ( M  +  N ) )  X. 
{ K } )  =  ( i  e.  ( 0..^ ( M  +  N ) ) 
|->  K )
8381, 82eqtri 2475 . 2  |-  C  =  ( i  e.  ( 0..^ ( M  +  N ) )  |->  K )
8471, 80, 833eqtr4g 2512 1  |-  ( ph  ->  ( A ++  B )  =  C )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 371    = wceq 1446    e. wcel 1889   _Vcvv 3047   ifcif 3883   {csn 3970    |-> cmpt 4464    X. cxp 4835   -->wf 5581   ` cfv 5585  (class class class)co 6295   Fincfn 7574   0cc0 9544   1c1 9545    + caddc 9547    x. cmul 9549    - cmin 9865   NN0cn0 10876   ZZcz 10944  ..^cfzo 11922   #chash 12522   ++ cconcat 12665
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-rep 4518  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588  ax-cnex 9600  ax-resscn 9601  ax-1cn 9602  ax-icn 9603  ax-addcl 9604  ax-addrcl 9605  ax-mulcl 9606  ax-mulrcl 9607  ax-mulcom 9608  ax-addass 9609  ax-mulass 9610  ax-distr 9611  ax-i2m1 9612  ax-1ne0 9613  ax-1rid 9614  ax-rnegex 9615  ax-rrecex 9616  ax-cnre 9617  ax-pre-lttri 9618  ax-pre-lttrn 9619  ax-pre-ltadd 9620  ax-pre-mulgt0 9621
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-nel 2627  df-ral 2744  df-rex 2745  df-reu 2746  df-rmo 2747  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-tp 3975  df-op 3977  df-uni 4202  df-int 4238  df-iun 4283  df-br 4406  df-opab 4465  df-mpt 4466  df-tr 4501  df-eprel 4748  df-id 4752  df-po 4758  df-so 4759  df-fr 4796  df-we 4798  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-pred 5383  df-ord 5429  df-on 5430  df-lim 5431  df-suc 5432  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-riota 6257  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6698  df-1st 6798  df-2nd 6799  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-1o 7187  df-oadd 7191  df-er 7368  df-en 7575  df-dom 7576  df-sdom 7577  df-fin 7578  df-card 8378  df-cda 8603  df-pnf 9682  df-mnf 9683  df-xr 9684  df-ltxr 9685  df-le 9686  df-sub 9867  df-neg 9868  df-nn 10617  df-n0 10877  df-z 10945  df-uz 11167  df-fz 11792  df-fzo 11923  df-hash 12523  df-concat 12673
This theorem is referenced by:  ofcccat  29442
  Copyright terms: Public domain W3C validator