Proof of Theorem ofcccat
Step | Hyp | Ref
| Expression |
1 | | ofcccat.1 |
. . 3
⊢ (𝜑 → 𝐹 ∈ Word 𝑆) |
2 | | ofcccat.2 |
. . 3
⊢ (𝜑 → 𝐺 ∈ Word 𝑆) |
3 | | ofcccat.3 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ 𝑇) |
4 | | fconst6g 6255 |
. . . 4
⊢ (𝐾 ∈ 𝑇 → ((0..^(♯‘𝐹)) × {𝐾}):(0..^(♯‘𝐹))⟶𝑇) |
5 | | iswrdi 13515 |
. . . 4
⊢
(((0..^(♯‘𝐹)) × {𝐾}):(0..^(♯‘𝐹))⟶𝑇 → ((0..^(♯‘𝐹)) × {𝐾}) ∈ Word 𝑇) |
6 | 3, 4, 5 | 3syl 18 |
. . 3
⊢ (𝜑 → ((0..^(♯‘𝐹)) × {𝐾}) ∈ Word 𝑇) |
7 | | fconst6g 6255 |
. . . 4
⊢ (𝐾 ∈ 𝑇 → ((0..^(♯‘𝐺)) × {𝐾}):(0..^(♯‘𝐺))⟶𝑇) |
8 | | iswrdi 13515 |
. . . 4
⊢
(((0..^(♯‘𝐺)) × {𝐾}):(0..^(♯‘𝐺))⟶𝑇 → ((0..^(♯‘𝐺)) × {𝐾}) ∈ Word 𝑇) |
9 | 3, 7, 8 | 3syl 18 |
. . 3
⊢ (𝜑 → ((0..^(♯‘𝐺)) × {𝐾}) ∈ Word 𝑇) |
10 | | fzofi 12987 |
. . . . 5
⊢
(0..^(♯‘𝐹)) ∈ Fin |
11 | | snfi 8205 |
. . . . 5
⊢ {𝐾} ∈ Fin |
12 | | hashxp 13433 |
. . . . 5
⊢
(((0..^(♯‘𝐹)) ∈ Fin ∧ {𝐾} ∈ Fin) →
(♯‘((0..^(♯‘𝐹)) × {𝐾})) =
((♯‘(0..^(♯‘𝐹))) · (♯‘{𝐾}))) |
13 | 10, 11, 12 | mp2an 710 |
. . . 4
⊢
(♯‘((0..^(♯‘𝐹)) × {𝐾})) =
((♯‘(0..^(♯‘𝐹))) · (♯‘{𝐾})) |
14 | | wrdfin 13529 |
. . . . . . . 8
⊢ (𝐹 ∈ Word 𝑆 → 𝐹 ∈ Fin) |
15 | | hashcl 13359 |
. . . . . . . 8
⊢ (𝐹 ∈ Fin →
(♯‘𝐹) ∈
ℕ0) |
16 | 1, 14, 15 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝐹) ∈
ℕ0) |
17 | | hashfzo0 13429 |
. . . . . . 7
⊢
((♯‘𝐹)
∈ ℕ0 → (♯‘(0..^(♯‘𝐹))) = (♯‘𝐹)) |
18 | 16, 17 | syl 17 |
. . . . . 6
⊢ (𝜑 →
(♯‘(0..^(♯‘𝐹))) = (♯‘𝐹)) |
19 | | hashsng 13371 |
. . . . . . 7
⊢ (𝐾 ∈ 𝑇 → (♯‘{𝐾}) = 1) |
20 | 3, 19 | syl 17 |
. . . . . 6
⊢ (𝜑 → (♯‘{𝐾}) = 1) |
21 | 18, 20 | oveq12d 6832 |
. . . . 5
⊢ (𝜑 →
((♯‘(0..^(♯‘𝐹))) · (♯‘{𝐾})) = ((♯‘𝐹) · 1)) |
22 | 16 | nn0cnd 11565 |
. . . . . 6
⊢ (𝜑 → (♯‘𝐹) ∈
ℂ) |
23 | 22 | mulid1d 10269 |
. . . . 5
⊢ (𝜑 → ((♯‘𝐹) · 1) =
(♯‘𝐹)) |
24 | 21, 23 | eqtrd 2794 |
. . . 4
⊢ (𝜑 →
((♯‘(0..^(♯‘𝐹))) · (♯‘{𝐾})) = (♯‘𝐹)) |
25 | 13, 24 | syl5req 2807 |
. . 3
⊢ (𝜑 → (♯‘𝐹) =
(♯‘((0..^(♯‘𝐹)) × {𝐾}))) |
26 | | fzofi 12987 |
. . . . 5
⊢
(0..^(♯‘𝐺)) ∈ Fin |
27 | | hashxp 13433 |
. . . . 5
⊢
(((0..^(♯‘𝐺)) ∈ Fin ∧ {𝐾} ∈ Fin) →
(♯‘((0..^(♯‘𝐺)) × {𝐾})) =
((♯‘(0..^(♯‘𝐺))) · (♯‘{𝐾}))) |
28 | 26, 11, 27 | mp2an 710 |
. . . 4
⊢
(♯‘((0..^(♯‘𝐺)) × {𝐾})) =
((♯‘(0..^(♯‘𝐺))) · (♯‘{𝐾})) |
29 | | wrdfin 13529 |
. . . . . . . 8
⊢ (𝐺 ∈ Word 𝑆 → 𝐺 ∈ Fin) |
30 | | hashcl 13359 |
. . . . . . . 8
⊢ (𝐺 ∈ Fin →
(♯‘𝐺) ∈
ℕ0) |
31 | 2, 29, 30 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝐺) ∈
ℕ0) |
32 | | hashfzo0 13429 |
. . . . . . 7
⊢
((♯‘𝐺)
∈ ℕ0 → (♯‘(0..^(♯‘𝐺))) = (♯‘𝐺)) |
33 | 31, 32 | syl 17 |
. . . . . 6
⊢ (𝜑 →
(♯‘(0..^(♯‘𝐺))) = (♯‘𝐺)) |
34 | 33, 20 | oveq12d 6832 |
. . . . 5
⊢ (𝜑 →
((♯‘(0..^(♯‘𝐺))) · (♯‘{𝐾})) = ((♯‘𝐺) · 1)) |
35 | 31 | nn0cnd 11565 |
. . . . . 6
⊢ (𝜑 → (♯‘𝐺) ∈
ℂ) |
36 | 35 | mulid1d 10269 |
. . . . 5
⊢ (𝜑 → ((♯‘𝐺) · 1) =
(♯‘𝐺)) |
37 | 34, 36 | eqtrd 2794 |
. . . 4
⊢ (𝜑 →
((♯‘(0..^(♯‘𝐺))) · (♯‘{𝐾})) = (♯‘𝐺)) |
38 | 28, 37 | syl5req 2807 |
. . 3
⊢ (𝜑 → (♯‘𝐺) =
(♯‘((0..^(♯‘𝐺)) × {𝐾}))) |
39 | 1, 2, 6, 9, 25, 38 | ofccat 13929 |
. 2
⊢ (𝜑 → ((𝐹 ++ 𝐺) ∘𝑓 𝑅(((0..^(♯‘𝐹)) × {𝐾}) ++ ((0..^(♯‘𝐺)) × {𝐾}))) = ((𝐹 ∘𝑓 𝑅((0..^(♯‘𝐹)) × {𝐾})) ++ (𝐺 ∘𝑓 𝑅((0..^(♯‘𝐺)) × {𝐾})))) |
40 | | ccatcl 13566 |
. . . . . 6
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝐺 ∈ Word 𝑆) → (𝐹 ++ 𝐺) ∈ Word 𝑆) |
41 | 1, 2, 40 | syl2anc 696 |
. . . . 5
⊢ (𝜑 → (𝐹 ++ 𝐺) ∈ Word 𝑆) |
42 | | wrdf 13516 |
. . . . 5
⊢ ((𝐹 ++ 𝐺) ∈ Word 𝑆 → (𝐹 ++ 𝐺):(0..^(♯‘(𝐹 ++ 𝐺)))⟶𝑆) |
43 | 41, 42 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐹 ++ 𝐺):(0..^(♯‘(𝐹 ++ 𝐺)))⟶𝑆) |
44 | | ovexd 6844 |
. . . 4
⊢ (𝜑 → (0..^(♯‘(𝐹 ++ 𝐺))) ∈ V) |
45 | 43, 44, 3 | ofcof 30499 |
. . 3
⊢ (𝜑 → ((𝐹 ++ 𝐺)∘𝑓/𝑐𝑅𝐾) = ((𝐹 ++ 𝐺) ∘𝑓 𝑅((0..^(♯‘(𝐹 ++ 𝐺))) × {𝐾}))) |
46 | | ccatlen 13567 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝐺 ∈ Word 𝑆) → (♯‘(𝐹 ++ 𝐺)) = ((♯‘𝐹) + (♯‘𝐺))) |
47 | 1, 2, 46 | syl2anc 696 |
. . . . . . 7
⊢ (𝜑 → (♯‘(𝐹 ++ 𝐺)) = ((♯‘𝐹) + (♯‘𝐺))) |
48 | 47 | oveq2d 6830 |
. . . . . 6
⊢ (𝜑 → (0..^(♯‘(𝐹 ++ 𝐺))) = (0..^((♯‘𝐹) + (♯‘𝐺)))) |
49 | 48 | xpeq1d 5295 |
. . . . 5
⊢ (𝜑 →
((0..^(♯‘(𝐹 ++
𝐺))) × {𝐾}) = ((0..^((♯‘𝐹) + (♯‘𝐺))) × {𝐾})) |
50 | | eqid 2760 |
. . . . . 6
⊢
((0..^(♯‘𝐹)) × {𝐾}) = ((0..^(♯‘𝐹)) × {𝐾}) |
51 | | eqid 2760 |
. . . . . 6
⊢
((0..^(♯‘𝐺)) × {𝐾}) = ((0..^(♯‘𝐺)) × {𝐾}) |
52 | | eqid 2760 |
. . . . . 6
⊢
((0..^((♯‘𝐹) + (♯‘𝐺))) × {𝐾}) = ((0..^((♯‘𝐹) + (♯‘𝐺))) × {𝐾}) |
53 | 50, 51, 52, 3, 16, 31 | ccatmulgnn0dir 30949 |
. . . . 5
⊢ (𝜑 →
(((0..^(♯‘𝐹))
× {𝐾}) ++
((0..^(♯‘𝐺))
× {𝐾})) =
((0..^((♯‘𝐹) +
(♯‘𝐺))) ×
{𝐾})) |
54 | 49, 53 | eqtr4d 2797 |
. . . 4
⊢ (𝜑 →
((0..^(♯‘(𝐹 ++
𝐺))) × {𝐾}) = (((0..^(♯‘𝐹)) × {𝐾}) ++ ((0..^(♯‘𝐺)) × {𝐾}))) |
55 | 54 | oveq2d 6830 |
. . 3
⊢ (𝜑 → ((𝐹 ++ 𝐺) ∘𝑓 𝑅((0..^(♯‘(𝐹 ++ 𝐺))) × {𝐾})) = ((𝐹 ++ 𝐺) ∘𝑓 𝑅(((0..^(♯‘𝐹)) × {𝐾}) ++ ((0..^(♯‘𝐺)) × {𝐾})))) |
56 | 45, 55 | eqtrd 2794 |
. 2
⊢ (𝜑 → ((𝐹 ++ 𝐺)∘𝑓/𝑐𝑅𝐾) = ((𝐹 ++ 𝐺) ∘𝑓 𝑅(((0..^(♯‘𝐹)) × {𝐾}) ++ ((0..^(♯‘𝐺)) × {𝐾})))) |
57 | | wrdf 13516 |
. . . . 5
⊢ (𝐹 ∈ Word 𝑆 → 𝐹:(0..^(♯‘𝐹))⟶𝑆) |
58 | 1, 57 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹:(0..^(♯‘𝐹))⟶𝑆) |
59 | 10 | a1i 11 |
. . . 4
⊢ (𝜑 → (0..^(♯‘𝐹)) ∈ Fin) |
60 | 58, 59, 3 | ofcof 30499 |
. . 3
⊢ (𝜑 → (𝐹∘𝑓/𝑐𝑅𝐾) = (𝐹 ∘𝑓 𝑅((0..^(♯‘𝐹)) × {𝐾}))) |
61 | | wrdf 13516 |
. . . . 5
⊢ (𝐺 ∈ Word 𝑆 → 𝐺:(0..^(♯‘𝐺))⟶𝑆) |
62 | 2, 61 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐺:(0..^(♯‘𝐺))⟶𝑆) |
63 | 26 | a1i 11 |
. . . 4
⊢ (𝜑 → (0..^(♯‘𝐺)) ∈ Fin) |
64 | 62, 63, 3 | ofcof 30499 |
. . 3
⊢ (𝜑 → (𝐺∘𝑓/𝑐𝑅𝐾) = (𝐺 ∘𝑓 𝑅((0..^(♯‘𝐺)) × {𝐾}))) |
65 | 60, 64 | oveq12d 6832 |
. 2
⊢ (𝜑 → ((𝐹∘𝑓/𝑐𝑅𝐾) ++ (𝐺∘𝑓/𝑐𝑅𝐾)) = ((𝐹 ∘𝑓 𝑅((0..^(♯‘𝐹)) × {𝐾})) ++ (𝐺 ∘𝑓 𝑅((0..^(♯‘𝐺)) × {𝐾})))) |
66 | 39, 56, 65 | 3eqtr4d 2804 |
1
⊢ (𝜑 → ((𝐹 ++ 𝐺)∘𝑓/𝑐𝑅𝐾) = ((𝐹∘𝑓/𝑐𝑅𝐾) ++ (𝐺∘𝑓/𝑐𝑅𝐾))) |