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. grpstr
   33. grpbase
   34. grpplusg
   35. ressplusg
   36. grpbasex
   37. grpplusgx
   38. mulrndx
   39. mulridx
   40. basendxnmulrndx
   41. plusgndxnmulrndx
   42. rngstr
   43. rngbase
   44. rngplusg
   45. rngmulr
   46. starvndx
   47. starvid
   48. starvndxnbasendx
   49. starvndxnplusgndx
   50. starvndxnmulrndx
   51. ressmulr
   52. ressstarv
   53. srngstr
   54. srngbase
   55. srngplusg
   56. srngmulr
   57. srnginvl
   58. scandx
   59. scaid
   60. scandxnbasendx
   61. scandxnplusgndx
   62. scandxnmulrndx
   63. vscandx
   64. vscaid
   65. vscandxnbasendx
   66. vscandxnplusgndx
   67. vscandxnmulrndx
   68. vscandxnscandx
   69. lmodstr
   70. lmodbase
   71. lmodplusg
   72. lmodsca
   73. lmodvsca
   74. ipndx
   75. ipid
   76. ipndxnbasendx
   77. ipndxnplusgndx
   78. ipndxnmulrndx
   79. slotsdifipndx
   80. ipsstr
   81. ipsbase
   82. ipsaddg
   83. ipsmulr
   84. ipssca
   85. ipsvsca
   86. ipsip
   87. resssca
   88. ressvsca
   89. ressip
   90. phlstr
   91. phlbase
   92. phlplusg
   93. phlsca
   94. phlvsca
   95. phlip
   96. tsetndx
   97. tsetid
   98. tsetndxnn
   99. basendxlttsetndx
   100. tsetndxnbasendx
   101. tsetndxnplusgndx
   102. tsetndxnmulrndx
   103. tsetndxnstarvndx
   104. slotstnscsi
   105. topgrpstr
   106. topgrpbas
   107. topgrpplusg
   108. topgrptset
   109. resstset
   110. plendx
   111. pleid
   112. plendxnn
   113. basendxltplendx
   114. plendxnbasendx
   115. plendxnplusgndx
   116. plendxnmulrndx
   117. plendxnscandx
   118. plendxnvscandx
   119. slotsdifplendx
   120. otpsstr
   121. otpsbas
   122. otpstset
   123. otpsle
   124. ressle
   125. ocndx
   126. ocid
   127. basendxnocndx
   128. plendxnocndx
   129. dsndx
   130. dsid
   131. dsndxnn
   132. basendxltdsndx
   133. dsndxnbasendx
   134. dsndxnplusgndx
   135. dsndxnmulrndx
   136. slotsdnscsi
   137. dsndxntsetndx
   138. slotsdifdsndx
   139. unifndx
   140. unifid
   141. unifndxnn
   142. basendxltunifndx
   143. unifndxnbasendx
   144. unifndxntsetndx
   145. slotsdifunifndx
   146. ressunif
   147. odrngstr
   148. odrngbas
   149. odrngplusg
   150. odrngmulr
   151. odrngtset
   152. odrngle
   153. odrngds
   154. ressds
   155. homndx
   156. homid
   157. ccondx
   158. ccoid
   159. slotsbhcdif
   160. slotsdifplendx2
   161. slotsdifocndx
   162. resshom
   163. 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