Step | Hyp | Ref
| Expression |
1 | | oveq2 7370 |
. . . . . 6
โข (๐ฅ = โ
โ (๐ด โm ๐ฅ) = (๐ด โm
โ
)) |
2 | 1 | fveq2d 6851 |
. . . . 5
โข (๐ฅ = โ
โ
(โฏโ(๐ด
โm ๐ฅ)) =
(โฏโ(๐ด
โm โ
))) |
3 | | fveq2 6847 |
. . . . . 6
โข (๐ฅ = โ
โ
(โฏโ๐ฅ) =
(โฏโโ
)) |
4 | 3 | oveq2d 7378 |
. . . . 5
โข (๐ฅ = โ
โ
((โฏโ๐ด)โ(โฏโ๐ฅ)) = ((โฏโ๐ด)โ(โฏโโ
))) |
5 | 2, 4 | eqeq12d 2753 |
. . . 4
โข (๐ฅ = โ
โ
((โฏโ(๐ด
โm ๐ฅ)) =
((โฏโ๐ด)โ(โฏโ๐ฅ)) โ (โฏโ(๐ด โm โ
)) =
((โฏโ๐ด)โ(โฏโโ
)))) |
6 | 5 | imbi2d 341 |
. . 3
โข (๐ฅ = โ
โ ((๐ด โ Fin โ
(โฏโ(๐ด
โm ๐ฅ)) =
((โฏโ๐ด)โ(โฏโ๐ฅ))) โ (๐ด โ Fin โ (โฏโ(๐ด โm โ
)) =
((โฏโ๐ด)โ(โฏโโ
))))) |
7 | | oveq2 7370 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (๐ด โm ๐ฅ) = (๐ด โm ๐ฆ)) |
8 | 7 | fveq2d 6851 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (โฏโ(๐ด โm ๐ฅ)) = (โฏโ(๐ด โm ๐ฆ))) |
9 | | fveq2 6847 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (โฏโ๐ฅ) = (โฏโ๐ฆ)) |
10 | 9 | oveq2d 7378 |
. . . . 5
โข (๐ฅ = ๐ฆ โ ((โฏโ๐ด)โ(โฏโ๐ฅ)) = ((โฏโ๐ด)โ(โฏโ๐ฆ))) |
11 | 8, 10 | eqeq12d 2753 |
. . . 4
โข (๐ฅ = ๐ฆ โ ((โฏโ(๐ด โm ๐ฅ)) = ((โฏโ๐ด)โ(โฏโ๐ฅ)) โ (โฏโ(๐ด โm ๐ฆ)) = ((โฏโ๐ด)โ(โฏโ๐ฆ)))) |
12 | 11 | imbi2d 341 |
. . 3
โข (๐ฅ = ๐ฆ โ ((๐ด โ Fin โ (โฏโ(๐ด โm ๐ฅ)) = ((โฏโ๐ด)โ(โฏโ๐ฅ))) โ (๐ด โ Fin โ (โฏโ(๐ด โm ๐ฆ)) = ((โฏโ๐ด)โ(โฏโ๐ฆ))))) |
13 | | oveq2 7370 |
. . . . . 6
โข (๐ฅ = (๐ฆ โช {๐ง}) โ (๐ด โm ๐ฅ) = (๐ด โm (๐ฆ โช {๐ง}))) |
14 | 13 | fveq2d 6851 |
. . . . 5
โข (๐ฅ = (๐ฆ โช {๐ง}) โ (โฏโ(๐ด โm ๐ฅ)) = (โฏโ(๐ด โm (๐ฆ โช {๐ง})))) |
15 | | fveq2 6847 |
. . . . . 6
โข (๐ฅ = (๐ฆ โช {๐ง}) โ (โฏโ๐ฅ) = (โฏโ(๐ฆ โช {๐ง}))) |
16 | 15 | oveq2d 7378 |
. . . . 5
โข (๐ฅ = (๐ฆ โช {๐ง}) โ ((โฏโ๐ด)โ(โฏโ๐ฅ)) = ((โฏโ๐ด)โ(โฏโ(๐ฆ โช {๐ง})))) |
17 | 14, 16 | eqeq12d 2753 |
. . . 4
โข (๐ฅ = (๐ฆ โช {๐ง}) โ ((โฏโ(๐ด โm ๐ฅ)) = ((โฏโ๐ด)โ(โฏโ๐ฅ)) โ (โฏโ(๐ด โm (๐ฆ โช {๐ง}))) = ((โฏโ๐ด)โ(โฏโ(๐ฆ โช {๐ง}))))) |
18 | 17 | imbi2d 341 |
. . 3
โข (๐ฅ = (๐ฆ โช {๐ง}) โ ((๐ด โ Fin โ (โฏโ(๐ด โm ๐ฅ)) = ((โฏโ๐ด)โ(โฏโ๐ฅ))) โ (๐ด โ Fin โ (โฏโ(๐ด โm (๐ฆ โช {๐ง}))) = ((โฏโ๐ด)โ(โฏโ(๐ฆ โช {๐ง})))))) |
19 | | oveq2 7370 |
. . . . . 6
โข (๐ฅ = ๐ต โ (๐ด โm ๐ฅ) = (๐ด โm ๐ต)) |
20 | 19 | fveq2d 6851 |
. . . . 5
โข (๐ฅ = ๐ต โ (โฏโ(๐ด โm ๐ฅ)) = (โฏโ(๐ด โm ๐ต))) |
21 | | fveq2 6847 |
. . . . . 6
โข (๐ฅ = ๐ต โ (โฏโ๐ฅ) = (โฏโ๐ต)) |
22 | 21 | oveq2d 7378 |
. . . . 5
โข (๐ฅ = ๐ต โ ((โฏโ๐ด)โ(โฏโ๐ฅ)) = ((โฏโ๐ด)โ(โฏโ๐ต))) |
23 | 20, 22 | eqeq12d 2753 |
. . . 4
โข (๐ฅ = ๐ต โ ((โฏโ(๐ด โm ๐ฅ)) = ((โฏโ๐ด)โ(โฏโ๐ฅ)) โ (โฏโ(๐ด โm ๐ต)) = ((โฏโ๐ด)โ(โฏโ๐ต)))) |
24 | 23 | imbi2d 341 |
. . 3
โข (๐ฅ = ๐ต โ ((๐ด โ Fin โ (โฏโ(๐ด โm ๐ฅ)) = ((โฏโ๐ด)โ(โฏโ๐ฅ))) โ (๐ด โ Fin โ (โฏโ(๐ด โm ๐ต)) = ((โฏโ๐ด)โ(โฏโ๐ต))))) |
25 | | hashcl 14263 |
. . . . . 6
โข (๐ด โ Fin โ
(โฏโ๐ด) โ
โ0) |
26 | 25 | nn0cnd 12482 |
. . . . 5
โข (๐ด โ Fin โ
(โฏโ๐ด) โ
โ) |
27 | 26 | exp0d 14052 |
. . . 4
โข (๐ด โ Fin โ
((โฏโ๐ด)โ0)
= 1) |
28 | | hash0 14274 |
. . . . . 6
โข
(โฏโโ
) = 0 |
29 | 28 | oveq2i 7373 |
. . . . 5
โข
((โฏโ๐ด)โ(โฏโโ
)) =
((โฏโ๐ด)โ0) |
30 | 29 | a1i 11 |
. . . 4
โข (๐ด โ Fin โ
((โฏโ๐ด)โ(โฏโโ
)) =
((โฏโ๐ด)โ0)) |
31 | | mapdm0 8787 |
. . . . . 6
โข (๐ด โ Fin โ (๐ด โm โ
) =
{โ
}) |
32 | 31 | fveq2d 6851 |
. . . . 5
โข (๐ด โ Fin โ
(โฏโ(๐ด
โm โ
)) = (โฏโ{โ
})) |
33 | | 0ex 5269 |
. . . . . 6
โข โ
โ V |
34 | | hashsng 14276 |
. . . . . 6
โข (โ
โ V โ (โฏโ{โ
}) = 1) |
35 | 33, 34 | mp1i 13 |
. . . . 5
โข (๐ด โ Fin โ
(โฏโ{โ
}) = 1) |
36 | 32, 35 | eqtrd 2777 |
. . . 4
โข (๐ด โ Fin โ
(โฏโ(๐ด
โm โ
)) = 1) |
37 | 27, 30, 36 | 3eqtr4rd 2788 |
. . 3
โข (๐ด โ Fin โ
(โฏโ(๐ด
โm โ
)) = ((โฏโ๐ด)โ(โฏโโ
))) |
38 | | oveq1 7369 |
. . . . . 6
โข
((โฏโ(๐ด
โm ๐ฆ)) =
((โฏโ๐ด)โ(โฏโ๐ฆ)) โ ((โฏโ(๐ด โm ๐ฆ)) ยท (โฏโ๐ด)) = (((โฏโ๐ด)โ(โฏโ๐ฆ)) ยท (โฏโ๐ด))) |
39 | | vex 3452 |
. . . . . . . . . . 11
โข ๐ฆ โ V |
40 | 39 | a1i 11 |
. . . . . . . . . 10
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ๐ฆ โ V) |
41 | | vsnex 5391 |
. . . . . . . . . . 11
โข {๐ง} โ V |
42 | 41 | a1i 11 |
. . . . . . . . . 10
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ {๐ง} โ V) |
43 | | elex 3466 |
. . . . . . . . . . 11
โข (๐ด โ Fin โ ๐ด โ V) |
44 | 43 | adantr 482 |
. . . . . . . . . 10
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ๐ด โ V) |
45 | | simprr 772 |
. . . . . . . . . . 11
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ยฌ ๐ง โ ๐ฆ) |
46 | | disjsn 4677 |
. . . . . . . . . . 11
โข ((๐ฆ โฉ {๐ง}) = โ
โ ยฌ ๐ง โ ๐ฆ) |
47 | 45, 46 | sylibr 233 |
. . . . . . . . . 10
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (๐ฆ โฉ {๐ง}) = โ
) |
48 | | mapunen 9097 |
. . . . . . . . . 10
โข (((๐ฆ โ V โง {๐ง} โ V โง ๐ด โ V) โง (๐ฆ โฉ {๐ง}) = โ
) โ (๐ด โm (๐ฆ โช {๐ง})) โ ((๐ด โm ๐ฆ) ร (๐ด โm {๐ง}))) |
49 | 40, 42, 44, 47, 48 | syl31anc 1374 |
. . . . . . . . 9
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (๐ด โm (๐ฆ โช {๐ง})) โ ((๐ด โm ๐ฆ) ร (๐ด โm {๐ง}))) |
50 | | simpl 484 |
. . . . . . . . . . 11
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ๐ด โ Fin) |
51 | | simprl 770 |
. . . . . . . . . . . 12
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ๐ฆ โ Fin) |
52 | | snfi 8995 |
. . . . . . . . . . . 12
โข {๐ง} โ Fin |
53 | | unfi 9123 |
. . . . . . . . . . . 12
โข ((๐ฆ โ Fin โง {๐ง} โ Fin) โ (๐ฆ โช {๐ง}) โ Fin) |
54 | 51, 52, 53 | sylancl 587 |
. . . . . . . . . . 11
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (๐ฆ โช {๐ง}) โ Fin) |
55 | | mapfi 9299 |
. . . . . . . . . . 11
โข ((๐ด โ Fin โง (๐ฆ โช {๐ง}) โ Fin) โ (๐ด โm (๐ฆ โช {๐ง})) โ Fin) |
56 | 50, 54, 55 | syl2anc 585 |
. . . . . . . . . 10
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (๐ด โm (๐ฆ โช {๐ง})) โ Fin) |
57 | | mapfi 9299 |
. . . . . . . . . . . 12
โข ((๐ด โ Fin โง ๐ฆ โ Fin) โ (๐ด โm ๐ฆ) โ Fin) |
58 | 57 | adantrr 716 |
. . . . . . . . . . 11
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (๐ด โm ๐ฆ) โ Fin) |
59 | | mapfi 9299 |
. . . . . . . . . . . 12
โข ((๐ด โ Fin โง {๐ง} โ Fin) โ (๐ด โm {๐ง}) โ Fin) |
60 | 50, 52, 59 | sylancl 587 |
. . . . . . . . . . 11
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (๐ด โm {๐ง}) โ Fin) |
61 | | xpfi 9268 |
. . . . . . . . . . 11
โข (((๐ด โm ๐ฆ) โ Fin โง (๐ด โm {๐ง}) โ Fin) โ ((๐ด โm ๐ฆ) ร (๐ด โm {๐ง})) โ Fin) |
62 | 58, 60, 61 | syl2anc 585 |
. . . . . . . . . 10
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ((๐ด โm ๐ฆ) ร (๐ด โm {๐ง})) โ Fin) |
63 | | hashen 14254 |
. . . . . . . . . 10
โข (((๐ด โm (๐ฆ โช {๐ง})) โ Fin โง ((๐ด โm ๐ฆ) ร (๐ด โm {๐ง})) โ Fin) โ ((โฏโ(๐ด โm (๐ฆ โช {๐ง}))) = (โฏโ((๐ด โm ๐ฆ) ร (๐ด โm {๐ง}))) โ (๐ด โm (๐ฆ โช {๐ง})) โ ((๐ด โm ๐ฆ) ร (๐ด โm {๐ง})))) |
64 | 56, 62, 63 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ((โฏโ(๐ด โm (๐ฆ โช {๐ง}))) = (โฏโ((๐ด โm ๐ฆ) ร (๐ด โm {๐ง}))) โ (๐ด โm (๐ฆ โช {๐ง})) โ ((๐ด โm ๐ฆ) ร (๐ด โm {๐ง})))) |
65 | 49, 64 | mpbird 257 |
. . . . . . . 8
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (โฏโ(๐ด โm (๐ฆ โช {๐ง}))) = (โฏโ((๐ด โm ๐ฆ) ร (๐ด โm {๐ง})))) |
66 | | hashxp 14341 |
. . . . . . . . 9
โข (((๐ด โm ๐ฆ) โ Fin โง (๐ด โm {๐ง}) โ Fin) โ
(โฏโ((๐ด
โm ๐ฆ)
ร (๐ด
โm {๐ง}))) =
((โฏโ(๐ด
โm ๐ฆ))
ยท (โฏโ(๐ด
โm {๐ง})))) |
67 | 58, 60, 66 | syl2anc 585 |
. . . . . . . 8
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (โฏโ((๐ด โm ๐ฆ) ร (๐ด โm {๐ง}))) = ((โฏโ(๐ด โm ๐ฆ)) ยท (โฏโ(๐ด โm {๐ง})))) |
68 | | vex 3452 |
. . . . . . . . . . . 12
โข ๐ง โ V |
69 | 68 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ๐ง โ V) |
70 | 50, 69 | mapsnend 8987 |
. . . . . . . . . 10
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (๐ด โm {๐ง}) โ ๐ด) |
71 | | hashen 14254 |
. . . . . . . . . . 11
โข (((๐ด โm {๐ง}) โ Fin โง ๐ด โ Fin) โ
((โฏโ(๐ด
โm {๐ง})) =
(โฏโ๐ด) โ
(๐ด โm
{๐ง}) โ ๐ด)) |
72 | 60, 50, 71 | syl2anc 585 |
. . . . . . . . . 10
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ((โฏโ(๐ด โm {๐ง})) = (โฏโ๐ด) โ (๐ด โm {๐ง}) โ ๐ด)) |
73 | 70, 72 | mpbird 257 |
. . . . . . . . 9
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (โฏโ(๐ด โm {๐ง})) = (โฏโ๐ด)) |
74 | 73 | oveq2d 7378 |
. . . . . . . 8
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ((โฏโ(๐ด โm ๐ฆ)) ยท (โฏโ(๐ด โm {๐ง}))) = ((โฏโ(๐ด โm ๐ฆ)) ยท (โฏโ๐ด))) |
75 | 65, 67, 74 | 3eqtrd 2781 |
. . . . . . 7
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (โฏโ(๐ด โm (๐ฆ โช {๐ง}))) = ((โฏโ(๐ด โm ๐ฆ)) ยท (โฏโ๐ด))) |
76 | | hashunsng 14299 |
. . . . . . . . . . 11
โข (๐ง โ V โ ((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โ (โฏโ(๐ฆ โช {๐ง})) = ((โฏโ๐ฆ) + 1))) |
77 | 76 | elv 3454 |
. . . . . . . . . 10
โข ((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โ (โฏโ(๐ฆ โช {๐ง})) = ((โฏโ๐ฆ) + 1)) |
78 | 77 | adantl 483 |
. . . . . . . . 9
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (โฏโ(๐ฆ โช {๐ง})) = ((โฏโ๐ฆ) + 1)) |
79 | 78 | oveq2d 7378 |
. . . . . . . 8
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ((โฏโ๐ด)โ(โฏโ(๐ฆ โช {๐ง}))) = ((โฏโ๐ด)โ((โฏโ๐ฆ) + 1))) |
80 | 26 | adantr 482 |
. . . . . . . . 9
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (โฏโ๐ด) โ โ) |
81 | | hashcl 14263 |
. . . . . . . . . 10
โข (๐ฆ โ Fin โ
(โฏโ๐ฆ) โ
โ0) |
82 | 81 | ad2antrl 727 |
. . . . . . . . 9
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ (โฏโ๐ฆ) โ
โ0) |
83 | 80, 82 | expp1d 14059 |
. . . . . . . 8
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ((โฏโ๐ด)โ((โฏโ๐ฆ) + 1)) = (((โฏโ๐ด)โ(โฏโ๐ฆ)) ยท (โฏโ๐ด))) |
84 | 79, 83 | eqtrd 2777 |
. . . . . . 7
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ((โฏโ๐ด)โ(โฏโ(๐ฆ โช {๐ง}))) = (((โฏโ๐ด)โ(โฏโ๐ฆ)) ยท (โฏโ๐ด))) |
85 | 75, 84 | eqeq12d 2753 |
. . . . . 6
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ((โฏโ(๐ด โm (๐ฆ โช {๐ง}))) = ((โฏโ๐ด)โ(โฏโ(๐ฆ โช {๐ง}))) โ ((โฏโ(๐ด โm ๐ฆ)) ยท (โฏโ๐ด)) = (((โฏโ๐ด)โ(โฏโ๐ฆ)) ยท (โฏโ๐ด)))) |
86 | 38, 85 | syl5ibr 246 |
. . . . 5
โข ((๐ด โ Fin โง (๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ)) โ ((โฏโ(๐ด โm ๐ฆ)) = ((โฏโ๐ด)โ(โฏโ๐ฆ)) โ (โฏโ(๐ด โm (๐ฆ โช {๐ง}))) = ((โฏโ๐ด)โ(โฏโ(๐ฆ โช {๐ง}))))) |
87 | 86 | expcom 415 |
. . . 4
โข ((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โ (๐ด โ Fin โ ((โฏโ(๐ด โm ๐ฆ)) = ((โฏโ๐ด)โ(โฏโ๐ฆ)) โ (โฏโ(๐ด โm (๐ฆ โช {๐ง}))) = ((โฏโ๐ด)โ(โฏโ(๐ฆ โช {๐ง})))))) |
88 | 87 | a2d 29 |
. . 3
โข ((๐ฆ โ Fin โง ยฌ ๐ง โ ๐ฆ) โ ((๐ด โ Fin โ (โฏโ(๐ด โm ๐ฆ)) = ((โฏโ๐ด)โ(โฏโ๐ฆ))) โ (๐ด โ Fin โ (โฏโ(๐ด โm (๐ฆ โช {๐ง}))) = ((โฏโ๐ด)โ(โฏโ(๐ฆ โช {๐ง})))))) |
89 | 6, 12, 18, 24, 37, 88 | findcard2s 9116 |
. 2
โข (๐ต โ Fin โ (๐ด โ Fin โ
(โฏโ(๐ด
โm ๐ต)) =
((โฏโ๐ด)โ(โฏโ๐ต)))) |
90 | 89 | impcom 409 |
1
โข ((๐ด โ Fin โง ๐ต โ Fin) โ
(โฏโ(๐ด
โm ๐ต)) =
((โฏโ๐ด)โ(โฏโ๐ต))) |