Proof of Theorem ofcccat
Step | Hyp | Ref
| Expression |
1 | | ofcccat.1 |
. . 3
⊢ (𝜑 → 𝐹 ∈ Word 𝑆) |
2 | | ofcccat.2 |
. . 3
⊢ (𝜑 → 𝐺 ∈ Word 𝑆) |
3 | | ofcccat.3 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ 𝑇) |
4 | | fconst6g 6608 |
. . . 4
⊢ (𝐾 ∈ 𝑇 → ((0..^(♯‘𝐹)) × {𝐾}):(0..^(♯‘𝐹))⟶𝑇) |
5 | | iswrdi 14073 |
. . . 4
⊢
(((0..^(♯‘𝐹)) × {𝐾}):(0..^(♯‘𝐹))⟶𝑇 → ((0..^(♯‘𝐹)) × {𝐾}) ∈ Word 𝑇) |
6 | 3, 4, 5 | 3syl 18 |
. . 3
⊢ (𝜑 → ((0..^(♯‘𝐹)) × {𝐾}) ∈ Word 𝑇) |
7 | | fconst6g 6608 |
. . . 4
⊢ (𝐾 ∈ 𝑇 → ((0..^(♯‘𝐺)) × {𝐾}):(0..^(♯‘𝐺))⟶𝑇) |
8 | | iswrdi 14073 |
. . . 4
⊢
(((0..^(♯‘𝐺)) × {𝐾}):(0..^(♯‘𝐺))⟶𝑇 → ((0..^(♯‘𝐺)) × {𝐾}) ∈ Word 𝑇) |
9 | 3, 7, 8 | 3syl 18 |
. . 3
⊢ (𝜑 → ((0..^(♯‘𝐺)) × {𝐾}) ∈ Word 𝑇) |
10 | | fzofi 13547 |
. . . . 5
⊢
(0..^(♯‘𝐹)) ∈ Fin |
11 | | snfi 8721 |
. . . . 5
⊢ {𝐾} ∈ Fin |
12 | | hashxp 14001 |
. . . . 5
⊢
(((0..^(♯‘𝐹)) ∈ Fin ∧ {𝐾} ∈ Fin) →
(♯‘((0..^(♯‘𝐹)) × {𝐾})) =
((♯‘(0..^(♯‘𝐹))) · (♯‘{𝐾}))) |
13 | 10, 11, 12 | mp2an 692 |
. . . 4
⊢
(♯‘((0..^(♯‘𝐹)) × {𝐾})) =
((♯‘(0..^(♯‘𝐹))) · (♯‘{𝐾})) |
14 | | lencl 14088 |
. . . . . . 7
⊢ (𝐹 ∈ Word 𝑆 → (♯‘𝐹) ∈
ℕ0) |
15 | | hashfzo0 13997 |
. . . . . . 7
⊢
((♯‘𝐹)
∈ ℕ0 → (♯‘(0..^(♯‘𝐹))) = (♯‘𝐹)) |
16 | 1, 14, 15 | 3syl 18 |
. . . . . 6
⊢ (𝜑 →
(♯‘(0..^(♯‘𝐹))) = (♯‘𝐹)) |
17 | | hashsng 13936 |
. . . . . . 7
⊢ (𝐾 ∈ 𝑇 → (♯‘{𝐾}) = 1) |
18 | 3, 17 | syl 17 |
. . . . . 6
⊢ (𝜑 → (♯‘{𝐾}) = 1) |
19 | 16, 18 | oveq12d 7231 |
. . . . 5
⊢ (𝜑 →
((♯‘(0..^(♯‘𝐹))) · (♯‘{𝐾})) = ((♯‘𝐹) · 1)) |
20 | 1, 14 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝐹) ∈
ℕ0) |
21 | 20 | nn0cnd 12152 |
. . . . . 6
⊢ (𝜑 → (♯‘𝐹) ∈
ℂ) |
22 | 21 | mulid1d 10850 |
. . . . 5
⊢ (𝜑 → ((♯‘𝐹) · 1) =
(♯‘𝐹)) |
23 | 19, 22 | eqtrd 2777 |
. . . 4
⊢ (𝜑 →
((♯‘(0..^(♯‘𝐹))) · (♯‘{𝐾})) = (♯‘𝐹)) |
24 | 13, 23 | eqtr2id 2791 |
. . 3
⊢ (𝜑 → (♯‘𝐹) =
(♯‘((0..^(♯‘𝐹)) × {𝐾}))) |
25 | | fzofi 13547 |
. . . . 5
⊢
(0..^(♯‘𝐺)) ∈ Fin |
26 | | hashxp 14001 |
. . . . 5
⊢
(((0..^(♯‘𝐺)) ∈ Fin ∧ {𝐾} ∈ Fin) →
(♯‘((0..^(♯‘𝐺)) × {𝐾})) =
((♯‘(0..^(♯‘𝐺))) · (♯‘{𝐾}))) |
27 | 25, 11, 26 | mp2an 692 |
. . . 4
⊢
(♯‘((0..^(♯‘𝐺)) × {𝐾})) =
((♯‘(0..^(♯‘𝐺))) · (♯‘{𝐾})) |
28 | | lencl 14088 |
. . . . . . 7
⊢ (𝐺 ∈ Word 𝑆 → (♯‘𝐺) ∈
ℕ0) |
29 | | hashfzo0 13997 |
. . . . . . 7
⊢
((♯‘𝐺)
∈ ℕ0 → (♯‘(0..^(♯‘𝐺))) = (♯‘𝐺)) |
30 | 2, 28, 29 | 3syl 18 |
. . . . . 6
⊢ (𝜑 →
(♯‘(0..^(♯‘𝐺))) = (♯‘𝐺)) |
31 | 30, 18 | oveq12d 7231 |
. . . . 5
⊢ (𝜑 →
((♯‘(0..^(♯‘𝐺))) · (♯‘{𝐾})) = ((♯‘𝐺) · 1)) |
32 | 2, 28 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝐺) ∈
ℕ0) |
33 | 32 | nn0cnd 12152 |
. . . . . 6
⊢ (𝜑 → (♯‘𝐺) ∈
ℂ) |
34 | 33 | mulid1d 10850 |
. . . . 5
⊢ (𝜑 → ((♯‘𝐺) · 1) =
(♯‘𝐺)) |
35 | 31, 34 | eqtrd 2777 |
. . . 4
⊢ (𝜑 →
((♯‘(0..^(♯‘𝐺))) · (♯‘{𝐾})) = (♯‘𝐺)) |
36 | 27, 35 | eqtr2id 2791 |
. . 3
⊢ (𝜑 → (♯‘𝐺) =
(♯‘((0..^(♯‘𝐺)) × {𝐾}))) |
37 | 1, 2, 6, 9, 24, 36 | ofccat 14532 |
. 2
⊢ (𝜑 → ((𝐹 ++ 𝐺) ∘f 𝑅(((0..^(♯‘𝐹)) × {𝐾}) ++ ((0..^(♯‘𝐺)) × {𝐾}))) = ((𝐹 ∘f 𝑅((0..^(♯‘𝐹)) × {𝐾})) ++ (𝐺 ∘f 𝑅((0..^(♯‘𝐺)) × {𝐾})))) |
38 | | ccatcl 14129 |
. . . . . 6
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝐺 ∈ Word 𝑆) → (𝐹 ++ 𝐺) ∈ Word 𝑆) |
39 | 1, 2, 38 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝐹 ++ 𝐺) ∈ Word 𝑆) |
40 | | wrdf 14074 |
. . . . 5
⊢ ((𝐹 ++ 𝐺) ∈ Word 𝑆 → (𝐹 ++ 𝐺):(0..^(♯‘(𝐹 ++ 𝐺)))⟶𝑆) |
41 | 39, 40 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐹 ++ 𝐺):(0..^(♯‘(𝐹 ++ 𝐺)))⟶𝑆) |
42 | | ovexd 7248 |
. . . 4
⊢ (𝜑 → (0..^(♯‘(𝐹 ++ 𝐺))) ∈ V) |
43 | 41, 42, 3 | ofcof 31787 |
. . 3
⊢ (𝜑 → ((𝐹 ++ 𝐺) ∘f/c 𝑅𝐾) = ((𝐹 ++ 𝐺) ∘f 𝑅((0..^(♯‘(𝐹 ++ 𝐺))) × {𝐾}))) |
44 | | eqid 2737 |
. . . . 5
⊢
((0..^((♯‘𝐹) + (♯‘𝐺))) × {𝐾}) = ((0..^((♯‘𝐹) + (♯‘𝐺))) × {𝐾}) |
45 | | ccatlen 14130 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝐺 ∈ Word 𝑆) → (♯‘(𝐹 ++ 𝐺)) = ((♯‘𝐹) + (♯‘𝐺))) |
46 | 1, 2, 45 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (♯‘(𝐹 ++ 𝐺)) = ((♯‘𝐹) + (♯‘𝐺))) |
47 | 46 | oveq2d 7229 |
. . . . . 6
⊢ (𝜑 → (0..^(♯‘(𝐹 ++ 𝐺))) = (0..^((♯‘𝐹) + (♯‘𝐺)))) |
48 | 47 | xpeq1d 5580 |
. . . . 5
⊢ (𝜑 →
((0..^(♯‘(𝐹 ++
𝐺))) × {𝐾}) = ((0..^((♯‘𝐹) + (♯‘𝐺))) × {𝐾})) |
49 | | eqid 2737 |
. . . . . 6
⊢
((0..^(♯‘𝐹)) × {𝐾}) = ((0..^(♯‘𝐹)) × {𝐾}) |
50 | | eqid 2737 |
. . . . . 6
⊢
((0..^(♯‘𝐺)) × {𝐾}) = ((0..^(♯‘𝐺)) × {𝐾}) |
51 | 49, 50, 44, 3, 20, 32 | ccatmulgnn0dir 32233 |
. . . . 5
⊢ (𝜑 →
(((0..^(♯‘𝐹))
× {𝐾}) ++
((0..^(♯‘𝐺))
× {𝐾})) =
((0..^((♯‘𝐹) +
(♯‘𝐺))) ×
{𝐾})) |
52 | 44, 48, 51 | 3eqtr4a 2804 |
. . . 4
⊢ (𝜑 →
((0..^(♯‘(𝐹 ++
𝐺))) × {𝐾}) = (((0..^(♯‘𝐹)) × {𝐾}) ++ ((0..^(♯‘𝐺)) × {𝐾}))) |
53 | 52 | oveq2d 7229 |
. . 3
⊢ (𝜑 → ((𝐹 ++ 𝐺) ∘f 𝑅((0..^(♯‘(𝐹 ++ 𝐺))) × {𝐾})) = ((𝐹 ++ 𝐺) ∘f 𝑅(((0..^(♯‘𝐹)) × {𝐾}) ++ ((0..^(♯‘𝐺)) × {𝐾})))) |
54 | 43, 53 | eqtrd 2777 |
. 2
⊢ (𝜑 → ((𝐹 ++ 𝐺) ∘f/c 𝑅𝐾) = ((𝐹 ++ 𝐺) ∘f 𝑅(((0..^(♯‘𝐹)) × {𝐾}) ++ ((0..^(♯‘𝐺)) × {𝐾})))) |
55 | | wrdf 14074 |
. . . . 5
⊢ (𝐹 ∈ Word 𝑆 → 𝐹:(0..^(♯‘𝐹))⟶𝑆) |
56 | 1, 55 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹:(0..^(♯‘𝐹))⟶𝑆) |
57 | | ovexd 7248 |
. . . 4
⊢ (𝜑 → (0..^(♯‘𝐹)) ∈ V) |
58 | 56, 57, 3 | ofcof 31787 |
. . 3
⊢ (𝜑 → (𝐹 ∘f/c 𝑅𝐾) = (𝐹 ∘f 𝑅((0..^(♯‘𝐹)) × {𝐾}))) |
59 | | wrdf 14074 |
. . . . 5
⊢ (𝐺 ∈ Word 𝑆 → 𝐺:(0..^(♯‘𝐺))⟶𝑆) |
60 | 2, 59 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐺:(0..^(♯‘𝐺))⟶𝑆) |
61 | | ovexd 7248 |
. . . 4
⊢ (𝜑 → (0..^(♯‘𝐺)) ∈ V) |
62 | 60, 61, 3 | ofcof 31787 |
. . 3
⊢ (𝜑 → (𝐺 ∘f/c 𝑅𝐾) = (𝐺 ∘f 𝑅((0..^(♯‘𝐺)) × {𝐾}))) |
63 | 58, 62 | oveq12d 7231 |
. 2
⊢ (𝜑 → ((𝐹 ∘f/c 𝑅𝐾) ++ (𝐺 ∘f/c 𝑅𝐾)) = ((𝐹 ∘f 𝑅((0..^(♯‘𝐹)) × {𝐾})) ++ (𝐺 ∘f 𝑅((0..^(♯‘𝐺)) × {𝐾})))) |
64 | 37, 54, 63 | 3eqtr4d 2787 |
1
⊢ (𝜑 → ((𝐹 ++ 𝐺) ∘f/c 𝑅𝐾) = ((𝐹 ∘f/c 𝑅𝐾) ++ (𝐺 ∘f/c 𝑅𝐾))) |