![]() |
Metamath
Proof Explorer Theorem List (p. 174 of 481) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30603) |
![]() (30604-32126) |
![]() (32127-48013) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | phlsca 17301 | The ring of scalars of a constructed pre-Hilbert space. (Contributed by Mario Carneiro, 6-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐻 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(Scalar‘ndx), 𝑇〉} ∪ {〈( ·𝑠 ‘ndx), · 〉, 〈(·𝑖‘ndx), , 〉}) ⇒ ⊢ (𝑇 ∈ 𝑋 → 𝑇 = (Scalar‘𝐻)) | ||
Theorem | phlvsca 17302 | The scalar product operation of a constructed pre-Hilbert space. (Contributed by Mario Carneiro, 6-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐻 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(Scalar‘ndx), 𝑇〉} ∪ {〈( ·𝑠 ‘ndx), · 〉, 〈(·𝑖‘ndx), , 〉}) ⇒ ⊢ ( · ∈ 𝑋 → · = ( ·𝑠 ‘𝐻)) | ||
Theorem | phlip 17303 | The inner product (Hermitian form) operation of a constructed pre-Hilbert space. (Contributed by Mario Carneiro, 6-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐻 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(Scalar‘ndx), 𝑇〉} ∪ {〈( ·𝑠 ‘ndx), · 〉, 〈(·𝑖‘ndx), , 〉}) ⇒ ⊢ ( , ∈ 𝑋 → , = (·𝑖‘𝐻)) | ||
Theorem | tsetndx 17304 | Index value of the df-tset 17223 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
⊢ (TopSet‘ndx) = 9 | ||
Theorem | tsetid 17305 | Utility theorem: index-independent form of df-tset 17223. (Contributed by NM, 20-Oct-2012.) |
⊢ TopSet = Slot (TopSet‘ndx) | ||
Theorem | tsetndxnn 17306 | The index of the slot for the group operation in an extensible structure is a positive integer. (Contributed by AV, 31-Oct-2024.) |
⊢ (TopSet‘ndx) ∈ ℕ | ||
Theorem | basendxlttsetndx 17307 | The index of the slot for the base set is less then the index of the slot for the topology in an extensible structure. (Contributed by AV, 31-Oct-2024.) |
⊢ (Base‘ndx) < (TopSet‘ndx) | ||
Theorem | tsetndxnbasendx 17308 | The slot for the topology is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 31-Oct-2024.) |
⊢ (TopSet‘ndx) ≠ (Base‘ndx) | ||
Theorem | tsetndxnplusgndx 17309 | The slot for the topology is not the slot for the group operation in an extensible structure. Formerly part of proof for oppgtset 19266. (Contributed by AV, 18-Oct-2024.) |
⊢ (TopSet‘ndx) ≠ (+g‘ndx) | ||
Theorem | tsetndxnmulrndx 17310 | The slot for the topology is not the slot for the ring multiplication operation in an extensible structure. (Contributed by AV, 31-Oct-2024.) |
⊢ (TopSet‘ndx) ≠ (.r‘ndx) | ||
Theorem | tsetndxnstarvndx 17311 | The slot for the topology is not the slot for the involution in an extensible structure. Formerly part of proof for cnfldfunALT 21245. (Contributed by AV, 11-Nov-2024.) |
⊢ (TopSet‘ndx) ≠ (*𝑟‘ndx) | ||
Theorem | slotstnscsi 17312 | The slots Scalar, ·𝑠 and ·𝑖 are different from the slot TopSet. Formerly part of sralem 21023 and proofs using it. (Contributed by AV, 29-Oct-2024.) |
⊢ ((TopSet‘ndx) ≠ (Scalar‘ndx) ∧ (TopSet‘ndx) ≠ ( ·𝑠 ‘ndx) ∧ (TopSet‘ndx) ≠ (·𝑖‘ndx)) | ||
Theorem | topgrpstr 17313 | A constructed topological group is a structure. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝑊 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(TopSet‘ndx), 𝐽〉} ⇒ ⊢ 𝑊 Struct 〈1, 9〉 | ||
Theorem | topgrpbas 17314 | The base set of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝑊 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(TopSet‘ndx), 𝐽〉} ⇒ ⊢ (𝐵 ∈ 𝑋 → 𝐵 = (Base‘𝑊)) | ||
Theorem | topgrpplusg 17315 | The additive operation of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝑊 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(TopSet‘ndx), 𝐽〉} ⇒ ⊢ ( + ∈ 𝑋 → + = (+g‘𝑊)) | ||
Theorem | topgrptset 17316 | The topology of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝑊 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(TopSet‘ndx), 𝐽〉} ⇒ ⊢ (𝐽 ∈ 𝑋 → 𝐽 = (TopSet‘𝑊)) | ||
Theorem | resstset 17317 | TopSet is unaffected by restriction. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐽 = (TopSet‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐽 = (TopSet‘𝐻)) | ||
Theorem | plendx 17318 | Index value of the df-ple 17224 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.) (New usage is discouraged.) |
⊢ (le‘ndx) = ;10 | ||
Theorem | pleid 17319 | Utility theorem: self-referencing, index-independent form of df-ple 17224. (Contributed by NM, 9-Nov-2012.) (Revised by AV, 9-Sep-2021.) |
⊢ le = Slot (le‘ndx) | ||
Theorem | plendxnn 17320 | The index value of the order slot is a positive integer. This property should be ensured for every concrete coding because otherwise it could not be used in an extensible structure (slots must be positive integers). (Contributed by AV, 30-Oct-2024.) |
⊢ (le‘ndx) ∈ ℕ | ||
Theorem | basendxltplendx 17321 | The index value of the Base slot is less than the index value of the le slot. (Contributed by AV, 30-Oct-2024.) |
⊢ (Base‘ndx) < (le‘ndx) | ||
Theorem | plendxnbasendx 17322 | The slot for the order is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 30-Oct-2024.) |
⊢ (le‘ndx) ≠ (Base‘ndx) | ||
Theorem | plendxnplusgndx 17323 | The slot for the "less than or equal to" ordering is not the slot for the group operation in an extensible structure. Formerly part of proof for oppgle 32562. (Contributed by AV, 18-Oct-2024.) |
⊢ (le‘ndx) ≠ (+g‘ndx) | ||
Theorem | plendxnmulrndx 17324 | The slot for the "less than or equal to" ordering is not the slot for the ring multiplication operation in an extensible structure. Formerly part of proof for opsrmulr 21920. (Contributed by AV, 1-Nov-2024.) |
⊢ (le‘ndx) ≠ (.r‘ndx) | ||
Theorem | plendxnscandx 17325 | The slot for the "less than or equal to" ordering is not the slot for the scalar in an extensible structure. Formerly part of proof for opsrsca 21924. (Contributed by AV, 1-Nov-2024.) |
⊢ (le‘ndx) ≠ (Scalar‘ndx) | ||
Theorem | plendxnvscandx 17326 | The slot for the "less than or equal to" ordering is not the slot for the scalar product in an extensible structure. Formerly part of proof for opsrvsca 21922. (Contributed by AV, 1-Nov-2024.) |
⊢ (le‘ndx) ≠ ( ·𝑠 ‘ndx) | ||
Theorem | slotsdifplendx 17327 | The index of the slot for the distance is not the index of other slots. Formerly part of proof for cnfldfunALT 21245. (Contributed by AV, 11-Nov-2024.) |
⊢ ((*𝑟‘ndx) ≠ (le‘ndx) ∧ (TopSet‘ndx) ≠ (le‘ndx)) | ||
Theorem | otpsstr 17328 | Functionality of a topological ordered space. (Contributed by Mario Carneiro, 12-Nov-2015.) (Revised by AV, 9-Sep-2021.) |
⊢ 𝐾 = {〈(Base‘ndx), 𝐵〉, 〈(TopSet‘ndx), 𝐽〉, 〈(le‘ndx), ≤ 〉} ⇒ ⊢ 𝐾 Struct 〈1, ;10〉 | ||
Theorem | otpsbas 17329 | The base set of a topological ordered space. (Contributed by Mario Carneiro, 12-Nov-2015.) (Revised by AV, 9-Sep-2021.) |
⊢ 𝐾 = {〈(Base‘ndx), 𝐵〉, 〈(TopSet‘ndx), 𝐽〉, 〈(le‘ndx), ≤ 〉} ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐾)) | ||
Theorem | otpstset 17330 | The open sets of a topological ordered space. (Contributed by Mario Carneiro, 12-Nov-2015.) (Revised by AV, 9-Sep-2021.) |
⊢ 𝐾 = {〈(Base‘ndx), 𝐵〉, 〈(TopSet‘ndx), 𝐽〉, 〈(le‘ndx), ≤ 〉} ⇒ ⊢ (𝐽 ∈ 𝑉 → 𝐽 = (TopSet‘𝐾)) | ||
Theorem | otpsle 17331 | The order of a topological ordered space. (Contributed by Mario Carneiro, 12-Nov-2015.) (Revised by AV, 9-Sep-2021.) |
⊢ 𝐾 = {〈(Base‘ndx), 𝐵〉, 〈(TopSet‘ndx), 𝐽〉, 〈(le‘ndx), ≤ 〉} ⇒ ⊢ ( ≤ ∈ 𝑉 → ≤ = (le‘𝐾)) | ||
Theorem | ressle 17332 | le is unaffected by restriction. (Contributed by Mario Carneiro, 3-Nov-2015.) |
⊢ 𝑊 = (𝐾 ↾s 𝐴) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐴 ∈ 𝑉 → ≤ = (le‘𝑊)) | ||
Theorem | ocndx 17333 | Index value of the df-ocomp 17225 slot. (Contributed by Mario Carneiro, 25-Oct-2015.) (New usage is discouraged.) |
⊢ (oc‘ndx) = ;11 | ||
Theorem | ocid 17334 | Utility theorem: index-independent form of df-ocomp 17225. (Contributed by Mario Carneiro, 25-Oct-2015.) |
⊢ oc = Slot (oc‘ndx) | ||
Theorem | basendxnocndx 17335 | The slot for the orthocomplementation is not the slot for the base set in an extensible structure. Formerly part of proof for thlbas 21558. (Contributed by AV, 11-Nov-2024.) |
⊢ (Base‘ndx) ≠ (oc‘ndx) | ||
Theorem | plendxnocndx 17336 | The slot for the orthocomplementation is not the slot for the order in an extensible structure. Formerly part of proof for thlle 21560. (Contributed by AV, 11-Nov-2024.) |
⊢ (le‘ndx) ≠ (oc‘ndx) | ||
Theorem | dsndx 17337 | Index value of the df-ds 17226 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
⊢ (dist‘ndx) = ;12 | ||
Theorem | dsid 17338 | Utility theorem: index-independent form of df-ds 17226. (Contributed by Mario Carneiro, 23-Dec-2013.) |
⊢ dist = Slot (dist‘ndx) | ||
Theorem | dsndxnn 17339 | The index of the slot for the distance in an extensible structure is a positive integer. Formerly part of proof for tmslem 24309. (Contributed by AV, 28-Oct-2024.) |
⊢ (dist‘ndx) ∈ ℕ | ||
Theorem | basendxltdsndx 17340 | The index of the slot for the base set is less then the index of the slot for the distance in an extensible structure. Formerly part of proof for tmslem 24309. (Contributed by AV, 28-Oct-2024.) |
⊢ (Base‘ndx) < (dist‘ndx) | ||
Theorem | dsndxnbasendx 17341 | The slot for the distance is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 28-Oct-2024.) |
⊢ (dist‘ndx) ≠ (Base‘ndx) | ||
Theorem | dsndxnplusgndx 17342 | The slot for the distance function is not the slot for the group operation in an extensible structure. Formerly part of proof for mgpds 20048. (Contributed by AV, 18-Oct-2024.) |
⊢ (dist‘ndx) ≠ (+g‘ndx) | ||
Theorem | dsndxnmulrndx 17343 | The slot for the distance function is not the slot for the ring multiplication operation in an extensible structure. (Contributed by AV, 31-Oct-2024.) |
⊢ (dist‘ndx) ≠ (.r‘ndx) | ||
Theorem | slotsdnscsi 17344 | The slots Scalar, ·𝑠 and ·𝑖 are different from the slot dist. Formerly part of sralem 21023 and proofs using it. (Contributed by AV, 29-Oct-2024.) |
⊢ ((dist‘ndx) ≠ (Scalar‘ndx) ∧ (dist‘ndx) ≠ ( ·𝑠 ‘ndx) ∧ (dist‘ndx) ≠ (·𝑖‘ndx)) | ||
Theorem | dsndxntsetndx 17345 | The slot for the distance function is not the slot for the topology in an extensible structure. Formerly part of proof for tngds 24483. (Contributed by AV, 29-Oct-2024.) |
⊢ (dist‘ndx) ≠ (TopSet‘ndx) | ||
Theorem | slotsdifdsndx 17346 | The index of the slot for the distance is not the index of other slots. Formerly part of proof for cnfldfunALT 21245. (Contributed by AV, 11-Nov-2024.) |
⊢ ((*𝑟‘ndx) ≠ (dist‘ndx) ∧ (le‘ndx) ≠ (dist‘ndx)) | ||
Theorem | unifndx 17347 | Index value of the df-unif 17227 slot. (Contributed by Thierry Arnoux, 17-Dec-2017.) (New usage is discouraged.) |
⊢ (UnifSet‘ndx) = ;13 | ||
Theorem | unifid 17348 | Utility theorem: index-independent form of df-unif 17227. (Contributed by Thierry Arnoux, 17-Dec-2017.) |
⊢ UnifSet = Slot (UnifSet‘ndx) | ||
Theorem | unifndxnn 17349 | The index of the slot for the uniform set in an extensible structure is a positive integer. Formerly part of proof for tuslem 24090. (Contributed by AV, 28-Oct-2024.) |
⊢ (UnifSet‘ndx) ∈ ℕ | ||
Theorem | basendxltunifndx 17350 | The index of the slot for the base set is less then the index of the slot for the uniform set in an extensible structure. Formerly part of proof for tuslem 24090. (Contributed by AV, 28-Oct-2024.) |
⊢ (Base‘ndx) < (UnifSet‘ndx) | ||
Theorem | unifndxnbasendx 17351 | The slot for the uniform set is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) |
⊢ (UnifSet‘ndx) ≠ (Base‘ndx) | ||
Theorem | unifndxntsetndx 17352 | The slot for the uniform set is not the slot for the topology in an extensible structure. Formerly part of proof for tuslem 24090. (Contributed by AV, 28-Oct-2024.) |
⊢ (UnifSet‘ndx) ≠ (TopSet‘ndx) | ||
Theorem | slotsdifunifndx 17353 | The index of the slot for the uniform set is not the index of other slots. Formerly part of proof for cnfldfunALT 21245. (Contributed by AV, 10-Nov-2024.) |
⊢ (((+g‘ndx) ≠ (UnifSet‘ndx) ∧ (.r‘ndx) ≠ (UnifSet‘ndx) ∧ (*𝑟‘ndx) ≠ (UnifSet‘ndx)) ∧ ((le‘ndx) ≠ (UnifSet‘ndx) ∧ (dist‘ndx) ≠ (UnifSet‘ndx))) | ||
Theorem | ressunif 17354 | UnifSet is unaffected by restriction. (Contributed by Thierry Arnoux, 7-Dec-2017.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝑈 = (UnifSet‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝑈 = (UnifSet‘𝐻)) | ||
Theorem | odrngstr 17355 | Functionality of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015.) (Proof shortened by AV, 15-Sep-2021.) |
⊢ 𝑊 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(TopSet‘ndx), 𝐽〉, 〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), 𝐷〉}) ⇒ ⊢ 𝑊 Struct 〈1, ;12〉 | ||
Theorem | odrngbas 17356 | The base set of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑊 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(TopSet‘ndx), 𝐽〉, 〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), 𝐷〉}) ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝑊)) | ||
Theorem | odrngplusg 17357 | The addition operation of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑊 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(TopSet‘ndx), 𝐽〉, 〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), 𝐷〉}) ⇒ ⊢ ( + ∈ 𝑉 → + = (+g‘𝑊)) | ||
Theorem | odrngmulr 17358 | The multiplication operation of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑊 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(TopSet‘ndx), 𝐽〉, 〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), 𝐷〉}) ⇒ ⊢ ( · ∈ 𝑉 → · = (.r‘𝑊)) | ||
Theorem | odrngtset 17359 | The open sets of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑊 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(TopSet‘ndx), 𝐽〉, 〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), 𝐷〉}) ⇒ ⊢ (𝐽 ∈ 𝑉 → 𝐽 = (TopSet‘𝑊)) | ||
Theorem | odrngle 17360 | The order of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑊 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(TopSet‘ndx), 𝐽〉, 〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), 𝐷〉}) ⇒ ⊢ ( ≤ ∈ 𝑉 → ≤ = (le‘𝑊)) | ||
Theorem | odrngds 17361 | The metric of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑊 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(TopSet‘ndx), 𝐽〉, 〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), 𝐷〉}) ⇒ ⊢ (𝐷 ∈ 𝑉 → 𝐷 = (dist‘𝑊)) | ||
Theorem | ressds 17362 | dist is unaffected by restriction. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐷 = (dist‘𝐻)) | ||
Theorem | homndx 17363 | Index value of the df-hom 17228 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.) |
⊢ (Hom ‘ndx) = ;14 | ||
Theorem | homid 17364 | Utility theorem: index-independent form of df-hom 17228. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ Hom = Slot (Hom ‘ndx) | ||
Theorem | ccondx 17365 | Index value of the df-cco 17229 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.) |
⊢ (comp‘ndx) = ;15 | ||
Theorem | ccoid 17366 | Utility theorem: index-independent form of df-cco 17229. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ comp = Slot (comp‘ndx) | ||
Theorem | slotsbhcdif 17367 | The slots Base, Hom and comp are different. (Contributed by AV, 5-Mar-2020.) (Proof shortened by AV, 28-Oct-2024.) |
⊢ ((Base‘ndx) ≠ (Hom ‘ndx) ∧ (Base‘ndx) ≠ (comp‘ndx) ∧ (Hom ‘ndx) ≠ (comp‘ndx)) | ||
Theorem | slotsbhcdifOLD 17368 | Obsolete proof of slotsbhcdif 17367 as of 28-Oct-2024. The slots Base, Hom and comp are different. (Contributed by AV, 5-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((Base‘ndx) ≠ (Hom ‘ndx) ∧ (Base‘ndx) ≠ (comp‘ndx) ∧ (Hom ‘ndx) ≠ (comp‘ndx)) | ||
Theorem | slotsdifplendx2 17369 | The index of the slot for the "less than or equal to" ordering is not the index of other slots. Formerly part of proof for prstcleval 47849. (Contributed by AV, 12-Nov-2024.) |
⊢ ((le‘ndx) ≠ (comp‘ndx) ∧ (le‘ndx) ≠ (Hom ‘ndx)) | ||
Theorem | slotsdifocndx 17370 | The index of the slot for the orthocomplementation is not the index of other slots. Formerly part of proof for prstcocval 47852. (Contributed by AV, 12-Nov-2024.) |
⊢ ((oc‘ndx) ≠ (comp‘ndx) ∧ (oc‘ndx) ≠ (Hom ‘ndx)) | ||
Theorem | resshom 17371 | Hom is unaffected by restriction. (Contributed by Mario Carneiro, 5-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾s 𝐴) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐻 = (Hom ‘𝐷)) | ||
Theorem | ressco 17372 | comp is unaffected by restriction. (Contributed by Mario Carneiro, 5-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾s 𝐴) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = (comp‘𝐷)) | ||
Syntax | crest 17373 | Extend class notation with the function returning a subspace topology. |
class ↾t | ||
Syntax | ctopn 17374 | Extend class notation with the topology extractor function. |
class TopOpen | ||
Definition | df-rest 17375* | Function returning the subspace topology induced by the topology 𝑦 and the set 𝑥. (Contributed by FL, 20-Sep-2010.) (Revised by Mario Carneiro, 1-May-2015.) |
⊢ ↾t = (𝑗 ∈ V, 𝑥 ∈ V ↦ ran (𝑦 ∈ 𝑗 ↦ (𝑦 ∩ 𝑥))) | ||
Definition | df-topn 17376 | Define the topology extractor function. This differs from df-tset 17223 when a structure has been restricted using df-ress 17181; in this case the TopSet component will still have a topology over the larger set, and this function fixes this by restricting the topology as well. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ TopOpen = (𝑤 ∈ V ↦ ((TopSet‘𝑤) ↾t (Base‘𝑤))) | ||
Theorem | restfn 17377 | The subspace topology operator is a function on pairs. (Contributed by Mario Carneiro, 1-May-2015.) |
⊢ ↾t Fn (V × V) | ||
Theorem | topnfn 17378 | The topology extractor function is a function on the universe. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ TopOpen Fn V | ||
Theorem | restval 17379* | The subspace topology induced by the topology 𝐽 on the set 𝐴. (Contributed by FL, 20-Sep-2010.) (Revised by Mario Carneiro, 1-May-2015.) |
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝐽 ↾t 𝐴) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴))) | ||
Theorem | elrest 17380* | The predicate "is an open set of a subspace topology". (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵))) | ||
Theorem | elrestr 17381 | Sufficient condition for being an open set in a subspace. (Contributed by Jeff Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ ((𝐽 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐴 ∈ 𝐽) → (𝐴 ∩ 𝑆) ∈ (𝐽 ↾t 𝑆)) | ||
Theorem | 0rest 17382 | Value of the structure restriction when the topology input is empty. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ (∅ ↾t 𝐴) = ∅ | ||
Theorem | restid2 17383 | The subspace topology over a subset of the base set is the original topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴) → (𝐽 ↾t 𝐴) = 𝐽) | ||
Theorem | restsspw 17384 | The subspace topology is a collection of subsets of the restriction set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴 | ||
Theorem | firest 17385 | The finite intersections operator commutes with restriction. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ (fi‘(𝐽 ↾t 𝐴)) = ((fi‘𝐽) ↾t 𝐴) | ||
Theorem | restid 17386 | The subspace topology of the base set is the original topology. (Contributed by Jeff Hankins, 9-Jul-2009.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ 𝑉 → (𝐽 ↾t 𝑋) = 𝐽) | ||
Theorem | topnval 17387 | Value of the topology extractor function. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopSet‘𝑊) ⇒ ⊢ (𝐽 ↾t 𝐵) = (TopOpen‘𝑊) | ||
Theorem | topnid 17388 | Value of the topology extractor function when the topology is defined over the same set as the base. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopSet‘𝑊) ⇒ ⊢ (𝐽 ⊆ 𝒫 𝐵 → 𝐽 = (TopOpen‘𝑊)) | ||
Theorem | topnpropd 17389 | The topology extractor function depends only on the base and topology components. (Contributed by NM, 18-Jul-2006.) |
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) & ⊢ (𝜑 → (TopSet‘𝐾) = (TopSet‘𝐿)) ⇒ ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿)) | ||
Syntax | ctg 17390 | Extend class notation with a function that converts a basis to its corresponding topology. |
class topGen | ||
Syntax | cpt 17391 | Extend class notation with a function whose value is a product topology. |
class ∏t | ||
Syntax | c0g 17392 | Extend class notation with group identity element. |
class 0g | ||
Syntax | cgsu 17393 | Extend class notation to include finitely supported group sums. |
class Σg | ||
Definition | df-0g 17394* | Define group identity element. Remark: this definition is required here because the symbol 0g is already used in df-gsum 17395. The related theorems are provided later, see grpidval 18592. (Contributed by NM, 20-Aug-2011.) |
⊢ 0g = (𝑔 ∈ V ↦ (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥)))) | ||
Definition | df-gsum 17395* |
Define the group sum (also called "iterated sum") for the structure
𝐺 of a finite sequence of elements
whose values are defined by the
expression 𝐵 and whose set of indices is 𝐴. It
may be viewed
as a product (if 𝐺 is a multiplication), a sum (if
𝐺
is an
addition) or any other operation. The variable 𝑘 is normally a free
variable in 𝐵 (i.e., 𝐵 can be thought of as
𝐵(𝑘)). The
definition is meaningful in different contexts, depending on the size of
the index set 𝐴 and each demanding different
properties of 𝐺.
1. If 𝐴 = ∅ and 𝐺 has an identity element, then the sum equals this identity. See gsum0 18615. 2. If 𝐴 = (𝑀...𝑁) and 𝐺 is any magma, then the sum is the sum of the elements, evaluated left-to-right, i.e., (𝐵(1) + 𝐵(2)) + 𝐵(3), etc. See gsumval2 18617 and gsumnunsn 34015. 3. If 𝐴 is a finite set (or is nonzero for finitely many indices) and 𝐺 is a commutative monoid, then the sum adds up these elements in some order, which is then uniquely defined. See gsumval3 19823. 4. If 𝐴 is an infinite set and 𝐺 is a Hausdorff topological group, then there is a meaningful sum, but Σg cannot handle this case. See df-tsms 23950. Remark: this definition is required here because the symbol Σg is already used in df-prds 17400 and df-imas 17461. The related theorems are provided later, see gsumvalx 18607. (Contributed by FL, 5-Sep-2010.) (Revised by FL, 17-Oct-2011.) (Revised by Mario Carneiro, 7-Dec-2014.) |
⊢ Σg = (𝑤 ∈ V, 𝑓 ∈ V ↦ ⦋{𝑥 ∈ (Base‘𝑤) ∣ ∀𝑦 ∈ (Base‘𝑤)((𝑥(+g‘𝑤)𝑦) = 𝑦 ∧ (𝑦(+g‘𝑤)𝑥) = 𝑦)} / 𝑜⦌if(ran 𝑓 ⊆ 𝑜, (0g‘𝑤), if(dom 𝑓 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛))), (℩𝑥∃𝑔[(◡𝑓 “ (V ∖ 𝑜)) / 𝑦](𝑔:(1...(♯‘𝑦))–1-1-onto→𝑦 ∧ 𝑥 = (seq1((+g‘𝑤), (𝑓 ∘ 𝑔))‘(♯‘𝑦))))))) | ||
Definition | df-topgen 17396* | Define a function that converts a basis to its corresponding topology. Equivalent to the definition of a topology generated by a basis in [Munkres] p. 78 (see tgval2 22778). The first use of this definition is tgval 22777 but the token is used in df-pt 17397. See tgval3 22785 for an alternate expression for the value. (Contributed by NM, 16-Jul-2006.) |
⊢ topGen = (𝑥 ∈ V ↦ {𝑦 ∣ 𝑦 ⊆ ∪ (𝑥 ∩ 𝒫 𝑦)}) | ||
Definition | df-pt 17397* | Define the product topology on a collection of topologies. For convenience, it is defined on arbitrary collections of sets, expressed as a function from some index set to the subbases of each factor space. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ ∏t = (𝑓 ∈ V ↦ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))})) | ||
Syntax | cprds 17398 | The function constructing structure products. |
class Xs | ||
Syntax | cpws 17399 | The function constructing structure powers. |
class ↑s | ||
Definition | df-prds 17400* | Define a structure product. This can be a product of groups, rings, modules, or ordered topological fields; any unused components will have garbage in them but this is usually not relevant for the purpose of inheriting the structures present in the factors. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
⊢ Xs = (𝑠 ∈ V, 𝑟 ∈ V ↦ ⦋X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) / 𝑣⦌⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({〈(Base‘ndx), 𝑣〉, 〈(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))))〉, 〈(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))))〉} ∪ {〈(Scalar‘ndx), 𝑠〉, 〈( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))〉, 〈(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))〉}) ∪ ({〈(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))〉, 〈(le‘ndx), {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}〉, 〈(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))〉} ∪ {〈(Hom ‘ndx), ℎ〉, 〈(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(〈((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)〉(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))〉}))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |