Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ wa 397
= wceq 1542 ∈
wcel 2107 ∀wral 3062
‘cfv 6544 (class class class)co 7409
Basecbs 17144 +gcplusg 17197 .rcmulr 17198 Mndcmnd 18625
Grpcgrp 18819 mulGrpcmgp 19987 Ringcrg 20056 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914
ax-6 1972 ax-7 2012 ax-8 2109
ax-9 2117 ax-ext 2704 ax-nul 5307 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ne 2942 df-ral 3063 df-rab 3434 df-v 3477 df-sbc 3779 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-iota 6496 df-fv 6552 df-ov 7412 df-ring 20058 |
This theorem is referenced by: ringgrpd
20065 ringmnd
20066 ring0cl
20084 ringacl
20095 ringabl
20098 ringlz
20107 ringrz
20108 ringnegl
20114 ringnegr
20115 ringmneg1
20116 ringmneg2
20117 ringm2neg
20118 ringsubdi
20119 ringsubdir
20120 mulgass2
20121 ringlghm
20124 ringrghm
20125 prdsringd
20134 imasring
20143 opprring
20161 dvdsrneg
20184 dvdsr02
20186 unitnegcl
20211 dvrdir
20226 irrednegb
20245 dfrhm2
20253 isrhmd
20266 idrhm
20268 pwsco1rhm
20277 pwsco2rhm
20278 rhmopp
20288 0ringnnzr
20302 subrgsubg
20325 cntzsubr
20353 pwsdiagrhm
20354 subrgacs
20416 isabvd
20428 abvneg
20442 abvsubtri
20443 abvtrivd
20448 srng0
20468 idsrngd
20470 lmodfgrp
20480 lmod0vs
20505 lmodvsneg
20516 lmodsubvs
20528 lmodsubdi
20529 lmodsubdir
20530 rmodislmodlem
20539 rmodislmod
20540 rmodislmodOLD
20541 lssvnegcl
20567 lmodvsinv
20647 sralmod
20809 issubrgd
20811 lidlsubg
20838 2idlcpbl
20871 cnfld0
20969 cnfldneg
20971 cnfldsub
20973 cnsubglem
20994 zringgrp
21022 mulgrhm
21047 chrdvds
21080 chrcong
21081 zncyg
21104 cygznlem3
21125 zrhpsgnelbas
21147 ip2subdi
21197 asclghm
21437 psrlmod
21521 psrdi
21526 psrdir
21527 psrring
21531 mpllsslem
21559 mplsubrg
21564 mplcoe1
21592 mplind
21631 evlslem2
21642 mhplss
21698 coe1z
21785 coe1subfv
21788 evl1subd
21861 evl1gsumd
21876 matinvgcell
21937 mat0dim0
21969 mat1ghm
21985 dmatsubcl
22000 dmatsgrp
22001 scmataddcl
22018 scmatsubcl
22019 scmatsgrp
22021 scmatsgrp1
22024 scmatghm
22035 mdetralt
22110 mdetero
22112 mdetunilem6
22119 mdetunilem9
22122 mdetuni0
22123 m2detleiblem6
22128 cpmatinvcl
22219 cpmatsubgpmat
22222 mat2pmatghm
22232 pm2mpghm
22318 chmatcl
22330 chpmat0d
22336 chpmat1d
22338 chpdmatlem1
22340 chpdmatlem2
22341 chpscmat
22344 chpscmatgsumbin
22346 chpscmatgsummon
22347 chp0mat
22348 chpidmat
22349 chfacfisf
22356 chfacfscmulgsum
22362 chfacfpmmulgsum
22366 cayhamlem1
22368 cpmadugsumlemF
22378 cpmidgsum2
22381 trggrp
23676 tlmtgp
23700 abvmet
24084 nrgdsdi
24182 nrgdsdir
24183 tngnrg
24191 cnngp
24296 cnfldtgp
24385 cnncvsaddassdemo
24680 cphsubrglem
24694 mdegldg
25584 mdeg0
25588 mdegaddle
25592 deg1add
25621 deg1suble
25625 deg1sub
25626 deg1sublt
25628 ply1nzb
25640 ply1divmo
25653 ply1divex
25654 r1pcl
25675 r1pid
25677 dvdsq1p
25678 dvdsr1p
25679 ply1remlem
25680 ply1rem
25681 ig1peu
25689 reefgim
25962 lgsqrlem1
26849 lgsqrlem2
26850 lgsqrlem3
26851 lgsqrlem4
26852 abvcxp
27118 dvdschrmulg
32380 freshmansdream
32381 rmfsupp2
32387 orngsqr
32422 ornglmulle
32423 orngrmulle
32424 ornglmullt
32425 orngrmullt
32426 orngmullt
32427 ofldchr
32432 suborng
32433 isarchiofld
32435 reofld
32459 linds2eq
32497 qsidomlem1
32571 qsidomlem2
32572 qsnzr
32574 mxidlprm
32586 fedgmullem1
32714 ccfldsrarelvec
32745 zrhchr
32956 matunitlindflem1
36484 lfl0
37935 lflsub
37937 lfl0f
37939 lfladdass
37943 lfladd0l
37944 lflnegcl
37945 lflnegl
37946 ldualvsubcl
38026 ldualvsubval
38027 lkrin
38034 erng0g
39865 lclkrlem2m
40390 lcfrlem2
40414 lcdvsubval
40489 mapdpglem30
40573 baerlem3lem1
40578 baerlem5alem1
40579 baerlem5blem1
40580 baerlem5blem2
40583 hdmapinvlem3
40791 hdmapinvlem4
40792 hdmapglem7b
40799 hbtlem5
41870 mendlmod
41935 idomrootle
41937 c0rhm
46711 c0rnghm
46712 zrrnghm
46716 lidldomn1
46823 invginvrid
47043 evl1at0
47072 linply1
47074 |