Metamath Proof Explorer

Theorem ofcccat

Description: Letterwise operations on word concatenations. (Contributed by Thierry Arnoux, 5-Oct-2018)

Ref Expression
Hypotheses ofcccat.1 
|- ( ph -> F e. Word S )
ofcccat.2 
|- ( ph -> G e. Word S )
ofcccat.3 
|- ( ph -> K e. T )
Assertion ofcccat 
|- ( ph -> ( ( F ++ G ) oFC R K ) = ( ( F oFC R K ) ++ ( G oFC R K ) ) )

Proof

Step Hyp Ref Expression
1 ofcccat.1 
 |-  ( ph -> F e. Word S )
2 ofcccat.2 
 |-  ( ph -> G e. Word S )
3 ofcccat.3 
 |-  ( ph -> K e. T )
4 fconst6g 
 |-  ( K e. T -> ( ( 0 ..^ ( # ` F ) ) X. { K } ) : ( 0 ..^ ( # ` F ) ) --> T )
5 iswrdi 
 |-  ( ( ( 0 ..^ ( # ` F ) ) X. { K } ) : ( 0 ..^ ( # ` F ) ) --> T -> ( ( 0 ..^ ( # ` F ) ) X. { K } ) e. Word T )
6 3 4 5 3syl 
 |-  ( ph -> ( ( 0 ..^ ( # ` F ) ) X. { K } ) e. Word T )
7 fconst6g 
 |-  ( K e. T -> ( ( 0 ..^ ( # ` G ) ) X. { K } ) : ( 0 ..^ ( # ` G ) ) --> T )
8 iswrdi 
 |-  ( ( ( 0 ..^ ( # ` G ) ) X. { K } ) : ( 0 ..^ ( # ` G ) ) --> T -> ( ( 0 ..^ ( # ` G ) ) X. { K } ) e. Word T )
9 3 7 8 3syl 
 |-  ( ph -> ( ( 0 ..^ ( # ` G ) ) X. { K } ) e. Word T )
10 fzofi 
 |-  ( 0 ..^ ( # ` F ) ) e. Fin
11 snfi 
 |-  { K } e. Fin
12 hashxp 
 |-  ( ( ( 0 ..^ ( # ` F ) ) e. Fin /\ { K } e. Fin ) -> ( # ` ( ( 0 ..^ ( # ` F ) ) X. { K } ) ) = ( ( # ` ( 0 ..^ ( # ` F ) ) ) x. ( # ` { K } ) ) )
13 10 11 12 mp2an 
 |-  ( # ` ( ( 0 ..^ ( # ` F ) ) X. { K } ) ) = ( ( # ` ( 0 ..^ ( # ` F ) ) ) x. ( # ` { K } ) )
14 lencl 
 |-  ( F e. Word S -> ( # ` F ) e. NN0 )
15 hashfzo0 
 |-  ( ( # ` F ) e. NN0 -> ( # ` ( 0 ..^ ( # ` F ) ) ) = ( # ` F ) )
16 1 14 15 3syl 
 |-  ( ph -> ( # ` ( 0 ..^ ( # ` F ) ) ) = ( # ` F ) )
17 hashsng 
 |-  ( K e. T -> ( # ` { K } ) = 1 )
18 3 17 syl 
 |-  ( ph -> ( # ` { K } ) = 1 )
19 16 18 oveq12d 
 |-  ( ph -> ( ( # ` ( 0 ..^ ( # ` F ) ) ) x. ( # ` { K } ) ) = ( ( # ` F ) x. 1 ) )
20 1 14 syl 
 |-  ( ph -> ( # ` F ) e. NN0 )
21 20 nn0cnd 
 |-  ( ph -> ( # ` F ) e. CC )
22 21 mulridd 
 |-  ( ph -> ( ( # ` F ) x. 1 ) = ( # ` F ) )
23 19 22 eqtrd 
 |-  ( ph -> ( ( # ` ( 0 ..^ ( # ` F ) ) ) x. ( # ` { K } ) ) = ( # ` F ) )
24 13 23 eqtr2id 
 |-  ( ph -> ( # ` F ) = ( # ` ( ( 0 ..^ ( # ` F ) ) X. { K } ) ) )
25 fzofi 
 |-  ( 0 ..^ ( # ` G ) ) e. Fin
26 hashxp 
 |-  ( ( ( 0 ..^ ( # ` G ) ) e. Fin /\ { K } e. Fin ) -> ( # ` ( ( 0 ..^ ( # ` G ) ) X. { K } ) ) = ( ( # ` ( 0 ..^ ( # ` G ) ) ) x. ( # ` { K } ) ) )
27 25 11 26 mp2an 
 |-  ( # ` ( ( 0 ..^ ( # ` G ) ) X. { K } ) ) = ( ( # ` ( 0 ..^ ( # ` G ) ) ) x. ( # ` { K } ) )
28 lencl 
 |-  ( G e. Word S -> ( # ` G ) e. NN0 )
29 hashfzo0 
 |-  ( ( # ` G ) e. NN0 -> ( # ` ( 0 ..^ ( # ` G ) ) ) = ( # ` G ) )
30 2 28 29 3syl 
 |-  ( ph -> ( # ` ( 0 ..^ ( # ` G ) ) ) = ( # ` G ) )
31 30 18 oveq12d 
 |-  ( ph -> ( ( # ` ( 0 ..^ ( # ` G ) ) ) x. ( # ` { K } ) ) = ( ( # ` G ) x. 1 ) )
32 2 28 syl 
 |-  ( ph -> ( # ` G ) e. NN0 )
33 32 nn0cnd 
 |-  ( ph -> ( # ` G ) e. CC )
34 33 mulridd 
 |-  ( ph -> ( ( # ` G ) x. 1 ) = ( # ` G ) )
35 31 34 eqtrd 
 |-  ( ph -> ( ( # ` ( 0 ..^ ( # ` G ) ) ) x. ( # ` { K } ) ) = ( # ` G ) )
36 27 35 eqtr2id 
 |-  ( ph -> ( # ` G ) = ( # ` ( ( 0 ..^ ( # ` G ) ) X. { K } ) ) )
37 1 2 6 9 24 36 ofccat 
 |-  ( ph -> ( ( F ++ G ) oF R ( ( ( 0 ..^ ( # ` F ) ) X. { K } ) ++ ( ( 0 ..^ ( # ` G ) ) X. { K } ) ) ) = ( ( F oF R ( ( 0 ..^ ( # ` F ) ) X. { K } ) ) ++ ( G oF R ( ( 0 ..^ ( # ` G ) ) X. { K } ) ) ) )
38 ccatcl 
 |-  ( ( F e. Word S /\ G e. Word S ) -> ( F ++ G ) e. Word S )
39 1 2 38 syl2anc 
 |-  ( ph -> ( F ++ G ) e. Word S )
40 wrdf 
 |-  ( ( F ++ G ) e. Word S -> ( F ++ G ) : ( 0 ..^ ( # ` ( F ++ G ) ) ) --> S )
41 39 40 syl 
 |-  ( ph -> ( F ++ G ) : ( 0 ..^ ( # ` ( F ++ G ) ) ) --> S )
42 ovexd 
 |-  ( ph -> ( 0 ..^ ( # ` ( F ++ G ) ) ) e. _V )
43 41 42 3 ofcof 
 |-  ( ph -> ( ( F ++ G ) oFC R K ) = ( ( F ++ G ) oF R ( ( 0 ..^ ( # ` ( F ++ G ) ) ) X. { K } ) ) )
44 eqid 
 |-  ( ( 0 ..^ ( ( # ` F ) + ( # ` G ) ) ) X. { K } ) = ( ( 0 ..^ ( ( # ` F ) + ( # ` G ) ) ) X. { K } )
45 ccatlen 
 |-  ( ( F e. Word S /\ G e. Word S ) -> ( # ` ( F ++ G ) ) = ( ( # ` F ) + ( # ` G ) ) )
46 1 2 45 syl2anc 
 |-  ( ph -> ( # ` ( F ++ G ) ) = ( ( # ` F ) + ( # ` G ) ) )
47 46 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` ( F ++ G ) ) ) = ( 0 ..^ ( ( # ` F ) + ( # ` G ) ) ) )
48 47 xpeq1d 
 |-  ( ph -> ( ( 0 ..^ ( # ` ( F ++ G ) ) ) X. { K } ) = ( ( 0 ..^ ( ( # ` F ) + ( # ` G ) ) ) X. { K } ) )
49 eqid 
 |-  ( ( 0 ..^ ( # ` F ) ) X. { K } ) = ( ( 0 ..^ ( # ` F ) ) X. { K } )
50 eqid 
 |-  ( ( 0 ..^ ( # ` G ) ) X. { K } ) = ( ( 0 ..^ ( # ` G ) ) X. { K } )
51 49 50 44 3 20 32 ccatmulgnn0dir 
 |-  ( ph -> ( ( ( 0 ..^ ( # ` F ) ) X. { K } ) ++ ( ( 0 ..^ ( # ` G ) ) X. { K } ) ) = ( ( 0 ..^ ( ( # ` F ) + ( # ` G ) ) ) X. { K } ) )
52 44 48 51 3eqtr4a 
 |-  ( ph -> ( ( 0 ..^ ( # ` ( F ++ G ) ) ) X. { K } ) = ( ( ( 0 ..^ ( # ` F ) ) X. { K } ) ++ ( ( 0 ..^ ( # ` G ) ) X. { K } ) ) )
53 52 oveq2d 
 |-  ( ph -> ( ( F ++ G ) oF R ( ( 0 ..^ ( # ` ( F ++ G ) ) ) X. { K } ) ) = ( ( F ++ G ) oF R ( ( ( 0 ..^ ( # ` F ) ) X. { K } ) ++ ( ( 0 ..^ ( # ` G ) ) X. { K } ) ) ) )
54 43 53 eqtrd 
 |-  ( ph -> ( ( F ++ G ) oFC R K ) = ( ( F ++ G ) oF R ( ( ( 0 ..^ ( # ` F ) ) X. { K } ) ++ ( ( 0 ..^ ( # ` G ) ) X. { K } ) ) ) )
55 wrdf 
 |-  ( F e. Word S -> F : ( 0 ..^ ( # ` F ) ) --> S )
56 1 55 syl 
 |-  ( ph -> F : ( 0 ..^ ( # ` F ) ) --> S )
57 ovexd 
 |-  ( ph -> ( 0 ..^ ( # ` F ) ) e. _V )
58 56 57 3 ofcof 
 |-  ( ph -> ( F oFC R K ) = ( F oF R ( ( 0 ..^ ( # ` F ) ) X. { K } ) ) )
59 wrdf 
 |-  ( G e. Word S -> G : ( 0 ..^ ( # ` G ) ) --> S )
60 2 59 syl 
 |-  ( ph -> G : ( 0 ..^ ( # ` G ) ) --> S )
61 ovexd 
 |-  ( ph -> ( 0 ..^ ( # ` G ) ) e. _V )
62 60 61 3 ofcof 
 |-  ( ph -> ( G oFC R K ) = ( G oF R ( ( 0 ..^ ( # ` G ) ) X. { K } ) ) )
63 58 62 oveq12d 
 |-  ( ph -> ( ( F oFC R K ) ++ ( G oFC R K ) ) = ( ( F oF R ( ( 0 ..^ ( # ` F ) ) X. { K } ) ) ++ ( G oF R ( ( 0 ..^ ( # ` G ) ) X. { K } ) ) ) )
64 37 54 63 3eqtr4d 
 |-  ( ph -> ( ( F ++ G ) oFC R K ) = ( ( F oFC R K ) ++ ( G oFC R K ) ) )