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. psraddclOLD
  37. rhmpsrlem1
  38. rhmpsrlem2
  39. psrmulr
  40. psrmulfval
  41. psrmulval
  42. psrmulcllem
  43. psrmulcl
  44. psrsca
  45. psrvscafval
  46. psrvsca
  47. psrvscaval
  48. psrvscacl
  49. psr0cl
  50. psr0lid
  51. psrnegcl
  52. psrlinv
  53. psrgrp
  54. psrgrpOLD
  55. psr0
  56. psrneg
  57. psrlmod
  58. psr1cl
  59. psrlidm
  60. psrridm
  61. psrass1
  62. psrdi
  63. psrdir
  64. psrass23l
  65. psrcom
  66. psrass23
  67. psrring
  68. psr1
  69. psrcrng
  70. psrassa
  71. resspsrbas
  72. resspsradd
  73. resspsrmul
  74. resspsrvsca
  75. subrgpsr
  76. psrascl
  77. psrasclcl
  78. mvrfval
  79. mvrval
  80. mvrval2
  81. mvrid
  82. mvrf
  83. mvrf1
  84. mvrcl2
  85. reldmmpl
  86. mplval
  87. mplbas
  88. mplelbas
  89. mvrcl
  90. mvrf2
  91. mplrcl
  92. mplelsfi
  93. mplval2
  94. mplbasss
  95. mplelf
  96. mplsubglem
  97. mpllsslem
  98. mplsubglem2
  99. mplsubg
  100. mpllss
  101. mplsubrglem
  102. mplsubrg
  103. mpl0
  104. mplplusg
  105. mplmulr
  106. mpladd
  107. mplneg
  108. mplmul
  109. mpl1
  110. mplsca
  111. mplvsca2
  112. mplvsca
  113. mplvscaval
  114. mplgrp
  115. mpllmod
  116. mplring
  117. mpllvec
  118. mplcrng
  119. mplassa
  120. mplringd
  121. mpllmodd
  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