Step | Hyp | Ref
| Expression |
1 | | ofcccat.1 |
. . 3
โข (๐ โ ๐น โ Word ๐) |
2 | | ofcccat.2 |
. . 3
โข (๐ โ ๐บ โ Word ๐) |
3 | | ofcccat.3 |
. . . 4
โข (๐ โ ๐พ โ ๐) |
4 | | fconst6g 6781 |
. . . 4
โข (๐พ โ ๐ โ ((0..^(โฏโ๐น)) ร {๐พ}):(0..^(โฏโ๐น))โถ๐) |
5 | | iswrdi 14468 |
. . . 4
โข
(((0..^(โฏโ๐น)) ร {๐พ}):(0..^(โฏโ๐น))โถ๐ โ ((0..^(โฏโ๐น)) ร {๐พ}) โ Word ๐) |
6 | 3, 4, 5 | 3syl 18 |
. . 3
โข (๐ โ ((0..^(โฏโ๐น)) ร {๐พ}) โ Word ๐) |
7 | | fconst6g 6781 |
. . . 4
โข (๐พ โ ๐ โ ((0..^(โฏโ๐บ)) ร {๐พ}):(0..^(โฏโ๐บ))โถ๐) |
8 | | iswrdi 14468 |
. . . 4
โข
(((0..^(โฏโ๐บ)) ร {๐พ}):(0..^(โฏโ๐บ))โถ๐ โ ((0..^(โฏโ๐บ)) ร {๐พ}) โ Word ๐) |
9 | 3, 7, 8 | 3syl 18 |
. . 3
โข (๐ โ ((0..^(โฏโ๐บ)) ร {๐พ}) โ Word ๐) |
10 | | fzofi 13939 |
. . . . 5
โข
(0..^(โฏโ๐น)) โ Fin |
11 | | snfi 9044 |
. . . . 5
โข {๐พ} โ Fin |
12 | | hashxp 14394 |
. . . . 5
โข
(((0..^(โฏโ๐น)) โ Fin โง {๐พ} โ Fin) โ
(โฏโ((0..^(โฏโ๐น)) ร {๐พ})) =
((โฏโ(0..^(โฏโ๐น))) ยท (โฏโ{๐พ}))) |
13 | 10, 11, 12 | mp2an 691 |
. . . 4
โข
(โฏโ((0..^(โฏโ๐น)) ร {๐พ})) =
((โฏโ(0..^(โฏโ๐น))) ยท (โฏโ{๐พ})) |
14 | | lencl 14483 |
. . . . . . 7
โข (๐น โ Word ๐ โ (โฏโ๐น) โ
โ0) |
15 | | hashfzo0 14390 |
. . . . . . 7
โข
((โฏโ๐น)
โ โ0 โ (โฏโ(0..^(โฏโ๐น))) = (โฏโ๐น)) |
16 | 1, 14, 15 | 3syl 18 |
. . . . . 6
โข (๐ โ
(โฏโ(0..^(โฏโ๐น))) = (โฏโ๐น)) |
17 | | hashsng 14329 |
. . . . . . 7
โข (๐พ โ ๐ โ (โฏโ{๐พ}) = 1) |
18 | 3, 17 | syl 17 |
. . . . . 6
โข (๐ โ (โฏโ{๐พ}) = 1) |
19 | 16, 18 | oveq12d 7427 |
. . . . 5
โข (๐ โ
((โฏโ(0..^(โฏโ๐น))) ยท (โฏโ{๐พ})) = ((โฏโ๐น) ยท 1)) |
20 | 1, 14 | syl 17 |
. . . . . . 7
โข (๐ โ (โฏโ๐น) โ
โ0) |
21 | 20 | nn0cnd 12534 |
. . . . . 6
โข (๐ โ (โฏโ๐น) โ
โ) |
22 | 21 | mulridd 11231 |
. . . . 5
โข (๐ โ ((โฏโ๐น) ยท 1) =
(โฏโ๐น)) |
23 | 19, 22 | eqtrd 2773 |
. . . 4
โข (๐ โ
((โฏโ(0..^(โฏโ๐น))) ยท (โฏโ{๐พ})) = (โฏโ๐น)) |
24 | 13, 23 | eqtr2id 2786 |
. . 3
โข (๐ โ (โฏโ๐น) =
(โฏโ((0..^(โฏโ๐น)) ร {๐พ}))) |
25 | | fzofi 13939 |
. . . . 5
โข
(0..^(โฏโ๐บ)) โ Fin |
26 | | hashxp 14394 |
. . . . 5
โข
(((0..^(โฏโ๐บ)) โ Fin โง {๐พ} โ Fin) โ
(โฏโ((0..^(โฏโ๐บ)) ร {๐พ})) =
((โฏโ(0..^(โฏโ๐บ))) ยท (โฏโ{๐พ}))) |
27 | 25, 11, 26 | mp2an 691 |
. . . 4
โข
(โฏโ((0..^(โฏโ๐บ)) ร {๐พ})) =
((โฏโ(0..^(โฏโ๐บ))) ยท (โฏโ{๐พ})) |
28 | | lencl 14483 |
. . . . . . 7
โข (๐บ โ Word ๐ โ (โฏโ๐บ) โ
โ0) |
29 | | hashfzo0 14390 |
. . . . . . 7
โข
((โฏโ๐บ)
โ โ0 โ (โฏโ(0..^(โฏโ๐บ))) = (โฏโ๐บ)) |
30 | 2, 28, 29 | 3syl 18 |
. . . . . 6
โข (๐ โ
(โฏโ(0..^(โฏโ๐บ))) = (โฏโ๐บ)) |
31 | 30, 18 | oveq12d 7427 |
. . . . 5
โข (๐ โ
((โฏโ(0..^(โฏโ๐บ))) ยท (โฏโ{๐พ})) = ((โฏโ๐บ) ยท 1)) |
32 | 2, 28 | syl 17 |
. . . . . . 7
โข (๐ โ (โฏโ๐บ) โ
โ0) |
33 | 32 | nn0cnd 12534 |
. . . . . 6
โข (๐ โ (โฏโ๐บ) โ
โ) |
34 | 33 | mulridd 11231 |
. . . . 5
โข (๐ โ ((โฏโ๐บ) ยท 1) =
(โฏโ๐บ)) |
35 | 31, 34 | eqtrd 2773 |
. . . 4
โข (๐ โ
((โฏโ(0..^(โฏโ๐บ))) ยท (โฏโ{๐พ})) = (โฏโ๐บ)) |
36 | 27, 35 | eqtr2id 2786 |
. . 3
โข (๐ โ (โฏโ๐บ) =
(โฏโ((0..^(โฏโ๐บ)) ร {๐พ}))) |
37 | 1, 2, 6, 9, 24, 36 | ofccat 14916 |
. 2
โข (๐ โ ((๐น ++ ๐บ) โf ๐
(((0..^(โฏโ๐น)) ร {๐พ}) ++ ((0..^(โฏโ๐บ)) ร {๐พ}))) = ((๐น โf ๐
((0..^(โฏโ๐น)) ร {๐พ})) ++ (๐บ โf ๐
((0..^(โฏโ๐บ)) ร {๐พ})))) |
38 | | ccatcl 14524 |
. . . . . 6
โข ((๐น โ Word ๐ โง ๐บ โ Word ๐) โ (๐น ++ ๐บ) โ Word ๐) |
39 | 1, 2, 38 | syl2anc 585 |
. . . . 5
โข (๐ โ (๐น ++ ๐บ) โ Word ๐) |
40 | | wrdf 14469 |
. . . . 5
โข ((๐น ++ ๐บ) โ Word ๐ โ (๐น ++ ๐บ):(0..^(โฏโ(๐น ++ ๐บ)))โถ๐) |
41 | 39, 40 | syl 17 |
. . . 4
โข (๐ โ (๐น ++ ๐บ):(0..^(โฏโ(๐น ++ ๐บ)))โถ๐) |
42 | | ovexd 7444 |
. . . 4
โข (๐ โ (0..^(โฏโ(๐น ++ ๐บ))) โ V) |
43 | 41, 42, 3 | ofcof 33105 |
. . 3
โข (๐ โ ((๐น ++ ๐บ) โf/c ๐
๐พ) = ((๐น ++ ๐บ) โf ๐
((0..^(โฏโ(๐น ++ ๐บ))) ร {๐พ}))) |
44 | | eqid 2733 |
. . . . 5
โข
((0..^((โฏโ๐น) + (โฏโ๐บ))) ร {๐พ}) = ((0..^((โฏโ๐น) + (โฏโ๐บ))) ร {๐พ}) |
45 | | ccatlen 14525 |
. . . . . . . 8
โข ((๐น โ Word ๐ โง ๐บ โ Word ๐) โ (โฏโ(๐น ++ ๐บ)) = ((โฏโ๐น) + (โฏโ๐บ))) |
46 | 1, 2, 45 | syl2anc 585 |
. . . . . . 7
โข (๐ โ (โฏโ(๐น ++ ๐บ)) = ((โฏโ๐น) + (โฏโ๐บ))) |
47 | 46 | oveq2d 7425 |
. . . . . 6
โข (๐ โ (0..^(โฏโ(๐น ++ ๐บ))) = (0..^((โฏโ๐น) + (โฏโ๐บ)))) |
48 | 47 | xpeq1d 5706 |
. . . . 5
โข (๐ โ
((0..^(โฏโ(๐น ++
๐บ))) ร {๐พ}) = ((0..^((โฏโ๐น) + (โฏโ๐บ))) ร {๐พ})) |
49 | | eqid 2733 |
. . . . . 6
โข
((0..^(โฏโ๐น)) ร {๐พ}) = ((0..^(โฏโ๐น)) ร {๐พ}) |
50 | | eqid 2733 |
. . . . . 6
โข
((0..^(โฏโ๐บ)) ร {๐พ}) = ((0..^(โฏโ๐บ)) ร {๐พ}) |
51 | 49, 50, 44, 3, 20, 32 | ccatmulgnn0dir 33553 |
. . . . 5
โข (๐ โ
(((0..^(โฏโ๐น))
ร {๐พ}) ++
((0..^(โฏโ๐บ))
ร {๐พ})) =
((0..^((โฏโ๐น) +
(โฏโ๐บ))) ร
{๐พ})) |
52 | 44, 48, 51 | 3eqtr4a 2799 |
. . . 4
โข (๐ โ
((0..^(โฏโ(๐น ++
๐บ))) ร {๐พ}) = (((0..^(โฏโ๐น)) ร {๐พ}) ++ ((0..^(โฏโ๐บ)) ร {๐พ}))) |
53 | 52 | oveq2d 7425 |
. . 3
โข (๐ โ ((๐น ++ ๐บ) โf ๐
((0..^(โฏโ(๐น ++ ๐บ))) ร {๐พ})) = ((๐น ++ ๐บ) โf ๐
(((0..^(โฏโ๐น)) ร {๐พ}) ++ ((0..^(โฏโ๐บ)) ร {๐พ})))) |
54 | 43, 53 | eqtrd 2773 |
. 2
โข (๐ โ ((๐น ++ ๐บ) โf/c ๐
๐พ) = ((๐น ++ ๐บ) โf ๐
(((0..^(โฏโ๐น)) ร {๐พ}) ++ ((0..^(โฏโ๐บ)) ร {๐พ})))) |
55 | | wrdf 14469 |
. . . . 5
โข (๐น โ Word ๐ โ ๐น:(0..^(โฏโ๐น))โถ๐) |
56 | 1, 55 | syl 17 |
. . . 4
โข (๐ โ ๐น:(0..^(โฏโ๐น))โถ๐) |
57 | | ovexd 7444 |
. . . 4
โข (๐ โ (0..^(โฏโ๐น)) โ V) |
58 | 56, 57, 3 | ofcof 33105 |
. . 3
โข (๐ โ (๐น โf/c ๐
๐พ) = (๐น โf ๐
((0..^(โฏโ๐น)) ร {๐พ}))) |
59 | | wrdf 14469 |
. . . . 5
โข (๐บ โ Word ๐ โ ๐บ:(0..^(โฏโ๐บ))โถ๐) |
60 | 2, 59 | syl 17 |
. . . 4
โข (๐ โ ๐บ:(0..^(โฏโ๐บ))โถ๐) |
61 | | ovexd 7444 |
. . . 4
โข (๐ โ (0..^(โฏโ๐บ)) โ V) |
62 | 60, 61, 3 | ofcof 33105 |
. . 3
โข (๐ โ (๐บ โf/c ๐
๐พ) = (๐บ โf ๐
((0..^(โฏโ๐บ)) ร {๐พ}))) |
63 | 58, 62 | oveq12d 7427 |
. 2
โข (๐ โ ((๐น โf/c ๐
๐พ) ++ (๐บ โf/c ๐
๐พ)) = ((๐น โf ๐
((0..^(โฏโ๐น)) ร {๐พ})) ++ (๐บ โf ๐
((0..^(โฏโ๐บ)) ร {๐พ})))) |
64 | 37, 54, 63 | 3eqtr4d 2783 |
1
โข (๐ โ ((๐น ++ ๐บ) โf/c ๐
๐พ) = ((๐น โf/c ๐
๐พ) ++ (๐บ โf/c ๐
๐พ))) |