P. 173 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 17201-17300   *Has distinct variable group(s)

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