HomeTheorem List (p. 170 of 464)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 170 of 464) | < 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-29181) |
Hilbert Space Explorer
(29182-30704) |
Users' Mathboxes
(30705-46395) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Definition | df-plusg 16901 | Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form plusgid 16915 instead. (New usage is discouraged.) |
| ⊢ +g = Slot 2 | ||
| Definition | df-mulr 16902 | Define ring multiplication. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form mulrid 16930 instead. (New usage is discouraged.) |
| ⊢ .r = Slot 3 | ||
| Definition | df-starv 16903 | Define the involution function of a *-ring. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form starvid 16939 instead. (New usage is discouraged.) |
| ⊢ *𝑟 = Slot 4 | ||
| Definition | df-sca 16904 | Define scalar field component of a vector space 𝑣. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form scaid 16951 instead. (New usage is discouraged.) |
| ⊢ Scalar = Slot 5 | ||
| Definition | df-vsca 16905 | Define scalar product. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form vscaid 16956 instead. (New usage is discouraged.) |
| ⊢ ·𝑠 = Slot 6 | ||
| Definition | df-ip 16906 | Define Hermitian form (inner product). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form ipid 16967 instead. (New usage is discouraged.) |
| ⊢ ·𝑖 = Slot 8 | ||
| Definition | df-tset 16907 | Define the topology component of a topological space (structure). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form tsetid 16988 instead. (New usage is discouraged.) |
| ⊢ TopSet = Slot 9 | ||
| Definition | df-ple 16908 | Define "less than or equal to" ordering extractor for posets and related structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.) Use its index-independent form pleid 17001 instead. (New usage is discouraged.) |
| ⊢ le = Slot ;10 | ||
| Definition | df-ocomp 16909 | Define the orthocomplementation extractor for posets and related structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form ocid 17015 instead. (New usage is discouraged.) |
| ⊢ oc = Slot ;11 | ||
| Definition | df-ds 16910 | Define the distance function component of a metric space (structure). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form dsid 17017 instead. (New usage is discouraged.) |
| ⊢ dist = Slot ;12 | ||
| Definition | df-unif 16911 | Define the uniform structure component of a uniform space. (Contributed by Mario Carneiro, 14-Aug-2015.) Use its index-independent form unifid 17026 instead. (New usage is discouraged.) |
| ⊢ UnifSet = Slot ;13 | ||
| Definition | df-hom 16912 | Define the hom-set component of a category. (Contributed by Mario Carneiro, 2-Jan-2017.) Use its index-independent form homid 17041 instead. (New usage is discouraged.) |
| ⊢ Hom = Slot ;14 | ||
| Definition | df-cco 16913 | Define the composition operation of a category. (Contributed by Mario Carneiro, 2-Jan-2017.) Use its index-independent form ccoid 17043 instead. (New usage is discouraged.) |
| ⊢ comp = Slot ;15 | ||
| Theorem | plusgndx 16914 | Index value of the df-plusg 16901 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
| ⊢ (+g‘ndx) = 2 | ||
| Theorem | plusgid 16915 | Utility theorem: index-independent form of df-plusg 16901. (Contributed by NM, 20-Oct-2012.) |
| ⊢ +g = Slot (+g‘ndx) | ||
| Theorem | plusgndxnn 16916 | The index of the slot for the group operation in an extensible structure is a positive integer. (Contributed by AV, 17-Oct-2024.) |
| ⊢ (+g‘ndx) ∈ ℕ | ||
| Theorem | basendxltplusgndx 16917 | The index of the slot for the base set is less then the index of the slot for the group operation in an extensible structure. (Contributed by AV, 17-Oct-2024.) |
| ⊢ (Base‘ndx) < (+g‘ndx) | ||
| Theorem | basendxnplusgndx 16918 | The slot for the base set is not the slot for the group operation in an extensible structure. (Contributed by AV, 14-Nov-2021.) (Proof shortened by AV, 17-Oct-2024.) |
| ⊢ (Base‘ndx) ≠ (+g‘ndx) | ||
| Theorem | basendxnplusgndxOLD 16919 | Obsolete version of basendxnplusgndx 16918 as of 17-Oct-2024. The slot for the base set is not the slot for the group operation in an extensible structure. (Contributed by AV, 14-Nov-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (Base‘ndx) ≠ (+g‘ndx) | ||
| Theorem | grpstr 16920 | A constructed group is a structure on 1...2. Depending on hard-coded index values. Use grpstrndx 16921 instead. (Contributed by Mario Carneiro, 28-Sep-2013.) (Revised by Mario Carneiro, 30-Apr-2015.) (New usage is discouraged.) |
| ⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩} ⇒ ⊢ 𝐺 Struct ⟨1, 2⟩ | ||
| Theorem | grpstrndx 16921 | A constructed group is a structure. Version not depending on the implementation of the indices. (Contributed by AV, 27-Oct-2024.) |
| ⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩} ⇒ ⊢ 𝐺 Struct ⟨(Base‘ndx), (+g‘ndx)⟩ | ||
| Theorem | grpbase 16922 | The base set of a constructed group. (Contributed by Mario Carneiro, 2-Aug-2013.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by AV, 27-Oct-2024.) |
| ⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩} ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐺)) | ||
| Theorem | grpbaseOLD 16923 | Obsolete version of grpbase 16922 as of 27-Oct-2024. The base set of a constructed group. (Contributed by Mario Carneiro, 2-Aug-2013.) (Revised by Mario Carneiro, 30-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩} ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐺)) | ||
| Theorem | grpplusg 16924 | The operation of a constructed group. (Contributed by Mario Carneiro, 2-Aug-2013.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by AV, 27-Oct-2024.) |
| ⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩} ⇒ ⊢ ( + ∈ 𝑉 → + = (+g‘𝐺)) | ||
| Theorem | grpplusgOLD 16925 | Obsolete version of grpplusg 16924 as of 27-Oct-2024. The operation of a constructed group. (Contributed by Mario Carneiro, 2-Aug-2013.) (Revised by Mario Carneiro, 30-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩} ⇒ ⊢ ( + ∈ 𝑉 → + = (+g‘𝐺)) | ||
| Theorem | ressplusg 16926 | +g is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻)) | ||
| Theorem | grpbasex 16927 | 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 16922 instead. (New usage is discouraged.) (Contributed by NM, 17-Oct-2012.) |
| ⊢ 𝐵 ∈ V & ⊢ + ∈ V & ⊢ 𝐺 = {⟨1, 𝐵⟩, ⟨2, + ⟩} ⇒ ⊢ 𝐵 = (Base‘𝐺) | ||
| Theorem | grpplusgx 16928 | 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 16924 instead. (New usage is discouraged.) (Contributed by NM, 17-Oct-2012.) |
| ⊢ 𝐵 ∈ V & ⊢ + ∈ V & ⊢ 𝐺 = {⟨1, 𝐵⟩, ⟨2, + ⟩} ⇒ ⊢ + = (+g‘𝐺) | ||
| Theorem | mulrndx 16929 | Index value of the df-mulr 16902 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
| ⊢ (.r‘ndx) = 3 | ||
| Theorem | mulrid 16930 | Utility theorem: index-independent form of df-mulr 16902. (Contributed by Mario Carneiro, 8-Jun-2013.) |
| ⊢ .r = Slot (.r‘ndx) | ||
| Theorem | basendxnmulrndx 16931 | 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.) (Proof shortened by AV, 28-Oct-2024.) |
| ⊢ (Base‘ndx) ≠ (.r‘ndx) | ||
| Theorem | basendxnmulrndxOLD 16932 | Obsolete proof of basendxnmulrndx 16931 as of 28-Oct-2024. 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.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (Base‘ndx) ≠ (.r‘ndx) | ||
| Theorem | plusgndxnmulrndx 16933 | 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 | rngstr 16934 | 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 16935 | 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 16936 | 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 16937 | 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 16938 | Index value of the df-starv 16903 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
| ⊢ (*𝑟‘ndx) = 4 | ||
| Theorem | starvid 16939 | Utility theorem: index-independent form of df-starv 16903. (Contributed by Mario Carneiro, 6-Oct-2013.) |
| ⊢ *𝑟 = Slot (*𝑟‘ndx) | ||
| Theorem | starvndxnbasendx 16940 | The slot for the involution function is not the slot for the base set in an extensible structure. Formerly part of proof for ressstarv 16944. (Contributed by AV, 18-Oct-2024.) |
| ⊢ (*𝑟‘ndx) ≠ (Base‘ndx) | ||
| Theorem | starvndxnplusgndx 16941 | The slot for the involution function is not the slot for the base set in an extensible structure. Formerly part of proof for ressstarv 16944. (Contributed by AV, 18-Oct-2024.) |
| ⊢ (*𝑟‘ndx) ≠ (+g‘ndx) | ||
| Theorem | starvndxnmulrndx 16942 | The slot for the involution function is not the slot for the base set in an extensible structure. Formerly part of proof for ressstarv 16944. (Contributed by AV, 18-Oct-2024.) |
| ⊢ (*𝑟‘ndx) ≠ (.r‘ndx) | ||
| Theorem | ressmulr 16943 | .r is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
| ⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝑆)) | ||
| Theorem | ressstarv 16944 | *𝑟 is unaffected by restriction. (Contributed by Mario Carneiro, 9-Oct-2015.) |
| ⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ ∗ = (*𝑟‘𝑅) ⇒ ⊢ (𝐴 ∈ 𝑉 → ∗ = (*𝑟‘𝑆)) | ||
| Theorem | srngstr 16945 | 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 16946 | 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 16947 | 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 16948 | 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 16949 | The involution function of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.) |
| ⊢ 𝑅 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗ ⟩}) ⇒ ⊢ ( ∗ ∈ 𝑋 → ∗ = (*𝑟‘𝑅)) | ||
| Theorem | scandx 16950 | Index value of the df-sca 16904 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
| ⊢ (Scalar‘ndx) = 5 | ||
| Theorem | scaid 16951 | Utility theorem: index-independent form of scalar df-sca 16904. (Contributed by Mario Carneiro, 19-Jun-2014.) |
| ⊢ Scalar = Slot (Scalar‘ndx) | ||
| Theorem | scandxnbasendx 16952 | The slot for the scalar is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) |
| ⊢ (Scalar‘ndx) ≠ (Base‘ndx) | ||
| Theorem | scandxnplusgndx 16953 | The slot for the scalar field is not the slot for the group operation in an extensible structure. Formerly part of proof for mgpsca 19643. (Contributed by AV, 18-Oct-2024.) |
| ⊢ (Scalar‘ndx) ≠ (+g‘ndx) | ||
| Theorem | scandxnmulrndx 16954 | The slot for the scalar field is not the slot for the ring (multiplication) operation in an extensible structure. Formerly part of proof for mgpsca 19643. (Contributed by AV, 29-Oct-2024.) |
| ⊢ (Scalar‘ndx) ≠ (.r‘ndx) | ||
| Theorem | vscandx 16955 | Index value of the df-vsca 16905 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
| ⊢ ( ·𝑠 ‘ndx) = 6 | ||
| Theorem | vscaid 16956 | Utility theorem: index-independent form of scalar product df-vsca 16905. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
| ⊢ ·𝑠 = Slot ( ·𝑠 ‘ndx) | ||
| Theorem | vscandxnbasendx 16957 | The slot for the scalar product is not the slot for the base set in an extensible structure. Formerly part of proof for rmodislmod 20106. (Contributed by AV, 18-Oct-2024.) |
| ⊢ ( ·𝑠 ‘ndx) ≠ (Base‘ndx) | ||
| Theorem | vscandxnplusgndx 16958 | The slot for the scalar product is not the slot for the group operation in an extensible structure. Formerly part of proof for rmodislmod 20106. (Contributed by AV, 18-Oct-2024.) |
| ⊢ ( ·𝑠 ‘ndx) ≠ (+g‘ndx) | ||
| Theorem | vscandxnmulrndx 16959 | The slot for the scalar product is not the slot for the ring (multiplication) operation in an extensible structure. Formerly part of proof for rmodislmod 20106. (Contributed by AV, 29-Oct-2024.) |
| ⊢ ( ·𝑠 ‘ndx) ≠ (.r‘ndx) | ||
| Theorem | vscandxnscandx 16960 | The slot for the scalar product is not the slot for the scalar field in an extensible structure. Formerly part of proof for rmodislmod 20106. (Contributed by AV, 18-Oct-2024.) |
| ⊢ ( ·𝑠 ‘ndx) ≠ (Scalar‘ndx) | ||
| Theorem | lmodstr 16961 | 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 16962 | 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 16963 | 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 16964 | 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 16965 | 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 16966 | Index value of the df-ip 16906 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
| ⊢ (·𝑖‘ndx) = 8 | ||
| Theorem | ipid 16967 | Utility theorem: index-independent form of df-ip 16906. (Contributed by Mario Carneiro, 6-Oct-2013.) |
| ⊢ ·𝑖 = Slot (·𝑖‘ndx) | ||
| Theorem | ipndxnbasendx 16968 | The slot for the inner product is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) |
| ⊢ (·𝑖‘ndx) ≠ (Base‘ndx) | ||
| Theorem | ipndxnplusgndx 16969 | The slot for the inner product is not the slot for the group operation in an extensible structure. (Contributed by AV, 29-Oct-2024.) |
| ⊢ (·𝑖‘ndx) ≠ (+g‘ndx) | ||
| Theorem | ipndxnmulrndx 16970 | The slot for the inner product is not the slot for the ring (multiplication) operation in an extensible structure. Formerly part of proof for mgpsca 19643. (Contributed by AV, 29-Oct-2024.) |
| ⊢ (·𝑖‘ndx) ≠ (.r‘ndx) | ||
| Theorem | ipsstr 16971 | Lemma to shorten proofs of ipsbase 16972 through ipsvsca 16976. (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 16972 | 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 16973 | 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 16974 | 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 16975 | 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 16976 | 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 16977 | 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 16978 | Scalar is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐹 = (Scalar‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹 = (Scalar‘𝐻)) | ||
| Theorem | ressvsca 16979 | ·𝑠 is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ · = ( ·𝑠 ‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘𝐻)) | ||
| Theorem | ressip 16980 | The inner product is unaffected by restriction. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ , = (·𝑖‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → , = (·𝑖‘𝐻)) | ||
| Theorem | phlstr 16981 | A constructed pre-Hilbert space is a structure. Starting from lmodstr 16961 (which has 4 members), we chain strleun 16786 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 16982 | 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 16983 | 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 16984 | 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 16985 | 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 16986 | 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 16987 | Index value of the df-tset 16907 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
| ⊢ (TopSet‘ndx) = 9 | ||
| Theorem | tsetid 16988 | Utility theorem: index-independent form of df-tset 16907. (Contributed by NM, 20-Oct-2012.) |
| ⊢ TopSet = Slot (TopSet‘ndx) | ||
| Theorem | tsetndxnn 16989 | The index of the slot for the group operation in an extensible structure is a positive integer. (Contributed by AV, 31-Oct-2024.) |
| ⊢ (TopSet‘ndx) ∈ ℕ | ||
| Theorem | basendxlttsetndx 16990 | The index of the slot for the base set is less then the index of the slot for the topology in an extensible structure. (Contributed by AV, 31-Oct-2024.) |
| ⊢ (Base‘ndx) < (TopSet‘ndx) | ||
| Theorem | tsetndxnbasendx 16991 | The slot for the topology is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 31-Oct-2024.) |
| ⊢ (TopSet‘ndx) ≠ (Base‘ndx) | ||
| Theorem | tsetndxnplusgndx 16992 | The slot for the topology is not the slot for the group operation in an extensible structure. Formerly part of proof for oppgtset 18873. (Contributed by AV, 18-Oct-2024.) |
| ⊢ (TopSet‘ndx) ≠ (+g‘ndx) | ||
| Theorem | tsetndxnmulrndx 16993 | 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 | slotstnscsi 16994 | The slots Scalar, ·𝑠 and ·𝑖 are different from the slot TopSet. Formerly part of sralem 20354 and proofs using it. (Contributed by AV, 29-Oct-2024.) |
| ⊢ ((TopSet‘ndx) ≠ (Scalar‘ndx) ∧ (TopSet‘ndx) ≠ ( ·𝑠 ‘ndx) ∧ (TopSet‘ndx) ≠ (·𝑖‘ndx)) | ||
| Theorem | topgrpstr 16995 | 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 16996 | The base set of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) |
| ⊢ 𝑊 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩} ⇒ ⊢ (𝐵 ∈ 𝑋 → 𝐵 = (Base‘𝑊)) | ||
| Theorem | topgrpplusg 16997 | The additive operation of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) |
| ⊢ 𝑊 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩} ⇒ ⊢ ( + ∈ 𝑋 → + = (+g‘𝑊)) | ||
| Theorem | topgrptset 16998 | The topology of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) |
| ⊢ 𝑊 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩} ⇒ ⊢ (𝐽 ∈ 𝑋 → 𝐽 = (TopSet‘𝑊)) | ||
| Theorem | resstset 16999 | TopSet is unaffected by restriction. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐽 = (TopSet‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐽 = (TopSet‘𝐻)) | ||
| Theorem | plendx 17000 | Index value of the df-ple 16908 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.) |
| ⊢ (le‘ndx) = ;10 | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |