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 
|- ( ph -> K e. Z )
frlmfzoccat.l 
|- ( ph -> ( M + N ) = L )
frlmfzoccat.m 
|- ( ph -> M e. NN0 )
frlmfzoccat.n 
|- ( ph -> N e. NN0 )
frlmfzoccat.u 
|- ( ph -> U e. C )
frlmfzoccat.v 
|- ( ph -> V e. D )
Assertion frlmfzoccat 
|- ( ph -> ( U ++ V ) e. 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 
 |-  ( ph -> K e. Z )
8 frlmfzoccat.l 
 |-  ( ph -> ( M + N ) = L )
9 frlmfzoccat.m 
 |-  ( ph -> M e. NN0 )
10 frlmfzoccat.n 
 |-  ( ph -> N e. NN0 )
11 frlmfzoccat.u 
 |-  ( ph -> U e. C )
12 frlmfzoccat.v 
 |-  ( ph -> V e. D )
13 eqid 
 |-  ( Base ` K ) = ( Base ` K )
14 2 5 13 frlmfzowrd 
 |-  ( U e. C -> U e. Word ( Base ` K ) )
15 11 14 syl 
 |-  ( ph -> U e. Word ( Base ` K ) )
16 3 6 13 frlmfzowrd 
 |-  ( V e. D -> V e. Word ( Base ` K ) )
17 12 16 syl 
 |-  ( ph -> V e. Word ( Base ` K ) )
18 ccatcl 
 |-  ( ( U e. Word ( Base ` K ) /\ V e. Word ( Base ` K ) ) -> ( U ++ V ) e. Word ( Base ` K ) )
19 15 17 18 syl2anc 
 |-  ( ph -> ( U ++ V ) e. Word ( Base ` K ) )
20 ccatlen 
 |-  ( ( U e. Word ( Base ` K ) /\ V e. Word ( Base ` K ) ) -> ( # ` ( U ++ V ) ) = ( ( # ` U ) + ( # ` V ) ) )
21 15 17 20 syl2anc 
 |-  ( ph -> ( # ` ( U ++ V ) ) = ( ( # ` U ) + ( # ` V ) ) )
22 ovexd 
 |-  ( ph -> ( 0 ..^ M ) e. _V )
23 2 13 5 frlmbasf 
 |-  ( ( ( 0 ..^ M ) e. _V /\ U e. C ) -> U : ( 0 ..^ M ) --> ( Base ` K ) )
24 22 11 23 syl2anc 
 |-  ( ph -> U : ( 0 ..^ M ) --> ( Base ` K ) )
25 fnfzo0hash 
 |-  ( ( M e. NN0 /\ U : ( 0 ..^ M ) --> ( Base ` K ) ) -> ( # ` U ) = M )
26 9 24 25 syl2anc 
 |-  ( ph -> ( # ` U ) = M )
27 ovexd 
 |-  ( ph -> ( 0 ..^ N ) e. _V )
28 3 13 6 frlmbasf 
 |-  ( ( ( 0 ..^ N ) e. _V /\ V e. D ) -> V : ( 0 ..^ N ) --> ( Base ` K ) )
29 27 12 28 syl2anc 
 |-  ( ph -> V : ( 0 ..^ N ) --> ( Base ` K ) )
30 fnfzo0hash 
 |-  ( ( N e. NN0 /\ V : ( 0 ..^ N ) --> ( Base ` K ) ) -> ( # ` V ) = N )
31 10 29 30 syl2anc 
 |-  ( ph -> ( # ` V ) = N )
32 26 31 oveq12d 
 |-  ( ph -> ( ( # ` U ) + ( # ` V ) ) = ( M + N ) )
33 21 32 8 3eqtrd 
 |-  ( ph -> ( # ` ( U ++ V ) ) = L )
34 9 10 nn0addcld 
 |-  ( ph -> ( M + N ) e. NN0 )
35 8 34 eqeltrrd 
 |-  ( ph -> L e. NN0 )
36 1 4 13 frlmfzowrdb 
 |-  ( ( K e. Z /\ L e. NN0 ) -> ( ( U ++ V ) e. B <-> ( ( U ++ V ) e. Word ( Base ` K ) /\ ( # ` ( U ++ V ) ) = L ) ) )
37 7 35 36 syl2anc 
 |-  ( ph -> ( ( U ++ V ) e. B <-> ( ( U ++ V ) e. Word ( Base ` K ) /\ ( # ` ( U ++ V ) ) = L ) ) )
38 19 33 37 mpbir2and 
 |-  ( ph -> ( U ++ V ) e. B )