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	setsabsd 12501	Replacing the same components twice yields the same as the second setting only. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Jim Kingdon, 22-Jan-2023.)
|- ( ph -> S e. V )   &    |- ( ph -> A e. W )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. U )   =>    |- ( ph -> ( ( S sSet <. A , B >. ) sSet <. A , C >. ) = ( S sSet <. A , C >. ) )
Theorem	setscom 12502	Different components can be set in any order. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- A e. _V   &    |- B e. _V   =>    |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( ( S sSet <. A , C >. ) sSet <. B , D >. ) = ( ( S sSet <. B , D >. ) sSet <. A , C >. ) )
Theorem	setscomd 12503	Different components can be set in any order. (Contributed by Jim Kingdon, 20-Feb-2025.)
|- ( ph -> A e. Y )   &    |- ( ph -> B e. Z )   &    |- ( ph -> S e. V )   &    |- ( ph -> A =/= B )   &    |- ( ph -> C e. W )   &    |- ( ph -> D e. X )   =>    |- ( ph -> ( ( S sSet <. A , C >. ) sSet <. B , D >. ) = ( ( S sSet <. B , D >. ) sSet <. A , C >. ) )
Theorem	strslfvd 12504	Deduction version of strslfv 12507. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 30-Jan-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- ( ph -> S e. V )   &    |- ( ph -> Fun S )   &    |- ( ph -> <. ( E ` ndx ) , C >. e. S )   =>    |- ( ph -> C = ( E ` S ) )
Theorem	strslfv2d 12505	Deduction version of strslfv 12507. (Contributed by Mario Carneiro, 30-Apr-2015.) (Revised by Jim Kingdon, 30-Jan-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- ( ph -> S e. V )   &    |- ( ph -> Fun `' `' S )   &    |- ( ph -> <. ( E ` ndx ) , C >. e. S )   &    |- ( ph -> C e. W )   =>    |- ( ph -> C = ( E ` S ) )
Theorem	strslfv2 12506	A variation on strslfv 12507 to avoid asserting that S itself is a function, which involves sethood of all the ordered pair components of S. (Contributed by Mario Carneiro, 30-Apr-2015.) (Revised by Jim Kingdon, 30-Jan-2023.)
|- S e. _V   &    |- Fun `' `' S   &    |- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- <. ( E ` ndx ) , C >. e. S   =>    |- ( C e. V -> C = ( E ` S ) )
Theorem	strslfv 12507	Extract a structure component C (such as the base set) from a structure S with a component extractor E (such as the base set extractor df-base 12468). By virtue of ndxslid 12487, this can be done without having to refer to the hard-coded numeric index of E. (Contributed by Mario Carneiro, 6-Oct-2013.) (Revised by Jim Kingdon, 30-Jan-2023.)
|- S Struct X   &    |- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- { <. ( E ` ndx ) , C >. } C_ S   =>    |- ( C e. V -> C = ( E ` S ) )
Theorem	strslfv3 12508	Variant on strslfv 12507 for large structures. (Contributed by Mario Carneiro, 10-Jan-2017.) (Revised by Jim Kingdon, 30-Jan-2023.)
|- ( ph -> U = S )   &    |- S Struct X   &    |- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- { <. ( E ` ndx ) , C >. } C_ S   &    |- ( ph -> C e. V )   &    |- A = ( E ` U )   =>    |- ( ph -> A = C )
Theorem	strslssd 12509	Deduction version of strslss 12510. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by Jim Kingdon, 31-Jan-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- ( ph -> T e. V )   &    |- ( ph -> Fun T )   &    |- ( ph -> S C_ T )   &    |- ( ph -> <. ( E ` ndx ) , C >. e. S )   =>    |- ( ph -> ( E ` T ) = ( E ` S ) )
Theorem	strslss 12510	Propagate component extraction to a structure T from a subset structure S. (Contributed by Mario Carneiro, 11-Oct-2013.) (Revised by Jim Kingdon, 31-Jan-2023.)
|- T e. _V   &    |- Fun T   &    |- S C_ T   &    |- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- <. ( E ` ndx ) , C >. e. S   =>    |- ( E ` T ) = ( E ` S )
Theorem	strsl0 12511	All components of the empty set are empty sets. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 31-Jan-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   =>    |- (/) = ( E ` (/) )
Theorem	base0 12512	The base set of the empty structure. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- (/) = ( Base ` (/) )
Theorem	setsslid 12513	Value of the structure replacement function at a replaced index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   =>    |- ( ( W e. A /\ C e. V ) -> C = ( E ` ( W sSet <. ( E ` ndx ) , C >. ) ) )
Theorem	setsslnid 12514	Value of the structure replacement function at an untouched index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- ( E ` ndx ) =/= D   &    |- D e. NN   =>    |- ( ( W e. A /\ C e. V ) -> ( E ` W ) = ( E ` ( W sSet <. D , C >. ) ) )
Theorem	baseval 12515	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.)
|- K e. _V   =>    |- ( Base ` K ) = ( K ` 1 )
Theorem	baseid 12516	Utility theorem: index-independent form of df-base 12468. (Contributed by NM, 20-Oct-2012.)
|- Base = Slot ( Base ` ndx )
Theorem	basendx 12517	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 12516 and basendxnn 12518. 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 12622. Although we have a few theorems such as basendxnplusgndx 12583, 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 12518	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 ) e. NN
Theorem	baseslid 12519	The base set extractor is a slot. (Contributed by Jim Kingdon, 31-Jan-2023.)
|- ( Base = Slot ( Base ` ndx ) /\ ( Base ` ndx ) e. NN )
Theorem	basfn 12520	The base set extractor is a function on _V. (Contributed by Stefan O'Rear, 8-Jul-2015.)
|- Base Fn _V
Theorem	basmex 12521	A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 18-Nov-2024.)
|- B = ( Base ` G )   =>    |- ( A e. B -> G e. _V )
Theorem	basmexd 12522	A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 28-Nov-2024.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> A e. B )   =>    |- ( ph -> G e. _V )
Theorem	reldmress 12523	The structure restriction is a proper operator, so it can be used with ovprc1 5911. (Contributed by Stefan O'Rear, 29-Nov-2014.)
|- Rel dom ↾s
Theorem	ressvalsets 12524	Value of structure restriction. (Contributed by Jim Kingdon, 16-Jan-2025.)
|- ( ( W e. X /\ A e. Y ) -> ( W ↾s A ) = ( W sSet <. ( Base ` ndx ) , ( A i^i ( Base ` W ) ) >. ) )
Theorem	ressex 12525	Existence of structure restriction. (Contributed by Jim Kingdon, 16-Jan-2025.)
|- ( ( W e. X /\ A e. Y ) -> ( W ↾s A ) e. _V )
Theorem	ressval2 12526	Value of nontrivial structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
|- R = ( W ↾s A )   &    |- B = ( Base ` W )   =>    |- ( ( -. B C_ A /\ W e. X /\ A e. Y ) -> R = ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) )
Theorem	ressbasd 12527	Base set of a structure restriction. (Contributed by Stefan O'Rear, 26-Nov-2014.) (Proof shortened by AV, 7-Nov-2024.)
|- ( ph -> R = ( W ↾s A ) )   &    |- ( ph -> B = ( Base ` W ) )   &    |- ( ph -> W e. X )   &    |- ( ph -> A e. V )   =>    |- ( ph -> ( A i^i B ) = ( Base ` R ) )
Theorem	ressbas2d 12528	Base set of a structure restriction. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- ( ph -> R = ( W ↾s A ) )   &    |- ( ph -> B = ( Base ` W ) )   &    |- ( ph -> W e. X )   &    |- ( ph -> A C_ B )   =>    |- ( ph -> A = ( Base ` R ) )
Theorem	ressbasssd 12529	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.)
|- ( ph -> R = ( W ↾s A ) )   &    |- ( ph -> B = ( Base ` W ) )   &    |- ( ph -> W e. X )   &    |- ( ph -> A e. V )   =>    |- ( ph -> ( Base ` R ) C_ B )
Theorem	strressid 12530	Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Revised by Jim Kingdon, 17-Jan-2025.)
|- ( ph -> B = ( Base ` W ) )   &    |- ( ph -> W Struct <. M , N >. )   &    |- ( ph -> Fun W )   &    |- ( ph -> ( Base ` ndx ) e. dom W )   =>    |- ( ph -> ( W ↾s B ) = W )
Theorem	ressval3d 12531	Value of structure restriction, deduction version. (Contributed by AV, 14-Mar-2020.) (Revised by Jim Kingdon, 17-Jan-2025.)
|- R = ( S ↾s A )   &    |- B = ( Base ` S )   &    |- E = ( Base ` ndx )   &    |- ( ph -> S e. V )   &    |- ( ph -> Fun S )   &    |- ( ph -> E e. dom S )   &    |- ( ph -> A C_ B )   =>    |- ( ph -> R = ( S sSet <. E , A >. ) )
Theorem	resseqnbasd 12532	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.)
|- R = ( W ↾s A )   &    |- C = ( E ` W )   &    |- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- ( E ` ndx ) =/= ( Base ` ndx )   &    |- ( ph -> W e. X )   &    |- ( ph -> A e. V )   =>    |- ( ph -> C = ( E ` R ) )
Theorem	ressinbasd 12533	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.)
|- ( ph -> B = ( Base ` W ) )   &    |- ( ph -> A e. X )   &    |- ( ph -> W e. V )   =>    |- ( ph -> ( W ↾s A ) = ( W ↾s ( A i^i B ) ) )
Theorem	ressressg 12534	Restriction composition law. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Proof shortened by Mario Carneiro, 2-Dec-2014.)
|- ( ( A e. X /\ B e. Y /\ W e. Z ) -> ( ( W ↾s A ) ↾s B ) = ( W ↾s ( A i^i B ) ) )
Theorem	ressabsg 12535	Restriction absorption law. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- ( ( A e. X /\ B C_ A /\ W e. Y ) -> ( ( W ↾s A ) ↾s B ) = ( W ↾s B ) )
6.1.2  Slot definitions
Syntax	cplusg 12536	Extend class notation with group (addition) operation.
class +g
Syntax	cmulr 12537	Extend class notation with ring multiplication.
class .r
Syntax	cstv 12538	Extend class notation with involution.
class *r
Syntax	csca 12539	Extend class notation with scalar field.
class Scalar
Syntax	cvsca 12540	Extend class notation with scalar product.
class .s
Syntax	cip 12541	Extend class notation with Hermitian form (inner product).
class .i
Syntax	cts 12542	Extend class notation with the topology component of a topological space.
class TopSet
Syntax	cple 12543	Extend class notation with "less than or equal to" for posets.
class le
Syntax	coc 12544	Extend class notation with the class of orthocomplementation extractors.
class oc
Syntax	cds 12545	Extend class notation with the metric space distance function.
class dist
Syntax	cunif 12546	Extend class notation with the uniform structure.
class UnifSet
Syntax	chom 12547	Extend class notation with the hom-set structure.
class Hom
Syntax	cco 12548	Extend class notation with the composition operation.
class comp
Definition	df-plusg 12549	Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- +g = Slot 2
Definition	df-mulr 12550	Define ring multiplication. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- .r = Slot 3
Definition	df-starv 12551	Define the involution function of a *-ring. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- *r = Slot 4
Definition	df-sca 12552	Define scalar field component of a vector space v. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- Scalar = Slot 5
Definition	df-vsca 12553	Define scalar product. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- .s = Slot 6
Definition	df-ip 12554	Define Hermitian form (inner product). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- .i = Slot 8
Definition	df-tset 12555	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 12556	Define "less than or equal to" ordering extractor for posets and related structures. We use ; 1 0 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 ; 1 0
Definition	df-ocomp 12557	Define the orthocomplementation extractor for posets and related structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- oc = Slot ; 1 1
Definition	df-ds 12558	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 ; 1 2
Definition	df-unif 12559	Define the uniform structure component of a uniform space. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- UnifSet = Slot ; 1 3
Definition	df-hom 12560	Define the hom-set component of a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- Hom = Slot ; 1 4
Definition	df-cco 12561	Define the composition operation of a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- comp = Slot ; 1 5
Theorem	strleund 12562	Combine two structures into one. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
|- ( ph -> F Struct <. A , B >. )   &    |- ( ph -> G Struct <. C , D >. )   &    |- ( ph -> B < C )   =>    |- ( ph -> ( F u. G ) Struct <. A , D >. )
Theorem	strleun 12563	Combine two structures into one. (Contributed by Mario Carneiro, 29-Aug-2015.)
|- F Struct <. A , B >.   &    |- G Struct <. C , D >.   &    |- B < C   =>    |- ( F u. G ) Struct <. A , D >.
Theorem	strext 12564	Extending the upper range of a structure. This works because when we say that a structure has components in A ... C 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.)
|- ( ph -> F Struct <. A , B >. )   &    |- ( ph -> C e. ( ZZ>= ` B ) )   =>    |- ( ph -> F Struct <. A , C >. )
Theorem	strle1g 12565	Make a structure from a singleton. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
|- I e. NN   &    |- A = I   =>    |- ( X e. V -> { <. A , X >. } Struct <. I , I >. )
Theorem	strle2g 12566	Make a structure from a pair. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.)
|- I e. NN   &    |- A = I   &    |- I < J   &    |- J e. NN   &    |- B = J   =>    |- ( ( X e. V /\ Y e. W ) -> { <. A , X >. , <. B , Y >. } Struct <. I , J >. )
Theorem	strle3g 12567	Make a structure from a triple. (Contributed by Mario Carneiro, 29-Aug-2015.)
|- I e. NN   &    |- A = I   &    |- I < J   &    |- J e. NN   &    |- B = J   &    |- J < K   &    |- K e. NN   &    |- C = K   =>    |- ( ( X e. V /\ Y e. W /\ Z e. P ) -> { <. A , X >. , <. B , Y >. , <. C , Z >. } Struct <. I , K >. )
Theorem	plusgndx 12568	Index value of the df-plusg 12549 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( +g ` ndx ) = 2
Theorem	plusgid 12569	Utility theorem: index-independent form of df-plusg 12549. (Contributed by NM, 20-Oct-2012.)
|- +g = Slot ( +g ` ndx )
Theorem	plusgndxnn 12570	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 ) e. NN
Theorem	plusgslid 12571	Slot property of +g. (Contributed by Jim Kingdon, 3-Feb-2023.)
|- ( +g = Slot ( +g ` ndx ) /\ ( +g ` ndx ) e. NN )
Theorem	basendxltplusgndx 12572	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 12573	The slot of a structure which contains an ordered pair for that slot. (Contributed by Jim Kingdon, 5-Feb-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- ( ph -> S Struct X )   &    |- ( ph -> V e. Y )   &    |- ( ph -> <. ( E ` ndx ) , V >. e. S )   =>    |- ( ph -> V = ( E ` S ) )
Theorem	opelstrbas 12574	The base set of a structure with a base set. (Contributed by AV, 10-Nov-2021.)
|- ( ph -> S Struct X )   &    |- ( ph -> V e. Y )   &    |- ( ph -> <. ( Base ` ndx ) , V >. e. S )   =>    |- ( ph -> V = ( Base ` S ) )
Theorem	1strstrg 12575	A constructed one-slot structure. (Contributed by AV, 27-Mar-2020.) (Revised by Jim Kingdon, 28-Jan-2023.)
|- G = { <. ( Base ` ndx ) , B >. }   =>    |- ( B e. V -> G Struct <. 1 , 1 >. )
Theorem	1strbas 12576	The base set of a constructed one-slot structure. (Contributed by AV, 27-Mar-2020.)
|- G = { <. ( Base ` ndx ) , B >. }   =>    |- ( B e. V -> B = ( Base ` G ) )
Theorem	2strstrg 12577	A constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
|- G = { <. ( Base ` ndx ) , B >. , <. ( E ` ndx ) , .+ >. }   &    |- E = Slot N   &    |- 1 < N   &    |- N e. NN   =>    |- ( ( B e. V /\ .+ e. W ) -> G Struct <. 1 , N >. )
Theorem	2strbasg 12578	The base set of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
|- G = { <. ( Base ` ndx ) , B >. , <. ( E ` ndx ) , .+ >. }   &    |- E = Slot N   &    |- 1 < N   &    |- N e. NN   =>    |- ( ( B e. V /\ .+ e. W ) -> B = ( Base ` G ) )
Theorem	2stropg 12579	The other slot of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
|- G = { <. ( Base ` ndx ) , B >. , <. ( E ` ndx ) , .+ >. }   &    |- E = Slot N   &    |- 1 < N   &    |- N e. NN   =>    |- ( ( B e. V /\ .+ e. W ) -> .+ = ( E ` G ) )
Theorem	2strstr1g 12580	A constructed two-slot structure. Version of 2strstrg 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.)
|- G = { <. ( Base ` ndx ) , B >. , <. N , .+ >. }   &    |- ( Base ` ndx ) < N   &    |- N e. NN   =>    |- ( ( B e. V /\ .+ e. W ) -> G Struct <. ( Base ` ndx ) , N >. )
Theorem	2strbas1g 12581	The base set of a constructed two-slot structure. Version of 2strbasg 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.)
|- G = { <. ( Base ` ndx ) , B >. , <. N , .+ >. }   &    |- ( Base ` ndx ) < N   &    |- N e. NN   =>    |- ( ( B e. V /\ .+ e. W ) -> B = ( Base ` G ) )
Theorem	2strop1g 12582	The other slot of a constructed two-slot structure. Version of 2stropg 12579 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.)
|- G = { <. ( Base ` ndx ) , B >. , <. N , .+ >. }   &    |- ( Base ` ndx ) < N   &    |- N e. NN   &    |- E = Slot N   =>    |- ( ( B e. V /\ .+ e. W ) -> .+ = ( E ` G ) )
Theorem	basendxnplusgndx 12583	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 12584	A constructed group is a structure on 1 ... 2. (Contributed by Mario Carneiro, 28-Sep-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. }   =>    |- ( ( B e. V /\ .+ e. W ) -> G Struct <. 1 , 2 >. )
Theorem	grpbaseg 12585	The base set of a constructed group. (Contributed by Mario Carneiro, 2-Aug-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. }   =>    |- ( ( B e. V /\ .+ e. W ) -> B = ( Base ` G ) )
Theorem	grpplusgg 12586	The operation of a constructed group. (Contributed by Mario Carneiro, 2-Aug-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. }   =>    |- ( ( B e. V /\ .+ e. W ) -> .+ = ( +g ` G ) )
Theorem	ressplusgd 12587	+g is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- ( ph -> H = ( G ↾s A ) )   &    |- ( ph -> .+ = ( +g ` G ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> G e. W )   =>    |- ( ph -> .+ = ( +g ` H ) )
Theorem	mulrndx 12588	Index value of the df-mulr 12550 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( .r ` ndx ) = 3
Theorem	mulridx 12589	Utility theorem: index-independent form of df-mulr 12550. (Contributed by Mario Carneiro, 8-Jun-2013.)
|- .r = Slot ( .r ` ndx )
Theorem	mulrslid 12590	Slot property of .r. (Contributed by Jim Kingdon, 3-Feb-2023.)
|- ( .r = Slot ( .r ` ndx ) /\ ( .r ` ndx ) e. NN )
Theorem	plusgndxnmulrndx 12591	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 12592	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 12593	A constructed ring is a structure. (Contributed by Mario Carneiro, 28-Sep-2013.) (Revised by Jim Kingdon, 3-Feb-2023.)
|- R = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. }   =>    |- ( ( B e. V /\ .+ e. W /\ .x. e. X ) -> R Struct <. 1 , 3 >. )
Theorem	rngbaseg 12594	The base set of a constructed ring. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 3-Feb-2023.)
|- R = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. }   =>    |- ( ( B e. V /\ .+ e. W /\ .x. e. X ) -> B = ( Base ` R ) )
Theorem	rngplusgg 12595	The additive operation of a constructed ring. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- R = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. }   =>    |- ( ( B e. V /\ .+ e. W /\ .x. e. X ) -> .+ = ( +g ` R ) )
Theorem	rngmulrg 12596	The multiplicative operation of a constructed ring. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- R = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. }   =>    |- ( ( B e. V /\ .+ e. W /\ .x. e. X ) -> .x. = ( .r ` R ) )
Theorem	starvndx 12597	Index value of the df-starv 12551 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( *r ` ndx ) = 4
Theorem	starvid 12598	Utility theorem: index-independent form of df-starv 12551. (Contributed by Mario Carneiro, 6-Oct-2013.)
|- *r = Slot ( *r ` ndx )
Theorem	starvslid 12599	Slot property of *r. (Contributed by Jim Kingdon, 4-Feb-2023.)
|- ( *r = Slot ( *r ` ndx ) /\ ( *r ` ndx ) e. NN )
Theorem	starvndxnbasendx 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.)
|- ( *r ` ndx ) =/= ( Base ` ndx )