Step | Hyp | Ref
| Expression |
1 | | prodeq1 11560 |
. . 3
โข (๐ค = โ
โ โ๐ โ ๐ค ๐ต = โ๐ โ โ
๐ต) |
2 | | fveq2 5515 |
. . . 4
โข (๐ค = โ
โ
(โฏโ๐ค) =
(โฏโโ
)) |
3 | 2 | oveq2d 5890 |
. . 3
โข (๐ค = โ
โ (๐ตโ(โฏโ๐ค)) = (๐ตโ(โฏโโ
))) |
4 | 1, 3 | eqeq12d 2192 |
. 2
โข (๐ค = โ
โ (โ๐ โ ๐ค ๐ต = (๐ตโ(โฏโ๐ค)) โ โ๐ โ โ
๐ต = (๐ตโ(โฏโโ
)))) |
5 | | prodeq1 11560 |
. . 3
โข (๐ค = ๐ฆ โ โ๐ โ ๐ค ๐ต = โ๐ โ ๐ฆ ๐ต) |
6 | | fveq2 5515 |
. . . 4
โข (๐ค = ๐ฆ โ (โฏโ๐ค) = (โฏโ๐ฆ)) |
7 | 6 | oveq2d 5890 |
. . 3
โข (๐ค = ๐ฆ โ (๐ตโ(โฏโ๐ค)) = (๐ตโ(โฏโ๐ฆ))) |
8 | 5, 7 | eqeq12d 2192 |
. 2
โข (๐ค = ๐ฆ โ (โ๐ โ ๐ค ๐ต = (๐ตโ(โฏโ๐ค)) โ โ๐ โ ๐ฆ ๐ต = (๐ตโ(โฏโ๐ฆ)))) |
9 | | prodeq1 11560 |
. . 3
โข (๐ค = (๐ฆ โช {๐ง}) โ โ๐ โ ๐ค ๐ต = โ๐ โ (๐ฆ โช {๐ง})๐ต) |
10 | | fveq2 5515 |
. . . 4
โข (๐ค = (๐ฆ โช {๐ง}) โ (โฏโ๐ค) = (โฏโ(๐ฆ โช {๐ง}))) |
11 | 10 | oveq2d 5890 |
. . 3
โข (๐ค = (๐ฆ โช {๐ง}) โ (๐ตโ(โฏโ๐ค)) = (๐ตโ(โฏโ(๐ฆ โช {๐ง})))) |
12 | 9, 11 | eqeq12d 2192 |
. 2
โข (๐ค = (๐ฆ โช {๐ง}) โ (โ๐ โ ๐ค ๐ต = (๐ตโ(โฏโ๐ค)) โ โ๐ โ (๐ฆ โช {๐ง})๐ต = (๐ตโ(โฏโ(๐ฆ โช {๐ง}))))) |
13 | | prodeq1 11560 |
. . 3
โข (๐ค = ๐ด โ โ๐ โ ๐ค ๐ต = โ๐ โ ๐ด ๐ต) |
14 | | fveq2 5515 |
. . . 4
โข (๐ค = ๐ด โ (โฏโ๐ค) = (โฏโ๐ด)) |
15 | 14 | oveq2d 5890 |
. . 3
โข (๐ค = ๐ด โ (๐ตโ(โฏโ๐ค)) = (๐ตโ(โฏโ๐ด))) |
16 | 13, 15 | eqeq12d 2192 |
. 2
โข (๐ค = ๐ด โ (โ๐ โ ๐ค ๐ต = (๐ตโ(โฏโ๐ค)) โ โ๐ โ ๐ด ๐ต = (๐ตโ(โฏโ๐ด)))) |
17 | | prod0 11592 |
. . 3
โข
โ๐ โ
โ
๐ต =
1 |
18 | | hash0 10775 |
. . . . 5
โข
(โฏโโ
) = 0 |
19 | 18 | oveq2i 5885 |
. . . 4
โข (๐ตโ(โฏโโ
)) =
(๐ตโ0) |
20 | | simpr 110 |
. . . . 5
โข ((๐ด โ Fin โง ๐ต โ โ) โ ๐ต โ
โ) |
21 | 20 | exp0d 10647 |
. . . 4
โข ((๐ด โ Fin โง ๐ต โ โ) โ (๐ตโ0) = 1) |
22 | 19, 21 | eqtrid 2222 |
. . 3
โข ((๐ด โ Fin โง ๐ต โ โ) โ (๐ตโ(โฏโโ
)) =
1) |
23 | 17, 22 | eqtr4id 2229 |
. 2
โข ((๐ด โ Fin โง ๐ต โ โ) โ
โ๐ โ โ
๐ต = (๐ตโ(โฏโโ
))) |
24 | | simpr 110 |
. . . . 5
โข
(((((๐ด โ Fin
โง ๐ต โ โ)
โง ๐ฆ โ Fin) โง
(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ ๐ต = (๐ตโ(โฏโ๐ฆ))) โ โ๐ โ ๐ฆ ๐ต = (๐ตโ(โฏโ๐ฆ))) |
25 | 24 | oveq1d 5889 |
. . . 4
โข
(((((๐ด โ Fin
โง ๐ต โ โ)
โง ๐ฆ โ Fin) โง
(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ ๐ต = (๐ตโ(โฏโ๐ฆ))) โ (โ๐ โ ๐ฆ ๐ต ยท ๐ต) = ((๐ตโ(โฏโ๐ฆ)) ยท ๐ต)) |
26 | | nfcv 2319 |
. . . . . . 7
โข
โฒ๐๐ต |
27 | | simplr 528 |
. . . . . . 7
โข ((((๐ด โ Fin โง ๐ต โ โ) โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐ฆ โ Fin) |
28 | | simprr 531 |
. . . . . . 7
โข ((((๐ด โ Fin โง ๐ต โ โ) โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐ง โ (๐ด โ ๐ฆ)) |
29 | 28 | eldifbd 3141 |
. . . . . . 7
โข ((((๐ด โ Fin โง ๐ต โ โ) โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ยฌ ๐ง โ ๐ฆ) |
30 | | simp-4r 542 |
. . . . . . 7
โข
(((((๐ด โ Fin
โง ๐ต โ โ)
โง ๐ฆ โ Fin) โง
(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐ต โ โ) |
31 | | simpllr 534 |
. . . . . . 7
โข ((((๐ด โ Fin โง ๐ต โ โ) โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐ต โ โ) |
32 | | eqidd 2178 |
. . . . . . 7
โข (๐ = ๐ง โ ๐ต = ๐ต) |
33 | 26, 27, 28, 29, 30, 31, 32 | fprodunsn 11611 |
. . . . . 6
โข ((((๐ด โ Fin โง ๐ต โ โ) โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โ๐ โ (๐ฆ โช {๐ง})๐ต = (โ๐ โ ๐ฆ ๐ต ยท ๐ต)) |
34 | 27, 29 | jca 306 |
. . . . . . . . 9
โข ((((๐ด โ Fin โง ๐ต โ โ) โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) |
35 | | hashunsng 10786 |
. . . . . . . . 9
โข (๐ง โ (๐ด โ ๐ฆ) โ ((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โ (โฏโ(๐ฆ โช {๐ง})) = ((โฏโ๐ฆ) + 1))) |
36 | 28, 34, 35 | sylc 62 |
. . . . . . . 8
โข ((((๐ด โ Fin โง ๐ต โ โ) โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (โฏโ(๐ฆ โช {๐ง})) = ((โฏโ๐ฆ) + 1)) |
37 | 36 | oveq2d 5890 |
. . . . . . 7
โข ((((๐ด โ Fin โง ๐ต โ โ) โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (๐ตโ(โฏโ(๐ฆ โช {๐ง}))) = (๐ตโ((โฏโ๐ฆ) + 1))) |
38 | | hashcl 10760 |
. . . . . . . . 9
โข (๐ฆ โ Fin โ
(โฏโ๐ฆ) โ
โ0) |
39 | 27, 38 | syl 14 |
. . . . . . . 8
โข ((((๐ด โ Fin โง ๐ต โ โ) โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (โฏโ๐ฆ) โ
โ0) |
40 | 31, 39 | expp1d 10654 |
. . . . . . 7
โข ((((๐ด โ Fin โง ๐ต โ โ) โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (๐ตโ((โฏโ๐ฆ) + 1)) = ((๐ตโ(โฏโ๐ฆ)) ยท ๐ต)) |
41 | 37, 40 | eqtrd 2210 |
. . . . . 6
โข ((((๐ด โ Fin โง ๐ต โ โ) โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (๐ตโ(โฏโ(๐ฆ โช {๐ง}))) = ((๐ตโ(โฏโ๐ฆ)) ยท ๐ต)) |
42 | 33, 41 | eqeq12d 2192 |
. . . . 5
โข ((((๐ด โ Fin โง ๐ต โ โ) โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (โ๐ โ (๐ฆ โช {๐ง})๐ต = (๐ตโ(โฏโ(๐ฆ โช {๐ง}))) โ (โ๐ โ ๐ฆ ๐ต ยท ๐ต) = ((๐ตโ(โฏโ๐ฆ)) ยท ๐ต))) |
43 | 42 | adantr 276 |
. . . 4
โข
(((((๐ด โ Fin
โง ๐ต โ โ)
โง ๐ฆ โ Fin) โง
(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ ๐ต = (๐ตโ(โฏโ๐ฆ))) โ (โ๐ โ (๐ฆ โช {๐ง})๐ต = (๐ตโ(โฏโ(๐ฆ โช {๐ง}))) โ (โ๐ โ ๐ฆ ๐ต ยท ๐ต) = ((๐ตโ(โฏโ๐ฆ)) ยท ๐ต))) |
44 | 25, 43 | mpbird 167 |
. . 3
โข
(((((๐ด โ Fin
โง ๐ต โ โ)
โง ๐ฆ โ Fin) โง
(๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง โ๐ โ ๐ฆ ๐ต = (๐ตโ(โฏโ๐ฆ))) โ โ๐ โ (๐ฆ โช {๐ง})๐ต = (๐ตโ(โฏโ(๐ฆ โช {๐ง})))) |
45 | 44 | ex 115 |
. 2
โข ((((๐ด โ Fin โง ๐ต โ โ) โง ๐ฆ โ Fin) โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (โ๐ โ ๐ฆ ๐ต = (๐ตโ(โฏโ๐ฆ)) โ โ๐ โ (๐ฆ โช {๐ง})๐ต = (๐ตโ(โฏโ(๐ฆ โช {๐ง}))))) |
46 | | simpl 109 |
. 2
โข ((๐ด โ Fin โง ๐ต โ โ) โ ๐ด โ Fin) |
47 | 4, 8, 12, 16, 23, 45, 46 | findcard2sd 6891 |
1
โข ((๐ด โ Fin โง ๐ต โ โ) โ
โ๐ โ ๐ด ๐ต = (๐ตโ(โฏโ๐ด))) |