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
32214 psgnid
32256 cnmsgn0g
32305 altgnsg
32308 freshmansdream
32381 frobrhm
32382 fermltlchr
32478 znfermltl
32479 ringlsmss
32505 evls1fpws
32646 gsummoncoe1fzo
32668 ply1degltdimlem
32707 ply1degltdim
32708 iistmd
32882 evlsvvvallem
41133 evlsvvval
41135 evlsexpval
41139 selvvvval
41157 evlselv
41159 mhphf
41169 hbtlem4
41868 idomrootle
41937 isdomn3
41946 mon1psubm
41948 amgm2d
42950 amgm3d
42951 amgm4d
42952 c0rhm
46711 c0rnghm
46712 invginvrid
47043 ply1mulgsumlem4
47070 ply1mulgsum
47071 amgmw2d
47851 |