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	⊢ 𝐴 = ( ( 0 ..^ 𝑀 ) × { 𝐾 } )
	ccatmulgnn0dir.b	⊢ 𝐵 = ( ( 0 ..^ 𝑁 ) × { 𝐾 } )
	ccatmulgnn0dir.c	⊢ 𝐶 = ( ( 0 ..^ ( 𝑀 + 𝑁 ) ) × { 𝐾 } )
	ccatmulgnn0dir.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑆 )
	ccatmulgnn0dir.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
	ccatmulgnn0dir.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	ccatmulgnn0dir	⊢ ( 𝜑 → ( 𝐴 ++ 𝐵 ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		ccatmulgnn0dir.a	⊢ 𝐴 = ( ( 0 ..^ 𝑀 ) × { 𝐾 } )
2		ccatmulgnn0dir.b	⊢ 𝐵 = ( ( 0 ..^ 𝑁 ) × { 𝐾 } )
3		ccatmulgnn0dir.c	⊢ 𝐶 = ( ( 0 ..^ ( 𝑀 + 𝑁 ) ) × { 𝐾 } )
4		ccatmulgnn0dir.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑆 )
5		ccatmulgnn0dir.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
6		ccatmulgnn0dir.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
7	1	fveq2i	⊢ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐾 } ) )
8		fzofi	⊢ ( 0 ..^ 𝑀 ) ∈ Fin
9		snfi	⊢ { 𝐾 } ∈ Fin
10		hashxp	⊢ ( ( ( 0 ..^ 𝑀 ) ∈ Fin ∧ { 𝐾 } ∈ Fin ) → ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐾 } ) ) = ( ( ♯ ‘ ( 0 ..^ 𝑀 ) ) · ( ♯ ‘ { 𝐾 } ) ) )
11	8 9 10	mp2an	⊢ ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐾 } ) ) = ( ( ♯ ‘ ( 0 ..^ 𝑀 ) ) · ( ♯ ‘ { 𝐾 } ) )
12	7 11	eqtri	⊢ ( ♯ ‘ 𝐴 ) = ( ( ♯ ‘ ( 0 ..^ 𝑀 ) ) · ( ♯ ‘ { 𝐾 } ) )
13		hashfzo0	⊢ ( 𝑀 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝑀 ) ) = 𝑀 )
14	5 13	syl	⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ 𝑀 ) ) = 𝑀 )
15		hashsng	⊢ ( 𝐾 ∈ 𝑆 → ( ♯ ‘ { 𝐾 } ) = 1 )
16	4 15	syl	⊢ ( 𝜑 → ( ♯ ‘ { 𝐾 } ) = 1 )
17	14 16	oveq12d	⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ..^ 𝑀 ) ) · ( ♯ ‘ { 𝐾 } ) ) = ( 𝑀 · 1 ) )
18	12 17	eqtrid	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( 𝑀 · 1 ) )
19	5	nn0cnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
20	19	mulridd	⊢ ( 𝜑 → ( 𝑀 · 1 ) = 𝑀 )
21	18 20	eqtrd	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = 𝑀 )
22	2	fveq2i	⊢ ( ♯ ‘ 𝐵 ) = ( ♯ ‘ ( ( 0 ..^ 𝑁 ) × { 𝐾 } ) )
23		fzofi	⊢ ( 0 ..^ 𝑁 ) ∈ Fin
24		hashxp	⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ { 𝐾 } ∈ Fin ) → ( ♯ ‘ ( ( 0 ..^ 𝑁 ) × { 𝐾 } ) ) = ( ( ♯ ‘ ( 0 ..^ 𝑁 ) ) · ( ♯ ‘ { 𝐾 } ) ) )
25	23 9 24	mp2an	⊢ ( ♯ ‘ ( ( 0 ..^ 𝑁 ) × { 𝐾 } ) ) = ( ( ♯ ‘ ( 0 ..^ 𝑁 ) ) · ( ♯ ‘ { 𝐾 } ) )
26	22 25	eqtri	⊢ ( ♯ ‘ 𝐵 ) = ( ( ♯ ‘ ( 0 ..^ 𝑁 ) ) · ( ♯ ‘ { 𝐾 } ) )
27		hashfzo0	⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
28	6 27	syl	⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
29	28 16	oveq12d	⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ..^ 𝑁 ) ) · ( ♯ ‘ { 𝐾 } ) ) = ( 𝑁 · 1 ) )
30	26 29	eqtrid	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( 𝑁 · 1 ) )
31	6	nn0cnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
32	31	mulridd	⊢ ( 𝜑 → ( 𝑁 · 1 ) = 𝑁 )
33	30 32	eqtrd	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = 𝑁 )
34	21 33	oveq12d	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) = ( 𝑀 + 𝑁 ) )
35	34	oveq2d	⊢ ( 𝜑 → ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) = ( 0 ..^ ( 𝑀 + 𝑁 ) ) )
36		simpll	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → 𝜑 )
37		simpr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
38	21	oveq2d	⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐴 ) ) = ( 0 ..^ 𝑀 ) )
39	36 38	syl	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( 0 ..^ ( ♯ ‘ 𝐴 ) ) = ( 0 ..^ 𝑀 ) )
40	37 39	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
41		fconstg	⊢ ( 𝐾 ∈ 𝑆 → ( ( 0 ..^ 𝑀 ) × { 𝐾 } ) : ( 0 ..^ 𝑀 ) ⟶ { 𝐾 } )
42	4 41	syl	⊢ ( 𝜑 → ( ( 0 ..^ 𝑀 ) × { 𝐾 } ) : ( 0 ..^ 𝑀 ) ⟶ { 𝐾 } )
43	1	a1i	⊢ ( 𝜑 → 𝐴 = ( ( 0 ..^ 𝑀 ) × { 𝐾 } ) )
44	43	feq1d	⊢ ( 𝜑 → ( 𝐴 : ( 0 ..^ 𝑀 ) ⟶ { 𝐾 } ↔ ( ( 0 ..^ 𝑀 ) × { 𝐾 } ) : ( 0 ..^ 𝑀 ) ⟶ { 𝐾 } ) )
45	42 44	mpbird	⊢ ( 𝜑 → 𝐴 : ( 0 ..^ 𝑀 ) ⟶ { 𝐾 } )
46		fvconst	⊢ ( ( 𝐴 : ( 0 ..^ 𝑀 ) ⟶ { 𝐾 } ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐴 ‘ 𝑖 ) = 𝐾 )
47	45 46	sylan	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐴 ‘ 𝑖 ) = 𝐾 )
48	36 40 47	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( 𝐴 ‘ 𝑖 ) = 𝐾 )
49		simpll	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → 𝜑 )
50		simplr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )
51		simpr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
52	21 5	eqeltrd	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
53	49 52	syl	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
54	53	nn0zd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ℤ )
55	33 6	eqeltrd	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
56	49 55	syl	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
57	56	nn0zd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( ♯ ‘ 𝐵 ) ∈ ℤ )
58		fzocatel	⊢ ( ( ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℤ ) ) → ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) )
59	50 51 54 57 58	syl22anc	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) )
60	33	oveq2d	⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐵 ) ) = ( 0 ..^ 𝑁 ) )
61	49 60	syl	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( 0 ..^ ( ♯ ‘ 𝐵 ) ) = ( 0 ..^ 𝑁 ) )
62	59 61	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ 𝑁 ) )
63		fconstg	⊢ ( 𝐾 ∈ 𝑆 → ( ( 0 ..^ 𝑁 ) × { 𝐾 } ) : ( 0 ..^ 𝑁 ) ⟶ { 𝐾 } )
64	4 63	syl	⊢ ( 𝜑 → ( ( 0 ..^ 𝑁 ) × { 𝐾 } ) : ( 0 ..^ 𝑁 ) ⟶ { 𝐾 } )
65	2	a1i	⊢ ( 𝜑 → 𝐵 = ( ( 0 ..^ 𝑁 ) × { 𝐾 } ) )
66	65	feq1d	⊢ ( 𝜑 → ( 𝐵 : ( 0 ..^ 𝑁 ) ⟶ { 𝐾 } ↔ ( ( 0 ..^ 𝑁 ) × { 𝐾 } ) : ( 0 ..^ 𝑁 ) ⟶ { 𝐾 } ) )
67	64 66	mpbird	⊢ ( 𝜑 → 𝐵 : ( 0 ..^ 𝑁 ) ⟶ { 𝐾 } )
68		fvconst	⊢ ( ( 𝐵 : ( 0 ..^ 𝑁 ) ⟶ { 𝐾 } ∧ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 ‘ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ) = 𝐾 )
69	67 68	sylan	⊢ ( ( 𝜑 ∧ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 ‘ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ) = 𝐾 )
70	49 62 69	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( 𝐵 ‘ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ) = 𝐾 )
71	48 70	ifeqda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) → if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑖 ) , ( 𝐵 ‘ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ) ) = 𝐾 )
72	35 71	mpteq12dva	⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑖 ) , ( 𝐵 ‘ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ) ) ) = ( 𝑖 ∈ ( 0 ..^ ( 𝑀 + 𝑁 ) ) ↦ 𝐾 ) )
73		ovex	⊢ ( 0 ..^ 𝑀 ) ∈ V
74		snex	⊢ { 𝐾 } ∈ V
75	73 74	xpex	⊢ ( ( 0 ..^ 𝑀 ) × { 𝐾 } ) ∈ V
76	1 75	eqeltri	⊢ 𝐴 ∈ V
77		ovex	⊢ ( 0 ..^ 𝑁 ) ∈ V
78	77 74	xpex	⊢ ( ( 0 ..^ 𝑁 ) × { 𝐾 } ) ∈ V
79	2 78	eqeltri	⊢ 𝐵 ∈ V
80		ccatfval	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ++ 𝐵 ) = ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑖 ) , ( 𝐵 ‘ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ) ) ) )
81	76 79 80	mp2an	⊢ ( 𝐴 ++ 𝐵 ) = ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑖 ) , ( 𝐵 ‘ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ) ) )
82		fconstmpt	⊢ ( ( 0 ..^ ( 𝑀 + 𝑁 ) ) × { 𝐾 } ) = ( 𝑖 ∈ ( 0 ..^ ( 𝑀 + 𝑁 ) ) ↦ 𝐾 )
83	3 82	eqtri	⊢ 𝐶 = ( 𝑖 ∈ ( 0 ..^ ( 𝑀 + 𝑁 ) ) ↦ 𝐾 )
84	72 81 83	3eqtr4g	⊢ ( 𝜑 → ( 𝐴 ++ 𝐵 ) = 𝐶 )