Step | Hyp | Ref
| Expression |
1 | | sumeq1 11362 |
. . 3
โข (๐ค = โ
โ ฮฃ๐ โ ๐ค ๐ต = ฮฃ๐ โ โ
๐ต) |
2 | | fveq2 5515 |
. . . 4
โข (๐ค = โ
โ
(โฏโ๐ค) =
(โฏโโ
)) |
3 | 2 | oveq1d 5889 |
. . 3
โข (๐ค = โ
โ
((โฏโ๐ค) ยท
๐ต) =
((โฏโโ
) ยท ๐ต)) |
4 | 1, 3 | eqeq12d 2192 |
. 2
โข (๐ค = โ
โ (ฮฃ๐ โ ๐ค ๐ต = ((โฏโ๐ค) ยท ๐ต) โ ฮฃ๐ โ โ
๐ต = ((โฏโโ
) ยท ๐ต))) |
5 | | sumeq1 11362 |
. . 3
โข (๐ค = ๐ฆ โ ฮฃ๐ โ ๐ค ๐ต = ฮฃ๐ โ ๐ฆ ๐ต) |
6 | | fveq2 5515 |
. . . 4
โข (๐ค = ๐ฆ โ (โฏโ๐ค) = (โฏโ๐ฆ)) |
7 | 6 | oveq1d 5889 |
. . 3
โข (๐ค = ๐ฆ โ ((โฏโ๐ค) ยท ๐ต) = ((โฏโ๐ฆ) ยท ๐ต)) |
8 | 5, 7 | eqeq12d 2192 |
. 2
โข (๐ค = ๐ฆ โ (ฮฃ๐ โ ๐ค ๐ต = ((โฏโ๐ค) ยท ๐ต) โ ฮฃ๐ โ ๐ฆ ๐ต = ((โฏโ๐ฆ) ยท ๐ต))) |
9 | | sumeq1 11362 |
. . 3
โข (๐ค = (๐ฆ โช {๐ง}) โ ฮฃ๐ โ ๐ค ๐ต = ฮฃ๐ โ (๐ฆ โช {๐ง})๐ต) |
10 | | fveq2 5515 |
. . . 4
โข (๐ค = (๐ฆ โช {๐ง}) โ (โฏโ๐ค) = (โฏโ(๐ฆ โช {๐ง}))) |
11 | 10 | oveq1d 5889 |
. . 3
โข (๐ค = (๐ฆ โช {๐ง}) โ ((โฏโ๐ค) ยท ๐ต) = ((โฏโ(๐ฆ โช {๐ง})) ยท ๐ต)) |
12 | 9, 11 | eqeq12d 2192 |
. 2
โข (๐ค = (๐ฆ โช {๐ง}) โ (ฮฃ๐ โ ๐ค ๐ต = ((โฏโ๐ค) ยท ๐ต) โ ฮฃ๐ โ (๐ฆ โช {๐ง})๐ต = ((โฏโ(๐ฆ โช {๐ง})) ยท ๐ต))) |
13 | | sumeq1 11362 |
. . 3
โข (๐ค = ๐ด โ ฮฃ๐ โ ๐ค ๐ต = ฮฃ๐ โ ๐ด ๐ต) |
14 | | fveq2 5515 |
. . . 4
โข (๐ค = ๐ด โ (โฏโ๐ค) = (โฏโ๐ด)) |
15 | 14 | oveq1d 5889 |
. . 3
โข (๐ค = ๐ด โ ((โฏโ๐ค) ยท ๐ต) = ((โฏโ๐ด) ยท ๐ต)) |
16 | 13, 15 | eqeq12d 2192 |
. 2
โข (๐ค = ๐ด โ (ฮฃ๐ โ ๐ค ๐ต = ((โฏโ๐ค) ยท ๐ต) โ ฮฃ๐ โ ๐ด ๐ต = ((โฏโ๐ด) ยท ๐ต))) |
17 | | sum0 11395 |
. . 3
โข
ฮฃ๐ โ
โ
๐ต =
0 |
18 | | hash0 10775 |
. . . . 5
โข
(โฏโโ
) = 0 |
19 | 18 | oveq1i 5884 |
. . . 4
โข
((โฏโโ
) ยท ๐ต) = (0 ยท ๐ต) |
20 | | simpr 110 |
. . . . 5
โข ((๐ด โ Fin โง ๐ต โ โ) โ ๐ต โ
โ) |
21 | 20 | mul02d 8348 |
. . . 4
โข ((๐ด โ Fin โง ๐ต โ โ) โ (0
ยท ๐ต) =
0) |
22 | 19, 21 | eqtrid 2222 |
. . 3
โข ((๐ด โ Fin โง ๐ต โ โ) โ
((โฏโโ
) ยท ๐ต) = 0) |
23 | 17, 22 | eqtr4id 2229 |
. 2
โข ((๐ด โ Fin โง ๐ต โ โ) โ
ฮฃ๐ โ โ
๐ต =
((โฏโโ
) ยท ๐ต)) |
24 | | simpr 110 |
. . . . . 6
โข
(((((๐ด โ Fin
โง ๐ต โ โ)
โง ๐ฆ โ Fin) โง
(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ฮฃ๐ โ ๐ฆ ๐ต = ((โฏโ๐ฆ) ยท ๐ต)) โ ฮฃ๐ โ ๐ฆ ๐ต = ((โฏโ๐ฆ) ยท ๐ต)) |
25 | | vex 2740 |
. . . . . . . 8
โข ๐ง โ V |
26 | | eqidd 2178 |
. . . . . . . . 9
โข (๐ = ๐ง โ ๐ต = ๐ต) |
27 | 26 | sumsn 11418 |
. . . . . . . 8
โข ((๐ง โ V โง ๐ต โ โ) โ
ฮฃ๐ โ {๐ง}๐ต = ๐ต) |
28 | 25, 27 | mpan 424 |
. . . . . . 7
โข (๐ต โ โ โ
ฮฃ๐ โ {๐ง}๐ต = ๐ต) |
29 | 28 | ad4antlr 495 |
. . . . . 6
โข
(((((๐ด โ Fin
โง ๐ต โ โ)
โง ๐ฆ โ Fin) โง
(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ฮฃ๐ โ ๐ฆ ๐ต = ((โฏโ๐ฆ) ยท ๐ต)) โ ฮฃ๐ โ {๐ง}๐ต = ๐ต) |
30 | 24, 29 | oveq12d 5892 |
. . . . 5
โข
(((((๐ด โ Fin
โง ๐ต โ โ)
โง ๐ฆ โ Fin) โง
(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ฮฃ๐ โ ๐ฆ ๐ต = ((โฏโ๐ฆ) ยท ๐ต)) โ (ฮฃ๐ โ ๐ฆ ๐ต + ฮฃ๐ โ {๐ง}๐ต) = (((โฏโ๐ฆ) ยท ๐ต) + ๐ต)) |
31 | | simprr 531 |
. . . . . . . . 9
โข ((((๐ด โ Fin โง ๐ต โ โ) โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐ง โ (๐ด โ ๐ฆ)) |
32 | 31 | eldifbd 3141 |
. . . . . . . 8
โข ((((๐ด โ Fin โง ๐ต โ โ) โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ยฌ ๐ง โ ๐ฆ) |
33 | | disjsn 3654 |
. . . . . . . 8
โข ((๐ฆ โฉ {๐ง}) = โ
โ ยฌ ๐ง โ ๐ฆ) |
34 | 32, 33 | sylibr 134 |
. . . . . . 7
โข ((((๐ด โ Fin โง ๐ต โ โ) โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (๐ฆ โฉ {๐ง}) = โ
) |
35 | | eqidd 2178 |
. . . . . . 7
โข ((((๐ด โ Fin โง ๐ต โ โ) โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (๐ฆ โช {๐ง}) = (๐ฆ โช {๐ง})) |
36 | | simplr 528 |
. . . . . . . 8
โข ((((๐ด โ Fin โง ๐ต โ โ) โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐ฆ โ Fin) |
37 | | snfig 6813 |
. . . . . . . . . 10
โข (๐ง โ V โ {๐ง} โ Fin) |
38 | 37 | elv 2741 |
. . . . . . . . 9
โข {๐ง} โ Fin |
39 | 38 | a1i 9 |
. . . . . . . 8
โข ((((๐ด โ Fin โง ๐ต โ โ) โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ {๐ง} โ Fin) |
40 | | unfidisj 6920 |
. . . . . . . 8
โข ((๐ฆ โ Fin โง {๐ง} โ Fin โง (๐ฆ โฉ {๐ง}) = โ
) โ (๐ฆ โช {๐ง}) โ Fin) |
41 | 36, 39, 34, 40 | syl3anc 1238 |
. . . . . . 7
โข ((((๐ด โ Fin โง ๐ต โ โ) โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (๐ฆ โช {๐ง}) โ Fin) |
42 | | simp-4r 542 |
. . . . . . 7
โข
(((((๐ด โ Fin
โง ๐ต โ โ)
โง ๐ฆ โ Fin) โง
(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ (๐ฆ โช {๐ง})) โ ๐ต โ โ) |
43 | 34, 35, 41, 42 | fsumsplit 11414 |
. . . . . 6
โข ((((๐ด โ Fin โง ๐ต โ โ) โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ฮฃ๐ โ (๐ฆ โช {๐ง})๐ต = (ฮฃ๐ โ ๐ฆ ๐ต + ฮฃ๐ โ {๐ง}๐ต)) |
44 | 43 | adantr 276 |
. . . . 5
โข
(((((๐ด โ Fin
โง ๐ต โ โ)
โง ๐ฆ โ Fin) โง
(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ฮฃ๐ โ ๐ฆ ๐ต = ((โฏโ๐ฆ) ยท ๐ต)) โ ฮฃ๐ โ (๐ฆ โช {๐ง})๐ต = (ฮฃ๐ โ ๐ฆ ๐ต + ฮฃ๐ โ {๐ง}๐ต)) |
45 | | hashcl 10760 |
. . . . . . . 8
โข (๐ฆ โ Fin โ
(โฏโ๐ฆ) โ
โ0) |
46 | 45 | ad3antlr 493 |
. . . . . . 7
โข
(((((๐ด โ Fin
โง ๐ต โ โ)
โง ๐ฆ โ Fin) โง
(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ฮฃ๐ โ ๐ฆ ๐ต = ((โฏโ๐ฆ) ยท ๐ต)) โ (โฏโ๐ฆ) โ
โ0) |
47 | 46 | nn0cnd 9230 |
. . . . . 6
โข
(((((๐ด โ Fin
โง ๐ต โ โ)
โง ๐ฆ โ Fin) โง
(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ฮฃ๐ โ ๐ฆ ๐ต = ((โฏโ๐ฆ) ยท ๐ต)) โ (โฏโ๐ฆ) โ โ) |
48 | | simp-4r 542 |
. . . . . 6
โข
(((((๐ด โ Fin
โง ๐ต โ โ)
โง ๐ฆ โ Fin) โง
(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ฮฃ๐ โ ๐ฆ ๐ต = ((โฏโ๐ฆ) ยท ๐ต)) โ ๐ต โ โ) |
49 | 47, 48 | adddirp1d 7983 |
. . . . 5
โข
(((((๐ด โ Fin
โง ๐ต โ โ)
โง ๐ฆ โ Fin) โง
(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ฮฃ๐ โ ๐ฆ ๐ต = ((โฏโ๐ฆ) ยท ๐ต)) โ (((โฏโ๐ฆ) + 1) ยท ๐ต) = (((โฏโ๐ฆ) ยท ๐ต) + ๐ต)) |
50 | 30, 44, 49 | 3eqtr4d 2220 |
. . . 4
โข
(((((๐ด โ Fin
โง ๐ต โ โ)
โง ๐ฆ โ Fin) โง
(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ฮฃ๐ โ ๐ฆ ๐ต = ((โฏโ๐ฆ) ยท ๐ต)) โ ฮฃ๐ โ (๐ฆ โช {๐ง})๐ต = (((โฏโ๐ฆ) + 1) ยท ๐ต)) |
51 | 36 | adantr 276 |
. . . . . . 7
โข
(((((๐ด โ Fin
โง ๐ต โ โ)
โง ๐ฆ โ Fin) โง
(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ฮฃ๐ โ ๐ฆ ๐ต = ((โฏโ๐ฆ) ยท ๐ต)) โ ๐ฆ โ Fin) |
52 | 38 | a1i 9 |
. . . . . . 7
โข
(((((๐ด โ Fin
โง ๐ต โ โ)
โง ๐ฆ โ Fin) โง
(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ฮฃ๐ โ ๐ฆ ๐ต = ((โฏโ๐ฆ) ยท ๐ต)) โ {๐ง} โ Fin) |
53 | 34 | adantr 276 |
. . . . . . 7
โข
(((((๐ด โ Fin
โง ๐ต โ โ)
โง ๐ฆ โ Fin) โง
(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ฮฃ๐ โ ๐ฆ ๐ต = ((โฏโ๐ฆ) ยท ๐ต)) โ (๐ฆ โฉ {๐ง}) = โ
) |
54 | | hashun 10784 |
. . . . . . 7
โข ((๐ฆ โ Fin โง {๐ง} โ Fin โง (๐ฆ โฉ {๐ง}) = โ
) โ (โฏโ(๐ฆ โช {๐ง})) = ((โฏโ๐ฆ) + (โฏโ{๐ง}))) |
55 | 51, 52, 53, 54 | syl3anc 1238 |
. . . . . 6
โข
(((((๐ด โ Fin
โง ๐ต โ โ)
โง ๐ฆ โ Fin) โง
(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ฮฃ๐ โ ๐ฆ ๐ต = ((โฏโ๐ฆ) ยท ๐ต)) โ (โฏโ(๐ฆ โช {๐ง})) = ((โฏโ๐ฆ) + (โฏโ{๐ง}))) |
56 | | hashsng 10777 |
. . . . . . . 8
โข (๐ง โ V โ
(โฏโ{๐ง}) =
1) |
57 | 56 | elv 2741 |
. . . . . . 7
โข
(โฏโ{๐ง})
= 1 |
58 | 57 | oveq2i 5885 |
. . . . . 6
โข
((โฏโ๐ฆ) +
(โฏโ{๐ง})) =
((โฏโ๐ฆ) +
1) |
59 | 55, 58 | eqtrdi 2226 |
. . . . 5
โข
(((((๐ด โ Fin
โง ๐ต โ โ)
โง ๐ฆ โ Fin) โง
(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ฮฃ๐ โ ๐ฆ ๐ต = ((โฏโ๐ฆ) ยท ๐ต)) โ (โฏโ(๐ฆ โช {๐ง})) = ((โฏโ๐ฆ) + 1)) |
60 | 59 | oveq1d 5889 |
. . . 4
โข
(((((๐ด โ Fin
โง ๐ต โ โ)
โง ๐ฆ โ Fin) โง
(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ฮฃ๐ โ ๐ฆ ๐ต = ((โฏโ๐ฆ) ยท ๐ต)) โ ((โฏโ(๐ฆ โช {๐ง})) ยท ๐ต) = (((โฏโ๐ฆ) + 1) ยท ๐ต)) |
61 | 50, 60 | eqtr4d 2213 |
. . 3
โข
(((((๐ด โ Fin
โง ๐ต โ โ)
โง ๐ฆ โ Fin) โง
(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ฮฃ๐ โ ๐ฆ ๐ต = ((โฏโ๐ฆ) ยท ๐ต)) โ ฮฃ๐ โ (๐ฆ โช {๐ง})๐ต = ((โฏโ(๐ฆ โช {๐ง})) ยท ๐ต)) |
62 | 61 | ex 115 |
. 2
โข ((((๐ด โ Fin โง ๐ต โ โ) โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (ฮฃ๐ โ ๐ฆ ๐ต = ((โฏโ๐ฆ) ยท ๐ต) โ ฮฃ๐ โ (๐ฆ โช {๐ง})๐ต = ((โฏโ(๐ฆ โช {๐ง})) ยท ๐ต))) |
63 | | simpl 109 |
. 2
โข ((๐ด โ Fin โง ๐ต โ โ) โ ๐ด โ Fin) |
64 | 4, 8, 12, 16, 23, 62, 63 | findcard2sd 6891 |
1
โข ((๐ด โ Fin โง ๐ต โ โ) โ
ฮฃ๐ โ ๐ด ๐ต = ((โฏโ๐ด) ยท ๐ต)) |