Metamath Proof Explorer

Theorem frlmvscadiccat

Description: Scalar multiplication distributes over concatenation. (Contributed by SN, 6-Sep-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 ⊢ ( 𝜑 → 𝑉 ∈ 𝐷 )
frlmvscadiccat.o ⊢ 𝑂 = ( ·𝑠 ‘ 𝑊 )
frlmvscadiccat.p ⊢ ∙ = ( ·𝑠 ‘ 𝑋 )
frlmvscadiccat.q ⊢ · = ( ·𝑠 ‘ 𝑌 )
frlmvscadiccat.s ⊢ 𝑆 = ( Base ‘ 𝐾 )
frlmvscadiccat.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
Assertion frlmvscadiccat ( 𝜑 → ( 𝐴 𝑂 ( 𝑈 ++ 𝑉 ) ) = ( ( 𝐴 ∙ 𝑈 ) ++ ( 𝐴 · 𝑉 ) ) )

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 frlmvscadiccat.o ⊢ 𝑂 = ( ·𝑠 ‘ 𝑊 )
14 frlmvscadiccat.p ⊢ ∙ = ( ·𝑠 ‘ 𝑋 )
15 frlmvscadiccat.q ⊢ · = ( ·𝑠 ‘ 𝑌 )
16 frlmvscadiccat.s ⊢ 𝑆 = ( Base ‘ 𝐾 )
17 frlmvscadiccat.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
18 fconstg ⊢ ( 𝐴 ∈ 𝑆 → ( ( 0 ..^ 𝐿 ) × { 𝐴 } ) : ( 0 ..^ 𝐿 ) ⟶ { 𝐴 } )
19 17 18 syl ⊢ ( 𝜑 → ( ( 0 ..^ 𝐿 ) × { 𝐴 } ) : ( 0 ..^ 𝐿 ) ⟶ { 𝐴 } )
20 19 ffnd ⊢ ( 𝜑 → ( ( 0 ..^ 𝐿 ) × { 𝐴 } ) Fn ( 0 ..^ 𝐿 ) )
21 fconstg ⊢ ( 𝐴 ∈ 𝑆 → ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) : ( 0 ..^ 𝑀 ) ⟶ { 𝐴 } )
22 iswrdi ⊢ ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) : ( 0 ..^ 𝑀 ) ⟶ { 𝐴 } → ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ∈ Word { 𝐴 } )
23 17 21 22 3syl ⊢ ( 𝜑 → ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ∈ Word { 𝐴 } )
24 fconstg ⊢ ( 𝐴 ∈ 𝑆 → ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) : ( 0 ..^ 𝑁 ) ⟶ { 𝐴 } )
25 iswrdi ⊢ ( ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) : ( 0 ..^ 𝑁 ) ⟶ { 𝐴 } → ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ∈ Word { 𝐴 } )
26 17 24 25 3syl ⊢ ( 𝜑 → ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ∈ Word { 𝐴 } )
27 ccatvalfn ⊢ ( ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ∈ Word { 𝐴 } ∧ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ∈ Word { 𝐴 } ) → ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ++ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ) Fn ( 0 ..^ ( ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) + ( ♯ ‘ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ) ) ) )
28 23 26 27 syl2anc ⊢ ( 𝜑 → ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ++ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ) Fn ( 0 ..^ ( ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) + ( ♯ ‘ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ) ) ) )
29 fzofi ⊢ ( 0 ..^ 𝑀 ) ∈ Fin
30 snfi ⊢ { 𝐴 } ∈ Fin
31 hashxp ⊢ ( ( ( 0 ..^ 𝑀 ) ∈ Fin ∧ { 𝐴 } ∈ Fin ) → ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) = ( ( ♯ ‘ ( 0 ..^ 𝑀 ) ) · ( ♯ ‘ { 𝐴 } ) ) )
32 29 30 31 mp2an ⊢ ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) = ( ( ♯ ‘ ( 0 ..^ 𝑀 ) ) · ( ♯ ‘ { 𝐴 } ) )
33 hashsng ⊢ ( 𝐴 ∈ 𝑆 → ( ♯ ‘ { 𝐴 } ) = 1 )
34 17 33 syl ⊢ ( 𝜑 → ( ♯ ‘ { 𝐴 } ) = 1 )
35 34 oveq2d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ..^ 𝑀 ) ) · ( ♯ ‘ { 𝐴 } ) ) = ( ( ♯ ‘ ( 0 ..^ 𝑀 ) ) · 1 ) )
36 hashcl ⊢ ( ( 0 ..^ 𝑀 ) ∈ Fin → ( ♯ ‘ ( 0 ..^ 𝑀 ) ) ∈ ℕ0 )
37 29 36 mp1i ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ 𝑀 ) ) ∈ ℕ0 )
38 37 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ 𝑀 ) ) ∈ ℂ )
39 38 mulid1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ..^ 𝑀 ) ) · 1 ) = ( ♯ ‘ ( 0 ..^ 𝑀 ) ) )
40 hashfzo0 ⊢ ( 𝑀 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝑀 ) ) = 𝑀 )
41 9 40 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ 𝑀 ) ) = 𝑀 )
42 35 39 41 3eqtrd ⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ..^ 𝑀 ) ) · ( ♯ ‘ { 𝐴 } ) ) = 𝑀 )
43 32 42 syl5eq ⊢ ( 𝜑 → ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) = 𝑀 )
44 fzofi ⊢ ( 0 ..^ 𝑁 ) ∈ Fin
45 hashxp ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ { 𝐴 } ∈ Fin ) → ( ♯ ‘ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ) = ( ( ♯ ‘ ( 0 ..^ 𝑁 ) ) · ( ♯ ‘ { 𝐴 } ) ) )
46 44 30 45 mp2an ⊢ ( ♯ ‘ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ) = ( ( ♯ ‘ ( 0 ..^ 𝑁 ) ) · ( ♯ ‘ { 𝐴 } ) )
47 34 oveq2d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ..^ 𝑁 ) ) · ( ♯ ‘ { 𝐴 } ) ) = ( ( ♯ ‘ ( 0 ..^ 𝑁 ) ) · 1 ) )
48 hashcl ⊢ ( ( 0 ..^ 𝑁 ) ∈ Fin → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) ∈ ℕ0 )
49 44 48 mp1i ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) ∈ ℕ0 )
50 49 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) ∈ ℂ )
51 50 mulid1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ..^ 𝑁 ) ) · 1 ) = ( ♯ ‘ ( 0 ..^ 𝑁 ) ) )
52 hashfzo0 ⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
53 10 52 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
54 47 51 53 3eqtrd ⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ..^ 𝑁 ) ) · ( ♯ ‘ { 𝐴 } ) ) = 𝑁 )
55 46 54 syl5eq ⊢ ( 𝜑 → ( ♯ ‘ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ) = 𝑁 )
56 43 55 oveq12d ⊢ ( 𝜑 → ( ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) + ( ♯ ‘ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ) ) = ( 𝑀 + 𝑁 ) )
57 56 8 eqtrd ⊢ ( 𝜑 → ( ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) + ( ♯ ‘ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ) ) = 𝐿 )
58 57 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) + ( ♯ ‘ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ) ) ) = ( 0 ..^ 𝐿 ) )
59 58 fneq2d ⊢ ( 𝜑 → ( ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ++ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ) Fn ( 0 ..^ ( ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) + ( ♯ ‘ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ) ) ) ↔ ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ++ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ) Fn ( 0 ..^ 𝐿 ) ) )
60 28 59 mpbid ⊢ ( 𝜑 → ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ++ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ) Fn ( 0 ..^ 𝐿 ) )
61 43 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) = 𝑀 )
62 61 breq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → ( 𝑥 < ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) ↔ 𝑥 < 𝑀 ) )
63 62 ifbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → if ( 𝑥 < ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) , ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ‘ 𝑥 ) , ( ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ‘ ( 𝑥 − ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) ) ) ) = if ( 𝑥 < 𝑀 , ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ‘ 𝑥 ) , ( ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ‘ ( 𝑥 − ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) ) ) ) )
64 17 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → 𝐴 ∈ 𝑆 )
65 elfzouz ⊢ ( 𝑥 ∈ ( 0 ..^ 𝐿 ) → 𝑥 ∈ ( ℤ≥ ‘ 0 ) )
66 65 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) ∧ 𝑥 < 𝑀 ) → 𝑥 ∈ ( ℤ≥ ‘ 0 ) )
67 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) ∧ 𝑥 < 𝑀 ) → 𝑀 ∈ ℕ0 )
68 67 nn0zd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) ∧ 𝑥 < 𝑀 ) → 𝑀 ∈ ℤ )
69 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) ∧ 𝑥 < 𝑀 ) → 𝑥 < 𝑀 )
70 elfzo2 ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑀 ) ↔ ( 𝑥 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) )
71 66 68 69 70 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) ∧ 𝑥 < 𝑀 ) → 𝑥 ∈ ( 0 ..^ 𝑀 ) )
72 fvconst2g ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑥 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ‘ 𝑥 ) = 𝐴 )
73 64 71 72 syl2an2r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) ∧ 𝑥 < 𝑀 ) → ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ‘ 𝑥 ) = 𝐴 )
74 43 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) ∧ ¬ 𝑥 < 𝑀 ) → ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) = 𝑀 )
75 74 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) ∧ ¬ 𝑥 < 𝑀 ) → ( 𝑥 − ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) ) = ( 𝑥 − 𝑀 ) )
76 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑀 ∈ ℕ0 )
77 elfzonn0 ⊢ ( 𝑥 ∈ ( 0 ..^ 𝐿 ) → 𝑥 ∈ ℕ0 )
78 77 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑥 ∈ ℕ0 )
79 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → 𝑀 ∈ ℕ0 )
80 79 nn0red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → 𝑀 ∈ ℝ )
81 elfzoelz ⊢ ( 𝑥 ∈ ( 0 ..^ 𝐿 ) → 𝑥 ∈ ℤ )
82 81 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → 𝑥 ∈ ℤ )
83 82 zred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → 𝑥 ∈ ℝ )
84 80 83 lenltd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → ( 𝑀 ≤ 𝑥 ↔ ¬ 𝑥 < 𝑀 ) )
85 84 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑀 ≤ 𝑥 )
86 nn0sub2 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑥 ∈ ℕ0 ∧ 𝑀 ≤ 𝑥 ) → ( 𝑥 − 𝑀 ) ∈ ℕ0 )
87 76 78 85 86 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) ∧ ¬ 𝑥 < 𝑀 ) → ( 𝑥 − 𝑀 ) ∈ ℕ0 )
88 elnn0uz ⊢ ( ( 𝑥 − 𝑀 ) ∈ ℕ0 ↔ ( 𝑥 − 𝑀 ) ∈ ( ℤ≥ ‘ 0 ) )
89 87 88 sylib ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) ∧ ¬ 𝑥 < 𝑀 ) → ( 𝑥 − 𝑀 ) ∈ ( ℤ≥ ‘ 0 ) )
90 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑁 ∈ ℕ0 )
91 90 nn0zd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑁 ∈ ℤ )
92 elfzolt2 ⊢ ( 𝑥 ∈ ( 0 ..^ 𝐿 ) → 𝑥 < 𝐿 )
93 92 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → 𝑥 < 𝐿 )
94 80 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → 𝑀 ∈ ℂ )
95 83 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → 𝑥 ∈ ℂ )
96 94 95 pncan3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → ( 𝑀 + ( 𝑥 − 𝑀 ) ) = 𝑥 )
97 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → ( 𝑀 + 𝑁 ) = 𝐿 )
98 93 96 97 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → ( 𝑀 + ( 𝑥 − 𝑀 ) ) < ( 𝑀 + 𝑁 ) )
99 83 80 resubcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → ( 𝑥 − 𝑀 ) ∈ ℝ )
100 10 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → 𝑁 ∈ ℕ0 )
101 100 nn0red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → 𝑁 ∈ ℝ )
102 99 101 80 ltadd2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → ( ( 𝑥 − 𝑀 ) < 𝑁 ↔ ( 𝑀 + ( 𝑥 − 𝑀 ) ) < ( 𝑀 + 𝑁 ) ) )
103 98 102 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → ( 𝑥 − 𝑀 ) < 𝑁 )
104 103 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) ∧ ¬ 𝑥 < 𝑀 ) → ( 𝑥 − 𝑀 ) < 𝑁 )
105 elfzo2 ⊢ ( ( 𝑥 − 𝑀 ) ∈ ( 0 ..^ 𝑁 ) ↔ ( ( 𝑥 − 𝑀 ) ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝑥 − 𝑀 ) < 𝑁 ) )
106 89 91 104 105 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) ∧ ¬ 𝑥 < 𝑀 ) → ( 𝑥 − 𝑀 ) ∈ ( 0 ..^ 𝑁 ) )
107 75 106 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) ∧ ¬ 𝑥 < 𝑀 ) → ( 𝑥 − ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) ) ∈ ( 0 ..^ 𝑁 ) )
108 fvconst2g ⊢ ( ( 𝐴 ∈ 𝑆 ∧ ( 𝑥 − ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) ) ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ‘ ( 𝑥 − ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) ) ) = 𝐴 )
109 64 107 108 syl2an2r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) ∧ ¬ 𝑥 < 𝑀 ) → ( ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ‘ ( 𝑥 − ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) ) ) = 𝐴 )
110 73 109 ifeqda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → if ( 𝑥 < 𝑀 , ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ‘ 𝑥 ) , ( ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ‘ ( 𝑥 − ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) ) ) ) = 𝐴 )
111 63 110 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → 𝐴 = if ( 𝑥 < ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) , ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ‘ 𝑥 ) , ( ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ‘ ( 𝑥 − ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) ) ) ) )
112 fvconst2g ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → ( ( ( 0 ..^ 𝐿 ) × { 𝐴 } ) ‘ 𝑥 ) = 𝐴 )
113 17 112 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → ( ( ( 0 ..^ 𝐿 ) × { 𝐴 } ) ‘ 𝑥 ) = 𝐴 )
114 64 21 22 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ∈ Word { 𝐴 } )
115 64 24 25 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ∈ Word { 𝐴 } )
116 ccatsymb ⊢ ( ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ∈ Word { 𝐴 } ∧ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ∈ Word { 𝐴 } ∧ 𝑥 ∈ ℤ ) → ( ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ++ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ) ‘ 𝑥 ) = if ( 𝑥 < ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) , ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ‘ 𝑥 ) , ( ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ‘ ( 𝑥 − ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) ) ) ) )
117 114 115 82 116 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → ( ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ++ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ) ‘ 𝑥 ) = if ( 𝑥 < ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) , ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ‘ 𝑥 ) , ( ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ‘ ( 𝑥 − ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) ) ) ) )
118 111 113 117 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ 𝐿 ) ) → ( ( ( 0 ..^ 𝐿 ) × { 𝐴 } ) ‘ 𝑥 ) = ( ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ++ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ) ‘ 𝑥 ) )
119 20 60 118 eqfnfvd ⊢ ( 𝜑 → ( ( 0 ..^ 𝐿 ) × { 𝐴 } ) = ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ++ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ) )
120 119 oveq1d ⊢ ( 𝜑 → ( ( ( 0 ..^ 𝐿 ) × { 𝐴 } ) ∘f ( .r ‘ 𝐾 ) ( 𝑈 ++ 𝑉 ) ) = ( ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ++ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ) ∘f ( .r ‘ 𝐾 ) ( 𝑈 ++ 𝑉 ) ) )
121 2 5 16 frlmfzowrd ⊢ ( 𝑈 ∈ 𝐶 → 𝑈 ∈ Word 𝑆 )
122 11 121 syl ⊢ ( 𝜑 → 𝑈 ∈ Word 𝑆 )
123 3 6 16 frlmfzowrd ⊢ ( 𝑉 ∈ 𝐷 → 𝑉 ∈ Word 𝑆 )
124 12 123 syl ⊢ ( 𝜑 → 𝑉 ∈ Word 𝑆 )
125 32 35 syl5eq ⊢ ( 𝜑 → ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) = ( ( ♯ ‘ ( 0 ..^ 𝑀 ) ) · 1 ) )
126 ovexd ⊢ ( 𝜑 → ( 0 ..^ 𝑀 ) ∈ V )
127 2 16 5 frlmbasf ⊢ ( ( ( 0 ..^ 𝑀 ) ∈ V ∧ 𝑈 ∈ 𝐶 ) → 𝑈 : ( 0 ..^ 𝑀 ) ⟶ 𝑆 )
128 126 11 127 syl2anc ⊢ ( 𝜑 → 𝑈 : ( 0 ..^ 𝑀 ) ⟶ 𝑆 )
129 128 ffnd ⊢ ( 𝜑 → 𝑈 Fn ( 0 ..^ 𝑀 ) )
130 hashfn ⊢ ( 𝑈 Fn ( 0 ..^ 𝑀 ) → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ ( 0 ..^ 𝑀 ) ) )
131 129 130 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ ( 0 ..^ 𝑀 ) ) )
132 39 125 131 3eqtr4d ⊢ ( 𝜑 → ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ) = ( ♯ ‘ 𝑈 ) )
133 47 51 eqtrd ⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ..^ 𝑁 ) ) · ( ♯ ‘ { 𝐴 } ) ) = ( ♯ ‘ ( 0 ..^ 𝑁 ) ) )
134 46 133 syl5eq ⊢ ( 𝜑 → ( ♯ ‘ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ) = ( ♯ ‘ ( 0 ..^ 𝑁 ) ) )
135 ovexd ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ∈ V )
136 3 16 6 frlmbasf ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ V ∧ 𝑉 ∈ 𝐷 ) → 𝑉 : ( 0 ..^ 𝑁 ) ⟶ 𝑆 )
137 135 12 136 syl2anc ⊢ ( 𝜑 → 𝑉 : ( 0 ..^ 𝑁 ) ⟶ 𝑆 )
138 137 ffnd ⊢ ( 𝜑 → 𝑉 Fn ( 0 ..^ 𝑁 ) )
139 hashfn ⊢ ( 𝑉 Fn ( 0 ..^ 𝑁 ) → ( ♯ ‘ 𝑉 ) = ( ♯ ‘ ( 0 ..^ 𝑁 ) ) )
140 138 139 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑉 ) = ( ♯ ‘ ( 0 ..^ 𝑁 ) ) )
141 134 140 eqtr4d ⊢ ( 𝜑 → ( ♯ ‘ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ) = ( ♯ ‘ 𝑉 ) )
142 23 26 122 124 132 141 ofccat ⊢ ( 𝜑 → ( ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ++ ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ) ∘f ( .r ‘ 𝐾 ) ( 𝑈 ++ 𝑉 ) ) = ( ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ∘f ( .r ‘ 𝐾 ) 𝑈 ) ++ ( ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ∘f ( .r ‘ 𝐾 ) 𝑉 ) ) )
143 120 142 eqtrd ⊢ ( 𝜑 → ( ( ( 0 ..^ 𝐿 ) × { 𝐴 } ) ∘f ( .r ‘ 𝐾 ) ( 𝑈 ++ 𝑉 ) ) = ( ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ∘f ( .r ‘ 𝐾 ) 𝑈 ) ++ ( ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ∘f ( .r ‘ 𝐾 ) 𝑉 ) ) )
144 ovexd ⊢ ( 𝜑 → ( 0 ..^ 𝐿 ) ∈ V )
145 1 2 3 4 5 6 7 8 9 10 11 12 frlmfzoccat ⊢ ( 𝜑 → ( 𝑈 ++ 𝑉 ) ∈ 𝐵 )
146 eqid ⊢ ( .r ‘ 𝐾 ) = ( .r ‘ 𝐾 )
147 1 4 16 144 17 145 13 146 frlmvscafval ⊢ ( 𝜑 → ( 𝐴 𝑂 ( 𝑈 ++ 𝑉 ) ) = ( ( ( 0 ..^ 𝐿 ) × { 𝐴 } ) ∘f ( .r ‘ 𝐾 ) ( 𝑈 ++ 𝑉 ) ) )
148 2 5 16 126 17 11 14 146 frlmvscafval ⊢ ( 𝜑 → ( 𝐴 ∙ 𝑈 ) = ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ∘f ( .r ‘ 𝐾 ) 𝑈 ) )
149 3 6 16 135 17 12 15 146 frlmvscafval ⊢ ( 𝜑 → ( 𝐴 · 𝑉 ) = ( ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ∘f ( .r ‘ 𝐾 ) 𝑉 ) )
150 148 149 oveq12d ⊢ ( 𝜑 → ( ( 𝐴 ∙ 𝑈 ) ++ ( 𝐴 · 𝑉 ) ) = ( ( ( ( 0 ..^ 𝑀 ) × { 𝐴 } ) ∘f ( .r ‘ 𝐾 ) 𝑈 ) ++ ( ( ( 0 ..^ 𝑁 ) × { 𝐴 } ) ∘f ( .r ‘ 𝐾 ) 𝑉 ) ) )
151 143 147 150 3eqtr4d ⊢ ( 𝜑 → ( 𝐴 𝑂 ( 𝑈 ++ 𝑉 ) ) = ( ( 𝐴 ∙ 𝑈 ) ++ ( 𝐴 · 𝑉 ) ) )