Metamath Proof Explorer


Theorem cygznlem2a

Description: Lemma for cygzn . (Contributed by Mario Carneiro, 23-Dec-2016)

Ref Expression
Hypotheses cygzn.b โŠข ๐ต = ( Base โ€˜ ๐บ )
cygzn.n โŠข ๐‘ = if ( ๐ต โˆˆ Fin , ( โ™ฏ โ€˜ ๐ต ) , 0 )
cygzn.y โŠข ๐‘Œ = ( โ„ค/nโ„ค โ€˜ ๐‘ )
cygzn.m โŠข ยท = ( .g โ€˜ ๐บ )
cygzn.l โŠข ๐ฟ = ( โ„คRHom โ€˜ ๐‘Œ )
cygzn.e โŠข ๐ธ = { ๐‘ฅ โˆˆ ๐ต โˆฃ ran ( ๐‘› โˆˆ โ„ค โ†ฆ ( ๐‘› ยท ๐‘ฅ ) ) = ๐ต }
cygzn.g โŠข ( ๐œ‘ โ†’ ๐บ โˆˆ CycGrp )
cygzn.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ธ )
cygzn.f โŠข ๐น = ran ( ๐‘š โˆˆ โ„ค โ†ฆ โŸจ ( ๐ฟ โ€˜ ๐‘š ) , ( ๐‘š ยท ๐‘‹ ) โŸฉ )
Assertion cygznlem2a ( ๐œ‘ โ†’ ๐น : ( Base โ€˜ ๐‘Œ ) โŸถ ๐ต )

Proof

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 โ€˜ ๐‘Œ ) โŸถ ๐ต )