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 𝑊 = ( 𝐾 freeLMod ( 0 ..^ 𝐿 ) )
frlmfzoccat.x 𝑋 = ( 𝐾 freeLMod ( 0 ..^ 𝑀 ) )
frlmfzoccat.y 𝑌 = ( 𝐾 freeLMod ( 0 ..^ 𝑁 ) )
frlmfzoccat.b 𝐵 = ( Base ‘ 𝑊 )
frlmfzoccat.c 𝐶 = ( Base ‘ 𝑋 )
frlmfzoccat.d 𝐷 = ( Base ‘ 𝑌 )
frlmfzoccat.k ( 𝜑𝐾𝑍 )
frlmfzoccat.l ( 𝜑 → ( 𝑀 + 𝑁 ) = 𝐿 )
frlmfzoccat.m ( 𝜑𝑀 ∈ ℕ0 )
frlmfzoccat.n ( 𝜑𝑁 ∈ ℕ0 )
frlmfzoccat.u ( 𝜑𝑈𝐶 )
frlmfzoccat.v ( 𝜑𝑉𝐷 )
Assertion frlmfzoccat ( 𝜑 → ( 𝑈 ++ 𝑉 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 frlmfzoccat.w 𝑊 = ( 𝐾 freeLMod ( 0 ..^ 𝐿 ) )
2 frlmfzoccat.x 𝑋 = ( 𝐾 freeLMod ( 0 ..^ 𝑀 ) )
3 frlmfzoccat.y 𝑌 = ( 𝐾 freeLMod ( 0 ..^ 𝑁 ) )
4 frlmfzoccat.b 𝐵 = ( Base ‘ 𝑊 )
5 frlmfzoccat.c 𝐶 = ( Base ‘ 𝑋 )
6 frlmfzoccat.d 𝐷 = ( Base ‘ 𝑌 )
7 frlmfzoccat.k ( 𝜑𝐾𝑍 )
8 frlmfzoccat.l ( 𝜑 → ( 𝑀 + 𝑁 ) = 𝐿 )
9 frlmfzoccat.m ( 𝜑𝑀 ∈ ℕ0 )
10 frlmfzoccat.n ( 𝜑𝑁 ∈ ℕ0 )
11 frlmfzoccat.u ( 𝜑𝑈𝐶 )
12 frlmfzoccat.v ( 𝜑𝑉𝐷 )
13 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
14 2 5 13 frlmfzowrd ( 𝑈𝐶𝑈 ∈ Word ( Base ‘ 𝐾 ) )
15 11 14 syl ( 𝜑𝑈 ∈ Word ( Base ‘ 𝐾 ) )
16 3 6 13 frlmfzowrd ( 𝑉𝐷𝑉 ∈ Word ( Base ‘ 𝐾 ) )
17 12 16 syl ( 𝜑𝑉 ∈ Word ( Base ‘ 𝐾 ) )
18 ccatcl ( ( 𝑈 ∈ Word ( Base ‘ 𝐾 ) ∧ 𝑉 ∈ Word ( Base ‘ 𝐾 ) ) → ( 𝑈 ++ 𝑉 ) ∈ Word ( Base ‘ 𝐾 ) )
19 15 17 18 syl2anc ( 𝜑 → ( 𝑈 ++ 𝑉 ) ∈ Word ( Base ‘ 𝐾 ) )
20 ccatlen ( ( 𝑈 ∈ Word ( Base ‘ 𝐾 ) ∧ 𝑉 ∈ Word ( Base ‘ 𝐾 ) ) → ( ♯ ‘ ( 𝑈 ++ 𝑉 ) ) = ( ( ♯ ‘ 𝑈 ) + ( ♯ ‘ 𝑉 ) ) )
21 15 17 20 syl2anc ( 𝜑 → ( ♯ ‘ ( 𝑈 ++ 𝑉 ) ) = ( ( ♯ ‘ 𝑈 ) + ( ♯ ‘ 𝑉 ) ) )
22 ovexd ( 𝜑 → ( 0 ..^ 𝑀 ) ∈ V )
23 2 13 5 frlmbasf ( ( ( 0 ..^ 𝑀 ) ∈ V ∧ 𝑈𝐶 ) → 𝑈 : ( 0 ..^ 𝑀 ) ⟶ ( Base ‘ 𝐾 ) )
24 22 11 23 syl2anc ( 𝜑𝑈 : ( 0 ..^ 𝑀 ) ⟶ ( Base ‘ 𝐾 ) )
25 fnfzo0hash ( ( 𝑀 ∈ ℕ0𝑈 : ( 0 ..^ 𝑀 ) ⟶ ( Base ‘ 𝐾 ) ) → ( ♯ ‘ 𝑈 ) = 𝑀 )
26 9 24 25 syl2anc ( 𝜑 → ( ♯ ‘ 𝑈 ) = 𝑀 )
27 ovexd ( 𝜑 → ( 0 ..^ 𝑁 ) ∈ V )
28 3 13 6 frlmbasf ( ( ( 0 ..^ 𝑁 ) ∈ V ∧ 𝑉𝐷 ) → 𝑉 : ( 0 ..^ 𝑁 ) ⟶ ( Base ‘ 𝐾 ) )
29 27 12 28 syl2anc ( 𝜑𝑉 : ( 0 ..^ 𝑁 ) ⟶ ( Base ‘ 𝐾 ) )
30 fnfzo0hash ( ( 𝑁 ∈ ℕ0𝑉 : ( 0 ..^ 𝑁 ) ⟶ ( Base ‘ 𝐾 ) ) → ( ♯ ‘ 𝑉 ) = 𝑁 )
31 10 29 30 syl2anc ( 𝜑 → ( ♯ ‘ 𝑉 ) = 𝑁 )
32 26 31 oveq12d ( 𝜑 → ( ( ♯ ‘ 𝑈 ) + ( ♯ ‘ 𝑉 ) ) = ( 𝑀 + 𝑁 ) )
33 21 32 8 3eqtrd ( 𝜑 → ( ♯ ‘ ( 𝑈 ++ 𝑉 ) ) = 𝐿 )
34 9 10 nn0addcld ( 𝜑 → ( 𝑀 + 𝑁 ) ∈ ℕ0 )
35 8 34 eqeltrrd ( 𝜑𝐿 ∈ ℕ0 )
36 1 4 13 frlmfzowrdb ( ( 𝐾𝑍𝐿 ∈ ℕ0 ) → ( ( 𝑈 ++ 𝑉 ) ∈ 𝐵 ↔ ( ( 𝑈 ++ 𝑉 ) ∈ Word ( Base ‘ 𝐾 ) ∧ ( ♯ ‘ ( 𝑈 ++ 𝑉 ) ) = 𝐿 ) ) )
37 7 35 36 syl2anc ( 𝜑 → ( ( 𝑈 ++ 𝑉 ) ∈ 𝐵 ↔ ( ( 𝑈 ++ 𝑉 ) ∈ Word ( Base ‘ 𝐾 ) ∧ ( ♯ ‘ ( 𝑈 ++ 𝑉 ) ) = 𝐿 ) ) )
38 19 33 37 mpbir2and ( 𝜑 → ( 𝑈 ++ 𝑉 ) ∈ 𝐵 )