Home | Metamath
Proof Explorer Theorem List (p. 167 of 449) | < 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: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | grpplusg 16601 | The operation of a constructed group. (Contributed by Mario Carneiro, 2-Aug-2013.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉} ⇒ ⊢ ( + ∈ 𝑉 → + = (+g‘𝐺)) | ||
Theorem | ressplusg 16602 | +g is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻)) | ||
Theorem | grpbasex 16603 | The base of an explicitly given group. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use; use grpbase 16600 instead. (New usage is discouraged.) (Contributed by NM, 17-Oct-2012.) |
⊢ 𝐵 ∈ V & ⊢ + ∈ V & ⊢ 𝐺 = {〈1, 𝐵〉, 〈2, + 〉} ⇒ ⊢ 𝐵 = (Base‘𝐺) | ||
Theorem | grpplusgx 16604 | The operation of an explicitly given group. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use; use grpplusg 16601 instead. (New usage is discouraged.) (Contributed by NM, 17-Oct-2012.) |
⊢ 𝐵 ∈ V & ⊢ + ∈ V & ⊢ 𝐺 = {〈1, 𝐵〉, 〈2, + 〉} ⇒ ⊢ + = (+g‘𝐺) | ||
Theorem | mulrndx 16605 | Index value of the df-mulr 16569 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (.r‘ndx) = 3 | ||
Theorem | mulrid 16606 | Utility theorem: index-independent form of df-mulr 16569. (Contributed by Mario Carneiro, 8-Jun-2013.) |
⊢ .r = Slot (.r‘ndx) | ||
Theorem | plusgndxnmulrndx 16607 | The slot for the group (addition) operation is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 16-Feb-2020.) |
⊢ (+g‘ndx) ≠ (.r‘ndx) | ||
Theorem | basendxnmulrndx 16608 | The slot for the base set is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 16-Feb-2020.) |
⊢ (Base‘ndx) ≠ (.r‘ndx) | ||
Theorem | rngstr 16609 | A constructed ring is a structure. (Contributed by Mario Carneiro, 28-Sep-2013.) (Revised by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝑅 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ⇒ ⊢ 𝑅 Struct 〈1, 3〉 | ||
Theorem | rngbase 16610 | The base set of a constructed ring. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝑅 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝑅)) | ||
Theorem | rngplusg 16611 | The additive operation of a constructed ring. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝑅 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ⇒ ⊢ ( + ∈ 𝑉 → + = (+g‘𝑅)) | ||
Theorem | rngmulr 16612 | The multiplicative operation of a constructed ring. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝑅 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ⇒ ⊢ ( · ∈ 𝑉 → · = (.r‘𝑅)) | ||
Theorem | starvndx 16613 | Index value of the df-starv 16570 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (*𝑟‘ndx) = 4 | ||
Theorem | starvid 16614 | Utility theorem: index-independent form of df-starv 16570. (Contributed by Mario Carneiro, 6-Oct-2013.) |
⊢ *𝑟 = Slot (*𝑟‘ndx) | ||
Theorem | ressmulr 16615 | .r is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝑆)) | ||
Theorem | ressstarv 16616 | *𝑟 is unaffected by restriction. (Contributed by Mario Carneiro, 9-Oct-2015.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ ∗ = (*𝑟‘𝑅) ⇒ ⊢ (𝐴 ∈ 𝑉 → ∗ = (*𝑟‘𝑆)) | ||
Theorem | srngstr 16617 | A constructed star ring is a structure. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝑅 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(*𝑟‘ndx), ∗ 〉}) ⇒ ⊢ 𝑅 Struct 〈1, 4〉 | ||
Theorem | srngbase 16618 | The base set of a constructed star ring. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ 𝑅 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(*𝑟‘ndx), ∗ 〉}) ⇒ ⊢ (𝐵 ∈ 𝑋 → 𝐵 = (Base‘𝑅)) | ||
Theorem | srngplusg 16619 | The addition operation of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ 𝑅 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(*𝑟‘ndx), ∗ 〉}) ⇒ ⊢ ( + ∈ 𝑋 → + = (+g‘𝑅)) | ||
Theorem | srngmulr 16620 | The multiplication operation of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ 𝑅 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(*𝑟‘ndx), ∗ 〉}) ⇒ ⊢ ( · ∈ 𝑋 → · = (.r‘𝑅)) | ||
Theorem | srnginvl 16621 | The involution function of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ 𝑅 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(*𝑟‘ndx), ∗ 〉}) ⇒ ⊢ ( ∗ ∈ 𝑋 → ∗ = (*𝑟‘𝑅)) | ||
Theorem | scandx 16622 | Index value of the df-sca 16571 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (Scalar‘ndx) = 5 | ||
Theorem | scaid 16623 | Utility theorem: index-independent form of scalar df-sca 16571. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ Scalar = Slot (Scalar‘ndx) | ||
Theorem | vscandx 16624 | Index value of the df-vsca 16572 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ ( ·𝑠 ‘ndx) = 6 | ||
Theorem | vscaid 16625 | Utility theorem: index-independent form of scalar product df-vsca 16572. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ ·𝑠 = Slot ( ·𝑠 ‘ndx) | ||
Theorem | lmodstr 16626 | A constructed left module or left vector space is a structure. (Contributed by Mario Carneiro, 1-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝑊 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(Scalar‘ndx), 𝐹〉} ∪ {〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ 𝑊 Struct 〈1, 6〉 | ||
Theorem | lmodbase 16627 | The base set of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝑊 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(Scalar‘ndx), 𝐹〉} ∪ {〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ (𝐵 ∈ 𝑋 → 𝐵 = (Base‘𝑊)) | ||
Theorem | lmodplusg 16628 | The additive operation of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝑊 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(Scalar‘ndx), 𝐹〉} ∪ {〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ ( + ∈ 𝑋 → + = (+g‘𝑊)) | ||
Theorem | lmodsca 16629 | The set of scalars of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝑊 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(Scalar‘ndx), 𝐹〉} ∪ {〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ (𝐹 ∈ 𝑋 → 𝐹 = (Scalar‘𝑊)) | ||
Theorem | lmodvsca 16630 | The scalar product operation of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝑊 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(Scalar‘ndx), 𝐹〉} ∪ {〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ ( · ∈ 𝑋 → · = ( ·𝑠 ‘𝑊)) | ||
Theorem | ipndx 16631 | Index value of the df-ip 16573 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (·𝑖‘ndx) = 8 | ||
Theorem | ipid 16632 | Utility theorem: index-independent form of df-ip 16573. (Contributed by Mario Carneiro, 6-Oct-2013.) |
⊢ ·𝑖 = Slot (·𝑖‘ndx) | ||
Theorem | ipsstr 16633 | Lemma to shorten proofs of ipsbase 16634 through ipsvsca 16638. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉, 〈(·𝑖‘ndx), 𝐼〉}) ⇒ ⊢ 𝐴 Struct 〈1, 8〉 | ||
Theorem | ipsbase 16634 | The base set of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉, 〈(·𝑖‘ndx), 𝐼〉}) ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐴)) | ||
Theorem | ipsaddg 16635 | The additive operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉, 〈(·𝑖‘ndx), 𝐼〉}) ⇒ ⊢ ( + ∈ 𝑉 → + = (+g‘𝐴)) | ||
Theorem | ipsmulr 16636 | The multiplicative operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉, 〈(·𝑖‘ndx), 𝐼〉}) ⇒ ⊢ ( × ∈ 𝑉 → × = (.r‘𝐴)) | ||
Theorem | ipssca 16637 | The set of scalars of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉, 〈(·𝑖‘ndx), 𝐼〉}) ⇒ ⊢ (𝑆 ∈ 𝑉 → 𝑆 = (Scalar‘𝐴)) | ||
Theorem | ipsvsca 16638 | The scalar product operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉, 〈(·𝑖‘ndx), 𝐼〉}) ⇒ ⊢ ( · ∈ 𝑉 → · = ( ·𝑠 ‘𝐴)) | ||
Theorem | ipsip 16639 | The multiplicative operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉, 〈(·𝑖‘ndx), 𝐼〉}) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐼 = (·𝑖‘𝐴)) | ||
Theorem | resssca 16640 | Scalar is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐹 = (Scalar‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹 = (Scalar‘𝐻)) | ||
Theorem | ressvsca 16641 | ·𝑠 is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ · = ( ·𝑠 ‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘𝐻)) | ||
Theorem | ressip 16642 | The inner product is unaffected by restriction. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ , = (·𝑖‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → , = (·𝑖‘𝐻)) | ||
Theorem | phlstr 16643 | A constructed pre-Hilbert space is a structure. Starting from lmodstr 16626 (which has 4 members), we chain strleun 16581 once more, adding an ordered pair to the function, to get all 5 members. (Contributed by Mario Carneiro, 1-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐻 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(Scalar‘ndx), 𝑇〉} ∪ {〈( ·𝑠 ‘ndx), · 〉, 〈(·𝑖‘ndx), , 〉}) ⇒ ⊢ 𝐻 Struct 〈1, 8〉 | ||
Theorem | phlbase 16644 | The base set 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), , 〉}) ⇒ ⊢ (𝐵 ∈ 𝑋 → 𝐵 = (Base‘𝐻)) | ||
Theorem | phlplusg 16645 | The additive 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), , 〉}) ⇒ ⊢ ( + ∈ 𝑋 → + = (+g‘𝐻)) | ||
Theorem | phlsca 16646 | 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 16647 | 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 16648 | 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 16649 | Index value of the df-tset 16574 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (TopSet‘ndx) = 9 | ||
Theorem | tsetid 16650 | Utility theorem: index-independent form of df-tset 16574. (Contributed by NM, 20-Oct-2012.) |
⊢ TopSet = Slot (TopSet‘ndx) | ||
Theorem | topgrpstr 16651 | 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 16652 | The base set of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝑊 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(TopSet‘ndx), 𝐽〉} ⇒ ⊢ (𝐵 ∈ 𝑋 → 𝐵 = (Base‘𝑊)) | ||
Theorem | topgrpplusg 16653 | The additive operation of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝑊 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(TopSet‘ndx), 𝐽〉} ⇒ ⊢ ( + ∈ 𝑋 → + = (+g‘𝑊)) | ||
Theorem | topgrptset 16654 | The topology of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝑊 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(TopSet‘ndx), 𝐽〉} ⇒ ⊢ (𝐽 ∈ 𝑋 → 𝐽 = (TopSet‘𝑊)) | ||
Theorem | resstset 16655 | TopSet is unaffected by restriction. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐽 = (TopSet‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐽 = (TopSet‘𝐻)) | ||
Theorem | plendx 16656 | Index value of the df-ple 16575 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.) |
⊢ (le‘ndx) = ;10 | ||
Theorem | pleid 16657 | Utility theorem: self-referencing, index-independent form of df-ple 16575. (Contributed by NM, 9-Nov-2012.) (Revised by AV, 9-Sep-2021.) |
⊢ le = Slot (le‘ndx) | ||
Theorem | otpsstr 16658 | 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 16659 | 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 16660 | 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 16661 | 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 16662 | le is unaffected by restriction. (Contributed by Mario Carneiro, 3-Nov-2015.) |
⊢ 𝑊 = (𝐾 ↾s 𝐴) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐴 ∈ 𝑉 → ≤ = (le‘𝑊)) | ||
Theorem | ocndx 16663 | Index value of the df-ocomp 16576 slot. (Contributed by Mario Carneiro, 25-Oct-2015.) |
⊢ (oc‘ndx) = ;11 | ||
Theorem | ocid 16664 | Utility theorem: index-independent form of df-ocomp 16576. (Contributed by Mario Carneiro, 25-Oct-2015.) |
⊢ oc = Slot (oc‘ndx) | ||
Theorem | dsndx 16665 | Index value of the df-ds 16577 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (dist‘ndx) = ;12 | ||
Theorem | dsid 16666 | Utility theorem: index-independent form of df-ds 16577. (Contributed by Mario Carneiro, 23-Dec-2013.) |
⊢ dist = Slot (dist‘ndx) | ||
Theorem | unifndx 16667 | Index value of the df-unif 16578 slot. (Contributed by Thierry Arnoux, 17-Dec-2017.) |
⊢ (UnifSet‘ndx) = ;13 | ||
Theorem | unifid 16668 | Utility theorem: index-independent form of df-unif 16578. (Contributed by Thierry Arnoux, 17-Dec-2017.) |
⊢ UnifSet = Slot (UnifSet‘ndx) | ||
Theorem | odrngstr 16669 | 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 16670 | 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 16671 | 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 16672 | 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 16673 | 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 16674 | 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 16675 | 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 16676 | dist is unaffected by restriction. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐷 = (dist‘𝐻)) | ||
Theorem | homndx 16677 | Index value of the df-hom 16579 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ (Hom ‘ndx) = ;14 | ||
Theorem | homid 16678 | Utility theorem: index-independent form of df-hom 16579. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ Hom = Slot (Hom ‘ndx) | ||
Theorem | ccondx 16679 | Index value of the df-cco 16580 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ (comp‘ndx) = ;15 | ||
Theorem | ccoid 16680 | Utility theorem: index-independent form of df-cco 16580. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ comp = Slot (comp‘ndx) | ||
Theorem | resshom 16681 | Hom is unaffected by restriction. (Contributed by Mario Carneiro, 5-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾s 𝐴) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐻 = (Hom ‘𝐷)) | ||
Theorem | ressco 16682 | comp is unaffected by restriction. (Contributed by Mario Carneiro, 5-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾s 𝐴) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = (comp‘𝐷)) | ||
Theorem | slotsbhcdif 16683 | The slots Base, Hom and comp are different. (Contributed by AV, 5-Mar-2020.) |
⊢ ((Base‘ndx) ≠ (Hom ‘ndx) ∧ (Base‘ndx) ≠ (comp‘ndx) ∧ (Hom ‘ndx) ≠ (comp‘ndx)) | ||
Syntax | crest 16684 | Extend class notation with the function returning a subspace topology. |
class ↾t | ||
Syntax | ctopn 16685 | Extend class notation with the topology extractor function. |
class TopOpen | ||
Definition | df-rest 16686* | 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 16687 | Define the topology extractor function. This differs from df-tset 16574 when a structure has been restricted using df-ress 16481; 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 16688 | The subspace topology operator is a function on pairs. (Contributed by Mario Carneiro, 1-May-2015.) |
⊢ ↾t Fn (V × V) | ||
Theorem | topnfn 16689 | The topology extractor function is a function on the universe. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ TopOpen Fn V | ||
Theorem | restval 16690* | 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 16691* | 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 16692 | 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 16693 | Value of the structure restriction when the topology input is empty. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ (∅ ↾t 𝐴) = ∅ | ||
Theorem | restid2 16694 | The subspace topology over a subset of the base set is the original topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴) → (𝐽 ↾t 𝐴) = 𝐽) | ||
Theorem | restsspw 16695 | The subspace topology is a collection of subsets of the restriction set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴 | ||
Theorem | firest 16696 | The finite intersections operator commutes with restriction. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ (fi‘(𝐽 ↾t 𝐴)) = ((fi‘𝐽) ↾t 𝐴) | ||
Theorem | restid 16697 | 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 16698 | Value of the topology extractor function. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopSet‘𝑊) ⇒ ⊢ (𝐽 ↾t 𝐵) = (TopOpen‘𝑊) | ||
Theorem | topnid 16699 | 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 16700 | The topology extractor function depends only on the base and topology components. (Contributed by NM, 18-Jul-2006.) |
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) & ⊢ (𝜑 → (TopSet‘𝐾) = (TopSet‘𝐿)) ⇒ ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |