P. 134 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13301-13400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ressbasd 13301	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	ressbas2d 13302	Base set of a structure restriction. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ (𝜑 → 𝑅 = (𝑊 ↾s 𝐴))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = (Base‘𝑅))
Theorem	ressbasssd 13303	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.)
⊢ (𝜑 → 𝑅 = (𝑊 ↾s 𝐴))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (Base‘𝑅) ⊆ 𝐵)
Theorem	ressbasid 13304	The trivial structure restriction leaves the base set unchanged. (Contributed by Jim Kingdon, 29-Apr-2025.)
⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑉 → (Base‘(𝑊 ↾s 𝐵)) = 𝐵)
Theorem	strressid 13305	Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Revised by Jim Kingdon, 17-Jan-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝑊))    &   ⊢ (𝜑 → 𝑊 Struct ⟨𝑀, 𝑁⟩)    &   ⊢ (𝜑 → Fun 𝑊)    &   ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝑊)    ⇒   ⊢ (𝜑 → (𝑊 ↾s 𝐵) = 𝑊)
Theorem	ressval3d 13306	Value of structure restriction, deduction version. (Contributed by AV, 14-Mar-2020.) (Revised by Jim Kingdon, 17-Jan-2025.)
⊢ 𝑅 = (𝑆 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐸 = (Base‘ndx)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → Fun 𝑆)    &   ⊢ (𝜑 → 𝐸 ∈ dom 𝑆)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝑅 = (𝑆 sSet ⟨𝐸, 𝐴⟩))
Theorem	resseqnbasd 13307	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) ∈ ℕ)    &   ⊢ (𝐸‘ndx) ≠ (Base‘ndx)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐶 = (𝐸‘𝑅))
Theorem	ressinbasd 13308	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	ressressg 13309	Restriction composition law. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Proof shortened by Mario Carneiro, 2-Dec-2014.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑊 ∈ 𝑍) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵)))
Theorem	ressabsg 13310	Restriction absorption law. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐵))
6.1.2  Slot definitions
Syntax	cplusg 13311	Extend class notation with group (addition) operation.
class +g
Syntax	cmulr 13312	Extend class notation with ring multiplication.
class .r
Syntax	cstv 13313	Extend class notation with involution.
class *𝑟
Syntax	csca 13314	Extend class notation with scalar field.
class Scalar
Syntax	cvsca 13315	Extend class notation with scalar product.
class ·𝑠
Syntax	cip 13316	Extend class notation with Hermitian form (inner product).
class ·𝑖
Syntax	cts 13317	Extend class notation with the topology component of a topological space.
class TopSet
Syntax	cple 13318	Extend class notation with "less than or equal to" for posets.
class le
Syntax	coc 13319	Extend class notation with the class of orthocomplementation extractors.
class oc
Syntax	cds 13320	Extend class notation with the metric space distance function.
class dist
Syntax	cunif 13321	Extend class notation with the uniform structure.
class UnifSet
Syntax	chom 13322	Extend class notation with the hom-set structure.
class Hom
Syntax	cco 13323	Extend class notation with the composition operation.
class comp
Definition	df-plusg 13324	Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ +g = Slot 2
Definition	df-mulr 13325	Define ring multiplication. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ .r = Slot 3
Definition	df-starv 13326	Define the involution function of a *-ring. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ *𝑟 = Slot 4
Definition	df-sca 13327	Define scalar field component of a vector space 𝑣. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ Scalar = Slot 5
Definition	df-vsca 13328	Define scalar product. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ ·𝑠 = Slot 6
Definition	df-ip 13329	Define Hermitian form (inner product). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ ·𝑖 = Slot 8
Definition	df-tset 13330	Define the topology component of a topological space (structure). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ TopSet = Slot 9
Definition	df-ple 13331	Define "less than or equal to" ordering extractor for posets and related structures. We use ;10 for the index to avoid conflict with 1 through 9 used for other purposes. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.)
⊢ le = Slot ;10
Definition	df-ocomp 13332	Define the orthocomplementation extractor for posets and related structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ oc = Slot ;11
Definition	df-ds 13333	Define the distance function component of a metric space (structure). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ dist = Slot ;12
Definition	df-unif 13334	Define the uniform structure component of a uniform space. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ UnifSet = Slot ;13
Definition	df-hom 13335	Define the hom-set component of a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ Hom = Slot ;14
Definition	df-cco 13336	Define the composition operation of a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ comp = Slot ;15
Theorem	strleund 13337	Combine two structures into one. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
⊢ (𝜑 → 𝐹 Struct ⟨𝐴, 𝐵⟩)    &   ⊢ (𝜑 → 𝐺 Struct ⟨𝐶, 𝐷⟩)    &   ⊢ (𝜑 → 𝐵 < 𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∪ 𝐺) Struct ⟨𝐴, 𝐷⟩)
Theorem	strleun 13338	Combine two structures into one. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐹 Struct ⟨𝐴, 𝐵⟩    &   ⊢ 𝐺 Struct ⟨𝐶, 𝐷⟩    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ (𝐹 ∪ 𝐺) Struct ⟨𝐴, 𝐷⟩
Theorem	strext 13339	Extending the upper range of a structure. This works because when we say that a structure has components in 𝐴...𝐶 we are not saying that every slot in that range is present, just that all the slots that are present are within that range. (Contributed by Jim Kingdon, 26-Feb-2025.)
⊢ (𝜑 → 𝐹 Struct ⟨𝐴, 𝐵⟩)    &   ⊢ (𝜑 → 𝐶 ∈ (ℤ≥‘𝐵))    ⇒   ⊢ (𝜑 → 𝐹 Struct ⟨𝐴, 𝐶⟩)
Theorem	strle1g 13340	Make a structure from a singleton. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
⊢ 𝐼 ∈ ℕ    &   ⊢ 𝐴 = 𝐼    ⇒   ⊢ (𝑋 ∈ 𝑉 → {⟨𝐴, 𝑋⟩} Struct ⟨𝐼, 𝐼⟩)
Theorem	strle2g 13341	Make a structure from a pair. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
⊢ 𝐼 ∈ ℕ    &   ⊢ 𝐴 = 𝐼    &   ⊢ 𝐼 < 𝐽    &   ⊢ 𝐽 ∈ ℕ    &   ⊢ 𝐵 = 𝐽    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → {⟨𝐴, 𝑋⟩, ⟨𝐵, 𝑌⟩} Struct ⟨𝐼, 𝐽⟩)
Theorem	strle3g 13342	Make a structure from a triple. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐼 ∈ ℕ    &   ⊢ 𝐴 = 𝐼    &   ⊢ 𝐼 < 𝐽    &   ⊢ 𝐽 ∈ ℕ    &   ⊢ 𝐵 = 𝐽    &   ⊢ 𝐽 < 𝐾    &   ⊢ 𝐾 ∈ ℕ    &   ⊢ 𝐶 = 𝐾    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑃) → {⟨𝐴, 𝑋⟩, ⟨𝐵, 𝑌⟩, ⟨𝐶, 𝑍⟩} Struct ⟨𝐼, 𝐾⟩)
Theorem	plusgndx 13343	Index value of the df-plusg 13324 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (+g‘ndx) = 2
Theorem	plusgid 13344	Utility theorem: index-independent form of df-plusg 13324. (Contributed by NM, 20-Oct-2012.)
⊢ +g = Slot (+g‘ndx)
Theorem	plusgndxnn 13345	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	plusgslid 13346	Slot property of +g. (Contributed by Jim Kingdon, 3-Feb-2023.)
⊢ (+g = Slot (+g‘ndx) ∧ (+g‘ndx) ∈ ℕ)
Theorem	basendxltplusgndx 13347	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	opelstrsl 13348	The slot of a structure which contains an ordered pair for that slot. (Contributed by Jim Kingdon, 5-Feb-2023.)
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 Struct 𝑋)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑌)    &   ⊢ (𝜑 → ⟨(𝐸‘ndx), 𝑉⟩ ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝑉 = (𝐸‘𝑆))
Theorem	opelstrbas 13349	The base set of a structure with a base set. (Contributed by AV, 10-Nov-2021.)
⊢ (𝜑 → 𝑆 Struct 𝑋)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑌)    &   ⊢ (𝜑 → ⟨(Base‘ndx), 𝑉⟩ ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝑉 = (Base‘𝑆))
Theorem	1strstrg 13350	A constructed one-slot structure. (Contributed by AV, 27-Mar-2020.) (Revised by Jim Kingdon, 28-Jan-2023.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩}    ⇒   ⊢ (𝐵 ∈ 𝑉 → 𝐺 Struct ⟨1, 1⟩)
Theorem	1strbas 13351	The base set of a constructed one-slot structure. (Contributed by AV, 27-Mar-2020.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩}    ⇒   ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐺))
Theorem	2strstrndx 13352	A constructed two-slot structure not depending on the hard-coded index value of the base set. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 14-Dec-2025.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨𝑁, + ⟩}    &   ⊢ (Base‘ndx) < 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐺 Struct ⟨(Base‘ndx), 𝑁⟩)
Theorem	2strstrg 13353	A constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.) Use 2strstrndx 13352 instead. (New usage is discouraged.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(𝐸‘ndx), + ⟩}    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 1 < 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐺 Struct ⟨1, 𝑁⟩)
Theorem	2strbasg 13354	The base set of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(𝐸‘ndx), + ⟩}    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 1 < 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐵 = (Base‘𝐺))
Theorem	2stropg 13355	The other slot of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(𝐸‘ndx), + ⟩}    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 1 < 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → + = (𝐸‘𝐺))
Theorem	2strstr1g 13356	A constructed two-slot structure. Version of 2strstrg 13353 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 2-Feb-2023.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨𝑁, + ⟩}    &   ⊢ (Base‘ndx) < 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐺 Struct ⟨(Base‘ndx), 𝑁⟩)
Theorem	2strbas1g 13357	The base set of a constructed two-slot structure. Version of 2strbasg 13354 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 2-Feb-2023.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨𝑁, + ⟩}    &   ⊢ (Base‘ndx) < 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐵 = (Base‘𝐺))
Theorem	2strop1g 13358	The other slot of a constructed two-slot structure. Version of 2stropg 13355 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 2-Feb-2023.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨𝑁, + ⟩}    &   ⊢ (Base‘ndx) < 𝑁    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐸 = Slot 𝑁    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → + = (𝐸‘𝐺))
Theorem	basendxnplusgndx 13359	The slot for the base set is not the slot for the group operation in an extensible structure. (Contributed by AV, 14-Nov-2021.)
⊢ (Base‘ndx) ≠ (+g‘ndx)
Theorem	grpstrg 13360	A constructed group is a structure on 1...2. (Contributed by Mario Carneiro, 28-Sep-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩}    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐺 Struct ⟨1, 2⟩)
Theorem	grpbaseg 13361	The base set of a constructed group. (Contributed by Mario Carneiro, 2-Aug-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩}    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐵 = (Base‘𝐺))
Theorem	grpplusgg 13362	The operation of a constructed group. (Contributed by Mario Carneiro, 2-Aug-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩}    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → + = (+g‘𝐺))
Theorem	ressplusgd 13363	+g is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ (𝜑 → 𝐻 = (𝐺 ↾s 𝐴))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    ⇒   ⊢ (𝜑 → + = (+g‘𝐻))
Theorem	mulrndx 13364	Index value of the df-mulr 13325 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (.r‘ndx) = 3
Theorem	mulridx 13365	Utility theorem: index-independent form of df-mulr 13325. (Contributed by Mario Carneiro, 8-Jun-2013.)
⊢ .r = Slot (.r‘ndx)
Theorem	mulrslid 13366	Slot property of .r. (Contributed by Jim Kingdon, 3-Feb-2023.)
⊢ (.r = Slot (.r‘ndx) ∧ (.r‘ndx) ∈ ℕ)
Theorem	plusgndxnmulrndx 13367	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	basendxnmulrndx 13368	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.)
⊢ (Base‘ndx) ≠ (.r‘ndx)
Theorem	rngstrg 13369	A constructed ring is a structure. (Contributed by Mario Carneiro, 28-Sep-2013.) (Revised by Jim Kingdon, 3-Feb-2023.)
⊢ 𝑅 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊 ∧ · ∈ 𝑋) → 𝑅 Struct ⟨1, 3⟩)
Theorem	rngbaseg 13370	The base set of a constructed ring. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 3-Feb-2023.)
⊢ 𝑅 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩}    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊 ∧ · ∈ 𝑋) → 𝐵 = (Base‘𝑅))
Theorem	rngplusgg 13371	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	rngmulrg 13372	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 13373	Index value of the df-starv 13326 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (*𝑟‘ndx) = 4
Theorem	starvid 13374	Utility theorem: index-independent form of df-starv 13326. (Contributed by Mario Carneiro, 6-Oct-2013.)
⊢ *𝑟 = Slot (*𝑟‘ndx)
Theorem	starvslid 13375	Slot property of *𝑟. (Contributed by Jim Kingdon, 4-Feb-2023.)
⊢ (*𝑟 = Slot (*𝑟‘ndx) ∧ (*𝑟‘ndx) ∈ ℕ)
Theorem	starvndxnbasendx 13376	The slot for the involution function is not the slot for the base set in an extensible structure. (Contributed by AV, 18-Oct-2024.)
⊢ (*𝑟‘ndx) ≠ (Base‘ndx)
Theorem	starvndxnplusgndx 13377	The slot for the involution function is not the slot for the base set in an extensible structure. (Contributed by AV, 18-Oct-2024.)
⊢ (*𝑟‘ndx) ≠ (+g‘ndx)
Theorem	starvndxnmulrndx 13378	The slot for the involution function is not the slot for the base set in an extensible structure. (Contributed by AV, 18-Oct-2024.)
⊢ (*𝑟‘ndx) ≠ (.r‘ndx)
Theorem	ressmulrg 13379	.r is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → · = (.r‘𝑆))
Theorem	srngstrd 13380	A constructed star ring is a structure. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Jim Kingdon, 5-Feb-2023.)
⊢ 𝑅 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗ ⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → · ∈ 𝑋)    &   ⊢ (𝜑 → ∗ ∈ 𝑌)    ⇒   ⊢ (𝜑 → 𝑅 Struct ⟨1, 4⟩)
Theorem	srngbased 13381	The base set of a constructed star ring. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Jim Kingdon, 5-Feb-2023.)
⊢ 𝑅 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗ ⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → · ∈ 𝑋)    &   ⊢ (𝜑 → ∗ ∈ 𝑌)    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝑅))
Theorem	srngplusgd 13382	The addition operation of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.) (Revised by Jim Kingdon, 5-Feb-2023.)
⊢ 𝑅 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗ ⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → · ∈ 𝑋)    &   ⊢ (𝜑 → ∗ ∈ 𝑌)    ⇒   ⊢ (𝜑 → + = (+g‘𝑅))
Theorem	srngmulrd 13383	The multiplication operation of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑅 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗ ⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → · ∈ 𝑋)    &   ⊢ (𝜑 → ∗ ∈ 𝑌)    ⇒   ⊢ (𝜑 → · = (.r‘𝑅))
Theorem	srnginvld 13384	The involution function of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑅 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(*𝑟‘ndx), ∗ ⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → · ∈ 𝑋)    &   ⊢ (𝜑 → ∗ ∈ 𝑌)    ⇒   ⊢ (𝜑 → ∗ = (*𝑟‘𝑅))
Theorem	scandx 13385	Index value of the df-sca 13327 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (Scalar‘ndx) = 5
Theorem	scaid 13386	Utility theorem: index-independent form of scalar df-sca 13327. (Contributed by Mario Carneiro, 19-Jun-2014.)
⊢ Scalar = Slot (Scalar‘ndx)
Theorem	scaslid 13387	Slot property of Scalar. (Contributed by Jim Kingdon, 5-Feb-2023.)
⊢ (Scalar = Slot (Scalar‘ndx) ∧ (Scalar‘ndx) ∈ ℕ)
Theorem	scandxnbasendx 13388	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 13389	The slot for the scalar field is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.)
⊢ (Scalar‘ndx) ≠ (+g‘ndx)
Theorem	scandxnmulrndx 13390	The slot for the scalar field is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 29-Oct-2024.)
⊢ (Scalar‘ndx) ≠ (.r‘ndx)
Theorem	vscandx 13391	Index value of the df-vsca 13328 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ ( ·𝑠 ‘ndx) = 6
Theorem	vscaid 13392	Utility theorem: index-independent form of scalar product df-vsca 13328. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
⊢ ·𝑠 = Slot ( ·𝑠 ‘ndx)
Theorem	vscandxnbasendx 13393	The slot for the scalar product is not the slot for the base set in an extensible structure. (Contributed by AV, 18-Oct-2024.)
⊢ ( ·𝑠 ‘ndx) ≠ (Base‘ndx)
Theorem	vscandxnplusgndx 13394	The slot for the scalar product is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.)
⊢ ( ·𝑠 ‘ndx) ≠ (+g‘ndx)
Theorem	vscandxnmulrndx 13395	The slot for the scalar product is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 29-Oct-2024.)
⊢ ( ·𝑠 ‘ndx) ≠ (.r‘ndx)
Theorem	vscandxnscandx 13396	The slot for the scalar product is not the slot for the scalar field in an extensible structure. (Contributed by AV, 18-Oct-2024.)
⊢ ( ·𝑠 ‘ndx) ≠ (Scalar‘ndx)
Theorem	vscaslid 13397	Slot property of ·𝑠. (Contributed by Jim Kingdon, 5-Feb-2023.)
⊢ ( ·𝑠 = Slot ( ·𝑠 ‘ndx) ∧ ( ·𝑠 ‘ndx) ∈ ℕ)
Theorem	lmodstrd 13398	A constructed left module or left vector space is a structure. (Contributed by Mario Carneiro, 1-Oct-2013.) (Revised by Jim Kingdon, 5-Feb-2023.)
⊢ 𝑊 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(Scalar‘ndx), 𝐹⟩} ∪ {⟨( ·𝑠 ‘ndx), · ⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑌)    &   ⊢ (𝜑 → · ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝑊 Struct ⟨1, 6⟩)
Theorem	lmodbased 13399	The base set of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 6-Feb-2023.)
⊢ 𝑊 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(Scalar‘ndx), 𝐹⟩} ∪ {⟨( ·𝑠 ‘ndx), · ⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑌)    &   ⊢ (𝜑 → · ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝑊))
Theorem	lmodplusgd 13400	The additive operation of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 6-Feb-2023.)
⊢ 𝑊 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(Scalar‘ndx), 𝐹⟩} ∪ {⟨( ·𝑠 ‘ndx), · ⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑌)    &   ⊢ (𝜑 → · ∈ 𝑍)    ⇒   ⊢ (𝜑 → + = (+g‘𝑊))