Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 = wceq 1542
∈ wcel 2107 ∀wral 3065 ∃wrex 3074
‘cfv 6497 (class class class)co 7358
Basecbs 17084 +gcplusg 17134 0gc0g 17322 Mndcmnd 18557
Grpcgrp 18749 |
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 2708 |
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 2715 df-cleq 2729 df-clel 2815 df-ral 3066 df-rex 3075 df-rab 3409 df-v 3448 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-br 5107 df-iota 6449 df-fv 6505 df-ov 7361 df-grp 18752 |
This theorem is referenced by: grpcl
18757 grpass
18758 grpideu
18760 grpmndd
18761 grpplusf
18763 grpplusfo
18764 grpsgrp
18775 dfgrp2
18776 grpidcl
18779 grplid
18781 grprid
18782 dfgrp3
18847 prdsgrpd
18858 prdsinvgd
18859 mulgaddcom
18901 mulginvcom
18902 mulgz
18905 mulgneg2
18911 mulgass
18914 issubg3
18947 grpissubg
18949 0subg
18954 subgacs
18964 0ghm
19023 pwsdiagghm
19037 cntzsubg
19118 oppggrp
19139 symgsubmefmndALT
19186 psgnunilem5
19277 psgnuni
19282 0subgALT
19351 lsmcntzr
19463 pj1ghm
19486 isabl2
19573 cntrabl
19622 dprdfid
19797 dprdfeq0
19802 dprdlub
19806 dmdprdsplitlem
19817 dprddisj2
19819 dpjidcl
19838 pgpfaclem3
19863 simpgnideld
19879 dsmmsubg
21152 frlm0
21163 mdetunilem7
21970 istgp2
23445 cyc3genpm
32004 isarchi3
32026 ofldchr
32112 reofld
32139 lbslsat
32316 dimkerim
32325 fedgmullem2
32328 pwssplit4
41419 pwslnmlem2
41423 c0ghm
46216 c0snghm
46221 lcoel0
46516 |