Step | Hyp | Ref
| Expression |
1 | | ovexd 7444 |
. . 3
โข (๐ โ (๐ โ ๐) โ V) |
2 | | eqid 2733 |
. . . 4
โข (๐ฅ โ (๐ โ ๐) โฆ โจ((๐(proj1โ๐บ)๐)โ๐ฅ), ((๐(proj1โ๐บ)๐)โ๐ฅ)โฉ) = (๐ฅ โ (๐ โ ๐) โฆ โจ((๐(proj1โ๐บ)๐)โ๐ฅ), ((๐(proj1โ๐บ)๐)โ๐ฅ)โฉ) |
3 | | eqid 2733 |
. . . . . . 7
โข
(+gโ๐บ) = (+gโ๐บ) |
4 | | lsmhash.p |
. . . . . . 7
โข โ =
(LSSumโ๐บ) |
5 | | lsmhash.o |
. . . . . . 7
โข 0 =
(0gโ๐บ) |
6 | | lsmhash.z |
. . . . . . 7
โข ๐ = (Cntzโ๐บ) |
7 | | lsmhash.t |
. . . . . . 7
โข (๐ โ ๐ โ (SubGrpโ๐บ)) |
8 | | lsmhash.u |
. . . . . . 7
โข (๐ โ ๐ โ (SubGrpโ๐บ)) |
9 | | lsmhash.i |
. . . . . . 7
โข (๐ โ (๐ โฉ ๐) = { 0 }) |
10 | | lsmhash.s |
. . . . . . 7
โข (๐ โ ๐ โ (๐โ๐)) |
11 | | eqid 2733 |
. . . . . . 7
โข
(proj1โ๐บ) = (proj1โ๐บ) |
12 | 3, 4, 5, 6, 7, 8, 9, 10, 11 | pj1f 19565 |
. . . . . 6
โข (๐ โ (๐(proj1โ๐บ)๐):(๐ โ ๐)โถ๐) |
13 | 12 | ffvelcdmda 7087 |
. . . . 5
โข ((๐ โง ๐ฅ โ (๐ โ ๐)) โ ((๐(proj1โ๐บ)๐)โ๐ฅ) โ ๐) |
14 | 3, 4, 5, 6, 7, 8, 9, 10, 11 | pj2f 19566 |
. . . . . 6
โข (๐ โ (๐(proj1โ๐บ)๐):(๐ โ ๐)โถ๐) |
15 | 14 | ffvelcdmda 7087 |
. . . . 5
โข ((๐ โง ๐ฅ โ (๐ โ ๐)) โ ((๐(proj1โ๐บ)๐)โ๐ฅ) โ ๐) |
16 | 13, 15 | opelxpd 5716 |
. . . 4
โข ((๐ โง ๐ฅ โ (๐ โ ๐)) โ โจ((๐(proj1โ๐บ)๐)โ๐ฅ), ((๐(proj1โ๐บ)๐)โ๐ฅ)โฉ โ (๐ ร ๐)) |
17 | 7, 8 | jca 513 |
. . . . 5
โข (๐ โ (๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ))) |
18 | | xp1st 8007 |
. . . . . 6
โข (๐ฆ โ (๐ ร ๐) โ (1st โ๐ฆ) โ ๐) |
19 | | xp2nd 8008 |
. . . . . 6
โข (๐ฆ โ (๐ ร ๐) โ (2nd โ๐ฆ) โ ๐) |
20 | 18, 19 | jca 513 |
. . . . 5
โข (๐ฆ โ (๐ ร ๐) โ ((1st โ๐ฆ) โ ๐ โง (2nd โ๐ฆ) โ ๐)) |
21 | 3, 4 | lsmelvali 19518 |
. . . . 5
โข (((๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ)) โง ((1st โ๐ฆ) โ ๐ โง (2nd โ๐ฆ) โ ๐)) โ ((1st โ๐ฆ)(+gโ๐บ)(2nd โ๐ฆ)) โ (๐ โ ๐)) |
22 | 17, 20, 21 | syl2an 597 |
. . . 4
โข ((๐ โง ๐ฆ โ (๐ ร ๐)) โ ((1st โ๐ฆ)(+gโ๐บ)(2nd โ๐ฆ)) โ (๐ โ ๐)) |
23 | 7 | adantr 482 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ ร ๐))) โ ๐ โ (SubGrpโ๐บ)) |
24 | 8 | adantr 482 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ ร ๐))) โ ๐ โ (SubGrpโ๐บ)) |
25 | 9 | adantr 482 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ ร ๐))) โ (๐ โฉ ๐) = { 0 }) |
26 | 10 | adantr 482 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ ร ๐))) โ ๐ โ (๐โ๐)) |
27 | | simprl 770 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ ร ๐))) โ ๐ฅ โ (๐ โ ๐)) |
28 | 18 | ad2antll 728 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ ร ๐))) โ (1st โ๐ฆ) โ ๐) |
29 | 19 | ad2antll 728 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ ร ๐))) โ (2nd โ๐ฆ) โ ๐) |
30 | 3, 4, 5, 6, 23, 24, 25, 26, 11, 27, 28, 29 | pj1eq 19568 |
. . . . . 6
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ ร ๐))) โ (๐ฅ = ((1st โ๐ฆ)(+gโ๐บ)(2nd โ๐ฆ)) โ (((๐(proj1โ๐บ)๐)โ๐ฅ) = (1st โ๐ฆ) โง ((๐(proj1โ๐บ)๐)โ๐ฅ) = (2nd โ๐ฆ)))) |
31 | | eqcom 2740 |
. . . . . . 7
โข (((๐(proj1โ๐บ)๐)โ๐ฅ) = (1st โ๐ฆ) โ (1st โ๐ฆ) = ((๐(proj1โ๐บ)๐)โ๐ฅ)) |
32 | | eqcom 2740 |
. . . . . . 7
โข (((๐(proj1โ๐บ)๐)โ๐ฅ) = (2nd โ๐ฆ) โ (2nd โ๐ฆ) = ((๐(proj1โ๐บ)๐)โ๐ฅ)) |
33 | 31, 32 | anbi12i 628 |
. . . . . 6
โข ((((๐(proj1โ๐บ)๐)โ๐ฅ) = (1st โ๐ฆ) โง ((๐(proj1โ๐บ)๐)โ๐ฅ) = (2nd โ๐ฆ)) โ ((1st โ๐ฆ) = ((๐(proj1โ๐บ)๐)โ๐ฅ) โง (2nd โ๐ฆ) = ((๐(proj1โ๐บ)๐)โ๐ฅ))) |
34 | 30, 33 | bitrdi 287 |
. . . . 5
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ ร ๐))) โ (๐ฅ = ((1st โ๐ฆ)(+gโ๐บ)(2nd โ๐ฆ)) โ ((1st โ๐ฆ) = ((๐(proj1โ๐บ)๐)โ๐ฅ) โง (2nd โ๐ฆ) = ((๐(proj1โ๐บ)๐)โ๐ฅ)))) |
35 | | eqop 8017 |
. . . . . 6
โข (๐ฆ โ (๐ ร ๐) โ (๐ฆ = โจ((๐(proj1โ๐บ)๐)โ๐ฅ), ((๐(proj1โ๐บ)๐)โ๐ฅ)โฉ โ ((1st โ๐ฆ) = ((๐(proj1โ๐บ)๐)โ๐ฅ) โง (2nd โ๐ฆ) = ((๐(proj1โ๐บ)๐)โ๐ฅ)))) |
36 | 35 | ad2antll 728 |
. . . . 5
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ ร ๐))) โ (๐ฆ = โจ((๐(proj1โ๐บ)๐)โ๐ฅ), ((๐(proj1โ๐บ)๐)โ๐ฅ)โฉ โ ((1st โ๐ฆ) = ((๐(proj1โ๐บ)๐)โ๐ฅ) โง (2nd โ๐ฆ) = ((๐(proj1โ๐บ)๐)โ๐ฅ)))) |
37 | 34, 36 | bitr4d 282 |
. . . 4
โข ((๐ โง (๐ฅ โ (๐ โ ๐) โง ๐ฆ โ (๐ ร ๐))) โ (๐ฅ = ((1st โ๐ฆ)(+gโ๐บ)(2nd โ๐ฆ)) โ ๐ฆ = โจ((๐(proj1โ๐บ)๐)โ๐ฅ), ((๐(proj1โ๐บ)๐)โ๐ฅ)โฉ)) |
38 | 2, 16, 22, 37 | f1o2d 7660 |
. . 3
โข (๐ โ (๐ฅ โ (๐ โ ๐) โฆ โจ((๐(proj1โ๐บ)๐)โ๐ฅ), ((๐(proj1โ๐บ)๐)โ๐ฅ)โฉ):(๐ โ ๐)โ1-1-ontoโ(๐ ร ๐)) |
39 | 1, 38 | hasheqf1od 14313 |
. 2
โข (๐ โ (โฏโ(๐ โ ๐)) = (โฏโ(๐ ร ๐))) |
40 | | lsmhash.1 |
. . 3
โข (๐ โ ๐ โ Fin) |
41 | | lsmhash.2 |
. . 3
โข (๐ โ ๐ โ Fin) |
42 | | hashxp 14394 |
. . 3
โข ((๐ โ Fin โง ๐ โ Fin) โ
(โฏโ(๐ ร
๐)) = ((โฏโ๐) ยท (โฏโ๐))) |
43 | 40, 41, 42 | syl2anc 585 |
. 2
โข (๐ โ (โฏโ(๐ ร ๐)) = ((โฏโ๐) ยท (โฏโ๐))) |
44 | 39, 43 | eqtrd 2773 |
1
โข (๐ โ (โฏโ(๐ โ ๐)) = ((โฏโ๐) ยท (โฏโ๐))) |