| Metamath
Proof Explorer Theorem List (p. 174 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Syntax | cvsca 17301 | Extend class notation with scalar product. |
| class ·𝑠 | ||
| Syntax | cip 17302 | Extend class notation with Hermitian form (inner product). |
| class ·𝑖 | ||
| Syntax | cts 17303 | Extend class notation with the topology component of a topological space. |
| class TopSet | ||
| Syntax | cple 17304 | Extend class notation with "less than or equal to" for posets. |
| class le | ||
| Syntax | coc 17305 | Extend class notation with the class of orthocomplementation extractors. |
| class oc | ||
| Syntax | cds 17306 | Extend class notation with the metric space distance function. |
| class dist | ||
| Syntax | cunif 17307 | Extend class notation with the uniform structure. |
| class UnifSet | ||
| Syntax | chom 17308 | Extend class notation with the hom-set structure. |
| class Hom | ||
| Syntax | cco 17309 | Extend class notation with the composition operation. |
| class comp | ||
| Definition | df-plusg 17310 | 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 17324 instead. (New usage is discouraged.) |
| ⊢ +g = Slot 2 | ||
| Definition | df-mulr 17311 | Define ring multiplication. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form mulrid 11259 instead. (New usage is discouraged.) |
| ⊢ .r = Slot 3 | ||
| Definition | df-starv 17312 | 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 17347 instead. (New usage is discouraged.) |
| ⊢ *𝑟 = Slot 4 | ||
| Definition | df-sca 17313 | 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 17359 instead. (New usage is discouraged.) |
| ⊢ Scalar = Slot 5 | ||
| Definition | df-vsca 17314 | Define scalar product. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form vscaid 17364 instead. (New usage is discouraged.) |
| ⊢ ·𝑠 = Slot 6 | ||
| Definition | df-ip 17315 | Define Hermitian form (inner product). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form ipid 17375 instead. (New usage is discouraged.) |
| ⊢ ·𝑖 = Slot 8 | ||
| Definition | df-tset 17316 | 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 17397 instead. (New usage is discouraged.) |
| ⊢ TopSet = Slot 9 | ||
| Definition | df-ple 17317 | 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 17411 instead. (New usage is discouraged.) |
| ⊢ le = Slot ;10 | ||
| Definition | df-ocomp 17318 | 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 17426 instead. (New usage is discouraged.) |
| ⊢ oc = Slot ;11 | ||
| Definition | df-ds 17319 | 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 17430 instead. (New usage is discouraged.) |
| ⊢ dist = Slot ;12 | ||
| Definition | df-unif 17320 | Define the uniform structure component of a uniform space. (Contributed by Mario Carneiro, 14-Aug-2015.) Use its index-independent form unifid 17440 instead. (New usage is discouraged.) |
| ⊢ UnifSet = Slot ;13 | ||
| Definition | df-hom 17321 | Define the hom-set component of a category. (Contributed by Mario Carneiro, 2-Jan-2017.) Use its index-independent form homid 17456 instead. (New usage is discouraged.) |
| ⊢ Hom = Slot ;14 | ||
| Definition | df-cco 17322 | Define the composition operation of a category. (Contributed by Mario Carneiro, 2-Jan-2017.) Use its index-independent form ccoid 17458 instead. (New usage is discouraged.) |
| ⊢ comp = Slot ;15 | ||
| Theorem | plusgndx 17323 | Index value of the df-plusg 17310 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
| ⊢ (+g‘ndx) = 2 | ||
| Theorem | plusgid 17324 | Utility theorem: index-independent form of df-plusg 17310. (Contributed by NM, 20-Oct-2012.) |
| ⊢ +g = Slot (+g‘ndx) | ||
| Theorem | plusgndxnn 17325 | 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 17326 | 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 17327 | 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 | grpstr 17328 | A constructed group is a structure on 1...2. Depending on hard-coded index values. Use grpstrndx 17329 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 17329 | 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 17330 | 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 17331 | Obsolete version of grpbase 17330 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 17332 | 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 17333 | Obsolete version of grpplusg 17332 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 17334 | +g is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻)) | ||
| Theorem | grpbasex 17335 | 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 17330 instead. (New usage is discouraged.) (Contributed by NM, 17-Oct-2012.) |
| ⊢ 𝐵 ∈ V & ⊢ + ∈ V & ⊢ 𝐺 = {〈1, 𝐵〉, 〈2, + 〉} ⇒ ⊢ 𝐵 = (Base‘𝐺) | ||
| Theorem | grpplusgx 17336 | 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 17332 instead. (New usage is discouraged.) (Contributed by NM, 17-Oct-2012.) |
| ⊢ 𝐵 ∈ V & ⊢ + ∈ V & ⊢ 𝐺 = {〈1, 𝐵〉, 〈2, + 〉} ⇒ ⊢ + = (+g‘𝐺) | ||
| Theorem | mulrndx 17337 | Index value of the df-mulr 17311 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
| ⊢ (.r‘ndx) = 3 | ||
| Theorem | mulridx 17338 | Utility theorem: index-independent form of df-mulr 17311. (Contributed by Mario Carneiro, 8-Jun-2013.) |
| ⊢ .r = Slot (.r‘ndx) | ||
| Theorem | basendxnmulrndx 17339 | 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 17340 | Obsolete version of basendxnmulrndx 17339 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 17341 | 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 17342 | 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 17343 | 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 17344 | 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 17345 | 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 17346 | Index value of the df-starv 17312 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
| ⊢ (*𝑟‘ndx) = 4 | ||
| Theorem | starvid 17347 | Utility theorem: index-independent form of df-starv 17312. (Contributed by Mario Carneiro, 6-Oct-2013.) |
| ⊢ *𝑟 = Slot (*𝑟‘ndx) | ||
| Theorem | starvndxnbasendx 17348 | The slot for the involution function is not the slot for the base set in an extensible structure. Formerly part of proof for ressstarv 17352. (Contributed by AV, 18-Oct-2024.) |
| ⊢ (*𝑟‘ndx) ≠ (Base‘ndx) | ||
| Theorem | starvndxnplusgndx 17349 | The slot for the involution function is not the slot for the base set in an extensible structure. Formerly part of proof for ressstarv 17352. (Contributed by AV, 18-Oct-2024.) |
| ⊢ (*𝑟‘ndx) ≠ (+g‘ndx) | ||
| Theorem | starvndxnmulrndx 17350 | The slot for the involution function is not the slot for the base set in an extensible structure. Formerly part of proof for ressstarv 17352. (Contributed by AV, 18-Oct-2024.) |
| ⊢ (*𝑟‘ndx) ≠ (.r‘ndx) | ||
| Theorem | ressmulr 17351 | .r is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
| ⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝑆)) | ||
| Theorem | ressstarv 17352 | *𝑟 is unaffected by restriction. (Contributed by Mario Carneiro, 9-Oct-2015.) |
| ⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ ∗ = (*𝑟‘𝑅) ⇒ ⊢ (𝐴 ∈ 𝑉 → ∗ = (*𝑟‘𝑆)) | ||
| Theorem | srngstr 17353 | 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 17354 | 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 17355 | 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 17356 | 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 17357 | The involution function of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.) |
| ⊢ 𝑅 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(*𝑟‘ndx), ∗ 〉}) ⇒ ⊢ ( ∗ ∈ 𝑋 → ∗ = (*𝑟‘𝑅)) | ||
| Theorem | scandx 17358 | Index value of the df-sca 17313 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
| ⊢ (Scalar‘ndx) = 5 | ||
| Theorem | scaid 17359 | Utility theorem: index-independent form of scalar df-sca 17313. (Contributed by Mario Carneiro, 19-Jun-2014.) |
| ⊢ Scalar = Slot (Scalar‘ndx) | ||
| Theorem | scandxnbasendx 17360 | 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 17361 | The slot for the scalar field is not the slot for the group operation in an extensible structure. Formerly part of proof for mgpsca 20143. (Contributed by AV, 18-Oct-2024.) |
| ⊢ (Scalar‘ndx) ≠ (+g‘ndx) | ||
| Theorem | scandxnmulrndx 17362 | 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 20143. (Contributed by AV, 29-Oct-2024.) |
| ⊢ (Scalar‘ndx) ≠ (.r‘ndx) | ||
| Theorem | vscandx 17363 | Index value of the df-vsca 17314 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
| ⊢ ( ·𝑠 ‘ndx) = 6 | ||
| Theorem | vscaid 17364 | Utility theorem: index-independent form of scalar product df-vsca 17314. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
| ⊢ ·𝑠 = Slot ( ·𝑠 ‘ndx) | ||
| Theorem | vscandxnbasendx 17365 | The slot for the scalar product is not the slot for the base set in an extensible structure. Formerly part of proof for rmodislmod 20928. (Contributed by AV, 18-Oct-2024.) |
| ⊢ ( ·𝑠 ‘ndx) ≠ (Base‘ndx) | ||
| Theorem | vscandxnplusgndx 17366 | The slot for the scalar product is not the slot for the group operation in an extensible structure. Formerly part of proof for rmodislmod 20928. (Contributed by AV, 18-Oct-2024.) |
| ⊢ ( ·𝑠 ‘ndx) ≠ (+g‘ndx) | ||
| Theorem | vscandxnmulrndx 17367 | 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 20928. (Contributed by AV, 29-Oct-2024.) |
| ⊢ ( ·𝑠 ‘ndx) ≠ (.r‘ndx) | ||
| Theorem | vscandxnscandx 17368 | The slot for the scalar product is not the slot for the scalar field in an extensible structure. Formerly part of proof for rmodislmod 20928. (Contributed by AV, 18-Oct-2024.) |
| ⊢ ( ·𝑠 ‘ndx) ≠ (Scalar‘ndx) | ||
| Theorem | lmodstr 17369 | 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 17370 | 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 17371 | 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 17372 | 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 17373 | 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 17374 | Index value of the df-ip 17315 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
| ⊢ (·𝑖‘ndx) = 8 | ||
| Theorem | ipid 17375 | Utility theorem: index-independent form of df-ip 17315. (Contributed by Mario Carneiro, 6-Oct-2013.) |
| ⊢ ·𝑖 = Slot (·𝑖‘ndx) | ||
| Theorem | ipndxnbasendx 17376 | 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 17377 | 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 17378 | 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 20143. (Contributed by AV, 29-Oct-2024.) |
| ⊢ (·𝑖‘ndx) ≠ (.r‘ndx) | ||
| Theorem | slotsdifipndx 17379 | The slot for the scalar is not the index of other slots. Formerly part of proof for srasca 21183 and sravsca 21185. (Contributed by AV, 12-Nov-2024.) |
| ⊢ (( ·𝑠 ‘ndx) ≠ (·𝑖‘ndx) ∧ (Scalar‘ndx) ≠ (·𝑖‘ndx)) | ||
| Theorem | ipsstr 17380 | Lemma to shorten proofs of ipsbase 17381 through ipsvsca 17385. (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 17381 | 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 17382 | 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 17383 | 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 17384 | 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 17385 | 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 17386 | 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 17387 | Scalar is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐹 = (Scalar‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹 = (Scalar‘𝐻)) | ||
| Theorem | ressvsca 17388 | ·𝑠 is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ · = ( ·𝑠 ‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘𝐻)) | ||
| Theorem | ressip 17389 | The inner product is unaffected by restriction. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ , = (·𝑖‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → , = (·𝑖‘𝐻)) | ||
| Theorem | phlstr 17390 | A constructed pre-Hilbert space is a structure. Starting from lmodstr 17369 (which has 4 members), we chain strleun 17194 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 17391 | 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 17392 | 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 17393 | 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 17394 | 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 17395 | 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 17396 | Index value of the df-tset 17316 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
| ⊢ (TopSet‘ndx) = 9 | ||
| Theorem | tsetid 17397 | Utility theorem: index-independent form of df-tset 17316. (Contributed by NM, 20-Oct-2012.) |
| ⊢ TopSet = Slot (TopSet‘ndx) | ||
| Theorem | tsetndxnn 17398 | 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 17399 | 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 17400 | 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) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |