Step | Hyp | Ref
| Expression |
1 | | xpeq1 5652 |
. . . 4
โข (๐ฅ = โ
โ (๐ฅ ร ๐ต) = (โ
ร ๐ต)) |
2 | 1 | fveq2d 6851 |
. . 3
โข (๐ฅ = โ
โ
(โฏโ(๐ฅ ร
๐ต)) =
(โฏโ(โ
ร ๐ต))) |
3 | | fveq2 6847 |
. . . 4
โข (๐ฅ = โ
โ
(โฏโ๐ฅ) =
(โฏโโ
)) |
4 | 3 | oveq1d 7377 |
. . 3
โข (๐ฅ = โ
โ
((โฏโ๐ฅ) ยท
(โฏโ๐ต)) =
((โฏโโ
) ยท (โฏโ๐ต))) |
5 | 2, 4 | eqeq12d 2753 |
. 2
โข (๐ฅ = โ
โ
((โฏโ(๐ฅ ร
๐ต)) = ((โฏโ๐ฅ) ยท (โฏโ๐ต)) โ
(โฏโ(โ
ร ๐ต)) = ((โฏโโ
) ยท
(โฏโ๐ต)))) |
6 | | xpeq1 5652 |
. . . 4
โข (๐ฅ = ๐ฆ โ (๐ฅ ร ๐ต) = (๐ฆ ร ๐ต)) |
7 | 6 | fveq2d 6851 |
. . 3
โข (๐ฅ = ๐ฆ โ (โฏโ(๐ฅ ร ๐ต)) = (โฏโ(๐ฆ ร ๐ต))) |
8 | | fveq2 6847 |
. . . 4
โข (๐ฅ = ๐ฆ โ (โฏโ๐ฅ) = (โฏโ๐ฆ)) |
9 | 8 | oveq1d 7377 |
. . 3
โข (๐ฅ = ๐ฆ โ ((โฏโ๐ฅ) ยท (โฏโ๐ต)) = ((โฏโ๐ฆ) ยท (โฏโ๐ต))) |
10 | 7, 9 | eqeq12d 2753 |
. 2
โข (๐ฅ = ๐ฆ โ ((โฏโ(๐ฅ ร ๐ต)) = ((โฏโ๐ฅ) ยท (โฏโ๐ต)) โ (โฏโ(๐ฆ ร ๐ต)) = ((โฏโ๐ฆ) ยท (โฏโ๐ต)))) |
11 | | xpeq1 5652 |
. . . 4
โข (๐ฅ = (๐ฆ โช {๐ง}) โ (๐ฅ ร ๐ต) = ((๐ฆ โช {๐ง}) ร ๐ต)) |
12 | 11 | fveq2d 6851 |
. . 3
โข (๐ฅ = (๐ฆ โช {๐ง}) โ (โฏโ(๐ฅ ร ๐ต)) = (โฏโ((๐ฆ โช {๐ง}) ร ๐ต))) |
13 | | fveq2 6847 |
. . . 4
โข (๐ฅ = (๐ฆ โช {๐ง}) โ (โฏโ๐ฅ) = (โฏโ(๐ฆ โช {๐ง}))) |
14 | 13 | oveq1d 7377 |
. . 3
โข (๐ฅ = (๐ฆ โช {๐ง}) โ ((โฏโ๐ฅ) ยท (โฏโ๐ต)) = ((โฏโ(๐ฆ โช {๐ง})) ยท (โฏโ๐ต))) |
15 | 12, 14 | eqeq12d 2753 |
. 2
โข (๐ฅ = (๐ฆ โช {๐ง}) โ ((โฏโ(๐ฅ ร ๐ต)) = ((โฏโ๐ฅ) ยท (โฏโ๐ต)) โ (โฏโ((๐ฆ โช {๐ง}) ร ๐ต)) = ((โฏโ(๐ฆ โช {๐ง})) ยท (โฏโ๐ต)))) |
16 | | xpeq1 5652 |
. . . 4
โข (๐ฅ = ๐ด โ (๐ฅ ร ๐ต) = (๐ด ร ๐ต)) |
17 | 16 | fveq2d 6851 |
. . 3
โข (๐ฅ = ๐ด โ (โฏโ(๐ฅ ร ๐ต)) = (โฏโ(๐ด ร ๐ต))) |
18 | | fveq2 6847 |
. . . 4
โข (๐ฅ = ๐ด โ (โฏโ๐ฅ) = (โฏโ๐ด)) |
19 | 18 | oveq1d 7377 |
. . 3
โข (๐ฅ = ๐ด โ ((โฏโ๐ฅ) ยท (โฏโ๐ต)) = ((โฏโ๐ด) ยท (โฏโ๐ต))) |
20 | 17, 19 | eqeq12d 2753 |
. 2
โข (๐ฅ = ๐ด โ ((โฏโ(๐ฅ ร ๐ต)) = ((โฏโ๐ฅ) ยท (โฏโ๐ต)) โ (โฏโ(๐ด ร ๐ต)) = ((โฏโ๐ด) ยท (โฏโ๐ต)))) |
21 | | hashxplem.1 |
. . . 4
โข ๐ต โ Fin |
22 | | hashcl 14263 |
. . . . . 6
โข (๐ต โ Fin โ
(โฏโ๐ต) โ
โ0) |
23 | 22 | nn0cnd 12482 |
. . . . 5
โข (๐ต โ Fin โ
(โฏโ๐ต) โ
โ) |
24 | 23 | mul02d 11360 |
. . . 4
โข (๐ต โ Fin โ (0 ยท
(โฏโ๐ต)) =
0) |
25 | 21, 24 | ax-mp 5 |
. . 3
โข (0
ยท (โฏโ๐ต))
= 0 |
26 | | hash0 14274 |
. . . 4
โข
(โฏโโ
) = 0 |
27 | 26 | oveq1i 7372 |
. . 3
โข
((โฏโโ
) ยท (โฏโ๐ต)) = (0 ยท (โฏโ๐ต)) |
28 | | 0xp 5735 |
. . . . 5
โข (โ
ร ๐ต) =
โ
|
29 | 28 | fveq2i 6850 |
. . . 4
โข
(โฏโ(โ
ร ๐ต)) =
(โฏโโ
) |
30 | 29, 26 | eqtri 2765 |
. . 3
โข
(โฏโ(โ
ร ๐ต)) = 0 |
31 | 25, 27, 30 | 3eqtr4ri 2776 |
. 2
โข
(โฏโ(โ
ร ๐ต)) = ((โฏโโ
) ยท
(โฏโ๐ต)) |
32 | | oveq1 7369 |
. . . . 5
โข
((โฏโ(๐ฆ
ร ๐ต)) =
((โฏโ๐ฆ) ยท
(โฏโ๐ต)) โ
((โฏโ(๐ฆ ร
๐ต)) + (โฏโ๐ต)) = (((โฏโ๐ฆ) ยท (โฏโ๐ต)) + (โฏโ๐ต))) |
33 | 32 | adantl 483 |
. . . 4
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง (โฏโ(๐ฆ ร ๐ต)) = ((โฏโ๐ฆ) ยท (โฏโ๐ต))) โ ((โฏโ(๐ฆ ร ๐ต)) + (โฏโ๐ต)) = (((โฏโ๐ฆ) ยท (โฏโ๐ต)) + (โฏโ๐ต))) |
34 | | xpundir 5706 |
. . . . . . 7
โข ((๐ฆ โช {๐ง}) ร ๐ต) = ((๐ฆ ร ๐ต) โช ({๐ง} ร ๐ต)) |
35 | 34 | fveq2i 6850 |
. . . . . 6
โข
(โฏโ((๐ฆ
โช {๐ง}) ร ๐ต)) = (โฏโ((๐ฆ ร ๐ต) โช ({๐ง} ร ๐ต))) |
36 | | xpfi 9268 |
. . . . . . . . 9
โข ((๐ฆ โ Fin โง ๐ต โ Fin) โ (๐ฆ ร ๐ต) โ Fin) |
37 | 21, 36 | mpan2 690 |
. . . . . . . 8
โข (๐ฆ โ Fin โ (๐ฆ ร ๐ต) โ Fin) |
38 | | inxp 5793 |
. . . . . . . . 9
โข ((๐ฆ ร ๐ต) โฉ ({๐ง} ร ๐ต)) = ((๐ฆ โฉ {๐ง}) ร (๐ต โฉ ๐ต)) |
39 | | disjsn 4677 |
. . . . . . . . . . . 12
โข ((๐ฆ โฉ {๐ง}) = โ
โ ยฌ ๐ง โ ๐ฆ) |
40 | 39 | biimpri 227 |
. . . . . . . . . . 11
โข (ยฌ
๐ง โ ๐ฆ โ (๐ฆ โฉ {๐ง}) = โ
) |
41 | 40 | xpeq1d 5667 |
. . . . . . . . . 10
โข (ยฌ
๐ง โ ๐ฆ โ ((๐ฆ โฉ {๐ง}) ร (๐ต โฉ ๐ต)) = (โ
ร (๐ต โฉ ๐ต))) |
42 | | 0xp 5735 |
. . . . . . . . . 10
โข (โ
ร (๐ต โฉ ๐ต)) = โ
|
43 | 41, 42 | eqtrdi 2793 |
. . . . . . . . 9
โข (ยฌ
๐ง โ ๐ฆ โ ((๐ฆ โฉ {๐ง}) ร (๐ต โฉ ๐ต)) = โ
) |
44 | 38, 43 | eqtrid 2789 |
. . . . . . . 8
โข (ยฌ
๐ง โ ๐ฆ โ ((๐ฆ ร ๐ต) โฉ ({๐ง} ร ๐ต)) = โ
) |
45 | | snfi 8995 |
. . . . . . . . . 10
โข {๐ง} โ Fin |
46 | | xpfi 9268 |
. . . . . . . . . 10
โข (({๐ง} โ Fin โง ๐ต โ Fin) โ ({๐ง} ร ๐ต) โ Fin) |
47 | 45, 21, 46 | mp2an 691 |
. . . . . . . . 9
โข ({๐ง} ร ๐ต) โ Fin |
48 | | hashun 14289 |
. . . . . . . . 9
โข (((๐ฆ ร ๐ต) โ Fin โง ({๐ง} ร ๐ต) โ Fin โง ((๐ฆ ร ๐ต) โฉ ({๐ง} ร ๐ต)) = โ
) โ (โฏโ((๐ฆ ร ๐ต) โช ({๐ง} ร ๐ต))) = ((โฏโ(๐ฆ ร ๐ต)) + (โฏโ({๐ง} ร ๐ต)))) |
49 | 47, 48 | mp3an2 1450 |
. . . . . . . 8
โข (((๐ฆ ร ๐ต) โ Fin โง ((๐ฆ ร ๐ต) โฉ ({๐ง} ร ๐ต)) = โ
) โ (โฏโ((๐ฆ ร ๐ต) โช ({๐ง} ร ๐ต))) = ((โฏโ(๐ฆ ร ๐ต)) + (โฏโ({๐ง} ร ๐ต)))) |
50 | 37, 44, 49 | syl2an 597 |
. . . . . . 7
โข ((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โ (โฏโ((๐ฆ ร ๐ต) โช ({๐ง} ร ๐ต))) = ((โฏโ(๐ฆ ร ๐ต)) + (โฏโ({๐ง} ร ๐ต)))) |
51 | | snex 5393 |
. . . . . . . . . . 11
โข {๐ง} โ V |
52 | 21 | elexi 3467 |
. . . . . . . . . . 11
โข ๐ต โ V |
53 | 51, 52 | xpcomen 9014 |
. . . . . . . . . 10
โข ({๐ง} ร ๐ต) โ (๐ต ร {๐ง}) |
54 | | vex 3452 |
. . . . . . . . . . 11
โข ๐ง โ V |
55 | 52, 54 | xpsnen 9006 |
. . . . . . . . . 10
โข (๐ต ร {๐ง}) โ ๐ต |
56 | 53, 55 | entri 8955 |
. . . . . . . . 9
โข ({๐ง} ร ๐ต) โ ๐ต |
57 | | hashen 14254 |
. . . . . . . . . 10
โข ((({๐ง} ร ๐ต) โ Fin โง ๐ต โ Fin) โ ((โฏโ({๐ง} ร ๐ต)) = (โฏโ๐ต) โ ({๐ง} ร ๐ต) โ ๐ต)) |
58 | 47, 21, 57 | mp2an 691 |
. . . . . . . . 9
โข
((โฏโ({๐ง}
ร ๐ต)) =
(โฏโ๐ต) โ
({๐ง} ร ๐ต) โ ๐ต) |
59 | 56, 58 | mpbir 230 |
. . . . . . . 8
โข
(โฏโ({๐ง}
ร ๐ต)) =
(โฏโ๐ต) |
60 | 59 | oveq2i 7373 |
. . . . . . 7
โข
((โฏโ(๐ฆ
ร ๐ต)) +
(โฏโ({๐ง} ร
๐ต))) =
((โฏโ(๐ฆ ร
๐ต)) + (โฏโ๐ต)) |
61 | 50, 60 | eqtrdi 2793 |
. . . . . 6
โข ((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โ (โฏโ((๐ฆ ร ๐ต) โช ({๐ง} ร ๐ต))) = ((โฏโ(๐ฆ ร ๐ต)) + (โฏโ๐ต))) |
62 | 35, 61 | eqtrid 2789 |
. . . . 5
โข ((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โ (โฏโ((๐ฆ โช {๐ง}) ร ๐ต)) = ((โฏโ(๐ฆ ร ๐ต)) + (โฏโ๐ต))) |
63 | 62 | adantr 482 |
. . . 4
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง (โฏโ(๐ฆ ร ๐ต)) = ((โฏโ๐ฆ) ยท (โฏโ๐ต))) โ (โฏโ((๐ฆ โช {๐ง}) ร ๐ต)) = ((โฏโ(๐ฆ ร ๐ต)) + (โฏโ๐ต))) |
64 | | hashunsng 14299 |
. . . . . . . 8
โข (๐ง โ V โ ((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โ (โฏโ(๐ฆ โช {๐ง})) = ((โฏโ๐ฆ) + 1))) |
65 | 54, 64 | ax-mp 5 |
. . . . . . 7
โข ((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โ (โฏโ(๐ฆ โช {๐ง})) = ((โฏโ๐ฆ) + 1)) |
66 | 65 | oveq1d 7377 |
. . . . . 6
โข ((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โ ((โฏโ(๐ฆ โช {๐ง})) ยท (โฏโ๐ต)) = (((โฏโ๐ฆ) + 1) ยท (โฏโ๐ต))) |
67 | | hashcl 14263 |
. . . . . . . . . 10
โข (๐ฆ โ Fin โ
(โฏโ๐ฆ) โ
โ0) |
68 | 67 | nn0cnd 12482 |
. . . . . . . . 9
โข (๐ฆ โ Fin โ
(โฏโ๐ฆ) โ
โ) |
69 | | ax-1cn 11116 |
. . . . . . . . . 10
โข 1 โ
โ |
70 | | nn0cn 12430 |
. . . . . . . . . . 11
โข
((โฏโ๐ต)
โ โ0 โ (โฏโ๐ต) โ โ) |
71 | 21, 22, 70 | mp2b 10 |
. . . . . . . . . 10
โข
(โฏโ๐ต)
โ โ |
72 | | adddir 11153 |
. . . . . . . . . 10
โข
(((โฏโ๐ฆ)
โ โ โง 1 โ โ โง (โฏโ๐ต) โ โ) โ
(((โฏโ๐ฆ) + 1)
ยท (โฏโ๐ต))
= (((โฏโ๐ฆ)
ยท (โฏโ๐ต))
+ (1 ยท (โฏโ๐ต)))) |
73 | 69, 71, 72 | mp3an23 1454 |
. . . . . . . . 9
โข
((โฏโ๐ฆ)
โ โ โ (((โฏโ๐ฆ) + 1) ยท (โฏโ๐ต)) = (((โฏโ๐ฆ) ยท (โฏโ๐ต)) + (1 ยท
(โฏโ๐ต)))) |
74 | 68, 73 | syl 17 |
. . . . . . . 8
โข (๐ฆ โ Fin โ
(((โฏโ๐ฆ) + 1)
ยท (โฏโ๐ต))
= (((โฏโ๐ฆ)
ยท (โฏโ๐ต))
+ (1 ยท (โฏโ๐ต)))) |
75 | 71 | mulid2i 11167 |
. . . . . . . . 9
โข (1
ยท (โฏโ๐ต))
= (โฏโ๐ต) |
76 | 75 | oveq2i 7373 |
. . . . . . . 8
โข
(((โฏโ๐ฆ)
ยท (โฏโ๐ต))
+ (1 ยท (โฏโ๐ต))) = (((โฏโ๐ฆ) ยท (โฏโ๐ต)) + (โฏโ๐ต)) |
77 | 74, 76 | eqtrdi 2793 |
. . . . . . 7
โข (๐ฆ โ Fin โ
(((โฏโ๐ฆ) + 1)
ยท (โฏโ๐ต))
= (((โฏโ๐ฆ)
ยท (โฏโ๐ต))
+ (โฏโ๐ต))) |
78 | 77 | adantr 482 |
. . . . . 6
โข ((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โ (((โฏโ๐ฆ) + 1) ยท (โฏโ๐ต)) = (((โฏโ๐ฆ) ยท (โฏโ๐ต)) + (โฏโ๐ต))) |
79 | 66, 78 | eqtrd 2777 |
. . . . 5
โข ((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โ ((โฏโ(๐ฆ โช {๐ง})) ยท (โฏโ๐ต)) = (((โฏโ๐ฆ) ยท (โฏโ๐ต)) + (โฏโ๐ต))) |
80 | 79 | adantr 482 |
. . . 4
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง (โฏโ(๐ฆ ร ๐ต)) = ((โฏโ๐ฆ) ยท (โฏโ๐ต))) โ ((โฏโ(๐ฆ โช {๐ง})) ยท (โฏโ๐ต)) = (((โฏโ๐ฆ) ยท (โฏโ๐ต)) + (โฏโ๐ต))) |
81 | 33, 63, 80 | 3eqtr4d 2787 |
. . 3
โข (((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โง (โฏโ(๐ฆ ร ๐ต)) = ((โฏโ๐ฆ) ยท (โฏโ๐ต))) โ (โฏโ((๐ฆ โช {๐ง}) ร ๐ต)) = ((โฏโ(๐ฆ โช {๐ง})) ยท (โฏโ๐ต))) |
82 | 81 | ex 414 |
. 2
โข ((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โ ((โฏโ(๐ฆ ร ๐ต)) = ((โฏโ๐ฆ) ยท (โฏโ๐ต)) โ (โฏโ((๐ฆ โช {๐ง}) ร ๐ต)) = ((โฏโ(๐ฆ โช {๐ง})) ยท (โฏโ๐ต)))) |
83 | 5, 10, 15, 20, 31, 82 | findcard2s 9116 |
1
โข (๐ด โ Fin โ
(โฏโ(๐ด ร
๐ต)) = ((โฏโ๐ด) ยท (โฏโ๐ต))) |