Proof of Theorem ofcccat
Step | Hyp | Ref
| Expression |
1 | | ofcccat.1 |
. . 3
⊢ (𝜑 → 𝐹 ∈ Word 𝑆) |
2 | | ofcccat.2 |
. . 3
⊢ (𝜑 → 𝐺 ∈ Word 𝑆) |
3 | | ofcccat.3 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ 𝑇) |
4 | | fconst6g 6007 |
. . . 4
⊢ (𝐾 ∈ 𝑇 → ((0..^(#‘𝐹)) × {𝐾}):(0..^(#‘𝐹))⟶𝑇) |
5 | | iswrdi 13164 |
. . . 4
⊢
(((0..^(#‘𝐹))
× {𝐾}):(0..^(#‘𝐹))⟶𝑇 → ((0..^(#‘𝐹)) × {𝐾}) ∈ Word 𝑇) |
6 | 3, 4, 5 | 3syl 18 |
. . 3
⊢ (𝜑 → ((0..^(#‘𝐹)) × {𝐾}) ∈ Word 𝑇) |
7 | | fconst6g 6007 |
. . . 4
⊢ (𝐾 ∈ 𝑇 → ((0..^(#‘𝐺)) × {𝐾}):(0..^(#‘𝐺))⟶𝑇) |
8 | | iswrdi 13164 |
. . . 4
⊢
(((0..^(#‘𝐺))
× {𝐾}):(0..^(#‘𝐺))⟶𝑇 → ((0..^(#‘𝐺)) × {𝐾}) ∈ Word 𝑇) |
9 | 3, 7, 8 | 3syl 18 |
. . 3
⊢ (𝜑 → ((0..^(#‘𝐺)) × {𝐾}) ∈ Word 𝑇) |
10 | | fzofi 12635 |
. . . . 5
⊢
(0..^(#‘𝐹))
∈ Fin |
11 | | snfi 7923 |
. . . . 5
⊢ {𝐾} ∈ Fin |
12 | | hashxp 13081 |
. . . . 5
⊢
(((0..^(#‘𝐹))
∈ Fin ∧ {𝐾} ∈
Fin) → (#‘((0..^(#‘𝐹)) × {𝐾})) = ((#‘(0..^(#‘𝐹))) · (#‘{𝐾}))) |
13 | 10, 11, 12 | mp2an 704 |
. . . 4
⊢
(#‘((0..^(#‘𝐹)) × {𝐾})) = ((#‘(0..^(#‘𝐹))) · (#‘{𝐾})) |
14 | | wrdfin 13178 |
. . . . . . . 8
⊢ (𝐹 ∈ Word 𝑆 → 𝐹 ∈ Fin) |
15 | | hashcl 13009 |
. . . . . . . 8
⊢ (𝐹 ∈ Fin →
(#‘𝐹) ∈
ℕ0) |
16 | 1, 14, 15 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (#‘𝐹) ∈
ℕ0) |
17 | | hashfzo0 13077 |
. . . . . . 7
⊢
((#‘𝐹) ∈
ℕ0 → (#‘(0..^(#‘𝐹))) = (#‘𝐹)) |
18 | 16, 17 | syl 17 |
. . . . . 6
⊢ (𝜑 →
(#‘(0..^(#‘𝐹)))
= (#‘𝐹)) |
19 | | hashsng 13020 |
. . . . . . 7
⊢ (𝐾 ∈ 𝑇 → (#‘{𝐾}) = 1) |
20 | 3, 19 | syl 17 |
. . . . . 6
⊢ (𝜑 → (#‘{𝐾}) = 1) |
21 | 18, 20 | oveq12d 6567 |
. . . . 5
⊢ (𝜑 →
((#‘(0..^(#‘𝐹))) · (#‘{𝐾})) = ((#‘𝐹) · 1)) |
22 | 16 | nn0cnd 11230 |
. . . . . 6
⊢ (𝜑 → (#‘𝐹) ∈ ℂ) |
23 | 22 | mulid1d 9936 |
. . . . 5
⊢ (𝜑 → ((#‘𝐹) · 1) = (#‘𝐹)) |
24 | 21, 23 | eqtrd 2644 |
. . . 4
⊢ (𝜑 →
((#‘(0..^(#‘𝐹))) · (#‘{𝐾})) = (#‘𝐹)) |
25 | 13, 24 | syl5req 2657 |
. . 3
⊢ (𝜑 → (#‘𝐹) = (#‘((0..^(#‘𝐹)) × {𝐾}))) |
26 | | fzofi 12635 |
. . . . 5
⊢
(0..^(#‘𝐺))
∈ Fin |
27 | | hashxp 13081 |
. . . . 5
⊢
(((0..^(#‘𝐺))
∈ Fin ∧ {𝐾} ∈
Fin) → (#‘((0..^(#‘𝐺)) × {𝐾})) = ((#‘(0..^(#‘𝐺))) · (#‘{𝐾}))) |
28 | 26, 11, 27 | mp2an 704 |
. . . 4
⊢
(#‘((0..^(#‘𝐺)) × {𝐾})) = ((#‘(0..^(#‘𝐺))) · (#‘{𝐾})) |
29 | | wrdfin 13178 |
. . . . . . . 8
⊢ (𝐺 ∈ Word 𝑆 → 𝐺 ∈ Fin) |
30 | | hashcl 13009 |
. . . . . . . 8
⊢ (𝐺 ∈ Fin →
(#‘𝐺) ∈
ℕ0) |
31 | 2, 29, 30 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (#‘𝐺) ∈
ℕ0) |
32 | | hashfzo0 13077 |
. . . . . . 7
⊢
((#‘𝐺) ∈
ℕ0 → (#‘(0..^(#‘𝐺))) = (#‘𝐺)) |
33 | 31, 32 | syl 17 |
. . . . . 6
⊢ (𝜑 →
(#‘(0..^(#‘𝐺)))
= (#‘𝐺)) |
34 | 33, 20 | oveq12d 6567 |
. . . . 5
⊢ (𝜑 →
((#‘(0..^(#‘𝐺))) · (#‘{𝐾})) = ((#‘𝐺) · 1)) |
35 | 31 | nn0cnd 11230 |
. . . . . 6
⊢ (𝜑 → (#‘𝐺) ∈ ℂ) |
36 | 35 | mulid1d 9936 |
. . . . 5
⊢ (𝜑 → ((#‘𝐺) · 1) = (#‘𝐺)) |
37 | 34, 36 | eqtrd 2644 |
. . . 4
⊢ (𝜑 →
((#‘(0..^(#‘𝐺))) · (#‘{𝐾})) = (#‘𝐺)) |
38 | 28, 37 | syl5req 2657 |
. . 3
⊢ (𝜑 → (#‘𝐺) = (#‘((0..^(#‘𝐺)) × {𝐾}))) |
39 | 1, 2, 6, 9, 25, 38 | ofccat 13556 |
. 2
⊢ (𝜑 → ((𝐹 ++ 𝐺) ∘𝑓 𝑅(((0..^(#‘𝐹)) × {𝐾}) ++ ((0..^(#‘𝐺)) × {𝐾}))) = ((𝐹 ∘𝑓 𝑅((0..^(#‘𝐹)) × {𝐾})) ++ (𝐺 ∘𝑓 𝑅((0..^(#‘𝐺)) × {𝐾})))) |
40 | | ccatcl 13212 |
. . . . . 6
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝐺 ∈ Word 𝑆) → (𝐹 ++ 𝐺) ∈ Word 𝑆) |
41 | 1, 2, 40 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝐹 ++ 𝐺) ∈ Word 𝑆) |
42 | | wrdf 13165 |
. . . . 5
⊢ ((𝐹 ++ 𝐺) ∈ Word 𝑆 → (𝐹 ++ 𝐺):(0..^(#‘(𝐹 ++ 𝐺)))⟶𝑆) |
43 | 41, 42 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐹 ++ 𝐺):(0..^(#‘(𝐹 ++ 𝐺)))⟶𝑆) |
44 | | ovex 6577 |
. . . . 5
⊢
(0..^(#‘(𝐹 ++
𝐺))) ∈
V |
45 | 44 | a1i 11 |
. . . 4
⊢ (𝜑 → (0..^(#‘(𝐹 ++ 𝐺))) ∈ V) |
46 | 43, 45, 3 | ofcof 29496 |
. . 3
⊢ (𝜑 → ((𝐹 ++ 𝐺)∘𝑓/𝑐𝑅𝐾) = ((𝐹 ++ 𝐺) ∘𝑓 𝑅((0..^(#‘(𝐹 ++ 𝐺))) × {𝐾}))) |
47 | | ccatlen 13213 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝐺 ∈ Word 𝑆) → (#‘(𝐹 ++ 𝐺)) = ((#‘𝐹) + (#‘𝐺))) |
48 | 1, 2, 47 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (#‘(𝐹 ++ 𝐺)) = ((#‘𝐹) + (#‘𝐺))) |
49 | 48 | oveq2d 6565 |
. . . . . 6
⊢ (𝜑 → (0..^(#‘(𝐹 ++ 𝐺))) = (0..^((#‘𝐹) + (#‘𝐺)))) |
50 | 49 | xpeq1d 5062 |
. . . . 5
⊢ (𝜑 → ((0..^(#‘(𝐹 ++ 𝐺))) × {𝐾}) = ((0..^((#‘𝐹) + (#‘𝐺))) × {𝐾})) |
51 | | eqid 2610 |
. . . . . 6
⊢
((0..^(#‘𝐹))
× {𝐾}) =
((0..^(#‘𝐹)) ×
{𝐾}) |
52 | | eqid 2610 |
. . . . . 6
⊢
((0..^(#‘𝐺))
× {𝐾}) =
((0..^(#‘𝐺)) ×
{𝐾}) |
53 | | eqid 2610 |
. . . . . 6
⊢
((0..^((#‘𝐹) +
(#‘𝐺))) ×
{𝐾}) =
((0..^((#‘𝐹) +
(#‘𝐺))) ×
{𝐾}) |
54 | 51, 52, 53, 3, 16, 31 | ccatmulgnn0dir 29945 |
. . . . 5
⊢ (𝜑 → (((0..^(#‘𝐹)) × {𝐾}) ++ ((0..^(#‘𝐺)) × {𝐾})) = ((0..^((#‘𝐹) + (#‘𝐺))) × {𝐾})) |
55 | 50, 54 | eqtr4d 2647 |
. . . 4
⊢ (𝜑 → ((0..^(#‘(𝐹 ++ 𝐺))) × {𝐾}) = (((0..^(#‘𝐹)) × {𝐾}) ++ ((0..^(#‘𝐺)) × {𝐾}))) |
56 | 55 | oveq2d 6565 |
. . 3
⊢ (𝜑 → ((𝐹 ++ 𝐺) ∘𝑓 𝑅((0..^(#‘(𝐹 ++ 𝐺))) × {𝐾})) = ((𝐹 ++ 𝐺) ∘𝑓 𝑅(((0..^(#‘𝐹)) × {𝐾}) ++ ((0..^(#‘𝐺)) × {𝐾})))) |
57 | 46, 56 | eqtrd 2644 |
. 2
⊢ (𝜑 → ((𝐹 ++ 𝐺)∘𝑓/𝑐𝑅𝐾) = ((𝐹 ++ 𝐺) ∘𝑓 𝑅(((0..^(#‘𝐹)) × {𝐾}) ++ ((0..^(#‘𝐺)) × {𝐾})))) |
58 | | wrdf 13165 |
. . . . 5
⊢ (𝐹 ∈ Word 𝑆 → 𝐹:(0..^(#‘𝐹))⟶𝑆) |
59 | 1, 58 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹:(0..^(#‘𝐹))⟶𝑆) |
60 | 10 | a1i 11 |
. . . 4
⊢ (𝜑 → (0..^(#‘𝐹)) ∈ Fin) |
61 | 59, 60, 3 | ofcof 29496 |
. . 3
⊢ (𝜑 → (𝐹∘𝑓/𝑐𝑅𝐾) = (𝐹 ∘𝑓 𝑅((0..^(#‘𝐹)) × {𝐾}))) |
62 | | wrdf 13165 |
. . . . 5
⊢ (𝐺 ∈ Word 𝑆 → 𝐺:(0..^(#‘𝐺))⟶𝑆) |
63 | 2, 62 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐺:(0..^(#‘𝐺))⟶𝑆) |
64 | 26 | a1i 11 |
. . . 4
⊢ (𝜑 → (0..^(#‘𝐺)) ∈ Fin) |
65 | 63, 64, 3 | ofcof 29496 |
. . 3
⊢ (𝜑 → (𝐺∘𝑓/𝑐𝑅𝐾) = (𝐺 ∘𝑓 𝑅((0..^(#‘𝐺)) × {𝐾}))) |
66 | 61, 65 | oveq12d 6567 |
. 2
⊢ (𝜑 → ((𝐹∘𝑓/𝑐𝑅𝐾) ++ (𝐺∘𝑓/𝑐𝑅𝐾)) = ((𝐹 ∘𝑓 𝑅((0..^(#‘𝐹)) × {𝐾})) ++ (𝐺 ∘𝑓 𝑅((0..^(#‘𝐺)) × {𝐾})))) |
67 | 39, 57, 66 | 3eqtr4d 2654 |
1
⊢ (𝜑 → ((𝐹 ++ 𝐺)∘𝑓/𝑐𝑅𝐾) = ((𝐹∘𝑓/𝑐𝑅𝐾) ++ (𝐺∘𝑓/𝑐𝑅𝐾))) |