Home | Metamath
Proof Explorer Theorem List (p. 172 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | grpstrndx 17101 | 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 17102 | 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 17103 | Obsolete version of grpbase 17102 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 17104 | 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 17105 | Obsolete version of grpplusg 17104 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 17106 | +g is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻)) | ||
Theorem | grpbasex 17107 | 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 17102 instead. (New usage is discouraged.) (Contributed by NM, 17-Oct-2012.) |
⊢ 𝐵 ∈ V & ⊢ + ∈ V & ⊢ 𝐺 = {⟨1, 𝐵⟩, ⟨2, + ⟩} ⇒ ⊢ 𝐵 = (Base‘𝐺) | ||
Theorem | grpplusgx 17108 | 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 17104 instead. (New usage is discouraged.) (Contributed by NM, 17-Oct-2012.) |
⊢ 𝐵 ∈ V & ⊢ + ∈ V & ⊢ 𝐺 = {⟨1, 𝐵⟩, ⟨2, + ⟩} ⇒ ⊢ + = (+g‘𝐺) | ||
Theorem | mulrndx 17109 | Index value of the df-mulr 17082 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
⊢ (.r‘ndx) = 3 | ||
Theorem | mulrid 17110 | Utility theorem: index-independent form of df-mulr 17082. (Contributed by Mario Carneiro, 8-Jun-2013.) |
⊢ .r = Slot (.r‘ndx) | ||
Theorem | basendxnmulrndx 17111 | 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 17112 | Obsolete proof of basendxnmulrndx 17111 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 17113 | 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 17114 | 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 17115 | 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 17116 | 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 17117 | 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 17118 | Index value of the df-starv 17083 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
⊢ (*𝑟‘ndx) = 4 | ||
Theorem | starvid 17119 | Utility theorem: index-independent form of df-starv 17083. (Contributed by Mario Carneiro, 6-Oct-2013.) |
⊢ *𝑟 = Slot (*𝑟‘ndx) | ||
Theorem | starvndxnbasendx 17120 | The slot for the involution function is not the slot for the base set in an extensible structure. Formerly part of proof for ressstarv 17124. (Contributed by AV, 18-Oct-2024.) |
⊢ (*𝑟‘ndx) ≠ (Base‘ndx) | ||
Theorem | starvndxnplusgndx 17121 | The slot for the involution function is not the slot for the base set in an extensible structure. Formerly part of proof for ressstarv 17124. (Contributed by AV, 18-Oct-2024.) |
⊢ (*𝑟‘ndx) ≠ (+g‘ndx) | ||
Theorem | starvndxnmulrndx 17122 | The slot for the involution function is not the slot for the base set in an extensible structure. Formerly part of proof for ressstarv 17124. (Contributed by AV, 18-Oct-2024.) |
⊢ (*𝑟‘ndx) ≠ (.r‘ndx) | ||
Theorem | ressmulr 17123 | .r is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝑆)) | ||
Theorem | ressstarv 17124 | *𝑟 is unaffected by restriction. (Contributed by Mario Carneiro, 9-Oct-2015.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ ∗ = (*𝑟‘𝑅) ⇒ ⊢ (𝐴 ∈ 𝑉 → ∗ = (*𝑟‘𝑆)) | ||
Theorem | srngstr 17125 | 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 17126 | 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 17127 | 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 17128 | 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 17129 | The involution function of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ 𝑅 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗ ⟩}) ⇒ ⊢ ( ∗ ∈ 𝑋 → ∗ = (*𝑟‘𝑅)) | ||
Theorem | scandx 17130 | Index value of the df-sca 17084 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
⊢ (Scalar‘ndx) = 5 | ||
Theorem | scaid 17131 | Utility theorem: index-independent form of scalar df-sca 17084. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ Scalar = Slot (Scalar‘ndx) | ||
Theorem | scandxnbasendx 17132 | 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 17133 | The slot for the scalar field is not the slot for the group operation in an extensible structure. Formerly part of proof for mgpsca 19833. (Contributed by AV, 18-Oct-2024.) |
⊢ (Scalar‘ndx) ≠ (+g‘ndx) | ||
Theorem | scandxnmulrndx 17134 | 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 19833. (Contributed by AV, 29-Oct-2024.) |
⊢ (Scalar‘ndx) ≠ (.r‘ndx) | ||
Theorem | vscandx 17135 | Index value of the df-vsca 17085 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
⊢ ( ·𝑠 ‘ndx) = 6 | ||
Theorem | vscaid 17136 | Utility theorem: index-independent form of scalar product df-vsca 17085. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
⊢ ·𝑠 = Slot ( ·𝑠 ‘ndx) | ||
Theorem | vscandxnbasendx 17137 | The slot for the scalar product is not the slot for the base set in an extensible structure. Formerly part of proof for rmodislmod 20313. (Contributed by AV, 18-Oct-2024.) |
⊢ ( ·𝑠 ‘ndx) ≠ (Base‘ndx) | ||
Theorem | vscandxnplusgndx 17138 | The slot for the scalar product is not the slot for the group operation in an extensible structure. Formerly part of proof for rmodislmod 20313. (Contributed by AV, 18-Oct-2024.) |
⊢ ( ·𝑠 ‘ndx) ≠ (+g‘ndx) | ||
Theorem | vscandxnmulrndx 17139 | 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 20313. (Contributed by AV, 29-Oct-2024.) |
⊢ ( ·𝑠 ‘ndx) ≠ (.r‘ndx) | ||
Theorem | vscandxnscandx 17140 | The slot for the scalar product is not the slot for the scalar field in an extensible structure. Formerly part of proof for rmodislmod 20313. (Contributed by AV, 18-Oct-2024.) |
⊢ ( ·𝑠 ‘ndx) ≠ (Scalar‘ndx) | ||
Theorem | lmodstr 17141 | 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 17142 | 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 17143 | 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 17144 | 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 17145 | 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 17146 | Index value of the df-ip 17086 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
⊢ (·𝑖‘ndx) = 8 | ||
Theorem | ipid 17147 | Utility theorem: index-independent form of df-ip 17086. (Contributed by Mario Carneiro, 6-Oct-2013.) |
⊢ ·𝑖 = Slot (·𝑖‘ndx) | ||
Theorem | ipndxnbasendx 17148 | 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 17149 | 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 17150 | 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 19833. (Contributed by AV, 29-Oct-2024.) |
⊢ (·𝑖‘ndx) ≠ (.r‘ndx) | ||
Theorem | slotsdifipndx 17151 | The slot for the scalar is not the index of other slots. Formerly part of proof for srasca 20569 and sravsca 20571. (Contributed by AV, 12-Nov-2024.) |
⊢ (( ·𝑠 ‘ndx) ≠ (·𝑖‘ndx) ∧ (Scalar‘ndx) ≠ (·𝑖‘ndx)) | ||
Theorem | ipsstr 17152 | Lemma to shorten proofs of ipsbase 17153 through ipsvsca 17157. (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 17153 | 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 17154 | 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 17155 | 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 17156 | 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 17157 | 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 17158 | 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 17159 | Scalar is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐹 = (Scalar‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹 = (Scalar‘𝐻)) | ||
Theorem | ressvsca 17160 | ·𝑠 is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ · = ( ·𝑠 ‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘𝐻)) | ||
Theorem | ressip 17161 | The inner product is unaffected by restriction. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ , = (·𝑖‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → , = (·𝑖‘𝐻)) | ||
Theorem | phlstr 17162 | A constructed pre-Hilbert space is a structure. Starting from lmodstr 17141 (which has 4 members), we chain strleun 16964 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 17163 | 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 17164 | 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 17165 | 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 17166 | 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 17167 | 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 17168 | Index value of the df-tset 17087 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
⊢ (TopSet‘ndx) = 9 | ||
Theorem | tsetid 17169 | Utility theorem: index-independent form of df-tset 17087. (Contributed by NM, 20-Oct-2012.) |
⊢ TopSet = Slot (TopSet‘ndx) | ||
Theorem | tsetndxnn 17170 | 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 17171 | 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 17172 | 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 17173 | The slot for the topology is not the slot for the group operation in an extensible structure. Formerly part of proof for oppgtset 19064. (Contributed by AV, 18-Oct-2024.) |
⊢ (TopSet‘ndx) ≠ (+g‘ndx) | ||
Theorem | tsetndxnmulrndx 17174 | 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 | tsetndxnstarvndx 17175 | The slot for the topology is not the slot for the involution in an extensible structure. Formerly part of proof for cnfldfunALT 20732. (Contributed by AV, 11-Nov-2024.) |
⊢ (TopSet‘ndx) ≠ (*𝑟‘ndx) | ||
Theorem | slotstnscsi 17176 | The slots Scalar, ·𝑠 and ·𝑖 are different from the slot TopSet. Formerly part of sralem 20561 and proofs using it. (Contributed by AV, 29-Oct-2024.) |
⊢ ((TopSet‘ndx) ≠ (Scalar‘ndx) ∧ (TopSet‘ndx) ≠ ( ·𝑠 ‘ndx) ∧ (TopSet‘ndx) ≠ (·𝑖‘ndx)) | ||
Theorem | topgrpstr 17177 | 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 17178 | The base set of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝑊 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩} ⇒ ⊢ (𝐵 ∈ 𝑋 → 𝐵 = (Base‘𝑊)) | ||
Theorem | topgrpplusg 17179 | The additive operation of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝑊 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩} ⇒ ⊢ ( + ∈ 𝑋 → + = (+g‘𝑊)) | ||
Theorem | topgrptset 17180 | The topology of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝑊 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩} ⇒ ⊢ (𝐽 ∈ 𝑋 → 𝐽 = (TopSet‘𝑊)) | ||
Theorem | resstset 17181 | TopSet is unaffected by restriction. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝐽 = (TopSet‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐽 = (TopSet‘𝐻)) | ||
Theorem | plendx 17182 | Index value of the df-ple 17088 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.) (New usage is discouraged.) |
⊢ (le‘ndx) = ;10 | ||
Theorem | pleid 17183 | Utility theorem: self-referencing, index-independent form of df-ple 17088. (Contributed by NM, 9-Nov-2012.) (Revised by AV, 9-Sep-2021.) |
⊢ le = Slot (le‘ndx) | ||
Theorem | plendxnn 17184 | The index value of the order slot is a positive integer. This property should be ensured for every concrete coding because otherwise it could not be used in an extensible structure (slots must be positive integers). (Contributed by AV, 30-Oct-2024.) |
⊢ (le‘ndx) ∈ ℕ | ||
Theorem | basendxltplendx 17185 | The index value of the Base slot is less than the index value of the le slot. (Contributed by AV, 30-Oct-2024.) |
⊢ (Base‘ndx) < (le‘ndx) | ||
Theorem | plendxnbasendx 17186 | The slot for the order is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 30-Oct-2024.) |
⊢ (le‘ndx) ≠ (Base‘ndx) | ||
Theorem | plendxnplusgndx 17187 | The slot for the "less than or equal to" ordering is not the slot for the group operation in an extensible structure. Formerly part of proof for oppgle 31602. (Contributed by AV, 18-Oct-2024.) |
⊢ (le‘ndx) ≠ (+g‘ndx) | ||
Theorem | plendxnmulrndx 17188 | The slot for the "less than or equal to" ordering is not the slot for the ring multiplication operation in an extensible structure. Formerly part of proof for opsrmulr 21378. (Contributed by AV, 1-Nov-2024.) |
⊢ (le‘ndx) ≠ (.r‘ndx) | ||
Theorem | plendxnscandx 17189 | The slot for the "less than or equal to" ordering is not the slot for the scalar in an extensible structure. Formerly part of proof for opsrsca 21382. (Contributed by AV, 1-Nov-2024.) |
⊢ (le‘ndx) ≠ (Scalar‘ndx) | ||
Theorem | plendxnvscandx 17190 | The slot for the "less than or equal to" ordering is not the slot for the scalar product in an extensible structure. Formerly part of proof for opsrvsca 21380. (Contributed by AV, 1-Nov-2024.) |
⊢ (le‘ndx) ≠ ( ·𝑠 ‘ndx) | ||
Theorem | slotsdifplendx 17191 | The index of the slot for the distance is not the index of other slots. Formerly part of proof for cnfldfunALT 20732. (Contributed by AV, 11-Nov-2024.) |
⊢ ((*𝑟‘ndx) ≠ (le‘ndx) ∧ (TopSet‘ndx) ≠ (le‘ndx)) | ||
Theorem | otpsstr 17192 | 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 17193 | 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 17194 | 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 17195 | 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 17196 | le is unaffected by restriction. (Contributed by Mario Carneiro, 3-Nov-2015.) |
⊢ 𝑊 = (𝐾 ↾s 𝐴) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐴 ∈ 𝑉 → ≤ = (le‘𝑊)) | ||
Theorem | ocndx 17197 | Index value of the df-ocomp 17089 slot. (Contributed by Mario Carneiro, 25-Oct-2015.) (New usage is discouraged.) |
⊢ (oc‘ndx) = ;11 | ||
Theorem | ocid 17198 | Utility theorem: index-independent form of df-ocomp 17089. (Contributed by Mario Carneiro, 25-Oct-2015.) |
⊢ oc = Slot (oc‘ndx) | ||
Theorem | basendxnocndx 17199 | The slot for the orthocomplementation is not the slot for the base set in an extensible structure. Formerly part of proof for thlbas 21023. (Contributed by AV, 11-Nov-2024.) |
⊢ (Base‘ndx) ≠ (oc‘ndx) | ||
Theorem | plendxnocndx 17200 | The slot for the orthocomplementation is not the slot for the order in an extensible structure. Formerly part of proof for thlle 21025. (Contributed by AV, 11-Nov-2024.) |
⊢ (le‘ndx) ≠ (oc‘ndx) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |