![]() |
Metamath
Proof Explorer Theorem List (p. 173 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cvsca 17201 | Extend class notation with scalar product. |
class ·𝑠 | ||
Syntax | cip 17202 | Extend class notation with Hermitian form (inner product). |
class ·𝑖 | ||
Syntax | cts 17203 | Extend class notation with the topology component of a topological space. |
class TopSet | ||
Syntax | cple 17204 | Extend class notation with "less than or equal to" for posets. |
class le | ||
Syntax | coc 17205 | Extend class notation with the class of orthocomplementation extractors. |
class oc | ||
Syntax | cds 17206 | Extend class notation with the metric space distance function. |
class dist | ||
Syntax | cunif 17207 | Extend class notation with the uniform structure. |
class UnifSet | ||
Syntax | chom 17208 | Extend class notation with the hom-set structure. |
class Hom | ||
Syntax | cco 17209 | Extend class notation with the composition operation. |
class comp | ||
Definition | df-plusg 17210 | Define group operation. In the context of less restrictive structures, this operation is also called magma, semigroup or monoid operation. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form plusgid 17224 instead. (New usage is discouraged.) |
⊢ +g = Slot 2 | ||
Definition | df-mulr 17211 | Define ring multiplication. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form mulrid 11212 instead. (New usage is discouraged.) |
⊢ .r = Slot 3 | ||
Definition | df-starv 17212 | 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 17248 instead. (New usage is discouraged.) |
⊢ *𝑟 = Slot 4 | ||
Definition | df-sca 17213 | 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 17260 instead. (New usage is discouraged.) |
⊢ Scalar = Slot 5 | ||
Definition | df-vsca 17214 | Define scalar product. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form vscaid 17265 instead. (New usage is discouraged.) |
⊢ ·𝑠 = Slot 6 | ||
Definition | df-ip 17215 | Define Hermitian form (inner product). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form ipid 17276 instead. (New usage is discouraged.) |
⊢ ·𝑖 = Slot 8 | ||
Definition | df-tset 17216 | 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 17298 instead. (New usage is discouraged.) |
⊢ TopSet = Slot 9 | ||
Definition | df-ple 17217 | 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 17312 instead. (New usage is discouraged.) |
⊢ le = Slot ;10 | ||
Definition | df-ocomp 17218 | 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 17327 instead. (New usage is discouraged.) |
⊢ oc = Slot ;11 | ||
Definition | df-ds 17219 | 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 17331 instead. (New usage is discouraged.) |
⊢ dist = Slot ;12 | ||
Definition | df-unif 17220 | Define the uniform structure component of a uniform space. (Contributed by Mario Carneiro, 14-Aug-2015.) Use its index-independent form unifid 17341 instead. (New usage is discouraged.) |
⊢ UnifSet = Slot ;13 | ||
Definition | df-hom 17221 | Define the hom-set component of a category. (Contributed by Mario Carneiro, 2-Jan-2017.) Use its index-independent form homid 17357 instead. (New usage is discouraged.) |
⊢ Hom = Slot ;14 | ||
Definition | df-cco 17222 | Define the composition operation of a category. (Contributed by Mario Carneiro, 2-Jan-2017.) Use its index-independent form ccoid 17359 instead. (New usage is discouraged.) |
⊢ comp = Slot ;15 | ||
Theorem | plusgndx 17223 | Index value of the df-plusg 17210 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
⊢ (+g‘ndx) = 2 | ||
Theorem | plusgid 17224 | Utility theorem: index-independent form of df-plusg 17210. (Contributed by NM, 20-Oct-2012.) |
⊢ +g = Slot (+g‘ndx) | ||
Theorem | plusgndxnn 17225 | 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 17226 | 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 17227 | 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 17228 | Obsolete version of basendxnplusgndx 17227 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 17229 | A constructed group is a structure on 1...2. Depending on hard-coded index values. Use grpstrndx 17230 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 17230 | 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 17231 | 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 17232 | Obsolete version of grpbase 17231 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 17233 | 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 17234 | Obsolete version of grpplusg 17233 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 17235 | +g is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻)) | ||
Theorem | grpbasex 17236 | 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 17231 instead. (New usage is discouraged.) (Contributed by NM, 17-Oct-2012.) |
⊢ 𝐵 ∈ V & ⊢ + ∈ V & ⊢ 𝐺 = {⟨1, 𝐵⟩, ⟨2, + ⟩} ⇒ ⊢ 𝐵 = (Base‘𝐺) | ||
Theorem | grpplusgx 17237 | 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 17233 instead. (New usage is discouraged.) (Contributed by NM, 17-Oct-2012.) |
⊢ 𝐵 ∈ V & ⊢ + ∈ V & ⊢ 𝐺 = {⟨1, 𝐵⟩, ⟨2, + ⟩} ⇒ ⊢ + = (+g‘𝐺) | ||
Theorem | mulrndx 17238 | Index value of the df-mulr 17211 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
⊢ (.r‘ndx) = 3 | ||
Theorem | mulridx 17239 | Utility theorem: index-independent form of df-mulr 17211. (Contributed by Mario Carneiro, 8-Jun-2013.) |
⊢ .r = Slot (.r‘ndx) | ||
Theorem | basendxnmulrndx 17240 | 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 17241 | Obsolete proof of basendxnmulrndx 17240 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 17242 | 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 17243 | 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 17244 | 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 17245 | 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 17246 | 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 17247 | Index value of the df-starv 17212 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
⊢ (*𝑟‘ndx) = 4 | ||
Theorem | starvid 17248 | Utility theorem: index-independent form of df-starv 17212. (Contributed by Mario Carneiro, 6-Oct-2013.) |
⊢ *𝑟 = Slot (*𝑟‘ndx) | ||
Theorem | starvndxnbasendx 17249 | The slot for the involution function is not the slot for the base set in an extensible structure. Formerly part of proof for ressstarv 17253. (Contributed by AV, 18-Oct-2024.) |
⊢ (*𝑟‘ndx) ≠ (Base‘ndx) | ||
Theorem | starvndxnplusgndx 17250 | The slot for the involution function is not the slot for the base set in an extensible structure. Formerly part of proof for ressstarv 17253. (Contributed by AV, 18-Oct-2024.) |
⊢ (*𝑟‘ndx) ≠ (+g‘ndx) | ||
Theorem | starvndxnmulrndx 17251 | The slot for the involution function is not the slot for the base set in an extensible structure. Formerly part of proof for ressstarv 17253. (Contributed by AV, 18-Oct-2024.) |
⊢ (*𝑟‘ndx) ≠ (.r‘ndx) | ||
Theorem | ressmulr 17252 | .r is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝑆)) | ||
Theorem | ressstarv 17253 | *𝑟 is unaffected by restriction. (Contributed by Mario Carneiro, 9-Oct-2015.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ ∗ = (*𝑟‘𝑅) ⇒ ⊢ (𝐴 ∈ 𝑉 → ∗ = (*𝑟‘𝑆)) | ||
Theorem | srngstr 17254 | 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 17255 | 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 17256 | 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 17257 | 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 17258 | The involution function of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ 𝑅 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗ ⟩}) ⇒ ⊢ ( ∗ ∈ 𝑋 → ∗ = (*𝑟‘𝑅)) | ||
Theorem | scandx 17259 | Index value of the df-sca 17213 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
⊢ (Scalar‘ndx) = 5 | ||
Theorem | scaid 17260 | Utility theorem: index-independent form of scalar df-sca 17213. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ Scalar = Slot (Scalar‘ndx) | ||
Theorem | scandxnbasendx 17261 | 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 17262 | The slot for the scalar field is not the slot for the group operation in an extensible structure. Formerly part of proof for mgpsca 19995. (Contributed by AV, 18-Oct-2024.) |
⊢ (Scalar‘ndx) ≠ (+g‘ndx) | ||
Theorem | scandxnmulrndx 17263 | 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 19995. (Contributed by AV, 29-Oct-2024.) |
⊢ (Scalar‘ndx) ≠ (.r‘ndx) | ||
Theorem | vscandx 17264 | Index value of the df-vsca 17214 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
⊢ ( ·𝑠 ‘ndx) = 6 | ||
Theorem | vscaid 17265 | Utility theorem: index-independent form of scalar product df-vsca 17214. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ ·𝑠 = Slot ( ·𝑠 ‘ndx) | ||
Theorem | vscandxnbasendx 17266 | The slot for the scalar product is not the slot for the base set in an extensible structure. Formerly part of proof for rmodislmod 20540. (Contributed by AV, 18-Oct-2024.) |
⊢ ( ·𝑠 ‘ndx) ≠ (Base‘ndx) | ||
Theorem | vscandxnplusgndx 17267 | The slot for the scalar product is not the slot for the group operation in an extensible structure. Formerly part of proof for rmodislmod 20540. (Contributed by AV, 18-Oct-2024.) |
⊢ ( ·𝑠 ‘ndx) ≠ (+g‘ndx) | ||
Theorem | vscandxnmulrndx 17268 | 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 20540. (Contributed by AV, 29-Oct-2024.) |
⊢ ( ·𝑠 ‘ndx) ≠ (.r‘ndx) | ||
Theorem | vscandxnscandx 17269 | The slot for the scalar product is not the slot for the scalar field in an extensible structure. Formerly part of proof for rmodislmod 20540. (Contributed by AV, 18-Oct-2024.) |
⊢ ( ·𝑠 ‘ndx) ≠ (Scalar‘ndx) | ||
Theorem | lmodstr 17270 | 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 17271 | 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 17272 | 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 17273 | 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 17274 | 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 17275 | Index value of the df-ip 17215 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
⊢ (·𝑖‘ndx) = 8 | ||
Theorem | ipid 17276 | Utility theorem: index-independent form of df-ip 17215. (Contributed by Mario Carneiro, 6-Oct-2013.) |
⊢ ·𝑖 = Slot (·𝑖‘ndx) | ||
Theorem | ipndxnbasendx 17277 | 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 17278 | 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 17279 | 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 19995. (Contributed by AV, 29-Oct-2024.) |
⊢ (·𝑖‘ndx) ≠ (.r‘ndx) | ||
Theorem | slotsdifipndx 17280 | The slot for the scalar is not the index of other slots. Formerly part of proof for srasca 20798 and sravsca 20800. (Contributed by AV, 12-Nov-2024.) |
⊢ (( ·𝑠 ‘ndx) ≠ (·𝑖‘ndx) ∧ (Scalar‘ndx) ≠ (·𝑖‘ndx)) | ||
Theorem | ipsstr 17281 | Lemma to shorten proofs of ipsbase 17282 through ipsvsca 17286. (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 17282 | 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 17283 | 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 17284 | 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 17285 | 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 17286 | 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 17287 | 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 17288 | Scalar is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐹 = (Scalar‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹 = (Scalar‘𝐻)) | ||
Theorem | ressvsca 17289 | ·𝑠 is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ · = ( ·𝑠 ‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘𝐻)) | ||
Theorem | ressip 17290 | The inner product is unaffected by restriction. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ , = (·𝑖‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → , = (·𝑖‘𝐻)) | ||
Theorem | phlstr 17291 | A constructed pre-Hilbert space is a structure. Starting from lmodstr 17270 (which has 4 members), we chain strleun 17090 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 17292 | 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 17293 | 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 17294 | 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 17295 | 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 17296 | 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 17297 | Index value of the df-tset 17216 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
⊢ (TopSet‘ndx) = 9 | ||
Theorem | tsetid 17298 | Utility theorem: index-independent form of df-tset 17216. (Contributed by NM, 20-Oct-2012.) |
⊢ TopSet = Slot (TopSet‘ndx) | ||
Theorem | tsetndxnn 17299 | 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 17300 | 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) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |