Metamath Proof Explorer

Table of Contents - 7.1. Extensible structures

1. Basic definitions
   1. Extensible structures as structures with components
   2. Substitution of components
   3. Slots
   4. Structure component indices
   5. Base sets
   6. Base set restrictions
2. Slot definitions
   1. cplusg
   2. cmulr
   3. cstv
   4. csca
   5. cvsca
   6. cip
   7. cts
   8. cple
   9. coc
   10. cds
   11. cunif
   12. chom
   13. cco
   14. df-plusg
   15. df-mulr
   16. df-starv
   17. df-sca
   18. df-vsca
   19. df-ip
   20. df-tset
   21. df-ple
   22. df-ocomp
   23. df-ds
   24. df-unif
   25. df-hom
   26. df-cco
   27. plusgndx
   28. plusgid
   29. plusgndxnn
   30. basendxltplusgndx
   31. basendxnplusgndx
   32. basendxnplusgndxOLD
   33. grpstr
   34. grpstrndx
   35. grpbase
   36. grpbaseOLD
   37. grpplusg
   38. grpplusgOLD
   39. ressplusg
   40. grpbasex
   41. grpplusgx
   42. mulrndx
   43. mulrid
   44. basendxnmulrndx
   45. basendxnmulrndxOLD
   46. plusgndxnmulrndx
   47. rngstr
   48. rngbase
   49. rngplusg
   50. rngmulr
   51. starvndx
   52. starvid
   53. starvndxnbasendx
   54. starvndxnplusgndx
   55. starvndxnmulrndx
   56. ressmulr
   57. ressstarv
   58. srngstr
   59. srngbase
   60. srngplusg
   61. srngmulr
   62. srnginvl
   63. scandx
   64. scaid
   65. scandxnbasendx
   66. scandxnplusgndx
   67. scandxnmulrndx
   68. vscandx
   69. vscaid
   70. vscandxnbasendx
   71. vscandxnplusgndx
   72. vscandxnmulrndx
   73. vscandxnscandx
   74. lmodstr
   75. lmodbase
   76. lmodplusg
   77. lmodsca
   78. lmodvsca
   79. ipndx
   80. ipid
   81. ipndxnbasendx
   82. ipndxnplusgndx
   83. ipndxnmulrndx
   84. slotsdifipndx
   85. ipsstr
   86. ipsbase
   87. ipsaddg
   88. ipsmulr
   89. ipssca
   90. ipsvsca
   91. ipsip
   92. resssca
   93. ressvsca
   94. ressip
   95. phlstr
   96. phlbase
   97. phlplusg
   98. phlsca
   99. phlvsca
   100. phlip
   101. tsetndx
   102. tsetid
   103. tsetndxnn
   104. basendxlttsetndx
   105. tsetndxnbasendx
   106. tsetndxnplusgndx
   107. tsetndxnmulrndx
   108. tsetndxnstarvndx
   109. slotstnscsi
   110. topgrpstr
   111. topgrpbas
   112. topgrpplusg
   113. topgrptset
   114. resstset
   115. plendx
   116. pleid
   117. plendxnn
   118. basendxltplendx
   119. plendxnbasendx
   120. plendxnplusgndx
   121. plendxnmulrndx
   122. plendxnscandx
   123. plendxnvscandx
   124. slotsdifplendx
   125. otpsstr
   126. otpsbas
   127. otpstset
   128. otpsle
   129. ressle
   130. ocndx
   131. ocid
   132. basendxnocndx
   133. plendxnocndx
   134. dsndx
   135. dsid
   136. dsndxnn
   137. basendxltdsndx
   138. dsndxnbasendx
   139. dsndxnplusgndx
   140. dsndxnmulrndx
   141. slotsdnscsi
   142. dsndxntsetndx
   143. slotsdifdsndx
   144. unifndx
   145. unifid
   146. unifndxnn
   147. basendxltunifndx
   148. unifndxnbasendx
   149. unifndxntsetndx
   150. slotsdifunifndx
   151. ressunif
   152. odrngstr
   153. odrngbas
   154. odrngplusg
   155. odrngmulr
   156. odrngtset
   157. odrngle
   158. odrngds
   159. ressds
   160. homndx
   161. homid
   162. ccondx
   163. ccoid
   164. slotsbhcdif
   165. slotsbhcdifOLD
   166. slotsdifplendx2
   167. slotsdifocndx
   168. resshom
   169. ressco
3. Definition of the structure product
   1. crest
   2. ctopn
   3. df-rest
   4. df-topn
   5. restfn
   6. topnfn
   7. restval
   8. elrest
   9. elrestr
   10. 0rest
   11. restid2
   12. restsspw
   13. firest
   14. restid
   15. topnval
   16. topnid
   17. topnpropd
   18. ctg
   19. cpt
   20. c0g
   21. cgsu
   22. df-0g
   23. df-gsum
   24. df-topgen
   25. df-pt
   26. cprds
   27. cpws
   28. df-prds
   29. reldmprds
   30. df-pws
   31. prdsbasex
   32. imasvalstr
   33. prdsvalstr
   34. prdsbaslem
   35. prdsvallem
   36. prdsval
   37. prdssca
   38. prdsbas
   39. prdsplusg
   40. prdsmulr
   41. prdsvsca
   42. prdsip
   43. prdsle
   44. prdsless
   45. prdsds
   46. prdsdsfn
   47. prdstset
   48. prdshom
   49. prdsco
   50. prdsbas2
   51. prdsbasmpt
   52. prdsbasfn
   53. prdsbasprj
   54. prdsplusgval
   55. prdsplusgfval
   56. prdsmulrval
   57. prdsmulrfval
   58. prdsleval
   59. prdsdsval
   60. prdsvscaval
   61. prdsvscafval
   62. prdsbas3
   63. prdsbasmpt2
   64. prdsbascl
   65. prdsdsval2
   66. prdsdsval3
   67. pwsval
   68. pwsbas
   69. pwselbasb
   70. pwselbas
   71. pwsplusgval
   72. pwsmulrval
   73. pwsle
   74. pwsleval
   75. pwsvscafval
   76. pwsvscaval
   77. pwssca
   78. pwsdiagel
   79. pwssnf1o
4. Definition of the structure quotient
   1. cordt
   2. cxrs
   3. df-ordt
   4. df-xrs
   5. cqtop
   6. cimas
   7. cqus
   8. cxps
   9. df-qtop
   10. df-imas
   11. df-qus
   12. df-xps
   13. imasval
   14. imasbas
   15. imasds
   16. imasdsfn
   17. imasdsval
   18. imasdsval2
   19. imasplusg
   20. imasmulr
   21. imassca
   22. imasvsca
   23. imasip
   24. imastset
   25. imasle
   26. f1ocpbllem
   27. f1ocpbl
   28. f1ovscpbl
   29. f1olecpbl
   30. imasaddfnlem
   31. imasaddvallem
   32. imasaddflem
   33. imasaddfn
   34. imasaddval
   35. imasaddf
   36. imasmulfn
   37. imasmulval
   38. imasmulf
   39. imasvscafn
   40. imasvscaval
   41. imasvscaf
   42. imasless
   43. imasleval
   44. qusval
   45. quslem
   46. qusin
   47. qusbas
   48. quss
   49. divsfval
   50. ercpbllem
   51. ercpbl
   52. erlecpbl
   53. qusaddvallem
   54. qusaddflem
   55. qusaddval
   56. qusaddf
   57. qusmulval
   58. qusmulf
   59. fnpr2o
   60. fnpr2ob
   61. fvpr0o
   62. fvpr1o
   63. fvprif
   64. xpsfrnel
   65. xpsfeq
   66. xpsfrnel2
   67. xpscf
   68. xpsfval
   69. xpsff1o
   70. xpsfrn
   71. xpsff1o2
   72. xpsval
   73. xpsrnbas
   74. xpsbas
   75. xpsaddlem
   76. xpsadd
   77. xpsmul
   78. xpssca
   79. xpsvsca
   80. xpsless
   81. xpsle