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 ⊢ ( 𝜑 → ( 𝑈 ++ 𝑉 ) ∈ 𝐵 )