| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | frlmvscadiccat.a | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑆) | 
| 2 |  | fconstg 6795 | . . . . . . 7
⊢ (𝐴 ∈ 𝑆 → ((0..^𝐿) × {𝐴}):(0..^𝐿)⟶{𝐴}) | 
| 3 | 1, 2 | syl 17 | . . . . . 6
⊢ (𝜑 → ((0..^𝐿) × {𝐴}):(0..^𝐿)⟶{𝐴}) | 
| 4 | 3 | ffnd 6737 | . . . . 5
⊢ (𝜑 → ((0..^𝐿) × {𝐴}) Fn (0..^𝐿)) | 
| 5 |  | fconstg 6795 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑆 → ((0..^𝑀) × {𝐴}):(0..^𝑀)⟶{𝐴}) | 
| 6 |  | iswrdi 14556 | . . . . . . . 8
⊢
(((0..^𝑀) ×
{𝐴}):(0..^𝑀)⟶{𝐴} → ((0..^𝑀) × {𝐴}) ∈ Word {𝐴}) | 
| 7 | 1, 5, 6 | 3syl 18 | . . . . . . 7
⊢ (𝜑 → ((0..^𝑀) × {𝐴}) ∈ Word {𝐴}) | 
| 8 |  | fconstg 6795 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑆 → ((0..^𝑁) × {𝐴}):(0..^𝑁)⟶{𝐴}) | 
| 9 |  | iswrdi 14556 | . . . . . . . 8
⊢
(((0..^𝑁) ×
{𝐴}):(0..^𝑁)⟶{𝐴} → ((0..^𝑁) × {𝐴}) ∈ Word {𝐴}) | 
| 10 | 1, 8, 9 | 3syl 18 | . . . . . . 7
⊢ (𝜑 → ((0..^𝑁) × {𝐴}) ∈ Word {𝐴}) | 
| 11 |  | ccatvalfn 14619 | . . . . . . 7
⊢
((((0..^𝑀) ×
{𝐴}) ∈ Word {𝐴} ∧ ((0..^𝑁) × {𝐴}) ∈ Word {𝐴}) → (((0..^𝑀) × {𝐴}) ++ ((0..^𝑁) × {𝐴})) Fn (0..^((♯‘((0..^𝑀) × {𝐴})) + (♯‘((0..^𝑁) × {𝐴}))))) | 
| 12 | 7, 10, 11 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (((0..^𝑀) × {𝐴}) ++ ((0..^𝑁) × {𝐴})) Fn (0..^((♯‘((0..^𝑀) × {𝐴})) + (♯‘((0..^𝑁) × {𝐴}))))) | 
| 13 |  | fzofi 14015 | . . . . . . . . . . . 12
⊢
(0..^𝑀) ∈
Fin | 
| 14 |  | snfi 9083 | . . . . . . . . . . . 12
⊢ {𝐴} ∈ Fin | 
| 15 |  | hashxp 14473 | . . . . . . . . . . . 12
⊢
(((0..^𝑀) ∈ Fin
∧ {𝐴} ∈ Fin)
→ (♯‘((0..^𝑀) × {𝐴})) = ((♯‘(0..^𝑀)) · (♯‘{𝐴}))) | 
| 16 | 13, 14, 15 | mp2an 692 | . . . . . . . . . . 11
⊢
(♯‘((0..^𝑀) × {𝐴})) = ((♯‘(0..^𝑀)) · (♯‘{𝐴})) | 
| 17 |  | hashsng 14408 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑆 → (♯‘{𝐴}) = 1) | 
| 18 | 1, 17 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘{𝐴}) = 1) | 
| 19 | 18 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (𝜑 → ((♯‘(0..^𝑀)) ·
(♯‘{𝐴})) =
((♯‘(0..^𝑀))
· 1)) | 
| 20 |  | hashcl 14395 | . . . . . . . . . . . . . . 15
⊢
((0..^𝑀) ∈ Fin
→ (♯‘(0..^𝑀)) ∈
ℕ0) | 
| 21 | 13, 20 | mp1i 13 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (♯‘(0..^𝑀)) ∈
ℕ0) | 
| 22 | 21 | nn0cnd 12589 | . . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘(0..^𝑀)) ∈
ℂ) | 
| 23 | 22 | mulridd 11278 | . . . . . . . . . . . 12
⊢ (𝜑 → ((♯‘(0..^𝑀)) · 1) =
(♯‘(0..^𝑀))) | 
| 24 |  | frlmfzoccat.m | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈
ℕ0) | 
| 25 |  | hashfzo0 14469 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ0
→ (♯‘(0..^𝑀)) = 𝑀) | 
| 26 | 24, 25 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (♯‘(0..^𝑀)) = 𝑀) | 
| 27 | 19, 23, 26 | 3eqtrd 2781 | . . . . . . . . . . 11
⊢ (𝜑 → ((♯‘(0..^𝑀)) ·
(♯‘{𝐴})) =
𝑀) | 
| 28 | 16, 27 | eqtrid 2789 | . . . . . . . . . 10
⊢ (𝜑 → (♯‘((0..^𝑀) × {𝐴})) = 𝑀) | 
| 29 |  | fzofi 14015 | . . . . . . . . . . . 12
⊢
(0..^𝑁) ∈
Fin | 
| 30 |  | hashxp 14473 | . . . . . . . . . . . 12
⊢
(((0..^𝑁) ∈ Fin
∧ {𝐴} ∈ Fin)
→ (♯‘((0..^𝑁) × {𝐴})) = ((♯‘(0..^𝑁)) · (♯‘{𝐴}))) | 
| 31 | 29, 14, 30 | mp2an 692 | . . . . . . . . . . 11
⊢
(♯‘((0..^𝑁) × {𝐴})) = ((♯‘(0..^𝑁)) · (♯‘{𝐴})) | 
| 32 | 18 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (𝜑 → ((♯‘(0..^𝑁)) ·
(♯‘{𝐴})) =
((♯‘(0..^𝑁))
· 1)) | 
| 33 |  | hashcl 14395 | . . . . . . . . . . . . . . 15
⊢
((0..^𝑁) ∈ Fin
→ (♯‘(0..^𝑁)) ∈
ℕ0) | 
| 34 | 29, 33 | mp1i 13 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (♯‘(0..^𝑁)) ∈
ℕ0) | 
| 35 | 34 | nn0cnd 12589 | . . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘(0..^𝑁)) ∈
ℂ) | 
| 36 | 35 | mulridd 11278 | . . . . . . . . . . . 12
⊢ (𝜑 → ((♯‘(0..^𝑁)) · 1) =
(♯‘(0..^𝑁))) | 
| 37 |  | frlmfzoccat.n | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 38 |  | hashfzo0 14469 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ (♯‘(0..^𝑁)) = 𝑁) | 
| 39 | 37, 38 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (♯‘(0..^𝑁)) = 𝑁) | 
| 40 | 32, 36, 39 | 3eqtrd 2781 | . . . . . . . . . . 11
⊢ (𝜑 → ((♯‘(0..^𝑁)) ·
(♯‘{𝐴})) =
𝑁) | 
| 41 | 31, 40 | eqtrid 2789 | . . . . . . . . . 10
⊢ (𝜑 → (♯‘((0..^𝑁) × {𝐴})) = 𝑁) | 
| 42 | 28, 41 | oveq12d 7449 | . . . . . . . . 9
⊢ (𝜑 →
((♯‘((0..^𝑀)
× {𝐴})) +
(♯‘((0..^𝑁)
× {𝐴}))) = (𝑀 + 𝑁)) | 
| 43 |  | frlmfzoccat.l | . . . . . . . . 9
⊢ (𝜑 → (𝑀 + 𝑁) = 𝐿) | 
| 44 | 42, 43 | eqtrd 2777 | . . . . . . . 8
⊢ (𝜑 →
((♯‘((0..^𝑀)
× {𝐴})) +
(♯‘((0..^𝑁)
× {𝐴}))) = 𝐿) | 
| 45 | 44 | oveq2d 7447 | . . . . . . 7
⊢ (𝜑 →
(0..^((♯‘((0..^𝑀) × {𝐴})) + (♯‘((0..^𝑁) × {𝐴})))) = (0..^𝐿)) | 
| 46 | 45 | fneq2d 6662 | . . . . . 6
⊢ (𝜑 → ((((0..^𝑀) × {𝐴}) ++ ((0..^𝑁) × {𝐴})) Fn (0..^((♯‘((0..^𝑀) × {𝐴})) + (♯‘((0..^𝑁) × {𝐴})))) ↔ (((0..^𝑀) × {𝐴}) ++ ((0..^𝑁) × {𝐴})) Fn (0..^𝐿))) | 
| 47 | 12, 46 | mpbid 232 | . . . . 5
⊢ (𝜑 → (((0..^𝑀) × {𝐴}) ++ ((0..^𝑁) × {𝐴})) Fn (0..^𝐿)) | 
| 48 | 28 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → (♯‘((0..^𝑀) × {𝐴})) = 𝑀) | 
| 49 | 48 | breq2d 5155 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → (𝑥 < (♯‘((0..^𝑀) × {𝐴})) ↔ 𝑥 < 𝑀)) | 
| 50 | 49 | ifbid 4549 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → if(𝑥 < (♯‘((0..^𝑀) × {𝐴})), (((0..^𝑀) × {𝐴})‘𝑥), (((0..^𝑁) × {𝐴})‘(𝑥 − (♯‘((0..^𝑀) × {𝐴}))))) = if(𝑥 < 𝑀, (((0..^𝑀) × {𝐴})‘𝑥), (((0..^𝑁) × {𝐴})‘(𝑥 − (♯‘((0..^𝑀) × {𝐴})))))) | 
| 51 | 1 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → 𝐴 ∈ 𝑆) | 
| 52 |  | elfzouz 13703 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (0..^𝐿) → 𝑥 ∈
(ℤ≥‘0)) | 
| 53 | 52 | ad2antlr 727 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) ∧ 𝑥 < 𝑀) → 𝑥 ∈
(ℤ≥‘0)) | 
| 54 | 24 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) ∧ 𝑥 < 𝑀) → 𝑀 ∈
ℕ0) | 
| 55 | 54 | nn0zd 12639 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) ∧ 𝑥 < 𝑀) → 𝑀 ∈ ℤ) | 
| 56 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) ∧ 𝑥 < 𝑀) → 𝑥 < 𝑀) | 
| 57 |  | elfzo2 13702 | . . . . . . . . . 10
⊢ (𝑥 ∈ (0..^𝑀) ↔ (𝑥 ∈ (ℤ≥‘0)
∧ 𝑀 ∈ ℤ
∧ 𝑥 < 𝑀)) | 
| 58 | 53, 55, 56, 57 | syl3anbrc 1344 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) ∧ 𝑥 < 𝑀) → 𝑥 ∈ (0..^𝑀)) | 
| 59 |  | fvconst2g 7222 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑥 ∈ (0..^𝑀)) → (((0..^𝑀) × {𝐴})‘𝑥) = 𝐴) | 
| 60 | 51, 58, 59 | syl2an2r 685 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) ∧ 𝑥 < 𝑀) → (((0..^𝑀) × {𝐴})‘𝑥) = 𝐴) | 
| 61 | 28 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) ∧ ¬ 𝑥 < 𝑀) → (♯‘((0..^𝑀) × {𝐴})) = 𝑀) | 
| 62 | 61 | oveq2d 7447 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) ∧ ¬ 𝑥 < 𝑀) → (𝑥 − (♯‘((0..^𝑀) × {𝐴}))) = (𝑥 − 𝑀)) | 
| 63 | 24 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) ∧ ¬ 𝑥 < 𝑀) → 𝑀 ∈
ℕ0) | 
| 64 |  | elfzonn0 13747 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (0..^𝐿) → 𝑥 ∈ ℕ0) | 
| 65 | 64 | ad2antlr 727 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) ∧ ¬ 𝑥 < 𝑀) → 𝑥 ∈ ℕ0) | 
| 66 | 24 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → 𝑀 ∈
ℕ0) | 
| 67 | 66 | nn0red 12588 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → 𝑀 ∈ ℝ) | 
| 68 |  | elfzoelz 13699 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (0..^𝐿) → 𝑥 ∈ ℤ) | 
| 69 | 68 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → 𝑥 ∈ ℤ) | 
| 70 | 69 | zred 12722 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → 𝑥 ∈ ℝ) | 
| 71 | 67, 70 | lenltd 11407 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → (𝑀 ≤ 𝑥 ↔ ¬ 𝑥 < 𝑀)) | 
| 72 | 71 | biimpar 477 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) ∧ ¬ 𝑥 < 𝑀) → 𝑀 ≤ 𝑥) | 
| 73 |  | nn0sub2 12679 | . . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ0
∧ 𝑥 ∈
ℕ0 ∧ 𝑀
≤ 𝑥) → (𝑥 − 𝑀) ∈
ℕ0) | 
| 74 | 63, 65, 72, 73 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) ∧ ¬ 𝑥 < 𝑀) → (𝑥 − 𝑀) ∈
ℕ0) | 
| 75 |  | elnn0uz 12923 | . . . . . . . . . . . 12
⊢ ((𝑥 − 𝑀) ∈ ℕ0 ↔ (𝑥 − 𝑀) ∈
(ℤ≥‘0)) | 
| 76 | 74, 75 | sylib 218 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) ∧ ¬ 𝑥 < 𝑀) → (𝑥 − 𝑀) ∈
(ℤ≥‘0)) | 
| 77 | 37 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) ∧ ¬ 𝑥 < 𝑀) → 𝑁 ∈
ℕ0) | 
| 78 | 77 | nn0zd 12639 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) ∧ ¬ 𝑥 < 𝑀) → 𝑁 ∈ ℤ) | 
| 79 |  | elfzolt2 13708 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0..^𝐿) → 𝑥 < 𝐿) | 
| 80 | 79 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → 𝑥 < 𝐿) | 
| 81 | 67 | recnd 11289 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → 𝑀 ∈ ℂ) | 
| 82 | 70 | recnd 11289 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → 𝑥 ∈ ℂ) | 
| 83 | 81, 82 | pncan3d 11623 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → (𝑀 + (𝑥 − 𝑀)) = 𝑥) | 
| 84 | 43 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → (𝑀 + 𝑁) = 𝐿) | 
| 85 | 80, 83, 84 | 3brtr4d 5175 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → (𝑀 + (𝑥 − 𝑀)) < (𝑀 + 𝑁)) | 
| 86 | 70, 67 | resubcld 11691 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → (𝑥 − 𝑀) ∈ ℝ) | 
| 87 | 37 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → 𝑁 ∈
ℕ0) | 
| 88 | 87 | nn0red 12588 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → 𝑁 ∈ ℝ) | 
| 89 | 86, 88, 67 | ltadd2d 11417 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → ((𝑥 − 𝑀) < 𝑁 ↔ (𝑀 + (𝑥 − 𝑀)) < (𝑀 + 𝑁))) | 
| 90 | 85, 89 | mpbird 257 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → (𝑥 − 𝑀) < 𝑁) | 
| 91 | 90 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) ∧ ¬ 𝑥 < 𝑀) → (𝑥 − 𝑀) < 𝑁) | 
| 92 |  | elfzo2 13702 | . . . . . . . . . . 11
⊢ ((𝑥 − 𝑀) ∈ (0..^𝑁) ↔ ((𝑥 − 𝑀) ∈ (ℤ≥‘0)
∧ 𝑁 ∈ ℤ
∧ (𝑥 − 𝑀) < 𝑁)) | 
| 93 | 76, 78, 91, 92 | syl3anbrc 1344 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) ∧ ¬ 𝑥 < 𝑀) → (𝑥 − 𝑀) ∈ (0..^𝑁)) | 
| 94 | 62, 93 | eqeltrd 2841 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) ∧ ¬ 𝑥 < 𝑀) → (𝑥 − (♯‘((0..^𝑀) × {𝐴}))) ∈ (0..^𝑁)) | 
| 95 |  | fvconst2g 7222 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝑆 ∧ (𝑥 − (♯‘((0..^𝑀) × {𝐴}))) ∈ (0..^𝑁)) → (((0..^𝑁) × {𝐴})‘(𝑥 − (♯‘((0..^𝑀) × {𝐴})))) = 𝐴) | 
| 96 | 51, 94, 95 | syl2an2r 685 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) ∧ ¬ 𝑥 < 𝑀) → (((0..^𝑁) × {𝐴})‘(𝑥 − (♯‘((0..^𝑀) × {𝐴})))) = 𝐴) | 
| 97 | 60, 96 | ifeqda 4562 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → if(𝑥 < 𝑀, (((0..^𝑀) × {𝐴})‘𝑥), (((0..^𝑁) × {𝐴})‘(𝑥 − (♯‘((0..^𝑀) × {𝐴}))))) = 𝐴) | 
| 98 | 50, 97 | eqtr2d 2778 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → 𝐴 = if(𝑥 < (♯‘((0..^𝑀) × {𝐴})), (((0..^𝑀) × {𝐴})‘𝑥), (((0..^𝑁) × {𝐴})‘(𝑥 − (♯‘((0..^𝑀) × {𝐴})))))) | 
| 99 |  | fvconst2g 7222 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑆 ∧ 𝑥 ∈ (0..^𝐿)) → (((0..^𝐿) × {𝐴})‘𝑥) = 𝐴) | 
| 100 | 1, 99 | sylan 580 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → (((0..^𝐿) × {𝐴})‘𝑥) = 𝐴) | 
| 101 | 51, 5, 6 | 3syl 18 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → ((0..^𝑀) × {𝐴}) ∈ Word {𝐴}) | 
| 102 | 51, 8, 9 | 3syl 18 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → ((0..^𝑁) × {𝐴}) ∈ Word {𝐴}) | 
| 103 |  | ccatsymb 14620 | . . . . . . 7
⊢
((((0..^𝑀) ×
{𝐴}) ∈ Word {𝐴} ∧ ((0..^𝑁) × {𝐴}) ∈ Word {𝐴} ∧ 𝑥 ∈ ℤ) → ((((0..^𝑀) × {𝐴}) ++ ((0..^𝑁) × {𝐴}))‘𝑥) = if(𝑥 < (♯‘((0..^𝑀) × {𝐴})), (((0..^𝑀) × {𝐴})‘𝑥), (((0..^𝑁) × {𝐴})‘(𝑥 − (♯‘((0..^𝑀) × {𝐴})))))) | 
| 104 | 101, 102,
69, 103 | syl3anc 1373 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → ((((0..^𝑀) × {𝐴}) ++ ((0..^𝑁) × {𝐴}))‘𝑥) = if(𝑥 < (♯‘((0..^𝑀) × {𝐴})), (((0..^𝑀) × {𝐴})‘𝑥), (((0..^𝑁) × {𝐴})‘(𝑥 − (♯‘((0..^𝑀) × {𝐴})))))) | 
| 105 | 98, 100, 104 | 3eqtr4d 2787 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝐿)) → (((0..^𝐿) × {𝐴})‘𝑥) = ((((0..^𝑀) × {𝐴}) ++ ((0..^𝑁) × {𝐴}))‘𝑥)) | 
| 106 | 4, 47, 105 | eqfnfvd 7054 | . . . 4
⊢ (𝜑 → ((0..^𝐿) × {𝐴}) = (((0..^𝑀) × {𝐴}) ++ ((0..^𝑁) × {𝐴}))) | 
| 107 | 106 | oveq1d 7446 | . . 3
⊢ (𝜑 → (((0..^𝐿) × {𝐴}) ∘f
(.r‘𝐾)(𝑈 ++ 𝑉)) = ((((0..^𝑀) × {𝐴}) ++ ((0..^𝑁) × {𝐴})) ∘f
(.r‘𝐾)(𝑈 ++ 𝑉))) | 
| 108 |  | frlmfzoccat.u | . . . . 5
⊢ (𝜑 → 𝑈 ∈ 𝐶) | 
| 109 |  | frlmfzoccat.x | . . . . . 6
⊢ 𝑋 = (𝐾 freeLMod (0..^𝑀)) | 
| 110 |  | frlmfzoccat.c | . . . . . 6
⊢ 𝐶 = (Base‘𝑋) | 
| 111 |  | frlmvscadiccat.s | . . . . . 6
⊢ 𝑆 = (Base‘𝐾) | 
| 112 | 109, 110,
111 | frlmfzowrd 42512 | . . . . 5
⊢ (𝑈 ∈ 𝐶 → 𝑈 ∈ Word 𝑆) | 
| 113 | 108, 112 | syl 17 | . . . 4
⊢ (𝜑 → 𝑈 ∈ Word 𝑆) | 
| 114 |  | frlmfzoccat.v | . . . . 5
⊢ (𝜑 → 𝑉 ∈ 𝐷) | 
| 115 |  | frlmfzoccat.y | . . . . . 6
⊢ 𝑌 = (𝐾 freeLMod (0..^𝑁)) | 
| 116 |  | frlmfzoccat.d | . . . . . 6
⊢ 𝐷 = (Base‘𝑌) | 
| 117 | 115, 116,
111 | frlmfzowrd 42512 | . . . . 5
⊢ (𝑉 ∈ 𝐷 → 𝑉 ∈ Word 𝑆) | 
| 118 | 114, 117 | syl 17 | . . . 4
⊢ (𝜑 → 𝑉 ∈ Word 𝑆) | 
| 119 | 16, 19 | eqtrid 2789 | . . . . 5
⊢ (𝜑 → (♯‘((0..^𝑀) × {𝐴})) = ((♯‘(0..^𝑀)) · 1)) | 
| 120 |  | ovexd 7466 | . . . . . . . 8
⊢ (𝜑 → (0..^𝑀) ∈ V) | 
| 121 | 109, 111,
110 | frlmbasf 21780 | . . . . . . . 8
⊢
(((0..^𝑀) ∈ V
∧ 𝑈 ∈ 𝐶) → 𝑈:(0..^𝑀)⟶𝑆) | 
| 122 | 120, 108,
121 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → 𝑈:(0..^𝑀)⟶𝑆) | 
| 123 | 122 | ffnd 6737 | . . . . . 6
⊢ (𝜑 → 𝑈 Fn (0..^𝑀)) | 
| 124 |  | hashfn 14414 | . . . . . 6
⊢ (𝑈 Fn (0..^𝑀) → (♯‘𝑈) = (♯‘(0..^𝑀))) | 
| 125 | 123, 124 | syl 17 | . . . . 5
⊢ (𝜑 → (♯‘𝑈) = (♯‘(0..^𝑀))) | 
| 126 | 23, 119, 125 | 3eqtr4d 2787 | . . . 4
⊢ (𝜑 → (♯‘((0..^𝑀) × {𝐴})) = (♯‘𝑈)) | 
| 127 | 32, 36 | eqtrd 2777 | . . . . . 6
⊢ (𝜑 → ((♯‘(0..^𝑁)) ·
(♯‘{𝐴})) =
(♯‘(0..^𝑁))) | 
| 128 | 31, 127 | eqtrid 2789 | . . . . 5
⊢ (𝜑 → (♯‘((0..^𝑁) × {𝐴})) = (♯‘(0..^𝑁))) | 
| 129 |  | ovexd 7466 | . . . . . . . 8
⊢ (𝜑 → (0..^𝑁) ∈ V) | 
| 130 | 115, 111,
116 | frlmbasf 21780 | . . . . . . . 8
⊢
(((0..^𝑁) ∈ V
∧ 𝑉 ∈ 𝐷) → 𝑉:(0..^𝑁)⟶𝑆) | 
| 131 | 129, 114,
130 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → 𝑉:(0..^𝑁)⟶𝑆) | 
| 132 | 131 | ffnd 6737 | . . . . . 6
⊢ (𝜑 → 𝑉 Fn (0..^𝑁)) | 
| 133 |  | hashfn 14414 | . . . . . 6
⊢ (𝑉 Fn (0..^𝑁) → (♯‘𝑉) = (♯‘(0..^𝑁))) | 
| 134 | 132, 133 | syl 17 | . . . . 5
⊢ (𝜑 → (♯‘𝑉) = (♯‘(0..^𝑁))) | 
| 135 | 128, 134 | eqtr4d 2780 | . . . 4
⊢ (𝜑 → (♯‘((0..^𝑁) × {𝐴})) = (♯‘𝑉)) | 
| 136 | 7, 10, 113, 118, 126, 135 | ofccat 15008 | . . 3
⊢ (𝜑 → ((((0..^𝑀) × {𝐴}) ++ ((0..^𝑁) × {𝐴})) ∘f
(.r‘𝐾)(𝑈 ++ 𝑉)) = ((((0..^𝑀) × {𝐴}) ∘f
(.r‘𝐾)𝑈) ++ (((0..^𝑁) × {𝐴}) ∘f
(.r‘𝐾)𝑉))) | 
| 137 | 107, 136 | eqtrd 2777 | . 2
⊢ (𝜑 → (((0..^𝐿) × {𝐴}) ∘f
(.r‘𝐾)(𝑈 ++ 𝑉)) = ((((0..^𝑀) × {𝐴}) ∘f
(.r‘𝐾)𝑈) ++ (((0..^𝑁) × {𝐴}) ∘f
(.r‘𝐾)𝑉))) | 
| 138 |  | frlmfzoccat.w | . . 3
⊢ 𝑊 = (𝐾 freeLMod (0..^𝐿)) | 
| 139 |  | frlmfzoccat.b | . . 3
⊢ 𝐵 = (Base‘𝑊) | 
| 140 |  | ovexd 7466 | . . 3
⊢ (𝜑 → (0..^𝐿) ∈ V) | 
| 141 |  | frlmfzoccat.k | . . . 4
⊢ (𝜑 → 𝐾 ∈ 𝑍) | 
| 142 | 138, 109,
115, 139, 110, 116, 141, 43, 24, 37, 108, 114 | frlmfzoccat 42515 | . . 3
⊢ (𝜑 → (𝑈 ++ 𝑉) ∈ 𝐵) | 
| 143 |  | frlmvscadiccat.o | . . 3
⊢ 𝑂 = (
·𝑠 ‘𝑊) | 
| 144 |  | eqid 2737 | . . 3
⊢
(.r‘𝐾) = (.r‘𝐾) | 
| 145 | 138, 139,
111, 140, 1, 142, 143, 144 | frlmvscafval 21786 | . 2
⊢ (𝜑 → (𝐴𝑂(𝑈 ++ 𝑉)) = (((0..^𝐿) × {𝐴}) ∘f
(.r‘𝐾)(𝑈 ++ 𝑉))) | 
| 146 |  | frlmvscadiccat.p | . . . 4
⊢  ∙ = (
·𝑠 ‘𝑋) | 
| 147 | 109, 110,
111, 120, 1, 108, 146, 144 | frlmvscafval 21786 | . . 3
⊢ (𝜑 → (𝐴 ∙ 𝑈) = (((0..^𝑀) × {𝐴}) ∘f
(.r‘𝐾)𝑈)) | 
| 148 |  | frlmvscadiccat.q | . . . 4
⊢  · = (
·𝑠 ‘𝑌) | 
| 149 | 115, 116,
111, 129, 1, 114, 148, 144 | frlmvscafval 21786 | . . 3
⊢ (𝜑 → (𝐴 · 𝑉) = (((0..^𝑁) × {𝐴}) ∘f
(.r‘𝐾)𝑉)) | 
| 150 | 147, 149 | oveq12d 7449 | . 2
⊢ (𝜑 → ((𝐴 ∙ 𝑈) ++ (𝐴 · 𝑉)) = ((((0..^𝑀) × {𝐴}) ∘f
(.r‘𝐾)𝑈) ++ (((0..^𝑁) × {𝐴}) ∘f
(.r‘𝐾)𝑉))) | 
| 151 | 137, 145,
150 | 3eqtr4d 2787 | 1
⊢ (𝜑 → (𝐴𝑂(𝑈 ++ 𝑉)) = ((𝐴 ∙ 𝑈) ++ (𝐴 · 𝑉))) |