Theorem ccatmulgnn0dir

Description: Concatenation of words follow the rule mulgnn0dir (although applying mulgnn0dir 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)

	Ref	Expression
Hypotheses	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	ccatmulgnn0dir	|- ( ph -> ( A ++ B ) = C )

Proof

Step	Hyp	Ref	Expression
1		ccatmulgnn0dir.a	|- A = ( ( 0 ..^ M ) X. { K } )
2		ccatmulgnn0dir.b	|- B = ( ( 0 ..^ N ) X. { K } )
3		ccatmulgnn0dir.c	|- C = ( ( 0 ..^ ( M + N ) ) X. { K } )
4		ccatmulgnn0dir.k	|- ( ph -> K e. S )
5		ccatmulgnn0dir.m	|- ( ph -> M e. NN0 )
6		ccatmulgnn0dir.n	|- ( ph -> N e. NN0 )
7	1	fveq2i	|- ( # ` A ) = ( # ` ( ( 0 ..^ M ) X. { K } ) )
8		fzofi	|- ( 0 ..^ M ) e. Fin
9		snfi	|- { K } e. Fin
10		hashxp	|- ( ( ( 0 ..^ M ) e. Fin /\ { K } e. Fin ) -> ( # ` ( ( 0 ..^ M ) X. { K } ) ) = ( ( # ` ( 0 ..^ M ) ) x. ( # ` { K } ) ) )
11	8 9 10	mp2an	|- ( # ` ( ( 0 ..^ M ) X. { K } ) ) = ( ( # ` ( 0 ..^ M ) ) x. ( # ` { K } ) )
12	7 11	eqtri	|- ( # ` A ) = ( ( # ` ( 0 ..^ M ) ) x. ( # ` { K } ) )
13		hashfzo0	|- ( M e. NN0 -> ( # ` ( 0 ..^ M ) ) = M )
14	5 13	syl	|- ( ph -> ( # ` ( 0 ..^ M ) ) = M )
15		hashsng	|- ( K e. S -> ( # ` { K } ) = 1 )
16	4 15	syl	|- ( ph -> ( # ` { K } ) = 1 )
17	14 16	oveq12d	|- ( ph -> ( ( # ` ( 0 ..^ M ) ) x. ( # ` { K } ) ) = ( M x. 1 ) )
18	12 17	syl5eq	|- ( ph -> ( # ` A ) = ( M x. 1 ) )
19	5	nn0cnd	|- ( ph -> M e. CC )
20	19	mulid1d	|- ( ph -> ( M x. 1 ) = M )
21	18 20	eqtrd	|- ( ph -> ( # ` A ) = M )
22	2	fveq2i	|- ( # ` B ) = ( # ` ( ( 0 ..^ N ) X. { K } ) )
23		fzofi	|- ( 0 ..^ N ) e. Fin
24		hashxp	|- ( ( ( 0 ..^ N ) e. Fin /\ { K } e. Fin ) -> ( # ` ( ( 0 ..^ N ) X. { K } ) ) = ( ( # ` ( 0 ..^ N ) ) x. ( # ` { K } ) ) )
25	23 9 24	mp2an	|- ( # ` ( ( 0 ..^ N ) X. { K } ) ) = ( ( # ` ( 0 ..^ N ) ) x. ( # ` { K } ) )
26	22 25	eqtri	|- ( # ` B ) = ( ( # ` ( 0 ..^ N ) ) x. ( # ` { K } ) )
27		hashfzo0	|- ( N e. NN0 -> ( # ` ( 0 ..^ N ) ) = N )
28	6 27	syl	|- ( ph -> ( # ` ( 0 ..^ N ) ) = N )
29	28 16	oveq12d	|- ( ph -> ( ( # ` ( 0 ..^ N ) ) x. ( # ` { K } ) ) = ( N x. 1 ) )
30	26 29	syl5eq	|- ( ph -> ( # ` B ) = ( N x. 1 ) )
31	6	nn0cnd	|- ( ph -> N e. CC )
32	31	mulid1d	|- ( ph -> ( N x. 1 ) = N )
33	30 32	eqtrd	|- ( ph -> ( # ` B ) = N )
34	21 33	oveq12d	|- ( ph -> ( ( # ` A ) + ( # ` B ) ) = ( M + N ) )
35	34	oveq2d	|- ( ph -> ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) = ( 0 ..^ ( M + N ) ) )
36		simpll	|- ( ( ( ph /\ i e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) -> ph )
37		simpr	|- ( ( ( ph /\ i e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) -> i e. ( 0 ..^ ( # ` A ) ) )
38	21	oveq2d	|- ( ph -> ( 0 ..^ ( # ` A ) ) = ( 0 ..^ M ) )
39	36 38	syl	|- ( ( ( ph /\ i e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) -> ( 0 ..^ ( # ` A ) ) = ( 0 ..^ M ) )
40	37 39	eleqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) -> i e. ( 0 ..^ M ) )
41		fconstg	|- ( K e. S -> ( ( 0 ..^ M ) X. { K } ) : ( 0 ..^ M ) --> { K } )
42	4 41	syl	|- ( ph -> ( ( 0 ..^ M ) X. { K } ) : ( 0 ..^ M ) --> { K } )
43	1	a1i	|- ( ph -> A = ( ( 0 ..^ M ) X. { K } ) )
44	43	feq1d	|- ( ph -> ( A : ( 0 ..^ M ) --> { K } <-> ( ( 0 ..^ M ) X. { K } ) : ( 0 ..^ M ) --> { K } ) )
45	42 44	mpbird	|- ( ph -> A : ( 0 ..^ M ) --> { K } )
46		fvconst	|- ( ( A : ( 0 ..^ M ) --> { K } /\ i e. ( 0 ..^ M ) ) -> ( A ` i ) = K )
47	45 46	sylan	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( A ` i ) = K )
48	36 40 47	syl2anc	|- ( ( ( ph /\ i e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) -> ( A ` i ) = K )
49		simpll	|- ( ( ( ph /\ i e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) ) /\ -. i e. ( 0 ..^ ( # ` A ) ) ) -> ph )
50		simplr	|- ( ( ( ph /\ i e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) ) /\ -. i e. ( 0 ..^ ( # ` A ) ) ) -> i e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) )
51		simpr	|- ( ( ( ph /\ i e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) ) /\ -. i e. ( 0 ..^ ( # ` A ) ) ) -> -. i e. ( 0 ..^ ( # ` A ) ) )
52	21 5	eqeltrd	|- ( ph -> ( # ` A ) e. NN0 )
53	49 52	syl	|- ( ( ( ph /\ i e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) ) /\ -. i e. ( 0 ..^ ( # ` A ) ) ) -> ( # ` A ) e. NN0 )
54	53	nn0zd	|- ( ( ( ph /\ i e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) ) /\ -. i e. ( 0 ..^ ( # ` A ) ) ) -> ( # ` A ) e. ZZ )
55	33 6	eqeltrd	|- ( ph -> ( # ` B ) e. NN0 )
56	49 55	syl	|- ( ( ( ph /\ i e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) ) /\ -. i e. ( 0 ..^ ( # ` A ) ) ) -> ( # ` B ) e. NN0 )
57	56	nn0zd	|- ( ( ( ph /\ i e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) ) /\ -. i e. ( 0 ..^ ( # ` A ) ) ) -> ( # ` B ) e. ZZ )
58		fzocatel	|- ( ( ( i e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) /\ -. i e. ( 0 ..^ ( # ` A ) ) ) /\ ( ( # ` A ) e. ZZ /\ ( # ` B ) e. ZZ ) ) -> ( i - ( # ` A ) ) e. ( 0 ..^ ( # ` B ) ) )
59	50 51 54 57 58	syl22anc	|- ( ( ( ph /\ i e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) ) /\ -. i e. ( 0 ..^ ( # ` A ) ) ) -> ( i - ( # ` A ) ) e. ( 0 ..^ ( # ` B ) ) )
60	33	oveq2d	|- ( ph -> ( 0 ..^ ( # ` B ) ) = ( 0 ..^ N ) )
61	49 60	syl	|- ( ( ( ph /\ i e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) ) /\ -. i e. ( 0 ..^ ( # ` A ) ) ) -> ( 0 ..^ ( # ` B ) ) = ( 0 ..^ N ) )
62	59 61	eleqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) ) /\ -. i e. ( 0 ..^ ( # ` A ) ) ) -> ( i - ( # ` A ) ) e. ( 0 ..^ N ) )
63		fconstg	|- ( K e. S -> ( ( 0 ..^ N ) X. { K } ) : ( 0 ..^ N ) --> { K } )
64	4 63	syl	|- ( ph -> ( ( 0 ..^ N ) X. { K } ) : ( 0 ..^ N ) --> { K } )
65	2	a1i	|- ( ph -> B = ( ( 0 ..^ N ) X. { K } ) )
66	65	feq1d	|- ( ph -> ( B : ( 0 ..^ N ) --> { K } <-> ( ( 0 ..^ N ) X. { K } ) : ( 0 ..^ N ) --> { K } ) )
67	64 66	mpbird	|- ( ph -> B : ( 0 ..^ N ) --> { K } )
68		fvconst	|- ( ( B : ( 0 ..^ N ) --> { K } /\ ( i - ( # ` A ) ) e. ( 0 ..^ N ) ) -> ( B ` ( i - ( # ` A ) ) ) = K )
69	67 68	sylan	|- ( ( ph /\ ( i - ( # ` A ) ) e. ( 0 ..^ N ) ) -> ( B ` ( i - ( # ` A ) ) ) = K )
70	49 62 69	syl2anc	|- ( ( ( ph /\ i e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) ) /\ -. i e. ( 0 ..^ ( # ` A ) ) ) -> ( B ` ( i - ( # ` A ) ) ) = K )
71	48 70	ifeqda	|- ( ( ph /\ i e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) ) -> if ( i e. ( 0 ..^ ( # ` A ) ) , ( A ` i ) , ( B ` ( i - ( # ` A ) ) ) ) = K )
72	35 71	mpteq12dva	|- ( ph -> ( i e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( i e. ( 0 ..^ ( # ` A ) ) , ( A ` i ) , ( B ` ( i - ( # ` A ) ) ) ) ) = ( i e. ( 0 ..^ ( M + N ) ) |-> K ) )
73		ovex	|- ( 0 ..^ M ) e. _V
74		snex	|- { K } e. _V
75	73 74	xpex	|- ( ( 0 ..^ M ) X. { K } ) e. _V
76	1 75	eqeltri	|- A e. _V
77		ovex	|- ( 0 ..^ N ) e. _V
78	77 74	xpex	|- ( ( 0 ..^ N ) X. { K } ) e. _V
79	2 78	eqeltri	|- B e. _V
80		ccatfval	|- ( ( A e. _V /\ B e. _V ) -> ( A ++ B ) = ( i e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( i e. ( 0 ..^ ( # ` A ) ) , ( A ` i ) , ( B ` ( i - ( # ` A ) ) ) ) ) )
81	76 79 80	mp2an	|- ( A ++ B ) = ( i e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( i e. ( 0 ..^ ( # ` A ) ) , ( A ` i ) , ( B ` ( i - ( # ` A ) ) ) ) )
82		fconstmpt	|- ( ( 0 ..^ ( M + N ) ) X. { K } ) = ( i e. ( 0 ..^ ( M + N ) ) |-> K )
83	3 82	eqtri	|- C = ( i e. ( 0 ..^ ( M + N ) ) |-> K )
84	72 81 83	3eqtr4g	|- ( ph -> ( A ++ B ) = C )