Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cygznlem2 | Structured version Visualization version GIF version |
Description: Lemma for cygzn 20876. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by Mario Carneiro, 23-Dec-2016.) |
Ref | Expression |
---|---|
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 (๐ โ โค โฆ โจ(๐ฟโ๐), (๐ ยท ๐)โฉ) |
Ref | Expression |
---|---|
cygznlem2 | โข ((๐ โง ๐ โ โค) โ (๐นโ(๐ฟโ๐)) = (๐ ยท ๐)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cygzn.f | . 2 โข ๐น = ran (๐ โ โค โฆ โจ(๐ฟโ๐), (๐ ยท ๐)โฉ) | |
2 | fvexd 6834 | . 2 โข ((๐ โง ๐ โ โค) โ (๐ฟโ๐) โ V) | |
3 | ovexd 7364 | . 2 โข ((๐ โง ๐ โ โค) โ (๐ ยท ๐) โ V) | |
4 | fveq2 6819 | . 2 โข (๐ = ๐ โ (๐ฟโ๐) = (๐ฟโ๐)) | |
5 | oveq1 7336 | . 2 โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) | |
6 | cygzn.b | . . . 4 โข ๐ต = (Baseโ๐บ) | |
7 | cygzn.n | . . . 4 โข ๐ = if(๐ต โ Fin, (โฏโ๐ต), 0) | |
8 | cygzn.y | . . . 4 โข ๐ = (โค/nโคโ๐) | |
9 | cygzn.m | . . . 4 โข ยท = (.gโ๐บ) | |
10 | cygzn.l | . . . 4 โข ๐ฟ = (โคRHomโ๐) | |
11 | cygzn.e | . . . 4 โข ๐ธ = {๐ฅ โ ๐ต โฃ ran (๐ โ โค โฆ (๐ ยท ๐ฅ)) = ๐ต} | |
12 | cygzn.g | . . . 4 โข (๐ โ ๐บ โ CycGrp) | |
13 | cygzn.x | . . . 4 โข (๐ โ ๐ โ ๐ธ) | |
14 | 6, 7, 8, 9, 10, 11, 12, 13, 1 | cygznlem2a 20873 | . . 3 โข (๐ โ ๐น:(Baseโ๐)โถ๐ต) |
15 | 14 | ffund 6649 | . 2 โข (๐ โ Fun ๐น) |
16 | 1, 2, 3, 4, 5, 15 | fliftval 7237 | 1 โข ((๐ โง ๐ โ โค) โ (๐นโ(๐ฟโ๐)) = (๐ ยท ๐)) |
Colors of variables: wff setvar class |
Syntax hints: โ wi 4 โง wa 396 = wceq 1540 โ wcel 2105 {crab 3403 Vcvv 3441 ifcif 4472 โจcop 4578 โฆ cmpt 5172 ran crn 5615 โcfv 6473 (class class class)co 7329 Fincfn 8796 0cc0 10964 โคcz 12412 โฏchash 14137 Basecbs 17001 .gcmg 18788 CycGrpccyg 19564 โคRHomczrh 20799 โค/nโคczn 20802 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-rep 5226 ax-sep 5240 ax-nul 5247 ax-pow 5305 ax-pr 5369 ax-un 7642 ax-inf2 9490 ax-cnex 11020 ax-resscn 11021 ax-1cn 11022 ax-icn 11023 ax-addcl 11024 ax-addrcl 11025 ax-mulcl 11026 ax-mulrcl 11027 ax-mulcom 11028 ax-addass 11029 ax-mulass 11030 ax-distr 11031 ax-i2m1 11032 ax-1ne0 11033 ax-1rid 11034 ax-rnegex 11035 ax-rrecex 11036 ax-cnre 11037 ax-pre-lttri 11038 ax-pre-lttrn 11039 ax-pre-ltadd 11040 ax-pre-mulgt0 11041 ax-pre-sup 11042 ax-addf 11043 ax-mulf 11044 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3349 df-reu 3350 df-rab 3404 df-v 3443 df-sbc 3727 df-csb 3843 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3916 df-nul 4269 df-if 4473 df-pw 4548 df-sn 4573 df-pr 4575 df-tp 4577 df-op 4579 df-uni 4852 df-int 4894 df-iun 4940 df-br 5090 df-opab 5152 df-mpt 5173 df-tr 5207 df-id 5512 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5569 df-se 5570 df-we 5571 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6232 df-ord 6299 df-on 6300 df-lim 6301 df-suc 6302 df-iota 6425 df-fun 6475 df-fn 6476 df-f 6477 df-f1 6478 df-fo 6479 df-f1o 6480 df-fv 6481 df-isom 6482 df-riota 7286 df-ov 7332 df-oprab 7333 df-mpo 7334 df-om 7773 df-1st 7891 df-2nd 7892 df-tpos 8104 df-frecs 8159 df-wrecs 8190 df-recs 8264 df-rdg 8303 df-1o 8359 df-oadd 8363 df-omul 8364 df-er 8561 df-ec 8563 df-qs 8567 df-map 8680 df-en 8797 df-dom 8798 df-sdom 8799 df-fin 8800 df-sup 9291 df-inf 9292 df-oi 9359 df-card 9788 df-acn 9791 df-pnf 11104 df-mnf 11105 df-xr 11106 df-ltxr 11107 df-le 11108 df-sub 11300 df-neg 11301 df-div 11726 df-nn 12067 df-2 12129 df-3 12130 df-4 12131 df-5 12132 df-6 12133 df-7 12134 df-8 12135 df-9 12136 df-n0 12327 df-z 12413 df-dec 12531 df-uz 12676 df-rp 12824 df-fz 13333 df-fl 13605 df-mod 13683 df-seq 13815 df-exp 13876 df-hash 14138 df-cj 14901 df-re 14902 df-im 14903 df-sqrt 15037 df-abs 15038 df-dvds 16055 df-struct 16937 df-sets 16954 df-slot 16972 df-ndx 16984 df-base 17002 df-ress 17031 df-plusg 17064 df-mulr 17065 df-starv 17066 df-sca 17067 df-vsca 17068 df-ip 17069 df-tset 17070 df-ple 17071 df-ds 17073 df-unif 17074 df-0g 17241 df-imas 17308 df-qus 17309 df-mgm 18415 df-sgrp 18464 df-mnd 18475 df-mhm 18519 df-grp 18668 df-minusg 18669 df-sbg 18670 df-mulg 18789 df-subg 18840 df-nsg 18841 df-eqg 18842 df-ghm 18920 df-od 19224 df-cmn 19475 df-abl 19476 df-cyg 19565 df-mgp 19808 df-ur 19825 df-ring 19872 df-cring 19873 df-oppr 19949 df-dvdsr 19970 df-rnghom 20046 df-subrg 20119 df-lmod 20223 df-lss 20292 df-lsp 20332 df-sra 20532 df-rgmod 20533 df-lidl 20534 df-rsp 20535 df-2idl 20601 df-cnfld 20696 df-zring 20769 df-zrh 20803 df-zn 20806 |
This theorem is referenced by: cygznlem3 20875 |
Copyright terms: Public domain | W3C validator |