P. 174 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 17301-17400   *Has distinct variable group(s)

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 11256 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 17348 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 17360 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 17365 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 17376 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 17398 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 17412 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 17427 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 17431 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 17441 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 17457 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 17459 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	basendxnplusgndxOLD 17328	Obsolete version of basendxnplusgndx 17327 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 17329	A constructed group is a structure on 1...2. Depending on hard-coded index values. Use grpstrndx 17330 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 17330	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 17331	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 17332	Obsolete version of grpbase 17331 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 17333	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 17334	Obsolete version of grpplusg 17333 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 17335	+g is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻))
Theorem	grpbasex 17336	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 17331 instead. (New usage is discouraged.) (Contributed by NM, 17-Oct-2012.)
⊢ 𝐵 ∈ V    &   ⊢ + ∈ V    &   ⊢ 𝐺 = {⟨1, 𝐵⟩, ⟨2, + ⟩}    ⇒   ⊢ 𝐵 = (Base‘𝐺)
Theorem	grpplusgx 17337	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 17333 instead. (New usage is discouraged.) (Contributed by NM, 17-Oct-2012.)
⊢ 𝐵 ∈ V    &   ⊢ + ∈ V    &   ⊢ 𝐺 = {⟨1, 𝐵⟩, ⟨2, + ⟩}    ⇒   ⊢ + = (+g‘𝐺)
Theorem	mulrndx 17338	Index value of the df-mulr 17311 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.)
⊢ (.r‘ndx) = 3
Theorem	mulridx 17339	Utility theorem: index-independent form of df-mulr 17311. (Contributed by Mario Carneiro, 8-Jun-2013.)
⊢ .r = Slot (.r‘ndx)
Theorem	basendxnmulrndx 17340	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 17341	Obsolete version of basendxnmulrndx 17340 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 17342	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 17343	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 17344	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 17345	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 17346	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 17347	Index value of the df-starv 17312 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.)
⊢ (*𝑟‘ndx) = 4
Theorem	starvid 17348	Utility theorem: index-independent form of df-starv 17312. (Contributed by Mario Carneiro, 6-Oct-2013.)
⊢ *𝑟 = Slot (*𝑟‘ndx)
Theorem	starvndxnbasendx 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 17353. (Contributed by AV, 18-Oct-2024.)
⊢ (*𝑟‘ndx) ≠ (Base‘ndx)
Theorem	starvndxnplusgndx 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 17353. (Contributed by AV, 18-Oct-2024.)
⊢ (*𝑟‘ndx) ≠ (+g‘ndx)
Theorem	starvndxnmulrndx 17351	The slot for the involution function is not the slot for the base set in an extensible structure. Formerly part of proof for ressstarv 17353. (Contributed by AV, 18-Oct-2024.)
⊢ (*𝑟‘ndx) ≠ (.r‘ndx)
Theorem	ressmulr 17352	.r is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝑆))
Theorem	ressstarv 17353	*𝑟 is unaffected by restriction. (Contributed by Mario Carneiro, 9-Oct-2015.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ ∗ = (*𝑟‘𝑅)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ∗ = (*𝑟‘𝑆))
Theorem	srngstr 17354	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 17355	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 17356	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 17357	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 17358	The involution function of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑅 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗ ⟩})    ⇒   ⊢ ( ∗ ∈ 𝑋 → ∗ = (*𝑟‘𝑅))
Theorem	scandx 17359	Index value of the df-sca 17313 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.)
⊢ (Scalar‘ndx) = 5
Theorem	scaid 17360	Utility theorem: index-independent form of scalar df-sca 17313. (Contributed by Mario Carneiro, 19-Jun-2014.)
⊢ Scalar = Slot (Scalar‘ndx)
Theorem	scandxnbasendx 17361	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 17362	The slot for the scalar field is not the slot for the group operation in an extensible structure. Formerly part of proof for mgpsca 20159. (Contributed by AV, 18-Oct-2024.)
⊢ (Scalar‘ndx) ≠ (+g‘ndx)
Theorem	scandxnmulrndx 17363	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 20159. (Contributed by AV, 29-Oct-2024.)
⊢ (Scalar‘ndx) ≠ (.r‘ndx)
Theorem	vscandx 17364	Index value of the df-vsca 17314 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.)
⊢ ( ·𝑠 ‘ndx) = 6
Theorem	vscaid 17365	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 17366	The slot for the scalar product is not the slot for the base set in an extensible structure. Formerly part of proof for rmodislmod 20944. (Contributed by AV, 18-Oct-2024.)
⊢ ( ·𝑠 ‘ndx) ≠ (Base‘ndx)
Theorem	vscandxnplusgndx 17367	The slot for the scalar product is not the slot for the group operation in an extensible structure. Formerly part of proof for rmodislmod 20944. (Contributed by AV, 18-Oct-2024.)
⊢ ( ·𝑠 ‘ndx) ≠ (+g‘ndx)
Theorem	vscandxnmulrndx 17368	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 20944. (Contributed by AV, 29-Oct-2024.)
⊢ ( ·𝑠 ‘ndx) ≠ (.r‘ndx)
Theorem	vscandxnscandx 17369	The slot for the scalar product is not the slot for the scalar field in an extensible structure. Formerly part of proof for rmodislmod 20944. (Contributed by AV, 18-Oct-2024.)
⊢ ( ·𝑠 ‘ndx) ≠ (Scalar‘ndx)
Theorem	lmodstr 17370	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 17371	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 17372	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 17373	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 17374	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 17375	Index value of the df-ip 17315 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.)
⊢ (·𝑖‘ndx) = 8
Theorem	ipid 17376	Utility theorem: index-independent form of df-ip 17315. (Contributed by Mario Carneiro, 6-Oct-2013.)
⊢ ·𝑖 = Slot (·𝑖‘ndx)
Theorem	ipndxnbasendx 17377	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 17378	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 17379	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 20159. (Contributed by AV, 29-Oct-2024.)
⊢ (·𝑖‘ndx) ≠ (.r‘ndx)
Theorem	slotsdifipndx 17380	The slot for the scalar is not the index of other slots. Formerly part of proof for srasca 21200 and sravsca 21202. (Contributed by AV, 12-Nov-2024.)
⊢ (( ·𝑠 ‘ndx) ≠ (·𝑖‘ndx) ∧ (Scalar‘ndx) ≠ (·𝑖‘ndx))
Theorem	ipsstr 17381	Lemma to shorten proofs of ipsbase 17382 through ipsvsca 17386. (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 17382	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 17383	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 17384	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 17385	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 17386	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 17387	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 17388	Scalar is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝐹 = (Scalar‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐹 = (Scalar‘𝐻))
Theorem	ressvsca 17389	·𝑠 is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘𝐻))
Theorem	ressip 17390	The inner product is unaffected by restriction. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ , = (·𝑖‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → , = (·𝑖‘𝐻))
Theorem	phlstr 17391	A constructed pre-Hilbert space is a structure. Starting from lmodstr 17370 (which has 4 members), we chain strleun 17190 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 17392	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 17393	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 17394	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 17395	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 17396	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 17397	Index value of the df-tset 17316 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.)
⊢ (TopSet‘ndx) = 9
Theorem	tsetid 17398	Utility theorem: index-independent form of df-tset 17316. (Contributed by NM, 20-Oct-2012.)
⊢ TopSet = Slot (TopSet‘ndx)
Theorem	tsetndxnn 17399	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 17400	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)