Metamath Proof Explorer

Table of Contents - 11.3.1. Definition and basic properties

  1. cmps
  2. cmvr
  3. cmpl
  4. cltb
  5. copws
  6. df-psr
  7. df-mvr
  8. df-mpl
  9. df-ltbag
  10. df-opsr
  11. reldmpsr
  12. psrval
  13. psrvalstr
  14. psrbag
  15. psrbagf
  16. psrbagfsupp
  17. snifpsrbag
  18. fczpsrbag
  19. psrbaglesupp
  20. psrbaglecl
  21. psrbagaddcl
  22. psrbagcon
  23. psrbaglefi
  24. psrbagconcl
  25. psrbagleadd1
  26. psrbagconf1o
  27. gsumbagdiaglem
  28. gsumbagdiag
  29. psrass1lem
  30. psrbas
  31. psrelbas
  32. psrelbasfun
  33. psrplusg
  34. psradd
  35. psraddcl
  36. rhmpsrlem1
  37. rhmpsrlem2
  38. psrmulr
  39. psrmulfval
  40. psrmulval
  41. psrmulcllem
  42. psrmulcl
  43. psrsca
  44. psrvscafval
  45. psrvsca
  46. psrvscaval
  47. psrvscacl
  48. psr0cl
  49. psr0lid
  50. psrnegcl
  51. psrlinv
  52. psrgrp
  53. psr0
  54. psrneg
  55. psrlmod
  56. psr1cl
  57. psrlidm
  58. psrridm
  59. psrass1
  60. psrdi
  61. psrdir
  62. psrass23l
  63. psrcom
  64. psrass23
  65. psrring
  66. psr1
  67. psrcrng
  68. psrassa
  69. resspsrbas
  70. resspsradd
  71. resspsrmul
  72. resspsrvsca
  73. subrgpsr
  74. psrascl
  75. psrasclcl
  76. mvrfval
  77. mvrval
  78. mvrval2
  79. mvrid
  80. mvrf
  81. mvrf1
  82. mvrcl2
  83. reldmmpl
  84. mplval
  85. mplbas
  86. mplelbas
  87. mvrcl
  88. mvrf2
  89. mplrcl
  90. mplelsfi
  91. mplval2
  92. mplbasss
  93. mplelf
  94. mplsubglem
  95. mpllsslem
  96. mplsubglem2
  97. mplsubg
  98. mpllss
  99. mplsubrglem
  100. mplsubrg
  101. mpl0
  102. mplplusg
  103. mplmulr
  104. mpladd
  105. mplneg
  106. mplmul
  107. mpl1
  108. mplsca
  109. mplvsca2
  110. mplvsca
  111. mplvscaval
  112. mplgrp
  113. mpllmod
  114. mplring
  115. mpllvec
  116. mplcrng
  117. mplassa
  118. mplringd
  119. mpllmodd
  120. mplascl0
  121. mplascl1
  122. ressmplbas2
  123. ressmplbas
  124. ressmpladd
  125. ressmplmul
  126. ressmplvsca
  127. subrgmpl
  128. subrgmvr
  129. subrgmvrf
  130. mplmon
  131. mplmonmul
  132. mplcoe1
  133. mplcoe3
  134. mplcoe5lem
  135. mplcoe5
  136. mplcoe2
  137. mplbas2
  138. ltbval
  139. ltbwe
  140. reldmopsr
  141. opsrval
  142. opsrle
  143. opsrval2
  144. opsrbaslem
  145. opsrbas
  146. opsrplusg
  147. opsrmulr
  148. opsrvsca
  149. opsrsca
  150. opsrtoslem1
  151. opsrtoslem2
  152. opsrtos
  153. opsrso
  154. opsrcrng
  155. opsrassa
  156. mplmon2
  157. psrbag0
  158. psrbagsn
  159. mplascl
  160. mplasclf
  161. subrgascl
  162. subrgasclcl
  163. mplmon2cl
  164. mplmon2mul
  165. mplind
  166. mplcoe4