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
Definition	df-ress 17201*	Define a multifunction restriction operator for extensible structures, which can be used to turn statements about rings into statements about subrings, modules into submodules, etc. This definition knows nothing about individual structures and merely truncates the Base set while leaving operators alone; individual kinds of structures will need to handle this behavior, by ignoring operators' values outside the range (like Ring), defining a function using the base set and applying that (like TopGrp), or explicitly truncating the slot before use (like MetSp). (Credit for this operator goes to Mario Carneiro.) See ressbas 17206 for the altered base set, and resseqnbas 17212 (subrg0 20488, ressplusg 17254, subrg1 20491, ressmulr 17270) for the (un)altered other operations. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ ↾s = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩)))
Theorem	reldmress 17202	The structure restriction is a proper operator, so it can be used with ovprc1 7426. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ Rel dom ↾s
Theorem	ressval 17203	Value of structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet ⟨(Base‘ndx), (𝐴 ∩ 𝐵)⟩)))
Theorem	ressid2 17204	General behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊)
Theorem	ressval2 17205	Value of nontrivial structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet ⟨(Base‘ndx), (𝐴 ∩ 𝐵)⟩))
Theorem	ressbas 17206	Base set of a structure restriction. (Contributed by Stefan O'Rear, 26-Nov-2014.) (Proof shortened by AV, 7-Nov-2024.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) = (Base‘𝑅))
Theorem	ressbasssg 17207	The base set of a restriction to 𝐴 is a subset of 𝐴 and the base set 𝐵 of the original structure. (Contributed by SN, 10-Jan-2025.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ (Base‘𝑅) ⊆ (𝐴 ∩ 𝐵)
Theorem	ressbas2 17208	Base set of a structure restriction. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘𝑅))
Theorem	ressbasss 17209	The base set of a restriction is a subset of the base set of the original structure. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) (Proof shortened by SN, 25-Feb-2025.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ (Base‘𝑅) ⊆ 𝐵
Theorem	ressbasssOLD 17210	Obsolete version of ressbas 17206 as of 25-Feb-2025. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ (Base‘𝑅) ⊆ 𝐵
Theorem	ressbasss2 17211	The base set of a restriction to 𝐴 is a subset of 𝐴. (Contributed by SN, 10-Jan-2025.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    ⇒   ⊢ (Base‘𝑅) ⊆ 𝐴
Theorem	resseqnbas 17212	The components of an extensible structure except the base set remain unchanged on a structure restriction. (Contributed by Mario Carneiro, 26-Nov-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) (Revised by AV, 19-Oct-2024.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐶 = (𝐸‘𝑊)    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (Base‘ndx)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐶 = (𝐸‘𝑅))
Theorem	ress0 17213	All restrictions of the null set are trivial. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ (∅ ↾s 𝐴) = ∅
Theorem	ressid 17214	Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑋 → (𝑊 ↾s 𝐵) = 𝑊)
Theorem	ressinbas 17215	Restriction only cares about the part of the second set which intersects the base of the first. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ (𝐴 ∈ 𝑋 → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ 𝐵)))
Theorem	ressval3d 17216	Value of structure restriction, deduction version. (Contributed by AV, 14-Mar-2020.) (Revised by AV, 3-Jul-2022.) (Proof shortened by AV, 17-Oct-2024.)
⊢ 𝑅 = (𝑆 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐸 = (Base‘ndx)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → Fun 𝑆)    &   ⊢ (𝜑 → 𝐸 ∈ dom 𝑆)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝑅 = (𝑆 sSet ⟨𝐸, 𝐴⟩))
Theorem	ressress 17217	Restriction composition law. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Proof shortened by Mario Carneiro, 2-Dec-2014.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵)))
Theorem	ressabs 17218	Restriction absorption law. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐵))
Theorem	wunress 17219	Closure of structure restriction in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 28-Oct-2024.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑊 ↾s 𝐴) ∈ 𝑈)
7.1.2  Slot definitions
Syntax	cplusg 17220	Extend class notation with group (addition) operation.
class +g
Syntax	cmulr 17221	Extend class notation with ring multiplication.
class .r
Syntax	cstv 17222	Extend class notation with involution.
class *𝑟
Syntax	csca 17223	Extend class notation with scalar field.
class Scalar
Syntax	cvsca 17224	Extend class notation with scalar product.
class ·𝑠
Syntax	cip 17225	Extend class notation with Hermitian form (inner product).
class ·𝑖
Syntax	cts 17226	Extend class notation with the topology component of a topological space.
class TopSet
Syntax	cple 17227	Extend class notation with "less than or equal to" for posets.
class le
Syntax	coc 17228	Extend class notation with the class of orthocomplementation extractors.
class oc
Syntax	cds 17229	Extend class notation with the metric space distance function.
class dist
Syntax	cunif 17230	Extend class notation with the uniform structure.
class UnifSet
Syntax	chom 17231	Extend class notation with the hom-set structure.
class Hom
Syntax	cco 17232	Extend class notation with the composition operation.
class comp
Definition	df-plusg 17233	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 17247 instead. (New usage is discouraged.)
⊢ +g = Slot 2
Definition	df-mulr 17234	Define ring multiplication. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form mulrid 11172 instead. (New usage is discouraged.)
⊢ .r = Slot 3
Definition	df-starv 17235	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 17266 instead. (New usage is discouraged.)
⊢ *𝑟 = Slot 4
Definition	df-sca 17236	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 17278 instead. (New usage is discouraged.)
⊢ Scalar = Slot 5
Definition	df-vsca 17237	Define scalar product. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form vscaid 17283 instead. (New usage is discouraged.)
⊢ ·𝑠 = Slot 6
Definition	df-ip 17238	Define Hermitian form (inner product). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form ipid 17294 instead. (New usage is discouraged.)
⊢ ·𝑖 = Slot 8
Definition	df-tset 17239	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 17316 instead. (New usage is discouraged.)
⊢ TopSet = Slot 9
Definition	df-ple 17240	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 17330 instead. (New usage is discouraged.)
⊢ le = Slot ;10
Definition	df-ocomp 17241	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 17345 instead. (New usage is discouraged.)
⊢ oc = Slot ;11
Definition	df-ds 17242	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 17349 instead. (New usage is discouraged.)
⊢ dist = Slot ;12
Definition	df-unif 17243	Define the uniform structure component of a uniform space. (Contributed by Mario Carneiro, 14-Aug-2015.) Use its index-independent form unifid 17359 instead. (New usage is discouraged.)
⊢ UnifSet = Slot ;13
Definition	df-hom 17244	Define the hom-set component of a category. (Contributed by Mario Carneiro, 2-Jan-2017.) Use its index-independent form homid 17375 instead. (New usage is discouraged.)
⊢ Hom = Slot ;14
Definition	df-cco 17245	Define the composition operation of a category. (Contributed by Mario Carneiro, 2-Jan-2017.) Use its index-independent form ccoid 17377 instead. (New usage is discouraged.)
⊢ comp = Slot ;15
Theorem	plusgndx 17246	Index value of the df-plusg 17233 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.)
⊢ (+g‘ndx) = 2
Theorem	plusgid 17247	Utility theorem: index-independent form of df-plusg 17233. (Contributed by NM, 20-Oct-2012.)
⊢ +g = Slot (+g‘ndx)
Theorem	plusgndxnn 17248	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 17249	The index of the slot for the base set is less than 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 17250	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 17251	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 17252	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	grpplusg 17253	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	ressplusg 17254	+g is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻))
Theorem	grpbasex 17255	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 17252 instead. (New usage is discouraged.) (Contributed by NM, 17-Oct-2012.)
⊢ 𝐵 ∈ V    &   ⊢ + ∈ V    &   ⊢ 𝐺 = {⟨1, 𝐵⟩, ⟨2, + ⟩}    ⇒   ⊢ 𝐵 = (Base‘𝐺)
Theorem	grpplusgx 17256	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 17253 instead. (New usage is discouraged.) (Contributed by NM, 17-Oct-2012.)
⊢ 𝐵 ∈ V    &   ⊢ + ∈ V    &   ⊢ 𝐺 = {⟨1, 𝐵⟩, ⟨2, + ⟩}    ⇒   ⊢ + = (+g‘𝐺)
Theorem	mulrndx 17257	Index value of the df-mulr 17234 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.)
⊢ (.r‘ndx) = 3
Theorem	mulridx 17258	Utility theorem: index-independent form of df-mulr 17234. (Contributed by Mario Carneiro, 8-Jun-2013.)
⊢ .r = Slot (.r‘ndx)
Theorem	basendxnmulrndx 17259	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	plusgndxnmulrndx 17260	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 17261	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 17262	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 17263	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 17264	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 17265	Index value of the df-starv 17235 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.)
⊢ (*𝑟‘ndx) = 4
Theorem	starvid 17266	Utility theorem: index-independent form of df-starv 17235. (Contributed by Mario Carneiro, 6-Oct-2013.)
⊢ *𝑟 = Slot (*𝑟‘ndx)
Theorem	starvndxnbasendx 17267	The slot for the involution function is not the slot for the base set in an extensible structure. Formerly part of proof for ressstarv 17271. (Contributed by AV, 18-Oct-2024.)
⊢ (*𝑟‘ndx) ≠ (Base‘ndx)
Theorem	starvndxnplusgndx 17268	The slot for the involution function is not the slot for the base set in an extensible structure. Formerly part of proof for ressstarv 17271. (Contributed by AV, 18-Oct-2024.)
⊢ (*𝑟‘ndx) ≠ (+g‘ndx)
Theorem	starvndxnmulrndx 17269	The slot for the involution function is not the slot for the base set in an extensible structure. Formerly part of proof for ressstarv 17271. (Contributed by AV, 18-Oct-2024.)
⊢ (*𝑟‘ndx) ≠ (.r‘ndx)
Theorem	ressmulr 17270	.r is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝑆))
Theorem	ressstarv 17271	*𝑟 is unaffected by restriction. (Contributed by Mario Carneiro, 9-Oct-2015.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ ∗ = (*𝑟‘𝑅)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ∗ = (*𝑟‘𝑆))
Theorem	srngstr 17272	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 17273	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 17274	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 17275	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 17276	The involution function of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑅 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗ ⟩})    ⇒   ⊢ ( ∗ ∈ 𝑋 → ∗ = (*𝑟‘𝑅))
Theorem	scandx 17277	Index value of the df-sca 17236 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.)
⊢ (Scalar‘ndx) = 5
Theorem	scaid 17278	Utility theorem: index-independent form of scalar df-sca 17236. (Contributed by Mario Carneiro, 19-Jun-2014.)
⊢ Scalar = Slot (Scalar‘ndx)
Theorem	scandxnbasendx 17279	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 17280	The slot for the scalar field is not the slot for the group operation in an extensible structure. Formerly part of proof for mgpsca 20055. (Contributed by AV, 18-Oct-2024.)
⊢ (Scalar‘ndx) ≠ (+g‘ndx)
Theorem	scandxnmulrndx 17281	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 20055. (Contributed by AV, 29-Oct-2024.)
⊢ (Scalar‘ndx) ≠ (.r‘ndx)
Theorem	vscandx 17282	Index value of the df-vsca 17237 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.)
⊢ ( ·𝑠 ‘ndx) = 6
Theorem	vscaid 17283	Utility theorem: index-independent form of scalar product df-vsca 17237. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ ·𝑠 = Slot ( ·𝑠 ‘ndx)
Theorem	vscandxnbasendx 17284	The slot for the scalar product is not the slot for the base set in an extensible structure. Formerly part of proof for rmodislmod 20836. (Contributed by AV, 18-Oct-2024.)
⊢ ( ·𝑠 ‘ndx) ≠ (Base‘ndx)
Theorem	vscandxnplusgndx 17285	The slot for the scalar product is not the slot for the group operation in an extensible structure. Formerly part of proof for rmodislmod 20836. (Contributed by AV, 18-Oct-2024.)
⊢ ( ·𝑠 ‘ndx) ≠ (+g‘ndx)
Theorem	vscandxnmulrndx 17286	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 20836. (Contributed by AV, 29-Oct-2024.)
⊢ ( ·𝑠 ‘ndx) ≠ (.r‘ndx)
Theorem	vscandxnscandx 17287	The slot for the scalar product is not the slot for the scalar field in an extensible structure. Formerly part of proof for rmodislmod 20836. (Contributed by AV, 18-Oct-2024.)
⊢ ( ·𝑠 ‘ndx) ≠ (Scalar‘ndx)
Theorem	lmodstr 17288	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 17289	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 17290	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 17291	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 17292	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 17293	Index value of the df-ip 17238 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.)
⊢ (·𝑖‘ndx) = 8
Theorem	ipid 17294	Utility theorem: index-independent form of df-ip 17238. (Contributed by Mario Carneiro, 6-Oct-2013.)
⊢ ·𝑖 = Slot (·𝑖‘ndx)
Theorem	ipndxnbasendx 17295	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 17296	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 17297	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 20055. (Contributed by AV, 29-Oct-2024.)
⊢ (·𝑖‘ndx) ≠ (.r‘ndx)
Theorem	slotsdifipndx 17298	The slot for the scalar is not the index of other slots. Formerly part of proof for srasca 21087 and sravsca 21088. (Contributed by AV, 12-Nov-2024.)
⊢ (( ·𝑠 ‘ndx) ≠ (·𝑖‘ndx) ∧ (Scalar‘ndx) ≠ (·𝑖‘ndx))
Theorem	ipsstr 17299	Lemma to shorten proofs of ipsbase 17300 through ipsvsca 17304. (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 17300	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‘𝐴))