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: mgpf
20071 ringcl
20073 iscrng2
20075 ringass
20076 ringideu
20077 ringidcl
20083 ringidmlem
20085 ringsrg
20109 pwspjmhmmgpd
20141 pwsexpg
20142 unitsubm
20200 dfrhm2
20253 isrhm2d
20265 idrhm
20268 pwsco1rhm
20277 pwsco2rhm
20278 subrgcrng
20323 subrgsubm
20332 issubrg3
20347 cntzsubr
20353 pwsdiagrhm
20354 subrgacs
20416 cnfldexp
20978 expmhm
21014 nn0srg
21015 rge0srg
21016 assamulgscmlem2
21454 psrcrng
21533 mplcoe3
21593 mplcoe5lem
21594 mplcoe5
21595 evlsgsummul
21655 mhppwdeg
21693 ply1moncl
21793 coe1pwmul
21801 ply1coefsupp
21819 ply1coe
21820 gsummoncoe1
21828 lply1binomsc
21831 evls1gsummul
21844 evl1expd
21864 evl1gsummul
21879 evl1scvarpw
21882 evl1scvarpwval
21883 evl1gsummon
21884 ringvcl
21900 mat1mhm
21986 scmatmhm
22036 m1detdiag
22099 mdetdiaglem
22100 m2detleiblem2
22130 mat2pmatmhm
22235 pmatcollpwscmatlem1
22291 mply1topmatcllem
22305 mply1topmatcl
22307 pm2mpghm
22318 pm2mpmhm
22322 monmat2matmon
22326 pm2mp
22327 chpscmatgsumbin
22346 chpscmatgsummon
22347 chfacfscmulcl
22359 chfacfscmul0
22360 chfacfpmmulcl
22363 chfacfpmmul0
22364 chfacfpmmulgsum2
22367 cayhamlem1
22368 cpmadugsumlemB
22376 cpmadugsumlemC
22377 cpmadugsumlemF
22378 cayhamlem2
22386 cayhamlem4
22390 nrgtrg
24207 deg1pw
25638 plypf1
25726 efsubm
26060 amgm
26495 wilthlem2
26573 wilthlem3
26574 dchrelbas3
26741 lgsqrlem2
26850 lgsqrlem3
26851 lgsqrlem4
26852 cntrcrng
32245 psgnid
32287 cnmsgn0g
32336 altgnsg
32339 freshmansdream
32412 frobrhm
32413 fermltlchr
32509 znfermltl
32510 ringlsmss
32536 evls1fpws
32677 gsummoncoe1fzo
32699 ply1degltdimlem
32738 ply1degltdim
32739 iistmd
32913 evlsvvvallem
41181 evlsvvval
41183 evlsexpval
41187 selvvvval
41205 evlselv
41207 mhphf
41217 hbtlem4
41916 idomrootle
41985 isdomn3
41994 mon1psubm
41996 amgm2d
42998 amgm3d
42999 amgm4d
43000 c0rhm
46759 c0rnghm
46760 invginvrid
47091 ply1mulgsumlem4
47118 ply1mulgsum
47119 amgmw2d
47899 |