Metamath Proof Explorer


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 freeLMod 0 ..^ L
frlmfzoccat.x X = K freeLMod 0 ..^ M
frlmfzoccat.y Y = K freeLMod 0 ..^ N
frlmfzoccat.b B = Base W
frlmfzoccat.c C = Base X
frlmfzoccat.d D = Base Y
frlmfzoccat.k φ K Z
frlmfzoccat.l φ M + N = L
frlmfzoccat.m φ M 0
frlmfzoccat.n φ N 0
frlmfzoccat.u φ U C
frlmfzoccat.v φ V D
Assertion frlmfzoccat φ U ++ V B

Proof

Step Hyp Ref Expression
1 frlmfzoccat.w W = K freeLMod 0 ..^ L
2 frlmfzoccat.x X = K freeLMod 0 ..^ M
3 frlmfzoccat.y Y = K freeLMod 0 ..^ N
4 frlmfzoccat.b B = Base W
5 frlmfzoccat.c C = Base X
6 frlmfzoccat.d D = Base Y
7 frlmfzoccat.k φ K Z
8 frlmfzoccat.l φ M + N = L
9 frlmfzoccat.m φ M 0
10 frlmfzoccat.n φ N 0
11 frlmfzoccat.u φ U C
12 frlmfzoccat.v φ V D
13 eqid Base K = Base K
14 2 5 13 frlmfzowrd U C U Word Base K
15 11 14 syl φ U Word Base K
16 3 6 13 frlmfzowrd V D V Word Base K
17 12 16 syl φ V Word Base K
18 ccatcl U Word Base K V Word Base K U ++ V Word Base K
19 15 17 18 syl2anc φ U ++ V Word Base K
20 ccatlen U Word Base K V Word Base K U ++ V = U + V
21 15 17 20 syl2anc φ U ++ V = U + V
22 ovexd φ 0 ..^ M V
23 2 13 5 frlmbasf 0 ..^ M V U C U : 0 ..^ M Base K
24 22 11 23 syl2anc φ U : 0 ..^ M Base K
25 fnfzo0hash M 0 U : 0 ..^ M Base K U = M
26 9 24 25 syl2anc φ U = M
27 ovexd φ 0 ..^ N V
28 3 13 6 frlmbasf 0 ..^ N V V D V : 0 ..^ N Base K
29 27 12 28 syl2anc φ V : 0 ..^ N Base K
30 fnfzo0hash N 0 V : 0 ..^ N Base K V = N
31 10 29 30 syl2anc φ V = N
32 26 31 oveq12d φ U + V = M + N
33 21 32 8 3eqtrd φ U ++ V = L
34 9 10 nn0addcld φ M + N 0
35 8 34 eqeltrrd φ L 0
36 1 4 13 frlmfzowrdb K Z L 0 U ++ V B U ++ V Word Base K U ++ V = L
37 7 35 36 syl2anc φ U ++ V B U ++ V Word Base K U ++ V = L
38 19 33 37 mpbir2and φ U ++ V B