Metamath Proof Explorer

Theorem frlmvscadiccat

Description: Scalar multiplication distributes over concatenation. (Contributed by SN, 6-Sep-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 )
frlmvscadiccat.o 
|- O = ( .s ` W )
frlmvscadiccat.p 
|- .xb = ( .s ` X )
frlmvscadiccat.q 
|- .x. = ( .s ` Y )
frlmvscadiccat.s 
|- S = ( Base ` K )
frlmvscadiccat.a 
|- ( ph -> A e. S )
Assertion frlmvscadiccat 
|- ( ph -> ( A O ( U ++ V ) ) = ( ( A .xb U ) ++ ( A .x. V ) ) )

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 frlmvscadiccat.o 
 |-  O = ( .s ` W )
14 frlmvscadiccat.p 
 |-  .xb = ( .s ` X )
15 frlmvscadiccat.q 
 |-  .x. = ( .s ` Y )
16 frlmvscadiccat.s 
 |-  S = ( Base ` K )
17 frlmvscadiccat.a 
 |-  ( ph -> A e. S )
18 fconstg 
 |-  ( A e. S -> ( ( 0 ..^ L ) X. { A } ) : ( 0 ..^ L ) --> { A } )
19 17 18 syl 
 |-  ( ph -> ( ( 0 ..^ L ) X. { A } ) : ( 0 ..^ L ) --> { A } )
20 19 ffnd 
 |-  ( ph -> ( ( 0 ..^ L ) X. { A } ) Fn ( 0 ..^ L ) )
21 fconstg 
 |-  ( A e. S -> ( ( 0 ..^ M ) X. { A } ) : ( 0 ..^ M ) --> { A } )
22 iswrdi 
 |-  ( ( ( 0 ..^ M ) X. { A } ) : ( 0 ..^ M ) --> { A } -> ( ( 0 ..^ M ) X. { A } ) e. Word { A } )
23 17 21 22 3syl 
 |-  ( ph -> ( ( 0 ..^ M ) X. { A } ) e. Word { A } )
24 fconstg 
 |-  ( A e. S -> ( ( 0 ..^ N ) X. { A } ) : ( 0 ..^ N ) --> { A } )
25 iswrdi 
 |-  ( ( ( 0 ..^ N ) X. { A } ) : ( 0 ..^ N ) --> { A } -> ( ( 0 ..^ N ) X. { A } ) e. Word { A } )
26 17 24 25 3syl 
 |-  ( ph -> ( ( 0 ..^ N ) X. { A } ) e. Word { A } )
27 ccatvalfn 
 |-  ( ( ( ( 0 ..^ M ) X. { A } ) e. Word { A } /\ ( ( 0 ..^ N ) X. { A } ) e. Word { A } ) -> ( ( ( 0 ..^ M ) X. { A } ) ++ ( ( 0 ..^ N ) X. { A } ) ) Fn ( 0 ..^ ( ( # ` ( ( 0 ..^ M ) X. { A } ) ) + ( # ` ( ( 0 ..^ N ) X. { A } ) ) ) ) )
28 23 26 27 syl2anc 
 |-  ( ph -> ( ( ( 0 ..^ M ) X. { A } ) ++ ( ( 0 ..^ N ) X. { A } ) ) Fn ( 0 ..^ ( ( # ` ( ( 0 ..^ M ) X. { A } ) ) + ( # ` ( ( 0 ..^ N ) X. { A } ) ) ) ) )
29 fzofi 
 |-  ( 0 ..^ M ) e. Fin
30 snfi 
 |-  { A } e. Fin
31 hashxp 
 |-  ( ( ( 0 ..^ M ) e. Fin /\ { A } e. Fin ) -> ( # ` ( ( 0 ..^ M ) X. { A } ) ) = ( ( # ` ( 0 ..^ M ) ) x. ( # ` { A } ) ) )
32 29 30 31 mp2an 
 |-  ( # ` ( ( 0 ..^ M ) X. { A } ) ) = ( ( # ` ( 0 ..^ M ) ) x. ( # ` { A } ) )
33 hashsng 
 |-  ( A e. S -> ( # ` { A } ) = 1 )
34 17 33 syl 
 |-  ( ph -> ( # ` { A } ) = 1 )
35 34 oveq2d 
 |-  ( ph -> ( ( # ` ( 0 ..^ M ) ) x. ( # ` { A } ) ) = ( ( # ` ( 0 ..^ M ) ) x. 1 ) )
36 hashcl 
 |-  ( ( 0 ..^ M ) e. Fin -> ( # ` ( 0 ..^ M ) ) e. NN0 )
37 29 36 mp1i 
 |-  ( ph -> ( # ` ( 0 ..^ M ) ) e. NN0 )
38 37 nn0cnd 
 |-  ( ph -> ( # ` ( 0 ..^ M ) ) e. CC )
39 38 mulid1d 
 |-  ( ph -> ( ( # ` ( 0 ..^ M ) ) x. 1 ) = ( # ` ( 0 ..^ M ) ) )
40 hashfzo0 
 |-  ( M e. NN0 -> ( # ` ( 0 ..^ M ) ) = M )
41 9 40 syl 
 |-  ( ph -> ( # ` ( 0 ..^ M ) ) = M )
42 35 39 41 3eqtrd 
 |-  ( ph -> ( ( # ` ( 0 ..^ M ) ) x. ( # ` { A } ) ) = M )
43 32 42 syl5eq 
 |-  ( ph -> ( # ` ( ( 0 ..^ M ) X. { A } ) ) = M )
44 fzofi 
 |-  ( 0 ..^ N ) e. Fin
45 hashxp 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ { A } e. Fin ) -> ( # ` ( ( 0 ..^ N ) X. { A } ) ) = ( ( # ` ( 0 ..^ N ) ) x. ( # ` { A } ) ) )
46 44 30 45 mp2an 
 |-  ( # ` ( ( 0 ..^ N ) X. { A } ) ) = ( ( # ` ( 0 ..^ N ) ) x. ( # ` { A } ) )
47 34 oveq2d 
 |-  ( ph -> ( ( # ` ( 0 ..^ N ) ) x. ( # ` { A } ) ) = ( ( # ` ( 0 ..^ N ) ) x. 1 ) )
48 hashcl 
 |-  ( ( 0 ..^ N ) e. Fin -> ( # ` ( 0 ..^ N ) ) e. NN0 )
49 44 48 mp1i 
 |-  ( ph -> ( # ` ( 0 ..^ N ) ) e. NN0 )
50 49 nn0cnd 
 |-  ( ph -> ( # ` ( 0 ..^ N ) ) e. CC )
51 50 mulid1d 
 |-  ( ph -> ( ( # ` ( 0 ..^ N ) ) x. 1 ) = ( # ` ( 0 ..^ N ) ) )
52 hashfzo0 
 |-  ( N e. NN0 -> ( # ` ( 0 ..^ N ) ) = N )
53 10 52 syl 
 |-  ( ph -> ( # ` ( 0 ..^ N ) ) = N )
54 47 51 53 3eqtrd 
 |-  ( ph -> ( ( # ` ( 0 ..^ N ) ) x. ( # ` { A } ) ) = N )
55 46 54 syl5eq 
 |-  ( ph -> ( # ` ( ( 0 ..^ N ) X. { A } ) ) = N )
56 43 55 oveq12d 
 |-  ( ph -> ( ( # ` ( ( 0 ..^ M ) X. { A } ) ) + ( # ` ( ( 0 ..^ N ) X. { A } ) ) ) = ( M + N ) )
57 56 8 eqtrd 
 |-  ( ph -> ( ( # ` ( ( 0 ..^ M ) X. { A } ) ) + ( # ` ( ( 0 ..^ N ) X. { A } ) ) ) = L )
58 57 oveq2d 
 |-  ( ph -> ( 0 ..^ ( ( # ` ( ( 0 ..^ M ) X. { A } ) ) + ( # ` ( ( 0 ..^ N ) X. { A } ) ) ) ) = ( 0 ..^ L ) )
59 58 fneq2d 
 |-  ( ph -> ( ( ( ( 0 ..^ M ) X. { A } ) ++ ( ( 0 ..^ N ) X. { A } ) ) Fn ( 0 ..^ ( ( # ` ( ( 0 ..^ M ) X. { A } ) ) + ( # ` ( ( 0 ..^ N ) X. { A } ) ) ) ) <-> ( ( ( 0 ..^ M ) X. { A } ) ++ ( ( 0 ..^ N ) X. { A } ) ) Fn ( 0 ..^ L ) ) )
60 28 59 mpbid 
 |-  ( ph -> ( ( ( 0 ..^ M ) X. { A } ) ++ ( ( 0 ..^ N ) X. { A } ) ) Fn ( 0 ..^ L ) )
61 43 adantr 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> ( # ` ( ( 0 ..^ M ) X. { A } ) ) = M )
62 61 breq2d 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> ( x < ( # ` ( ( 0 ..^ M ) X. { A } ) ) <-> x < M ) )
63 62 ifbid 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> if ( x < ( # ` ( ( 0 ..^ M ) X. { A } ) ) , ( ( ( 0 ..^ M ) X. { A } ) ` x ) , ( ( ( 0 ..^ N ) X. { A } ) ` ( x - ( # ` ( ( 0 ..^ M ) X. { A } ) ) ) ) ) = if ( x < M , ( ( ( 0 ..^ M ) X. { A } ) ` x ) , ( ( ( 0 ..^ N ) X. { A } ) ` ( x - ( # ` ( ( 0 ..^ M ) X. { A } ) ) ) ) ) )
64 17 adantr 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> A e. S )
65 elfzouz 
 |-  ( x e. ( 0 ..^ L ) -> x e. ( ZZ>= ` 0 ) )
66 65 ad2antlr 
 |-  ( ( ( ph /\ x e. ( 0 ..^ L ) ) /\ x < M ) -> x e. ( ZZ>= ` 0 ) )
67 9 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 0 ..^ L ) ) /\ x < M ) -> M e. NN0 )
68 67 nn0zd 
 |-  ( ( ( ph /\ x e. ( 0 ..^ L ) ) /\ x < M ) -> M e. ZZ )
69 simpr 
 |-  ( ( ( ph /\ x e. ( 0 ..^ L ) ) /\ x < M ) -> x < M )
70 elfzo2 
 |-  ( x e. ( 0 ..^ M ) <-> ( x e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ x < M ) )
71 66 68 69 70 syl3anbrc 
 |-  ( ( ( ph /\ x e. ( 0 ..^ L ) ) /\ x < M ) -> x e. ( 0 ..^ M ) )
72 fvconst2g 
 |-  ( ( A e. S /\ x e. ( 0 ..^ M ) ) -> ( ( ( 0 ..^ M ) X. { A } ) ` x ) = A )
73 64 71 72 syl2an2r 
 |-  ( ( ( ph /\ x e. ( 0 ..^ L ) ) /\ x < M ) -> ( ( ( 0 ..^ M ) X. { A } ) ` x ) = A )
74 43 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 0 ..^ L ) ) /\ -. x < M ) -> ( # ` ( ( 0 ..^ M ) X. { A } ) ) = M )
75 74 oveq2d 
 |-  ( ( ( ph /\ x e. ( 0 ..^ L ) ) /\ -. x < M ) -> ( x - ( # ` ( ( 0 ..^ M ) X. { A } ) ) ) = ( x - M ) )
76 9 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 0 ..^ L ) ) /\ -. x < M ) -> M e. NN0 )
77 elfzonn0 
 |-  ( x e. ( 0 ..^ L ) -> x e. NN0 )
78 77 ad2antlr 
 |-  ( ( ( ph /\ x e. ( 0 ..^ L ) ) /\ -. x < M ) -> x e. NN0 )
79 9 adantr 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> M e. NN0 )
80 79 nn0red 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> M e. RR )
81 elfzoelz 
 |-  ( x e. ( 0 ..^ L ) -> x e. ZZ )
82 81 adantl 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> x e. ZZ )
83 82 zred 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> x e. RR )
84 80 83 lenltd 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> ( M <_ x <-> -. x < M ) )
85 84 biimpar 
 |-  ( ( ( ph /\ x e. ( 0 ..^ L ) ) /\ -. x < M ) -> M <_ x )
86 nn0sub2 
 |-  ( ( M e. NN0 /\ x e. NN0 /\ M <_ x ) -> ( x - M ) e. NN0 )
87 76 78 85 86 syl3anc 
 |-  ( ( ( ph /\ x e. ( 0 ..^ L ) ) /\ -. x < M ) -> ( x - M ) e. NN0 )
88 elnn0uz 
 |-  ( ( x - M ) e. NN0 <-> ( x - M ) e. ( ZZ>= ` 0 ) )
89 87 88 sylib 
 |-  ( ( ( ph /\ x e. ( 0 ..^ L ) ) /\ -. x < M ) -> ( x - M ) e. ( ZZ>= ` 0 ) )
90 10 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 0 ..^ L ) ) /\ -. x < M ) -> N e. NN0 )
91 90 nn0zd 
 |-  ( ( ( ph /\ x e. ( 0 ..^ L ) ) /\ -. x < M ) -> N e. ZZ )
92 elfzolt2 
 |-  ( x e. ( 0 ..^ L ) -> x < L )
93 92 adantl 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> x < L )
94 80 recnd 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> M e. CC )
95 83 recnd 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> x e. CC )
96 94 95 pncan3d 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> ( M + ( x - M ) ) = x )
97 8 adantr 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> ( M + N ) = L )
98 93 96 97 3brtr4d 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> ( M + ( x - M ) ) < ( M + N ) )
99 83 80 resubcld 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> ( x - M ) e. RR )
100 10 adantr 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> N e. NN0 )
101 100 nn0red 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> N e. RR )
102 99 101 80 ltadd2d 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> ( ( x - M ) < N <-> ( M + ( x - M ) ) < ( M + N ) ) )
103 98 102 mpbird 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> ( x - M ) < N )
104 103 adantr 
 |-  ( ( ( ph /\ x e. ( 0 ..^ L ) ) /\ -. x < M ) -> ( x - M ) < N )
105 elfzo2 
 |-  ( ( x - M ) e. ( 0 ..^ N ) <-> ( ( x - M ) e. ( ZZ>= ` 0 ) /\ N e. ZZ /\ ( x - M ) < N ) )
106 89 91 104 105 syl3anbrc 
 |-  ( ( ( ph /\ x e. ( 0 ..^ L ) ) /\ -. x < M ) -> ( x - M ) e. ( 0 ..^ N ) )
107 75 106 eqeltrd 
 |-  ( ( ( ph /\ x e. ( 0 ..^ L ) ) /\ -. x < M ) -> ( x - ( # ` ( ( 0 ..^ M ) X. { A } ) ) ) e. ( 0 ..^ N ) )
108 fvconst2g 
 |-  ( ( A e. S /\ ( x - ( # ` ( ( 0 ..^ M ) X. { A } ) ) ) e. ( 0 ..^ N ) ) -> ( ( ( 0 ..^ N ) X. { A } ) ` ( x - ( # ` ( ( 0 ..^ M ) X. { A } ) ) ) ) = A )
109 64 107 108 syl2an2r 
 |-  ( ( ( ph /\ x e. ( 0 ..^ L ) ) /\ -. x < M ) -> ( ( ( 0 ..^ N ) X. { A } ) ` ( x - ( # ` ( ( 0 ..^ M ) X. { A } ) ) ) ) = A )
110 73 109 ifeqda 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> if ( x < M , ( ( ( 0 ..^ M ) X. { A } ) ` x ) , ( ( ( 0 ..^ N ) X. { A } ) ` ( x - ( # ` ( ( 0 ..^ M ) X. { A } ) ) ) ) ) = A )
111 63 110 eqtr2d 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> A = if ( x < ( # ` ( ( 0 ..^ M ) X. { A } ) ) , ( ( ( 0 ..^ M ) X. { A } ) ` x ) , ( ( ( 0 ..^ N ) X. { A } ) ` ( x - ( # ` ( ( 0 ..^ M ) X. { A } ) ) ) ) ) )
112 fvconst2g 
 |-  ( ( A e. S /\ x e. ( 0 ..^ L ) ) -> ( ( ( 0 ..^ L ) X. { A } ) ` x ) = A )
113 17 112 sylan 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> ( ( ( 0 ..^ L ) X. { A } ) ` x ) = A )
114 64 21 22 3syl 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> ( ( 0 ..^ M ) X. { A } ) e. Word { A } )
115 64 24 25 3syl 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> ( ( 0 ..^ N ) X. { A } ) e. Word { A } )
116 ccatsymb 
 |-  ( ( ( ( 0 ..^ M ) X. { A } ) e. Word { A } /\ ( ( 0 ..^ N ) X. { A } ) e. Word { A } /\ x e. ZZ ) -> ( ( ( ( 0 ..^ M ) X. { A } ) ++ ( ( 0 ..^ N ) X. { A } ) ) ` x ) = if ( x < ( # ` ( ( 0 ..^ M ) X. { A } ) ) , ( ( ( 0 ..^ M ) X. { A } ) ` x ) , ( ( ( 0 ..^ N ) X. { A } ) ` ( x - ( # ` ( ( 0 ..^ M ) X. { A } ) ) ) ) ) )
117 114 115 82 116 syl3anc 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> ( ( ( ( 0 ..^ M ) X. { A } ) ++ ( ( 0 ..^ N ) X. { A } ) ) ` x ) = if ( x < ( # ` ( ( 0 ..^ M ) X. { A } ) ) , ( ( ( 0 ..^ M ) X. { A } ) ` x ) , ( ( ( 0 ..^ N ) X. { A } ) ` ( x - ( # ` ( ( 0 ..^ M ) X. { A } ) ) ) ) ) )
118 111 113 117 3eqtr4d 
 |-  ( ( ph /\ x e. ( 0 ..^ L ) ) -> ( ( ( 0 ..^ L ) X. { A } ) ` x ) = ( ( ( ( 0 ..^ M ) X. { A } ) ++ ( ( 0 ..^ N ) X. { A } ) ) ` x ) )
119 20 60 118 eqfnfvd 
 |-  ( ph -> ( ( 0 ..^ L ) X. { A } ) = ( ( ( 0 ..^ M ) X. { A } ) ++ ( ( 0 ..^ N ) X. { A } ) ) )
120 119 oveq1d 
 |-  ( ph -> ( ( ( 0 ..^ L ) X. { A } ) oF ( .r ` K ) ( U ++ V ) ) = ( ( ( ( 0 ..^ M ) X. { A } ) ++ ( ( 0 ..^ N ) X. { A } ) ) oF ( .r ` K ) ( U ++ V ) ) )
121 2 5 16 frlmfzowrd 
 |-  ( U e. C -> U e. Word S )
122 11 121 syl 
 |-  ( ph -> U e. Word S )
123 3 6 16 frlmfzowrd 
 |-  ( V e. D -> V e. Word S )
124 12 123 syl 
 |-  ( ph -> V e. Word S )
125 32 35 syl5eq 
 |-  ( ph -> ( # ` ( ( 0 ..^ M ) X. { A } ) ) = ( ( # ` ( 0 ..^ M ) ) x. 1 ) )
126 ovexd 
 |-  ( ph -> ( 0 ..^ M ) e. _V )
127 2 16 5 frlmbasf 
 |-  ( ( ( 0 ..^ M ) e. _V /\ U e. C ) -> U : ( 0 ..^ M ) --> S )
128 126 11 127 syl2anc 
 |-  ( ph -> U : ( 0 ..^ M ) --> S )
129 128 ffnd 
 |-  ( ph -> U Fn ( 0 ..^ M ) )
130 hashfn 
 |-  ( U Fn ( 0 ..^ M ) -> ( # ` U ) = ( # ` ( 0 ..^ M ) ) )
131 129 130 syl 
 |-  ( ph -> ( # ` U ) = ( # ` ( 0 ..^ M ) ) )
132 39 125 131 3eqtr4d 
 |-  ( ph -> ( # ` ( ( 0 ..^ M ) X. { A } ) ) = ( # ` U ) )
133 47 51 eqtrd 
 |-  ( ph -> ( ( # ` ( 0 ..^ N ) ) x. ( # ` { A } ) ) = ( # ` ( 0 ..^ N ) ) )
134 46 133 syl5eq 
 |-  ( ph -> ( # ` ( ( 0 ..^ N ) X. { A } ) ) = ( # ` ( 0 ..^ N ) ) )
135 ovexd 
 |-  ( ph -> ( 0 ..^ N ) e. _V )
136 3 16 6 frlmbasf 
 |-  ( ( ( 0 ..^ N ) e. _V /\ V e. D ) -> V : ( 0 ..^ N ) --> S )
137 135 12 136 syl2anc 
 |-  ( ph -> V : ( 0 ..^ N ) --> S )
138 137 ffnd 
 |-  ( ph -> V Fn ( 0 ..^ N ) )
139 hashfn 
 |-  ( V Fn ( 0 ..^ N ) -> ( # ` V ) = ( # ` ( 0 ..^ N ) ) )
140 138 139 syl 
 |-  ( ph -> ( # ` V ) = ( # ` ( 0 ..^ N ) ) )
141 134 140 eqtr4d 
 |-  ( ph -> ( # ` ( ( 0 ..^ N ) X. { A } ) ) = ( # ` V ) )
142 23 26 122 124 132 141 ofccat 
 |-  ( ph -> ( ( ( ( 0 ..^ M ) X. { A } ) ++ ( ( 0 ..^ N ) X. { A } ) ) oF ( .r ` K ) ( U ++ V ) ) = ( ( ( ( 0 ..^ M ) X. { A } ) oF ( .r ` K ) U ) ++ ( ( ( 0 ..^ N ) X. { A } ) oF ( .r ` K ) V ) ) )
143 120 142 eqtrd 
 |-  ( ph -> ( ( ( 0 ..^ L ) X. { A } ) oF ( .r ` K ) ( U ++ V ) ) = ( ( ( ( 0 ..^ M ) X. { A } ) oF ( .r ` K ) U ) ++ ( ( ( 0 ..^ N ) X. { A } ) oF ( .r ` K ) V ) ) )
144 ovexd 
 |-  ( ph -> ( 0 ..^ L ) e. _V )
145 1 2 3 4 5 6 7 8 9 10 11 12 frlmfzoccat 
 |-  ( ph -> ( U ++ V ) e. B )
146 eqid 
 |-  ( .r ` K ) = ( .r ` K )
147 1 4 16 144 17 145 13 146 frlmvscafval 
 |-  ( ph -> ( A O ( U ++ V ) ) = ( ( ( 0 ..^ L ) X. { A } ) oF ( .r ` K ) ( U ++ V ) ) )
148 2 5 16 126 17 11 14 146 frlmvscafval 
 |-  ( ph -> ( A .xb U ) = ( ( ( 0 ..^ M ) X. { A } ) oF ( .r ` K ) U ) )
149 3 6 16 135 17 12 15 146 frlmvscafval 
 |-  ( ph -> ( A .x. V ) = ( ( ( 0 ..^ N ) X. { A } ) oF ( .r ` K ) V ) )
150 148 149 oveq12d 
 |-  ( ph -> ( ( A .xb U ) ++ ( A .x. V ) ) = ( ( ( ( 0 ..^ M ) X. { A } ) oF ( .r ` K ) U ) ++ ( ( ( 0 ..^ N ) X. { A } ) oF ( .r ` K ) V ) ) )
151 143 147 150 3eqtr4d 
 |-  ( ph -> ( A O ( U ++ V ) ) = ( ( A .xb U ) ++ ( A .x. V ) ) )