Metamath Proof Explorer

Table of Contents - 10.2. Groups

1. Definition and basic properties
   1. cgrp
   2. cminusg
   3. csg
   4. df-grp
   5. df-minusg
   6. df-sbg
   7. isgrp
   8. grpmnd
   9. grpcl
   10. grpass
   11. grpinvex
   12. grpideu
   13. grpassd
   14. grpmndd
   15. grpcld
   16. grpplusf
   17. grpplusfo
   18. resgrpplusfrn
   19. grppropd
   20. grpprop
   21. grppropstr
   22. grpss
   23. isgrpd2e
   24. isgrpd2
   25. isgrpde
   26. isgrpd
   27. isgrpi
   28. grpsgrp
   29. grpmgmd
   30. dfgrp2
   31. dfgrp2e
   32. isgrpix
   33. grpidcl
   34. grpbn0
   35. grplid
   36. grprid
   37. grplidd
   38. grpridd
   39. grpn0
   40. hashfingrpnn
   41. grprcan
   42. grpinveu
   43. grpid
   44. isgrpid2
   45. grpidd2
   46. grpinvfval
   47. grpinvfvalALT
   48. grpinvval
   49. grpinvfn
   50. grpinvfvi
   51. grpsubfval
   52. grpsubfvalALT
   53. grpsubval
   54. grpinvf
   55. grpinvcl
   56. grpinvcld
   57. grplinv
   58. grprinv
   59. grpinvid1
   60. grpinvid2
   61. isgrpinv
   62. grplinvd
   63. grprinvd
   64. grplrinv
   65. grpidinv2
   66. grpidinv
   67. grpinvid
   68. grplcan
   69. grpasscan1
   70. grpasscan2
   71. grpidrcan
   72. grpidlcan
   73. grpinvinv
   74. grpinvcnv
   75. grpinv11
   76. grpinvf1o
   77. grpinvnz
   78. grpinvnzcl
   79. grpsubinv
   80. grplmulf1o
   81. grpraddf1o
   82. grpinvpropd
   83. grpidssd
   84. grpinvssd
   85. grpinvadd
   86. grpsubf
   87. grpsubcl
   88. grpsubrcan
   89. grpinvsub
   90. grpinvval2
   91. grpsubid
   92. grpsubid1
   93. grpsubeq0
   94. grpsubadd0sub
   95. grpsubadd
   96. grpsubsub
   97. grpaddsubass
   98. grppncan
   99. grpnpcan
   100. grpsubsub4
   101. grppnpcan2
   102. grpnpncan
   103. grpnpncan0
   104. grpnnncan2
   105. dfgrp3lem
   106. dfgrp3
   107. dfgrp3e
   108. grplactfval
   109. grplactval
   110. grplactcnv
   111. grplactf1o
   112. grpsubpropd
   113. grpsubpropd2
   114. grp1
   115. grp1inv
   116. prdsinvlem
   117. prdsgrpd
   118. prdsinvgd
   119. pwsgrp
   120. pwsinvg
   121. pwssub
   122. imasgrp2
   123. imasgrp
   124. imasgrpf1
   125. qusgrp2
   126. xpsgrp
   127. xpsinv
   128. xpsgrpsub
   129. mhmlem
   130. mhmid
   131. mhmmnd
   132. mhmfmhm
   133. ghmgrp
2. Group multiple operation
   1. cmg
   2. df-mulg
   3. mulgfval
   4. mulgfvalALT
   5. mulgval
   6. mulgfn
   7. mulgfvi
   8. mulg0
   9. mulgnn
   10. ressmulgnn
   11. ressmulgnn0
   12. mulgnngsum
   13. mulgnn0gsum
   14. mulg1
   15. mulgnnp1
   16. mulg2
   17. mulgnegnn
   18. mulgnn0p1
   19. mulgnnsubcl
   20. mulgnn0subcl
   21. mulgsubcl
   22. mulgnncl
   23. mulgnn0cl
   24. mulgcl
   25. mulgneg
   26. mulgnegneg
   27. mulgm1
   28. mulgnn0cld
   29. mulgcld
   30. mulgaddcomlem
   31. mulgaddcom
   32. mulginvcom
   33. mulginvinv
   34. mulgnn0z
   35. mulgz
   36. mulgnndir
   37. mulgnn0dir
   38. mulgdirlem
   39. mulgdir
   40. mulgp1
   41. mulgneg2
   42. mulgnnass
   43. mulgnn0ass
   44. mulgass
   45. mulgassr
   46. mulgmodid
   47. mulgsubdir
   48. mhmmulg
   49. mulgpropd
   50. submmulgcl
   51. submmulg
   52. pwsmulg
3. Subgroups and Quotient groups
   1. csubg
   2. cnsg
   3. cqg
   4. df-subg
   5. df-nsg
   6. df-eqg
   7. issubg
   8. subgss
   9. subgid
   10. subggrp
   11. subgbas
   12. subgrcl
   13. subg0
   14. subginv
   15. subg0cl
   16. subginvcl
   17. subgcl
   18. subgsubcl
   19. subgsub
   20. subgmulgcl
   21. subgmulg
   22. issubg2
   23. issubgrpd2
   24. issubgrpd
   25. issubg3
   26. issubg4
   27. grpissubg
   28. resgrpisgrp
   29. subgsubm
   30. subsubg
   31. subgint
   32. 0subg
   33. 0subgOLD
   34. trivsubgd
   35. trivsubgsnd
   36. isnsg
   37. isnsg2
   38. nsgbi
   39. nsgsubg
   40. nsgconj
   41. isnsg3
   42. subgacs
   43. nsgacs
   44. elnmz
   45. nmzbi
   46. nmzsubg
   47. ssnmz
   48. isnsg4
   49. nmznsg
   50. 0nsg
   51. nsgid
   52. 0idnsgd
   53. trivnsgd
   54. triv1nsgd
   55. 1nsgtrivd
   56. releqg
   57. eqgfval
   58. eqgval
   59. eqger
   60. eqglact
   61. eqgid
   62. eqgen
   63. eqgcpbl
   64. eqg0el
   65. quselbas
   66. quseccl0
   67. qusgrp
   68. quseccl
   69. qusadd
   70. qus0
   71. qusinv
   72. qussub
   73. ecqusaddd
   74. ecqusaddcl
   75. lagsubg2
   76. lagsubg
   77. eqg0subg
   78. eqg0subgecsn
   79. qus0subgbas
   80. qus0subgadd
4. Cyclic monoids and groups
   1. cycsubmel
   2. cycsubmcl
   3. cycsubm
   4. cyccom
   5. cycsubmcom
   6. cycsubggend
   7. cycsubgcl
   8. cycsubgss
   9. cycsubg
   10. cycsubgcld
   11. cycsubg2
   12. cycsubg2cl
5. Elementary theory of group homomorphisms
   1. cghm
   2. df-ghm
   3. reldmghm
   4. isghm
   5. isghm3
   6. ghmgrp1
   7. ghmgrp2
   8. ghmf
   9. ghmlin
   10. ghmid
   11. ghminv
   12. ghmsub
   13. isghmd
   14. ghmmhm
   15. ghmmhmb
   16. ghmmulg
   17. ghmrn
   18. 0ghm
   19. idghm
   20. resghm
   21. resghm2
   22. resghm2b
   23. ghmghmrn
   24. ghmco
   25. ghmima
   26. ghmpreima
   27. ghmeql
   28. ghmnsgima
   29. ghmnsgpreima
   30. ghmker
   31. ghmeqker
   32. pwsdiagghm
   33. f1ghm0to0
   34. ghmf1
   35. kerf1ghm
   36. ghmf1o
   37. conjghm
   38. conjsubg
   39. conjsubgen
   40. conjnmz
   41. conjnmzb
   42. conjnsg
   43. qusghm
   44. ghmpropd
6. Isomorphisms of groups
   1. cgim
   2. cgic
   3. df-gim
   4. df-gic
   5. gimfn
   6. isgim
   7. gimf1o
   8. gimghm
   9. isgim2
   10. subggim
   11. gimcnv
   12. gimco
   13. gim0to0
   14. brgic
   15. brgici
   16. gicref
   17. giclcl
   18. gicrcl
   19. gicsym
   20. gictr
   21. gicer
   22. gicen
   23. gicsubgen
   24. The first isomorphism theorem of groups
7. Group actions
   1. cga
   2. df-ga
   3. isga
   4. gagrp
   5. gaset
   6. gagrpid
   7. gaf
   8. gafo
   9. gaass
   10. ga0
   11. gaid
   12. subgga
   13. gass
   14. gasubg
   15. gaid2
   16. galcan
   17. gacan
   18. gapm
   19. gaorb
   20. gaorber
   21. gastacl
   22. gastacos
   23. orbstafun
   24. orbstaval
   25. orbsta
   26. orbsta2
8. Centralizers and centers
   1. ccntz
   2. ccntr
   3. df-cntz
   4. df-cntr
   5. cntrval
   6. cntzfval
   7. cntzval
   8. elcntz
   9. cntzel
   10. cntzsnval
   11. elcntzsn
   12. sscntz
   13. cntzrcl
   14. cntzssv
   15. cntzi
   16. elcntr
   17. cntrss
   18. cntri
   19. resscntz
   20. cntzsgrpcl
   21. cntz2ss
   22. cntzrec
   23. cntziinsn
   24. cntzsubm
   25. cntzsubg
   26. cntzidss
   27. cntzmhm
   28. cntzmhm2
   29. cntrsubgnsg
   30. cntrnsg
9. The opposite group
   1. coppg
   2. df-oppg
   3. oppgval
   4. oppgplusfval
   5. oppgplus
   6. setsplusg
   7. oppglemOLD
   8. oppgbas
   9. oppgbasOLD
   10. oppgtset
   11. oppgtsetOLD
   12. oppgtopn
   13. oppgmnd
   14. oppgmndb
   15. oppgid
   16. oppggrp
   17. oppggrpb
   18. oppginv
   19. invoppggim
   20. oppggic
   21. oppgsubm
   22. oppgsubg
   23. oppgcntz
   24. oppgcntr
   25. gsumwrev
10. Symmetric groups
    1. Definition and basic properties
    2. Cayley's theorem
    3. Permutations fixing one element
    4. Transpositions in the symmetric group
    5. The sign of a permutation
11. p-Groups and Sylow groups; Sylow's theorems
    1. cod
    2. cgex
    3. cpgp
    4. cslw
    5. df-od
    6. df-gex
    7. df-pgp
    8. df-slw
    9. odfval
    10. odfvalALT
    11. odval
    12. odlem1
    13. odcl
    14. odf
    15. odid
    16. odlem2
    17. odmodnn0
    18. mndodconglem
    19. mndodcong
    20. mndodcongi
    21. oddvdsnn0
    22. odnncl
    23. odmod
    24. oddvds
    25. oddvdsi
    26. odcong
    27. odeq
    28. odval2
    29. odcld
    30. odm1inv
    31. odmulgid
    32. odmulg2
    33. odmulg
    34. odmulgeq
    35. odbezout
    36. od1
    37. odeq1
    38. odinv
    39. odf1
    40. odinf
    41. dfod2
    42. odcl2
    43. oddvds2
    44. finodsubmsubg
    45. 0subgALT
    46. submod
    47. subgod
    48. odsubdvds
    49. odf1o1
    50. odf1o2
    51. odhash
    52. odhash2
    53. odhash3
    54. odngen
    55. gexval
    56. gexlem1
    57. gexcl
    58. gexid
    59. gexlem2
    60. gexdvdsi
    61. gexdvds
    62. gexdvds2
    63. gexod
    64. gexcl3
    65. gexnnod
    66. gexcl2
    67. gexdvds3
    68. gex1
    69. ispgp
    70. pgpprm
    71. pgpgrp
    72. pgpfi1
    73. pgp0
    74. subgpgp
    75. sylow1lem1
    76. sylow1lem2
    77. sylow1lem3
    78. sylow1lem4
    79. sylow1lem5
    80. sylow1
    81. odcau
    82. pgpfi
    83. pgpfi2
    84. pgphash
    85. isslw
    86. slwprm
    87. slwsubg
    88. slwispgp
    89. slwpss
    90. slwpgp
    91. pgpssslw
    92. slwn0
    93. subgslw
    94. sylow2alem1
    95. sylow2alem2
    96. sylow2a
    97. sylow2blem1
    98. sylow2blem2
    99. sylow2blem3
    100. sylow2b
    101. slwhash
    102. fislw
    103. sylow2
    104. sylow3lem1
    105. sylow3lem2
    106. sylow3lem3
    107. sylow3lem4
    108. sylow3lem5
    109. sylow3lem6
    110. sylow3
12. Direct products
    1. clsm
    2. cpj1
    3. df-lsm
    4. df-pj1
    5. lsmfval
    6. lsmvalx
    7. lsmelvalx
    8. lsmelvalix
    9. oppglsm
    10. lsmssv
    11. lsmless1x
    12. lsmless2x
    13. lsmub1x
    14. lsmub2x
    15. lsmval
    16. lsmelval
    17. lsmelvali
    18. lsmelvalm
    19. lsmelvalmi
    20. lsmsubm
    21. lsmsubg
    22. lsmcom2
    23. Direct products (extension)
13. Free groups
    1. cefg
    2. cfrgp
    3. cvrgp
    4. df-efg
    5. df-frgp
    6. df-vrgp
    7. efgmval
    8. efgmf
    9. efgmnvl
    10. efgrcl
    11. efglem
    12. efgval
    13. efger
    14. efgi
    15. efgi0
    16. efgi1
    17. efgtf
    18. efgtval
    19. efgval2
    20. efgi2
    21. efgtlen
    22. efginvrel2
    23. efginvrel1
    24. efgsf
    25. efgsdm
    26. efgsval
    27. efgsdmi
    28. efgsval2
    29. efgsrel
    30. efgs1
    31. efgs1b
    32. efgsp1
    33. efgsres
    34. efgsfo
    35. efgredlema
    36. efgredlemf
    37. efgredlemg
    38. efgredleme
    39. efgredlemd
    40. efgredlemc
    41. efgredlemb
    42. efgredlem
    43. efgred
    44. efgrelexlema
    45. efgrelexlemb
    46. efgrelex
    47. efgredeu
    48. efgred2
    49. efgcpbllema
    50. efgcpbllemb
    51. efgcpbl
    52. efgcpbl2
    53. frgpval
    54. frgpcpbl
    55. frgp0
    56. frgpeccl
    57. frgpgrp
    58. frgpadd
    59. frgpinv
    60. frgpmhm
    61. vrgpfval
    62. vrgpval
    63. vrgpf
    64. vrgpinv
    65. frgpuptf
    66. frgpuptinv
    67. frgpuplem
    68. frgpupf
    69. frgpupval
    70. frgpup1
    71. frgpup2
    72. frgpup3lem
    73. frgpup3
    74. 0frgp
14. Abelian groups
    1. Definition and basic properties
    2. Cyclic groups
    3. Group sum operation
    4. Group sums over (ranges of) integers
    5. Internal direct products
    6. The Fundamental Theorem of Abelian Groups
15. Simple groups
    1. Definition and basic properties
    2. Classification of abelian simple groups