| Metamath
Proof Explorer Theorem List (p. 175 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | tsetndxnplusgndx 17401 | The slot for the topology is not the slot for the group operation in an extensible structure. Formerly part of proof for oppgtset 19371. (Contributed by AV, 18-Oct-2024.) |
| ⊢ (TopSet‘ndx) ≠ (+g‘ndx) | ||
| Theorem | tsetndxnmulrndx 17402 | 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 17403 | The slot for the topology is not the slot for the involution in an extensible structure. Formerly part of proof for cnfldfunALT 21379. (Contributed by AV, 11-Nov-2024.) |
| ⊢ (TopSet‘ndx) ≠ (*𝑟‘ndx) | ||
| Theorem | slotstnscsi 17404 | The slots Scalar, ·𝑠 and ·𝑖 are different from the slot TopSet. Formerly part of sralem 21175 and proofs using it. (Contributed by AV, 29-Oct-2024.) |
| ⊢ ((TopSet‘ndx) ≠ (Scalar‘ndx) ∧ (TopSet‘ndx) ≠ ( ·𝑠 ‘ndx) ∧ (TopSet‘ndx) ≠ (·𝑖‘ndx)) | ||
| Theorem | topgrpstr 17405 | 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 17406 | The base set of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) |
| ⊢ 𝑊 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(TopSet‘ndx), 𝐽〉} ⇒ ⊢ (𝐵 ∈ 𝑋 → 𝐵 = (Base‘𝑊)) | ||
| Theorem | topgrpplusg 17407 | The additive operation of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) |
| ⊢ 𝑊 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(TopSet‘ndx), 𝐽〉} ⇒ ⊢ ( + ∈ 𝑋 → + = (+g‘𝑊)) | ||
| Theorem | topgrptset 17408 | The topology of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) |
| ⊢ 𝑊 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(TopSet‘ndx), 𝐽〉} ⇒ ⊢ (𝐽 ∈ 𝑋 → 𝐽 = (TopSet‘𝑊)) | ||
| Theorem | resstset 17409 | TopSet is unaffected by restriction. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐽 = (TopSet‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐽 = (TopSet‘𝐻)) | ||
| Theorem | plendx 17410 | Index value of the df-ple 17317 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.) (New usage is discouraged.) |
| ⊢ (le‘ndx) = ;10 | ||
| Theorem | pleid 17411 | Utility theorem: self-referencing, index-independent form of df-ple 17317. (Contributed by NM, 9-Nov-2012.) (Revised by AV, 9-Sep-2021.) |
| ⊢ le = Slot (le‘ndx) | ||
| Theorem | plendxnn 17412 | 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 17413 | 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 17414 | 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 17415 | 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 32951. (Contributed by AV, 18-Oct-2024.) |
| ⊢ (le‘ndx) ≠ (+g‘ndx) | ||
| Theorem | plendxnmulrndx 17416 | 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 22073. (Contributed by AV, 1-Nov-2024.) |
| ⊢ (le‘ndx) ≠ (.r‘ndx) | ||
| Theorem | plendxnscandx 17417 | 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 22077. (Contributed by AV, 1-Nov-2024.) |
| ⊢ (le‘ndx) ≠ (Scalar‘ndx) | ||
| Theorem | plendxnvscandx 17418 | 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 22075. (Contributed by AV, 1-Nov-2024.) |
| ⊢ (le‘ndx) ≠ ( ·𝑠 ‘ndx) | ||
| Theorem | slotsdifplendx 17419 | The index of the slot for the distance is not the index of other slots. Formerly part of proof for cnfldfunALT 21379. (Contributed by AV, 11-Nov-2024.) |
| ⊢ ((*𝑟‘ndx) ≠ (le‘ndx) ∧ (TopSet‘ndx) ≠ (le‘ndx)) | ||
| Theorem | otpsstr 17420 | 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 17421 | 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 17422 | 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 17423 | 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 17424 | le is unaffected by restriction. (Contributed by Mario Carneiro, 3-Nov-2015.) |
| ⊢ 𝑊 = (𝐾 ↾s 𝐴) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐴 ∈ 𝑉 → ≤ = (le‘𝑊)) | ||
| Theorem | ocndx 17425 | Index value of the df-ocomp 17318 slot. (Contributed by Mario Carneiro, 25-Oct-2015.) (New usage is discouraged.) |
| ⊢ (oc‘ndx) = ;11 | ||
| Theorem | ocid 17426 | Utility theorem: index-independent form of df-ocomp 17318. (Contributed by Mario Carneiro, 25-Oct-2015.) |
| ⊢ oc = Slot (oc‘ndx) | ||
| Theorem | basendxnocndx 17427 | The slot for the orthocomplementation is not the slot for the base set in an extensible structure. Formerly part of proof for thlbas 21714. (Contributed by AV, 11-Nov-2024.) |
| ⊢ (Base‘ndx) ≠ (oc‘ndx) | ||
| Theorem | plendxnocndx 17428 | The slot for the orthocomplementation is not the slot for the order in an extensible structure. Formerly part of proof for thlle 21716. (Contributed by AV, 11-Nov-2024.) |
| ⊢ (le‘ndx) ≠ (oc‘ndx) | ||
| Theorem | dsndx 17429 | Index value of the df-ds 17319 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
| ⊢ (dist‘ndx) = ;12 | ||
| Theorem | dsid 17430 | Utility theorem: index-independent form of df-ds 17319. (Contributed by Mario Carneiro, 23-Dec-2013.) |
| ⊢ dist = Slot (dist‘ndx) | ||
| Theorem | dsndxnn 17431 | The index of the slot for the distance in an extensible structure is a positive integer. Formerly part of proof for tmslem 24494. (Contributed by AV, 28-Oct-2024.) |
| ⊢ (dist‘ndx) ∈ ℕ | ||
| Theorem | basendxltdsndx 17432 | 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 24494. (Contributed by AV, 28-Oct-2024.) |
| ⊢ (Base‘ndx) < (dist‘ndx) | ||
| Theorem | dsndxnbasendx 17433 | 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 17434 | The slot for the distance function is not the slot for the group operation in an extensible structure. Formerly part of proof for mgpds 20146. (Contributed by AV, 18-Oct-2024.) |
| ⊢ (dist‘ndx) ≠ (+g‘ndx) | ||
| Theorem | dsndxnmulrndx 17435 | 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 17436 | The slots Scalar, ·𝑠 and ·𝑖 are different from the slot dist. Formerly part of sralem 21175 and proofs using it. (Contributed by AV, 29-Oct-2024.) |
| ⊢ ((dist‘ndx) ≠ (Scalar‘ndx) ∧ (dist‘ndx) ≠ ( ·𝑠 ‘ndx) ∧ (dist‘ndx) ≠ (·𝑖‘ndx)) | ||
| Theorem | dsndxntsetndx 17437 | The slot for the distance function is not the slot for the topology in an extensible structure. Formerly part of proof for tngds 24668. (Contributed by AV, 29-Oct-2024.) |
| ⊢ (dist‘ndx) ≠ (TopSet‘ndx) | ||
| Theorem | slotsdifdsndx 17438 | The index of the slot for the distance is not the index of other slots. Formerly part of proof for cnfldfunALT 21379. (Contributed by AV, 11-Nov-2024.) |
| ⊢ ((*𝑟‘ndx) ≠ (dist‘ndx) ∧ (le‘ndx) ≠ (dist‘ndx)) | ||
| Theorem | unifndx 17439 | Index value of the df-unif 17320 slot. (Contributed by Thierry Arnoux, 17-Dec-2017.) (New usage is discouraged.) |
| ⊢ (UnifSet‘ndx) = ;13 | ||
| Theorem | unifid 17440 | Utility theorem: index-independent form of df-unif 17320. (Contributed by Thierry Arnoux, 17-Dec-2017.) |
| ⊢ UnifSet = Slot (UnifSet‘ndx) | ||
| Theorem | unifndxnn 17441 | The index of the slot for the uniform set in an extensible structure is a positive integer. Formerly part of proof for tuslem 24275. (Contributed by AV, 28-Oct-2024.) |
| ⊢ (UnifSet‘ndx) ∈ ℕ | ||
| Theorem | basendxltunifndx 17442 | 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 24275. (Contributed by AV, 28-Oct-2024.) |
| ⊢ (Base‘ndx) < (UnifSet‘ndx) | ||
| Theorem | unifndxnbasendx 17443 | 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 17444 | The slot for the uniform set is not the slot for the topology in an extensible structure. Formerly part of proof for tuslem 24275. (Contributed by AV, 28-Oct-2024.) |
| ⊢ (UnifSet‘ndx) ≠ (TopSet‘ndx) | ||
| Theorem | slotsdifunifndx 17445 | The index of the slot for the uniform set is not the index of other slots. Formerly part of proof for cnfldfunALT 21379. (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 17446 | UnifSet is unaffected by restriction. (Contributed by Thierry Arnoux, 7-Dec-2017.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝑈 = (UnifSet‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝑈 = (UnifSet‘𝐻)) | ||
| Theorem | odrngstr 17447 | 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 17448 | 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 17449 | 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 17450 | 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 17451 | 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 17452 | 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 17453 | 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 17454 | dist is unaffected by restriction. (Contributed by Mario Carneiro, 26-Aug-2015.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐷 = (dist‘𝐻)) | ||
| Theorem | homndx 17455 | Index value of the df-hom 17321 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.) |
| ⊢ (Hom ‘ndx) = ;14 | ||
| Theorem | homid 17456 | Utility theorem: index-independent form of df-hom 17321. (Contributed by Mario Carneiro, 7-Jan-2017.) |
| ⊢ Hom = Slot (Hom ‘ndx) | ||
| Theorem | ccondx 17457 | Index value of the df-cco 17322 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.) |
| ⊢ (comp‘ndx) = ;15 | ||
| Theorem | ccoid 17458 | Utility theorem: index-independent form of df-cco 17322. (Contributed by Mario Carneiro, 7-Jan-2017.) |
| ⊢ comp = Slot (comp‘ndx) | ||
| Theorem | slotsbhcdif 17459 | 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 17460 | Obsolete version of slotsbhcdif 17459 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 17461 | 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 49157. (Contributed by AV, 12-Nov-2024.) |
| ⊢ ((le‘ndx) ≠ (comp‘ndx) ∧ (le‘ndx) ≠ (Hom ‘ndx)) | ||
| Theorem | slotsdifocndx 17462 | The index of the slot for the orthocomplementation is not the index of other slots. Formerly part of proof for prstcocval 49160. (Contributed by AV, 12-Nov-2024.) |
| ⊢ ((oc‘ndx) ≠ (comp‘ndx) ∧ (oc‘ndx) ≠ (Hom ‘ndx)) | ||
| Theorem | resshom 17463 | Hom is unaffected by restriction. (Contributed by Mario Carneiro, 5-Jan-2017.) |
| ⊢ 𝐷 = (𝐶 ↾s 𝐴) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐻 = (Hom ‘𝐷)) | ||
| Theorem | ressco 17464 | comp is unaffected by restriction. (Contributed by Mario Carneiro, 5-Jan-2017.) |
| ⊢ 𝐷 = (𝐶 ↾s 𝐴) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = (comp‘𝐷)) | ||
| Syntax | crest 17465 | Extend class notation with the function returning a subspace topology. |
| class ↾t | ||
| Syntax | ctopn 17466 | Extend class notation with the topology extractor function. |
| class TopOpen | ||
| Definition | df-rest 17467* | 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 17468 | Define the topology extractor function. This differs from df-tset 17316 when a structure has been restricted using df-ress 17275; 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 17469 | The subspace topology operator is a function on pairs. (Contributed by Mario Carneiro, 1-May-2015.) |
| ⊢ ↾t Fn (V × V) | ||
| Theorem | topnfn 17470 | The topology extractor function is a function on the universe. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| ⊢ TopOpen Fn V | ||
| Theorem | restval 17471* | 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 17472* | 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 17473 | 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 17474 | Value of the structure restriction when the topology input is empty. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| ⊢ (∅ ↾t 𝐴) = ∅ | ||
| Theorem | restid2 17475 | The subspace topology over a subset of the base set is the original topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴) → (𝐽 ↾t 𝐴) = 𝐽) | ||
| Theorem | restsspw 17476 | The subspace topology is a collection of subsets of the restriction set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| ⊢ (𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴 | ||
| Theorem | firest 17477 | The finite intersections operator commutes with restriction. (Contributed by Mario Carneiro, 30-Aug-2015.) |
| ⊢ (fi‘(𝐽 ↾t 𝐴)) = ((fi‘𝐽) ↾t 𝐴) | ||
| Theorem | restid 17478 | 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 17479 | Value of the topology extractor function. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopSet‘𝑊) ⇒ ⊢ (𝐽 ↾t 𝐵) = (TopOpen‘𝑊) | ||
| Theorem | topnid 17480 | 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 17481 | 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 17482 | Extend class notation with a function that converts a basis to its corresponding topology. |
| class topGen | ||
| Syntax | cpt 17483 | Extend class notation with a function whose value is a product topology. |
| class ∏t | ||
| Syntax | c0g 17484 | Extend class notation with group identity element. |
| class 0g | ||
| Syntax | cgsu 17485 | Extend class notation to include finitely supported group sums. |
| class Σg | ||
| Definition | df-0g 17486* | Define group identity element. Remark: this definition is required here because the symbol 0g is already used in df-gsum 17487. The related theorems are provided later, see grpidval 18674. (Contributed by NM, 20-Aug-2011.) |
| ⊢ 0g = (𝑔 ∈ V ↦ (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥)))) | ||
| Definition | df-gsum 17487* |
Define a finite group sum (also called "iterated sum") of a
structure.
Given 𝐺 Σg 𝐹 where 𝐹:𝐴⟶(Base‘𝐺), the set of
indices is 𝐴 and the values are given by 𝐹 at each
index. A
group sum over a multiplicative group may be viewed as a product. 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 18697. 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 18699 and gsumnunsn 34556. 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 19925. 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 24135. Remark: this definition is required here because the symbol Σg is already used in df-prds 17492 and df-imas 17553. The related theorems are provided later, see gsumvalx 18689. (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 17488* | 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 22963). The first use of this definition is tgval 22962 but the token is used in df-pt 17489. See tgval3 22970 for an alternate expression for the value. (Contributed by NM, 16-Jul-2006.) |
| ⊢ topGen = (𝑥 ∈ V ↦ {𝑦 ∣ 𝑦 ⊆ ∪ (𝑥 ∩ 𝒫 𝑦)}) | ||
| Definition | df-pt 17489* | 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 17490 | The function constructing structure products. |
| class Xs | ||
| Syntax | cpws 17491 | The function constructing structure powers. |
| class ↑s | ||
| Definition | df-prds 17492* | 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‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))〉}))) | ||
| Theorem | reldmprds 17493 | The structure product is a well-behaved binary operator. (Contributed by Stefan O'Rear, 7-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
| ⊢ Rel dom Xs | ||
| Definition | df-pws 17494* | Define a structure power, which is just a structure product where all the factors are the same. (Contributed by Mario Carneiro, 11-Jan-2015.) |
| ⊢ ↑s = (𝑟 ∈ V, 𝑖 ∈ V ↦ ((Scalar‘𝑟)Xs(𝑖 × {𝑟}))) | ||
| Theorem | prdsbasex 17495* | Lemma for structure products. (Contributed by Mario Carneiro, 3-Jan-2015.) |
| ⊢ 𝐵 = X𝑥 ∈ dom 𝑅(Base‘(𝑅‘𝑥)) ⇒ ⊢ 𝐵 ∈ V | ||
| Theorem | imasvalstr 17496 | An image structure value is a structure. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
| ⊢ 𝑈 = (({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉, 〈(·𝑖‘ndx), , 〉}) ∪ {〈(TopSet‘ndx), 𝑂〉, 〈(le‘ndx), 𝐿〉, 〈(dist‘ndx), 𝐷〉}) ⇒ ⊢ 𝑈 Struct 〈1, ;12〉 | ||
| Theorem | prdsvalstr 17497 | Structure product value is a structure. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
| ⊢ (({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉, 〈(·𝑖‘ndx), , 〉}) ∪ ({〈(TopSet‘ndx), 𝑂〉, 〈(le‘ndx), 𝐿〉, 〈(dist‘ndx), 𝐷〉} ∪ {〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), ∙ 〉})) Struct 〈1, ;15〉 | ||
| Theorem | prdsbaslem 17498 | Lemma for prdsbas 17502 and similar theorems. (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 12-Jul-2024.) |
| ⊢ (𝜑 → 𝑈 = (({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉, 〈(·𝑖‘ndx), , 〉}) ∪ ({〈(TopSet‘ndx), 𝑂〉, 〈(le‘ndx), 𝐿〉, 〈(dist‘ndx), 𝐷〉} ∪ {〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), ∙ 〉}))) & ⊢ 𝐴 = (𝐸‘𝑈) & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) & ⊢ {〈(𝐸‘ndx), 𝑇〉} ⊆ (({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉, 〈(·𝑖‘ndx), , 〉}) ∪ ({〈(TopSet‘ndx), 𝑂〉, 〈(le‘ndx), 𝐿〉, 〈(dist‘ndx), 𝐷〉} ∪ {〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), ∙ 〉})) ⇒ ⊢ (𝜑 → 𝐴 = 𝑇) | ||
| Theorem | prdsvallem 17499* | Lemma for prdsval 17500. (Contributed by Stefan O'Rear, 3-Jan-2015.) Extracted from the former proof of prdsval 17500, dependency on df-hom 17321 removed. (Revised by AV, 13-Oct-2024.) |
| ⊢ (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) ∈ V | ||
| Theorem | prdsval 17500* | Value of the structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
| ⊢ 𝑃 = (𝑆Xs𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ (𝜑 → dom 𝑅 = 𝐼) & ⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥))) & ⊢ (𝜑 → + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))) & ⊢ (𝜑 → × = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))) & ⊢ (𝜑 → · = (𝑓 ∈ 𝐾, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))) & ⊢ (𝜑 → , = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))) & ⊢ (𝜑 → 𝑂 = (∏t‘(TopOpen ∘ 𝑅))) & ⊢ (𝜑 → ≤ = {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}) & ⊢ (𝜑 → 𝐷 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))) & ⊢ (𝜑 → 𝐻 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))) & ⊢ (𝜑 → ∙ = (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ ((2nd ‘𝑎)𝐻𝑐), 𝑒 ∈ (𝐻‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(〈((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)〉(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) ⇒ ⊢ (𝜑 → 𝑃 = (({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉, 〈(·𝑖‘ndx), , 〉}) ∪ ({〈(TopSet‘ndx), 𝑂〉, 〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), 𝐷〉} ∪ {〈(Hom ‘ndx), 𝐻〉, 〈(comp‘ndx), ∙ 〉}))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |