This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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