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