Step |
Hyp |
Ref |
Expression |
1 |
|
cygzn.b |
โข ๐ต = ( Base โ ๐บ ) |
2 |
|
cygzn.n |
โข ๐ = if ( ๐ต โ Fin , ( โฏ โ ๐ต ) , 0 ) |
3 |
|
cygzn.y |
โข ๐ = ( โค/nโค โ ๐ ) |
4 |
|
cygzn.m |
โข ยท = ( .g โ ๐บ ) |
5 |
|
cygzn.l |
โข ๐ฟ = ( โคRHom โ ๐ ) |
6 |
|
cygzn.e |
โข ๐ธ = { ๐ฅ โ ๐ต โฃ ran ( ๐ โ โค โฆ ( ๐ ยท ๐ฅ ) ) = ๐ต } |
7 |
|
cygzn.g |
โข ( ๐ โ ๐บ โ CycGrp ) |
8 |
|
cygzn.x |
โข ( ๐ โ ๐ โ ๐ธ ) |
9 |
|
cygzn.f |
โข ๐น = ran ( ๐ โ โค โฆ โจ ( ๐ฟ โ ๐ ) , ( ๐ ยท ๐ ) โฉ ) |
10 |
|
fvexd |
โข ( ( ๐ โง ๐ โ โค ) โ ( ๐ฟ โ ๐ ) โ V ) |
11 |
|
cyggrp |
โข ( ๐บ โ CycGrp โ ๐บ โ Grp ) |
12 |
7 11
|
syl |
โข ( ๐ โ ๐บ โ Grp ) |
13 |
12
|
adantr |
โข ( ( ๐ โง ๐ โ โค ) โ ๐บ โ Grp ) |
14 |
|
simpr |
โข ( ( ๐ โง ๐ โ โค ) โ ๐ โ โค ) |
15 |
6
|
ssrab3 |
โข ๐ธ โ ๐ต |
16 |
15 8
|
sselid |
โข ( ๐ โ ๐ โ ๐ต ) |
17 |
16
|
adantr |
โข ( ( ๐ โง ๐ โ โค ) โ ๐ โ ๐ต ) |
18 |
1 4
|
mulgcl |
โข ( ( ๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต ) โ ( ๐ ยท ๐ ) โ ๐ต ) |
19 |
13 14 17 18
|
syl3anc |
โข ( ( ๐ โง ๐ โ โค ) โ ( ๐ ยท ๐ ) โ ๐ต ) |
20 |
|
fveq2 |
โข ( ๐ = ๐ โ ( ๐ฟ โ ๐ ) = ( ๐ฟ โ ๐ ) ) |
21 |
|
oveq1 |
โข ( ๐ = ๐ โ ( ๐ ยท ๐ ) = ( ๐ ยท ๐ ) ) |
22 |
1 2 3 4 5 6 7 8
|
cygznlem1 |
โข ( ( ๐ โง ( ๐ โ โค โง ๐ โ โค ) ) โ ( ( ๐ฟ โ ๐ ) = ( ๐ฟ โ ๐ ) โ ( ๐ ยท ๐ ) = ( ๐ ยท ๐ ) ) ) |
23 |
22
|
biimpd |
โข ( ( ๐ โง ( ๐ โ โค โง ๐ โ โค ) ) โ ( ( ๐ฟ โ ๐ ) = ( ๐ฟ โ ๐ ) โ ( ๐ ยท ๐ ) = ( ๐ ยท ๐ ) ) ) |
24 |
23
|
exp32 |
โข ( ๐ โ ( ๐ โ โค โ ( ๐ โ โค โ ( ( ๐ฟ โ ๐ ) = ( ๐ฟ โ ๐ ) โ ( ๐ ยท ๐ ) = ( ๐ ยท ๐ ) ) ) ) ) |
25 |
24
|
3imp2 |
โข ( ( ๐ โง ( ๐ โ โค โง ๐ โ โค โง ( ๐ฟ โ ๐ ) = ( ๐ฟ โ ๐ ) ) ) โ ( ๐ ยท ๐ ) = ( ๐ ยท ๐ ) ) |
26 |
9 10 19 20 21 25
|
fliftfund |
โข ( ๐ โ Fun ๐น ) |
27 |
9 10 19
|
fliftf |
โข ( ๐ โ ( Fun ๐น โ ๐น : ran ( ๐ โ โค โฆ ( ๐ฟ โ ๐ ) ) โถ ๐ต ) ) |
28 |
26 27
|
mpbid |
โข ( ๐ โ ๐น : ran ( ๐ โ โค โฆ ( ๐ฟ โ ๐ ) ) โถ ๐ต ) |
29 |
|
hashcl |
โข ( ๐ต โ Fin โ ( โฏ โ ๐ต ) โ โ0 ) |
30 |
29
|
adantl |
โข ( ( ๐ โง ๐ต โ Fin ) โ ( โฏ โ ๐ต ) โ โ0 ) |
31 |
|
0nn0 |
โข 0 โ โ0 |
32 |
31
|
a1i |
โข ( ( ๐ โง ยฌ ๐ต โ Fin ) โ 0 โ โ0 ) |
33 |
30 32
|
ifclda |
โข ( ๐ โ if ( ๐ต โ Fin , ( โฏ โ ๐ต ) , 0 ) โ โ0 ) |
34 |
2 33
|
eqeltrid |
โข ( ๐ โ ๐ โ โ0 ) |
35 |
|
eqid |
โข ( Base โ ๐ ) = ( Base โ ๐ ) |
36 |
3 35 5
|
znzrhfo |
โข ( ๐ โ โ0 โ ๐ฟ : โค โontoโ ( Base โ ๐ ) ) |
37 |
34 36
|
syl |
โข ( ๐ โ ๐ฟ : โค โontoโ ( Base โ ๐ ) ) |
38 |
|
fof |
โข ( ๐ฟ : โค โontoโ ( Base โ ๐ ) โ ๐ฟ : โค โถ ( Base โ ๐ ) ) |
39 |
37 38
|
syl |
โข ( ๐ โ ๐ฟ : โค โถ ( Base โ ๐ ) ) |
40 |
39
|
feqmptd |
โข ( ๐ โ ๐ฟ = ( ๐ โ โค โฆ ( ๐ฟ โ ๐ ) ) ) |
41 |
40
|
rneqd |
โข ( ๐ โ ran ๐ฟ = ran ( ๐ โ โค โฆ ( ๐ฟ โ ๐ ) ) ) |
42 |
|
forn |
โข ( ๐ฟ : โค โontoโ ( Base โ ๐ ) โ ran ๐ฟ = ( Base โ ๐ ) ) |
43 |
37 42
|
syl |
โข ( ๐ โ ran ๐ฟ = ( Base โ ๐ ) ) |
44 |
41 43
|
eqtr3d |
โข ( ๐ โ ran ( ๐ โ โค โฆ ( ๐ฟ โ ๐ ) ) = ( Base โ ๐ ) ) |
45 |
44
|
feq2d |
โข ( ๐ โ ( ๐น : ran ( ๐ โ โค โฆ ( ๐ฟ โ ๐ ) ) โถ ๐ต โ ๐น : ( Base โ ๐ ) โถ ๐ต ) ) |
46 |
28 45
|
mpbid |
โข ( ๐ โ ๐น : ( Base โ ๐ ) โถ ๐ต ) |