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