![]() |
Metamath
Proof Explorer Theorem List (p. 165 of 437) | < 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-28364) |
![]() (28365-29889) |
![]() (29890-43671) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | plusgndxnmulrndx 16401 | 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 16402 | 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 16403 | 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 16404 | 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 16405 | 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 16406 | 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 16407 | Index value of the df-starv 16364 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (*𝑟‘ndx) = 4 | ||
Theorem | starvid 16408 | Utility theorem: index-independent form of df-starv 16364. (Contributed by Mario Carneiro, 6-Oct-2013.) |
⊢ *𝑟 = Slot (*𝑟‘ndx) | ||
Theorem | ressmulr 16409 | .r is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝑆)) | ||
Theorem | ressstarv 16410 | *𝑟 is unaffected by restriction. (Contributed by Mario Carneiro, 9-Oct-2015.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ ∗ = (*𝑟‘𝑅) ⇒ ⊢ (𝐴 ∈ 𝑉 → ∗ = (*𝑟‘𝑆)) | ||
Theorem | srngstr 16411 | 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 16412 | 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 16413 | 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 16414 | 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 16415 | The involution function of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ 𝑅 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(*𝑟‘ndx), ∗ 〉}) ⇒ ⊢ ( ∗ ∈ 𝑋 → ∗ = (*𝑟‘𝑅)) | ||
Theorem | scandx 16416 | Index value of the df-sca 16365 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (Scalar‘ndx) = 5 | ||
Theorem | scaid 16417 | Utility theorem: index-independent form of scalar df-sca 16365. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ Scalar = Slot (Scalar‘ndx) | ||
Theorem | vscandx 16418 | Index value of the df-vsca 16366 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ ( ·𝑠 ‘ndx) = 6 | ||
Theorem | vscaid 16419 | Utility theorem: index-independent form of scalar product df-vsca 16366. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ ·𝑠 = Slot ( ·𝑠 ‘ndx) | ||
Theorem | lmodstr 16420 | 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 16421 | 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 16422 | 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 16423 | 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 16424 | 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 16425 | Index value of the df-ip 16367 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (·𝑖‘ndx) = 8 | ||
Theorem | ipid 16426 | Utility theorem: index-independent form of df-ip 16367. (Contributed by Mario Carneiro, 6-Oct-2013.) |
⊢ ·𝑖 = Slot (·𝑖‘ndx) | ||
Theorem | ipsstr 16427 | Lemma to shorten proofs of ipsbase 16428 through ipsvsca 16432. (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 16428 | 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 16429 | 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 16430 | 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 16431 | 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 16432 | 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 16433 | 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 16434 | Scalar is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐹 = (Scalar‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹 = (Scalar‘𝐻)) | ||
Theorem | ressvsca 16435 | ·𝑠 is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ · = ( ·𝑠 ‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘𝐻)) | ||
Theorem | ressip 16436 | The inner product is unaffected by restriction. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ , = (·𝑖‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → , = (·𝑖‘𝐻)) | ||
Theorem | phlstr 16437 | A constructed pre-Hilbert space is a structure. Starting from lmodstr 16420 (which has 4 members), we chain strleun 16375 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 16438 | 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 16439 | 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 16440 | 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 16441 | 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 16442 | 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 16443 | Index value of the df-tset 16368 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (TopSet‘ndx) = 9 | ||
Theorem | tsetid 16444 | Utility theorem: index-independent form of df-tset 16368. (Contributed by NM, 20-Oct-2012.) |
⊢ TopSet = Slot (TopSet‘ndx) | ||
Theorem | topgrpstr 16445 | 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 16446 | The base set of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝑊 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(TopSet‘ndx), 𝐽〉} ⇒ ⊢ (𝐵 ∈ 𝑋 → 𝐵 = (Base‘𝑊)) | ||
Theorem | topgrpplusg 16447 | The additive operation of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝑊 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(TopSet‘ndx), 𝐽〉} ⇒ ⊢ ( + ∈ 𝑋 → + = (+g‘𝑊)) | ||
Theorem | topgrptset 16448 | The topology of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝑊 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(TopSet‘ndx), 𝐽〉} ⇒ ⊢ (𝐽 ∈ 𝑋 → 𝐽 = (TopSet‘𝑊)) | ||
Theorem | resstset 16449 | TopSet is unaffected by restriction. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐽 = (TopSet‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐽 = (TopSet‘𝐻)) | ||
Theorem | plendx 16450 | Index value of the df-ple 16369 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.) |
⊢ (le‘ndx) = ;10 | ||
Theorem | pleid 16451 | Utility theorem: self-referencing, index-independent form of df-ple 16369. (Contributed by NM, 9-Nov-2012.) (Revised by AV, 9-Sep-2021.) |
⊢ le = Slot (le‘ndx) | ||
Theorem | otpsstr 16452 | 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 16453 | 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 16454 | 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 16455 | 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 16456 | le is unaffected by restriction. (Contributed by Mario Carneiro, 3-Nov-2015.) |
⊢ 𝑊 = (𝐾 ↾s 𝐴) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐴 ∈ 𝑉 → ≤ = (le‘𝑊)) | ||
Theorem | ocndx 16457 | Index value of the df-ocomp 16370 slot. (Contributed by Mario Carneiro, 25-Oct-2015.) |
⊢ (oc‘ndx) = ;11 | ||
Theorem | ocid 16458 | Utility theorem: index-independent form of df-ocomp 16370. (Contributed by Mario Carneiro, 25-Oct-2015.) |
⊢ oc = Slot (oc‘ndx) | ||
Theorem | dsndx 16459 | Index value of the df-ds 16371 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (dist‘ndx) = ;12 | ||
Theorem | dsid 16460 | Utility theorem: index-independent form of df-ds 16371. (Contributed by Mario Carneiro, 23-Dec-2013.) |
⊢ dist = Slot (dist‘ndx) | ||
Theorem | unifndx 16461 | Index value of the df-unif 16372 slot. (Contributed by Thierry Arnoux, 17-Dec-2017.) |
⊢ (UnifSet‘ndx) = ;13 | ||
Theorem | unifid 16462 | Utility theorem: index-independent form of df-unif 16372. (Contributed by Thierry Arnoux, 17-Dec-2017.) |
⊢ UnifSet = Slot (UnifSet‘ndx) | ||
Theorem | odrngstr 16463 | 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 16464 | 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 16465 | 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 16466 | 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 16467 | 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 16468 | 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 16469 | 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 16470 | dist is unaffected by restriction. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐷 = (dist‘𝐻)) | ||
Theorem | homndx 16471 | Index value of the df-hom 16373 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ (Hom ‘ndx) = ;14 | ||
Theorem | homid 16472 | Utility theorem: index-independent form of df-hom 16373. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ Hom = Slot (Hom ‘ndx) | ||
Theorem | ccondx 16473 | Index value of the df-cco 16374 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ (comp‘ndx) = ;15 | ||
Theorem | ccoid 16474 | Utility theorem: index-independent form of df-cco 16374. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ comp = Slot (comp‘ndx) | ||
Theorem | resshom 16475 | Hom is unaffected by restriction. (Contributed by Mario Carneiro, 5-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾s 𝐴) & ⊢ 𝐻 = (Hom ‘𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐻 = (Hom ‘𝐷)) | ||
Theorem | ressco 16476 | comp is unaffected by restriction. (Contributed by Mario Carneiro, 5-Jan-2017.) |
⊢ 𝐷 = (𝐶 ↾s 𝐴) & ⊢ · = (comp‘𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = (comp‘𝐷)) | ||
Theorem | slotsbhcdif 16477 | 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 16478 | Extend class notation with the function returning a subspace topology. |
class ↾t | ||
Syntax | ctopn 16479 | Extend class notation with the topology extractor function. |
class TopOpen | ||
Definition | df-rest 16480* | 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 16481 | Define the topology extractor function. This differs from df-tset 16368 when a structure has been restricted using df-ress 16274; 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 16482 | The subspace topology operator is a function on pairs. (Contributed by Mario Carneiro, 1-May-2015.) |
⊢ ↾t Fn (V × V) | ||
Theorem | topnfn 16483 | The topology extractor function is a function on the universe. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ TopOpen Fn V | ||
Theorem | restval 16484* | 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 16485* | 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 16486 | 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 16487 | Value of the structure restriction when the topology input is empty. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ (∅ ↾t 𝐴) = ∅ | ||
Theorem | restid2 16488 | The subspace topology over a subset of the base set is the original topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴) → (𝐽 ↾t 𝐴) = 𝐽) | ||
Theorem | restsspw 16489 | The subspace topology is a collection of subsets of the restriction set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴 | ||
Theorem | firest 16490 | The finite intersections operator commutes with restriction. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ (fi‘(𝐽 ↾t 𝐴)) = ((fi‘𝐽) ↾t 𝐴) | ||
Theorem | restid 16491 | 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 16492 | Value of the topology extractor function. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐽 = (TopSet‘𝑊) ⇒ ⊢ (𝐽 ↾t 𝐵) = (TopOpen‘𝑊) | ||
Theorem | topnid 16493 | 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 16494 | 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 16495 | Extend class notation with a function that converts a basis to its corresponding topology. |
class topGen | ||
Syntax | cpt 16496 | Extend class notation with a function whose value is a product topology. |
class ∏t | ||
Syntax | c0g 16497 | Extend class notation with group identity element. |
class 0g | ||
Syntax | cgsu 16498 | Extend class notation to include finitely supported group sums. |
class Σg | ||
Definition | df-0g 16499* | Define group identity element. Remark: this definition is required here because the symbol 0g is already used in df-gsum 16500. The related theorems are provided later, see grpidval 17657. (Contributed by NM, 20-Aug-2011.) |
⊢ 0g = (𝑔 ∈ V ↦ (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥)))) | ||
Definition | df-gsum 16500* |
Define the group 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. 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. 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. 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 22349. Remark: this definition is required here because the symbol Σg is already used in df-prds 16505 and df-imas 16565. The related theorems are provided later, see gsumvalx 17667. (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‘𝑤), (𝑓 ∘ 𝑔))‘(♯‘𝑦))))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |