Home | Metamath
Proof Explorer Theorem List (p. 161 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rngbase 16001 | 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 16002 | 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 16003 | 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 16004 | Index value of the df-starv 15956 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (*𝑟‘ndx) = 4 | ||
Theorem | starvid 16005 | Utility theorem: index-independent form of df-starv 15956. (Contributed by Mario Carneiro, 6-Oct-2013.) |
⊢ *𝑟 = Slot (*𝑟‘ndx) | ||
Theorem | ressmulr 16006 | .r is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝑆)) | ||
Theorem | ressstarv 16007 | *𝑟 is unaffected by restriction. (Contributed by Mario Carneiro, 9-Oct-2015.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ ∗ = (*𝑟‘𝑅) ⇒ ⊢ (𝐴 ∈ 𝑉 → ∗ = (*𝑟‘𝑆)) | ||
Theorem | srngfn 16008 | A constructed star ring is a function with domain contained in 1 thru 4. (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 16009 | 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 16010 | 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 16011 | 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 16012 | The involution function of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ 𝑅 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(*𝑟‘ndx), ∗ 〉}) ⇒ ⊢ ( ∗ ∈ 𝑋 → ∗ = (*𝑟‘𝑅)) | ||
Theorem | scandx 16013 | Index value of the df-sca 15957 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (Scalar‘ndx) = 5 | ||
Theorem | scaid 16014 | Utility theorem: index-independent form of scalar df-sca 15957. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ Scalar = Slot (Scalar‘ndx) | ||
Theorem | vscandx 16015 | Index value of the df-vsca 15958 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ ( ·𝑠 ‘ndx) = 6 | ||
Theorem | vscaid 16016 | Utility theorem: index-independent form of scalar product df-vsca 15958. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ ·𝑠 = Slot ( ·𝑠 ‘ndx) | ||
Theorem | lmodstr 16017 | A constructed left module or left vector space is a function. (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 16018 | 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 16019 | 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 16020 | 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 16021 | 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 16022 | Index value of the df-ip 15959 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (·𝑖‘ndx) = 8 | ||
Theorem | ipid 16023 | Utility theorem: index-independent form of df-ip 15959. (Contributed by Mario Carneiro, 6-Oct-2013.) |
⊢ ·𝑖 = Slot (·𝑖‘ndx) | ||
Theorem | ipsstr 16024 | Lemma to shorten proofs of ipsbase 16025 through ipsvsca 16029. (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 16025 | 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 16026 | 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 16027 | 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 16028 | 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 16029 | 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 16030 | 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 16031 | Scalar is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐹 = (Scalar‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹 = (Scalar‘𝐻)) | ||
Theorem | ressvsca 16032 | ·𝑠 is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ · = ( ·𝑠 ‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘𝐻)) | ||
Theorem | ressip 16033 | The inner product is unaffected by restriction. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ , = (·𝑖‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → , = (·𝑖‘𝐻)) | ||
Theorem | phlstr 16034 | A constructed pre-Hilbert space is a structure. Starting from lmodstr 16017 (which has 4 members), we chain strleun 15972 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 16035 | 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 16036 | 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 16037 | 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 16038 | 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 16039 | 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 16040 | Index value of the df-tset 15960 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (TopSet‘ndx) = 9 | ||
Theorem | tsetid 16041 | Utility theorem: index-independent form of df-tset 15960. (Contributed by NM, 20-Oct-2012.) |
⊢ TopSet = Slot (TopSet‘ndx) | ||
Theorem | topgrpstr 16042 | 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 16043 | The base set of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝑊 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(TopSet‘ndx), 𝐽〉} ⇒ ⊢ (𝐵 ∈ 𝑋 → 𝐵 = (Base‘𝑊)) | ||
Theorem | topgrpplusg 16044 | The additive operation of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝑊 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(TopSet‘ndx), 𝐽〉} ⇒ ⊢ ( + ∈ 𝑋 → + = (+g‘𝑊)) | ||
Theorem | topgrptset 16045 | The topology of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝑊 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(TopSet‘ndx), 𝐽〉} ⇒ ⊢ (𝐽 ∈ 𝑋 → 𝐽 = (TopSet‘𝑊)) | ||
Theorem | resstset 16046 | TopSet is unaffected by restriction. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐽 = (TopSet‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐽 = (TopSet‘𝐻)) | ||
Theorem | plendx 16047 | Index value of the df-ple 15961 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.) |
⊢ (le‘ndx) = ;10 | ||
Theorem | plendxOLD 16048 | Obsolete version of df-ple 15961 as of 9-Sep-2021. (Contributed by Mario Carneiro, 14-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (le‘ndx) = 10 | ||
Theorem | pleid 16049 | Utility theorem: self-referencing, index-independent form of df-ple 15961. (Contributed by NM, 9-Nov-2012.) (Revised by AV, 9-Sep-2021.) |
⊢ le = Slot (le‘ndx) | ||
Theorem | pleidOLD 16050 | Obsolete version of otpsstr 16051 as of 9-Sep-2021. (Contributed by Mario Carneiro, 9-Nov-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ le = Slot (le‘ndx) | ||
Theorem | otpsstr 16051 | 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 16052 | 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 16053 | 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 16054 | 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 | otpsstrOLD 16055 | Obsolete version of otpsstr 16051 as of 9-Sep-2021. (Contributed by Mario Carneiro, 12-Nov-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐾 = {〈(Base‘ndx), 𝐵〉, 〈(TopSet‘ndx), 𝐽〉, 〈(le‘ndx), ≤ 〉} ⇒ ⊢ 𝐾 Struct 〈1, 10〉 | ||
Theorem | otpsbasOLD 16056 | Obsolete version of otpsbas 16052 as of 9-Sep-2021. (Contributed by Mario Carneiro, 12-Nov-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐾 = {〈(Base‘ndx), 𝐵〉, 〈(TopSet‘ndx), 𝐽〉, 〈(le‘ndx), ≤ 〉} ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐾)) | ||
Theorem | otpstsetOLD 16057 | Obsolete version of otpstset 16053 as of 9-Sep-2021. (Contributed by Mario Carneiro, 12-Nov-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐾 = {〈(Base‘ndx), 𝐵〉, 〈(TopSet‘ndx), 𝐽〉, 〈(le‘ndx), ≤ 〉} ⇒ ⊢ (𝐽 ∈ 𝑉 → 𝐽 = (TopSet‘𝐾)) | ||
Theorem | otpsleOLD 16058 | Obsolete version of otpsle 16054 as of 9-Sep-2021. (Contributed by Mario Carneiro, 12-Nov-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐾 = {〈(Base‘ndx), 𝐵〉, 〈(TopSet‘ndx), 𝐽〉, 〈(le‘ndx), ≤ 〉} ⇒ ⊢ ( ≤ ∈ 𝑉 → ≤ = (le‘𝐾)) | ||
Theorem | ressle 16059 | le is unaffected by restriction. (Contributed by Mario Carneiro, 3-Nov-2015.) |
⊢ 𝑊 = (𝐾 ↾s 𝐴) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐴 ∈ 𝑉 → ≤ = (le‘𝑊)) | ||
Theorem | ocndx 16060 | Index value of the df-ocomp 15963 slot. (Contributed by Mario Carneiro, 25-Oct-2015.) |
⊢ (oc‘ndx) = ;11 | ||
Theorem | ocid 16061 | Utility theorem: index-independent form of df-ocomp 15963. (Contributed by Mario Carneiro, 25-Oct-2015.) |
⊢ oc = Slot (oc‘ndx) | ||
Theorem | dsndx 16062 | Index value of the df-ds 15964 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (dist‘ndx) = ;12 | ||
Theorem | dsid 16063 | Utility theorem: index-independent form of df-ds 15964. (Contributed by Mario Carneiro, 23-Dec-2013.) |
⊢ dist = Slot (dist‘ndx) | ||
Theorem | unifndx 16064 | Index value of the df-unif 15965 slot. (Contributed by Thierry Arnoux, 17-Dec-2017.) |
⊢ (UnifSet‘ndx) = ;13 | ||
Theorem | unifid 16065 | Utility theorem: index-independent form of df-unif 15965. (Contributed by Thierry Arnoux, 17-Dec-2017.) |
⊢ UnifSet = Slot (UnifSet‘ndx) | ||
Theorem | odrngstr 16066 | 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 16067 | 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 16068 | 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 16069 | 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 16070 | 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 16071 | 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 16072 | 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 16073 | dist is unaffected by restriction. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐷 = (dist‘𝐻)) | ||
Theorem | homndx 16074 | Index value of the df-hom 15966 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ (Hom ‘ndx) = ;14 | ||
Theorem | homid 16075 | Utility theorem: index-independent form of df-hom 15966. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ Hom = Slot (Hom ‘ndx) | ||
Theorem | ccondx 16076 | Index value of the df-cco 15967 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ (comp‘ndx) = ;15 | ||
Theorem | ccoid 16077 | Utility theorem: index-independent form of df-cco 15967. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ comp = Slot (comp‘ndx) | ||
Theorem | resshom 16078 | Hom is unaffected by restriction. (Contributed by Mario Carneiro, 5-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾s 𝐴) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐻 = (Hom ‘𝐷)) | ||
Theorem | ressco 16079 | comp is unaffected by restriction. (Contributed by Mario Carneiro, 5-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾s 𝐴) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = (comp‘𝐷)) | ||
Theorem | slotsbhcdif 16080 | 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 16081 | Extend class notation with the function returning a subspace topology. |
class ↾t | ||
Syntax | ctopn 16082 | Extend class notation with the topology extractor function. |
class TopOpen | ||
Definition | df-rest 16083* | 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 16084 | Define the topology extractor function. This differs from df-tset 15960 when a structure has been restricted using df-ress 15865; 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 16085 | The subspace topology operator is a function on pairs. (Contributed by Mario Carneiro, 1-May-2015.) |
⊢ ↾t Fn (V × V) | ||
Theorem | topnfn 16086 | The topology extractor function is a function on the universe. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ TopOpen Fn V | ||
Theorem | restval 16087* | 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 16088* | 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 16089 | 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 16090 | Value of the structure restriction when the topology input is empty. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ (∅ ↾t 𝐴) = ∅ | ||
Theorem | restid2 16091 | The subspace topology over a subset of the base set is the original topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴) → (𝐽 ↾t 𝐴) = 𝐽) | ||
Theorem | restsspw 16092 | The subspace topology is a collection of subsets of the restriction set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴 | ||
Theorem | firest 16093 | The finite intersections operator commutes with restriction. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ (fi‘(𝐽 ↾t 𝐴)) = ((fi‘𝐽) ↾t 𝐴) | ||
Theorem | restid 16094 | 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 16095 | Value of the topology extractor function. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopSet‘𝑊) ⇒ ⊢ (𝐽 ↾t 𝐵) = (TopOpen‘𝑊) | ||
Theorem | topnid 16096 | 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 16097 | 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 16098 | Extend class notation with a function that converts a basis to its corresponding topology. |
class topGen | ||
Syntax | cpt 16099 | Extend class notation with a function whose value is a product topology. |
class ∏t | ||
Syntax | c0g 16100 | Extend class notation with group identity element. |
class 0g |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |