Step |
Hyp |
Ref |
Expression |
1 |
|
0z |
โข 0 โ โค |
2 |
|
sgmval2 |
โข ( ( 0 โ โค โง ๐ด โ โ ) โ ( 0 ฯ ๐ด ) = ฮฃ ๐ โ { ๐ โ โ โฃ ๐ โฅ ๐ด } ( ๐ โ 0 ) ) |
3 |
1 2
|
mpan |
โข ( ๐ด โ โ โ ( 0 ฯ ๐ด ) = ฮฃ ๐ โ { ๐ โ โ โฃ ๐ โฅ ๐ด } ( ๐ โ 0 ) ) |
4 |
|
elrabi |
โข ( ๐ โ { ๐ โ โ โฃ ๐ โฅ ๐ด } โ ๐ โ โ ) |
5 |
4
|
nncnd |
โข ( ๐ โ { ๐ โ โ โฃ ๐ โฅ ๐ด } โ ๐ โ โ ) |
6 |
5
|
exp0d |
โข ( ๐ โ { ๐ โ โ โฃ ๐ โฅ ๐ด } โ ( ๐ โ 0 ) = 1 ) |
7 |
6
|
sumeq2i |
โข ฮฃ ๐ โ { ๐ โ โ โฃ ๐ โฅ ๐ด } ( ๐ โ 0 ) = ฮฃ ๐ โ { ๐ โ โ โฃ ๐ โฅ ๐ด } 1 |
8 |
|
fzfid |
โข ( ๐ด โ โ โ ( 1 ... ๐ด ) โ Fin ) |
9 |
|
dvdsssfz1 |
โข ( ๐ด โ โ โ { ๐ โ โ โฃ ๐ โฅ ๐ด } โ ( 1 ... ๐ด ) ) |
10 |
8 9
|
ssfid |
โข ( ๐ด โ โ โ { ๐ โ โ โฃ ๐ โฅ ๐ด } โ Fin ) |
11 |
|
ax-1cn |
โข 1 โ โ |
12 |
|
fsumconst |
โข ( ( { ๐ โ โ โฃ ๐ โฅ ๐ด } โ Fin โง 1 โ โ ) โ ฮฃ ๐ โ { ๐ โ โ โฃ ๐ โฅ ๐ด } 1 = ( ( โฏ โ { ๐ โ โ โฃ ๐ โฅ ๐ด } ) ยท 1 ) ) |
13 |
10 11 12
|
sylancl |
โข ( ๐ด โ โ โ ฮฃ ๐ โ { ๐ โ โ โฃ ๐ โฅ ๐ด } 1 = ( ( โฏ โ { ๐ โ โ โฃ ๐ โฅ ๐ด } ) ยท 1 ) ) |
14 |
7 13
|
eqtrid |
โข ( ๐ด โ โ โ ฮฃ ๐ โ { ๐ โ โ โฃ ๐ โฅ ๐ด } ( ๐ โ 0 ) = ( ( โฏ โ { ๐ โ โ โฃ ๐ โฅ ๐ด } ) ยท 1 ) ) |
15 |
|
hashcl |
โข ( { ๐ โ โ โฃ ๐ โฅ ๐ด } โ Fin โ ( โฏ โ { ๐ โ โ โฃ ๐ โฅ ๐ด } ) โ โ0 ) |
16 |
10 15
|
syl |
โข ( ๐ด โ โ โ ( โฏ โ { ๐ โ โ โฃ ๐ โฅ ๐ด } ) โ โ0 ) |
17 |
16
|
nn0cnd |
โข ( ๐ด โ โ โ ( โฏ โ { ๐ โ โ โฃ ๐ โฅ ๐ด } ) โ โ ) |
18 |
17
|
mulridd |
โข ( ๐ด โ โ โ ( ( โฏ โ { ๐ โ โ โฃ ๐ โฅ ๐ด } ) ยท 1 ) = ( โฏ โ { ๐ โ โ โฃ ๐ โฅ ๐ด } ) ) |
19 |
3 14 18
|
3eqtrd |
โข ( ๐ด โ โ โ ( 0 ฯ ๐ด ) = ( โฏ โ { ๐ โ โ โฃ ๐ โฅ ๐ด } ) ) |