P. 126 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12501-12600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	setscom 12501	Different components can be set in any order. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → ((𝑆 sSet ⟨𝐴, 𝐶⟩) sSet ⟨𝐵, 𝐷⟩) = ((𝑆 sSet ⟨𝐵, 𝐷⟩) sSet ⟨𝐴, 𝐶⟩))
Theorem	setscomd 12502	Different components can be set in any order. (Contributed by Jim Kingdon, 20-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ((𝑆 sSet ⟨𝐴, 𝐶⟩) sSet ⟨𝐵, 𝐷⟩) = ((𝑆 sSet ⟨𝐵, 𝐷⟩) sSet ⟨𝐴, 𝐶⟩))
Theorem	strslfvd 12503	Deduction version of strslfv 12506. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 30-Jan-2023.)
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → Fun 𝑆)    &   ⊢ (𝜑 → ⟨(𝐸‘ndx), 𝐶⟩ ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝐶 = (𝐸‘𝑆))
Theorem	strslfv2d 12504	Deduction version of strslfv 12506. (Contributed by Mario Carneiro, 30-Apr-2015.) (Revised by Jim Kingdon, 30-Jan-2023.)
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → Fun ◡◡𝑆)    &   ⊢ (𝜑 → ⟨(𝐸‘ndx), 𝐶⟩ ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐶 = (𝐸‘𝑆))
Theorem	strslfv2 12505	A variation on strslfv 12506 to avoid asserting that 𝑆 itself is a function, which involves sethood of all the ordered pair components of 𝑆. (Contributed by Mario Carneiro, 30-Apr-2015.) (Revised by Jim Kingdon, 30-Jan-2023.)
⊢ 𝑆 ∈ V    &   ⊢ Fun ◡◡𝑆    &   ⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    &   ⊢ ⟨(𝐸‘ndx), 𝐶⟩ ∈ 𝑆    ⇒   ⊢ (𝐶 ∈ 𝑉 → 𝐶 = (𝐸‘𝑆))
Theorem	strslfv 12506	Extract a structure component 𝐶 (such as the base set) from a structure 𝑆 with a component extractor 𝐸 (such as the base set extractor df-base 12467). By virtue of ndxslid 12486, this can be done without having to refer to the hard-coded numeric index of 𝐸. (Contributed by Mario Carneiro, 6-Oct-2013.) (Revised by Jim Kingdon, 30-Jan-2023.)
⊢ 𝑆 Struct 𝑋    &   ⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    &   ⊢ {⟨(𝐸‘ndx), 𝐶⟩} ⊆ 𝑆    ⇒   ⊢ (𝐶 ∈ 𝑉 → 𝐶 = (𝐸‘𝑆))
Theorem	strslfv3 12507	Variant on strslfv 12506 for large structures. (Contributed by Mario Carneiro, 10-Jan-2017.) (Revised by Jim Kingdon, 30-Jan-2023.)
⊢ (𝜑 → 𝑈 = 𝑆)    &   ⊢ 𝑆 Struct 𝑋    &   ⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    &   ⊢ {⟨(𝐸‘ndx), 𝐶⟩} ⊆ 𝑆    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ 𝐴 = (𝐸‘𝑈)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	strslssd 12508	Deduction version of strslss 12509. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by Jim Kingdon, 31-Jan-2023.)
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    &   ⊢ (𝜑 → Fun 𝑇)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑇)    &   ⊢ (𝜑 → ⟨(𝐸‘ndx), 𝐶⟩ ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐸‘𝑇) = (𝐸‘𝑆))
Theorem	strslss 12509	Propagate component extraction to a structure 𝑇 from a subset structure 𝑆. (Contributed by Mario Carneiro, 11-Oct-2013.) (Revised by Jim Kingdon, 31-Jan-2023.)
⊢ 𝑇 ∈ V    &   ⊢ Fun 𝑇    &   ⊢ 𝑆 ⊆ 𝑇    &   ⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    &   ⊢ ⟨(𝐸‘ndx), 𝐶⟩ ∈ 𝑆    ⇒   ⊢ (𝐸‘𝑇) = (𝐸‘𝑆)
Theorem	strsl0 12510	All components of the empty set are empty sets. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 31-Jan-2023.)
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    ⇒   ⊢ ∅ = (𝐸‘∅)
Theorem	base0 12511	The base set of the empty structure. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ ∅ = (Base‘∅)
Theorem	setsslid 12512	Value of the structure replacement function at a replaced index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2023.)
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    ⇒   ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 = (𝐸‘(𝑊 sSet ⟨(𝐸‘ndx), 𝐶⟩)))
Theorem	setsslnid 12513	Value of the structure replacement function at an untouched index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2023.)
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    &   ⊢ (𝐸‘ndx) ≠ 𝐷    &   ⊢ 𝐷 ∈ ℕ    ⇒   ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐸‘𝑊) = (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩)))
Theorem	baseval 12514	Value of the base set extractor. (Normally it is preferred to work with (Base‘ndx) rather than the hard-coded 1 in order to make structure theorems portable. This is an example of how to obtain it when needed.) (New usage is discouraged.) (Contributed by NM, 4-Sep-2011.)
⊢ 𝐾 ∈ V    ⇒   ⊢ (Base‘𝐾) = (𝐾‘1)
Theorem	baseid 12515	Utility theorem: index-independent form of df-base 12467. (Contributed by NM, 20-Oct-2012.)
⊢ Base = Slot (Base‘ndx)
Theorem	basendx 12516	Index value of the base set extractor. Use of this theorem is discouraged since the particular value 1 for the index is an implementation detail. It is generally sufficient to work with (Base‘ndx) and use theorems such as baseid 12515 and basendxnn 12517. The main circumstance in which it is necessary to look at indices directly is when showing that a set of indices are disjoint, in proofs such as lmodstrd 12621. Although we have a few theorems such as basendxnplusgndx 12582, we do not intend to add such theorems for every pair of indices (which would be quadradically many in the number of indices). (New usage is discouraged.) (Contributed by Mario Carneiro, 2-Aug-2013.)
⊢ (Base‘ndx) = 1
Theorem	basendxnn 12517	The index value of the base set extractor 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, 23-Sep-2020.)
⊢ (Base‘ndx) ∈ ℕ
Theorem	baseslid 12518	The base set extractor is a slot. (Contributed by Jim Kingdon, 31-Jan-2023.)
⊢ (Base = Slot (Base‘ndx) ∧ (Base‘ndx) ∈ ℕ)
Theorem	basfn 12519	The base set extractor is a function on V. (Contributed by Stefan O'Rear, 8-Jul-2015.)
⊢ Base Fn V
Theorem	basmex 12520	A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 18-Nov-2024.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝐵 → 𝐺 ∈ V)
Theorem	basmexd 12521	A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 28-Nov-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐺 ∈ V)
Theorem	reldmress 12522	The structure restriction is a proper operator, so it can be used with ovprc1 5910. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ Rel dom ↾s
Theorem	ressvalsets 12523	Value of structure restriction. (Contributed by Jim Kingdon, 16-Jan-2025.)
⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → (𝑊 ↾s 𝐴) = (𝑊 sSet ⟨(Base‘ndx), (𝐴 ∩ (Base‘𝑊))⟩))
Theorem	ressex 12524	Existence of structure restriction. (Contributed by Jim Kingdon, 16-Jan-2025.)
⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → (𝑊 ↾s 𝐴) ∈ V)
Theorem	ressval2 12525	Value of nontrivial structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet ⟨(Base‘ndx), (𝐴 ∩ 𝐵)⟩))
Theorem	ressbasd 12526	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 12527	Base set of a structure restriction. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ (𝜑 → 𝑅 = (𝑊 ↾s 𝐴))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = (Base‘𝑅))
Theorem	ressbasssd 12528	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	strressid 12529	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 12530	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 12531	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 12532	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 12533	Restriction composition law. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Proof shortened by Mario Carneiro, 2-Dec-2014.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑊 ∈ 𝑍) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵)))
Theorem	ressabsg 12534	Restriction absorption law. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐵))
6.1.2  Slot definitions
Syntax	cplusg 12535	Extend class notation with group (addition) operation.
class +g
Syntax	cmulr 12536	Extend class notation with ring multiplication.
class .r
Syntax	cstv 12537	Extend class notation with involution.
class *𝑟
Syntax	csca 12538	Extend class notation with scalar field.
class Scalar
Syntax	cvsca 12539	Extend class notation with scalar product.
class ·𝑠
Syntax	cip 12540	Extend class notation with Hermitian form (inner product).
class ·𝑖
Syntax	cts 12541	Extend class notation with the topology component of a topological space.
class TopSet
Syntax	cple 12542	Extend class notation with "less than or equal to" for posets.
class le
Syntax	coc 12543	Extend class notation with the class of orthocomplementation extractors.
class oc
Syntax	cds 12544	Extend class notation with the metric space distance function.
class dist
Syntax	cunif 12545	Extend class notation with the uniform structure.
class UnifSet
Syntax	chom 12546	Extend class notation with the hom-set structure.
class Hom
Syntax	cco 12547	Extend class notation with the composition operation.
class comp
Definition	df-plusg 12548	Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ +g = Slot 2
Definition	df-mulr 12549	Define ring multiplication. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ .r = Slot 3
Definition	df-starv 12550	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 12551	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 12552	Define scalar product. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ ·𝑠 = Slot 6
Definition	df-ip 12553	Define Hermitian form (inner product). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ ·𝑖 = Slot 8
Definition	df-tset 12554	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 12555	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 12556	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 12557	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 12558	Define the uniform structure component of a uniform space. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ UnifSet = Slot ;13
Definition	df-hom 12559	Define the hom-set component of a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ Hom = Slot ;14
Definition	df-cco 12560	Define the composition operation of a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ comp = Slot ;15
Theorem	strleund 12561	Combine two structures into one. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
⊢ (𝜑 → 𝐹 Struct ⟨𝐴, 𝐵⟩)    &   ⊢ (𝜑 → 𝐺 Struct ⟨𝐶, 𝐷⟩)    &   ⊢ (𝜑 → 𝐵 < 𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∪ 𝐺) Struct ⟨𝐴, 𝐷⟩)
Theorem	strleun 12562	Combine two structures into one. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐹 Struct ⟨𝐴, 𝐵⟩    &   ⊢ 𝐺 Struct ⟨𝐶, 𝐷⟩    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ (𝐹 ∪ 𝐺) Struct ⟨𝐴, 𝐷⟩
Theorem	strext 12563	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 12564	Make a structure from a singleton. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
⊢ 𝐼 ∈ ℕ    &   ⊢ 𝐴 = 𝐼    ⇒   ⊢ (𝑋 ∈ 𝑉 → {⟨𝐴, 𝑋⟩} Struct ⟨𝐼, 𝐼⟩)
Theorem	strle2g 12565	Make a structure from a pair. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
⊢ 𝐼 ∈ ℕ    &   ⊢ 𝐴 = 𝐼    &   ⊢ 𝐼 < 𝐽    &   ⊢ 𝐽 ∈ ℕ    &   ⊢ 𝐵 = 𝐽    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → {⟨𝐴, 𝑋⟩, ⟨𝐵, 𝑌⟩} Struct ⟨𝐼, 𝐽⟩)
Theorem	strle3g 12566	Make a structure from a triple. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐼 ∈ ℕ    &   ⊢ 𝐴 = 𝐼    &   ⊢ 𝐼 < 𝐽    &   ⊢ 𝐽 ∈ ℕ    &   ⊢ 𝐵 = 𝐽    &   ⊢ 𝐽 < 𝐾    &   ⊢ 𝐾 ∈ ℕ    &   ⊢ 𝐶 = 𝐾    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑃) → {⟨𝐴, 𝑋⟩, ⟨𝐵, 𝑌⟩, ⟨𝐶, 𝑍⟩} Struct ⟨𝐼, 𝐾⟩)
Theorem	plusgndx 12567	Index value of the df-plusg 12548 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (+g‘ndx) = 2
Theorem	plusgid 12568	Utility theorem: index-independent form of df-plusg 12548. (Contributed by NM, 20-Oct-2012.)
⊢ +g = Slot (+g‘ndx)
Theorem	plusgndxnn 12569	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 12570	Slot property of +g. (Contributed by Jim Kingdon, 3-Feb-2023.)
⊢ (+g = Slot (+g‘ndx) ∧ (+g‘ndx) ∈ ℕ)
Theorem	basendxltplusgndx 12571	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 12572	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 12573	The base set of a structure with a base set. (Contributed by AV, 10-Nov-2021.)
⊢ (𝜑 → 𝑆 Struct 𝑋)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑌)    &   ⊢ (𝜑 → ⟨(Base‘ndx), 𝑉⟩ ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝑉 = (Base‘𝑆))
Theorem	1strstrg 12574	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 12575	The base set of a constructed one-slot structure. (Contributed by AV, 27-Mar-2020.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩}    ⇒   ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐺))
Theorem	2strstrg 12576	A constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(𝐸‘ndx), + ⟩}    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 1 < 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐺 Struct ⟨1, 𝑁⟩)
Theorem	2strbasg 12577	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 12578	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 12579	A constructed two-slot structure. Version of 2strstrg 12576 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 12580	The base set of a constructed two-slot structure. Version of 2strbasg 12577 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 12581	The other slot of a constructed two-slot structure. Version of 2stropg 12578 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 12582	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 12583	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 12584	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 12585	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 12586	+g is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.)
⊢ (𝜑 → 𝐻 = (𝐺 ↾s 𝐴))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    ⇒   ⊢ (𝜑 → + = (+g‘𝐻))
Theorem	mulrndx 12587	Index value of the df-mulr 12549 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (.r‘ndx) = 3
Theorem	mulridx 12588	Utility theorem: index-independent form of df-mulr 12549. (Contributed by Mario Carneiro, 8-Jun-2013.)
⊢ .r = Slot (.r‘ndx)
Theorem	mulrslid 12589	Slot property of .r. (Contributed by Jim Kingdon, 3-Feb-2023.)
⊢ (.r = Slot (.r‘ndx) ∧ (.r‘ndx) ∈ ℕ)
Theorem	plusgndxnmulrndx 12590	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 12591	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 12592	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 12593	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 12594	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 12595	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 12596	Index value of the df-starv 12550 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (*𝑟‘ndx) = 4
Theorem	starvid 12597	Utility theorem: index-independent form of df-starv 12550. (Contributed by Mario Carneiro, 6-Oct-2013.)
⊢ *𝑟 = Slot (*𝑟‘ndx)
Theorem	starvslid 12598	Slot property of *𝑟. (Contributed by Jim Kingdon, 4-Feb-2023.)
⊢ (*𝑟 = Slot (*𝑟‘ndx) ∧ (*𝑟‘ndx) ∈ ℕ)
Theorem	starvndxnbasendx 12599	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 12600	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)