Theorem frlmfzoccat

Description: The concatenation of two vectors of dimension N and M forms a vector of dimension N + M . (Contributed by SN, 31-Aug-2023)

	Ref	Expression
Hypotheses	frlmfzoccat.w	$$⊢W=K\mathrm{freeLMod}\left(0..^L\right)$$
	frlmfzoccat.x	$$⊢X=K\mathrm{freeLMod}\left(0..^M\right)$$
	frlmfzoccat.y	$$⊢Y=K\mathrm{freeLMod}\left(0..^N\right)$$
	frlmfzoccat.b	$$⊢B={\mathrm{Base}}_W$$
	frlmfzoccat.c	$$⊢C={\mathrm{Base}}_X$$
	frlmfzoccat.d	$$⊢D={\mathrm{Base}}_Y$$
	frlmfzoccat.k	$$⊢\phi \to K\in Z$$
	frlmfzoccat.l	$$⊢\phi \to M+N=L$$
	frlmfzoccat.m	$$⊢\phi \to M\in {\mathbb{N}}_0$$
	frlmfzoccat.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	frlmfzoccat.u	$$⊢\phi \to U\in C$$
	frlmfzoccat.v	$$⊢\phi \to V\in D$$
Assertion	frlmfzoccat	$$⊢\phi \to U\mathrm{++}V\in B$$

Proof

Step	Hyp	Ref	Expression
1		frlmfzoccat.w	$$⊢W=K\mathrm{freeLMod}\left(0..^L\right)$$
2		frlmfzoccat.x	$$⊢X=K\mathrm{freeLMod}\left(0..^M\right)$$
3		frlmfzoccat.y	$$⊢Y=K\mathrm{freeLMod}\left(0..^N\right)$$
4		frlmfzoccat.b	$$⊢B={\mathrm{Base}}_W$$
5		frlmfzoccat.c	$$⊢C={\mathrm{Base}}_X$$
6		frlmfzoccat.d	$$⊢D={\mathrm{Base}}_Y$$
7		frlmfzoccat.k	$$⊢\phi \to K\in Z$$
8		frlmfzoccat.l	$$⊢\phi \to M+N=L$$
9		frlmfzoccat.m	$$⊢\phi \to M\in {\mathbb{N}}_0$$
10		frlmfzoccat.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
11		frlmfzoccat.u	$$⊢\phi \to U\in C$$
12		frlmfzoccat.v	$$⊢\phi \to V\in D$$
13		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
14	2 5 13	frlmfzowrd	$$⊢U\in C\to U\in \mathrm{Word}{\mathrm{Base}}_K$$
15	11 14	syl	$$⊢\phi \to U\in \mathrm{Word}{\mathrm{Base}}_K$$
16	3 6 13	frlmfzowrd	$$⊢V\in D\to V\in \mathrm{Word}{\mathrm{Base}}_K$$
17	12 16	syl	$$⊢\phi \to V\in \mathrm{Word}{\mathrm{Base}}_K$$
18		ccatcl	$$⊢\left(U\in \mathrm{Word}{\mathrm{Base}}_K\wedge V\in \mathrm{Word}{\mathrm{Base}}_K\right)\to U\mathrm{++}V\in \mathrm{Word}{\mathrm{Base}}_K$$
19	15 17 18	syl2anc	$$⊢\phi \to U\mathrm{++}V\in \mathrm{Word}{\mathrm{Base}}_K$$
20		ccatlen	$$⊢\left(U\in \mathrm{Word}{\mathrm{Base}}_K\wedge V\in \mathrm{Word}{\mathrm{Base}}_K\right)\to \left|U\mathrm{++}V\right|=\left|U\right|+\left|V\right|$$
21	15 17 20	syl2anc	$$⊢\phi \to \left|U\mathrm{++}V\right|=\left|U\right|+\left|V\right|$$
22		ovexd	$$⊢\phi \to \left(0..^M\right)\in \mathrm{V}$$
23	2 13 5	frlmbasf	$$⊢\left(\left(0..^M\right)\in \mathrm{V}\wedge U\in C\right)\to U:\left(0..^M\right)⟶{\mathrm{Base}}_K$$
24	22 11 23	syl2anc	$$⊢\phi \to U:\left(0..^M\right)⟶{\mathrm{Base}}_K$$
25		fnfzo0hash	$$⊢\left(M\in {\mathbb{N}}_0\wedge U:\left(0..^M\right)⟶{\mathrm{Base}}_K\right)\to \left|U\right|=M$$
26	9 24 25	syl2anc	$$⊢\phi \to \left|U\right|=M$$
27		ovexd	$$⊢\phi \to \left(0..^N\right)\in \mathrm{V}$$
28	3 13 6	frlmbasf	$$⊢\left(\left(0..^N\right)\in \mathrm{V}\wedge V\in D\right)\to V:\left(0..^N\right)⟶{\mathrm{Base}}_K$$
29	27 12 28	syl2anc	$$⊢\phi \to V:\left(0..^N\right)⟶{\mathrm{Base}}_K$$
30		fnfzo0hash	$$⊢\left(N\in {\mathbb{N}}_0\wedge V:\left(0..^N\right)⟶{\mathrm{Base}}_K\right)\to \left|V\right|=N$$
31	10 29 30	syl2anc	$$⊢\phi \to \left|V\right|=N$$
32	26 31	oveq12d	$$⊢\phi \to \left|U\right|+\left|V\right|=M+N$$
33	21 32 8	3eqtrd	$$⊢\phi \to \left|U\mathrm{++}V\right|=L$$
34	9 10	nn0addcld	$$⊢\phi \to M+N\in {\mathbb{N}}_0$$
35	8 34	eqeltrrd	$$⊢\phi \to L\in {\mathbb{N}}_0$$
36	1 4 13	frlmfzowrdb	$$⊢\left(K\in Z\wedge L\in {\mathbb{N}}_0\right)\to \left(U\mathrm{++}V\in B\leftrightarrow \left(U\mathrm{++}V\in \mathrm{Word}{\mathrm{Base}}_K\wedge \left|U\mathrm{++}V\right|=L\right)\right)$$
37	7 35 36	syl2anc	$$⊢\phi \to \left(U\mathrm{++}V\in B\leftrightarrow \left(U\mathrm{++}V\in \mathrm{Word}{\mathrm{Base}}_K\wedge \left|U\mathrm{++}V\right|=L\right)\right)$$
38	19 33 37	mpbir2and	$$⊢\phi \to U\mathrm{++}V\in B$$