P. 132 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13101-13200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isstructim 13101	The property of being a structure with components in M ... N. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
|- ( F Struct <. M , N >. -> ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( M ... N ) ) )
Theorem	isstructr 13102	The property of being a structure with components in M ... N. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
|- ( ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ ( Fun ( F \ { (/) } ) /\ F e. V /\ dom F C_ ( M ... N ) ) ) -> F Struct <. M , N >. )
Theorem	structcnvcnv 13103	Two ways to express the relational part of a structure. (Contributed by Mario Carneiro, 29-Aug-2015.)
|- ( F Struct X -> `' `' F = ( F \ { (/) } ) )
Theorem	structfung 13104	The converse of the converse of a structure is a function. Closed form of structfun 13105. (Contributed by AV, 12-Nov-2021.)
|- ( F Struct X -> Fun `' `' F )
Theorem	structfun 13105	Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Proof shortened by AV, 12-Nov-2021.)
|- F Struct X   =>    |- Fun `' `' F
Theorem	structfn 13106	Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.)
|- F Struct <. M , N >.   =>    |- ( Fun `' `' F /\ dom F C_ ( 1 ... N ) )
Theorem	strnfvnd 13107	Deduction version of strnfvn 13108. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 19-Jan-2023.)
|- E = Slot N   &    |- ( ph -> S e. V )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> ( E ` S ) = ( S ` N ) )
Theorem	strnfvn 13108	Value of a structure component extractor E. Normally, E is a defined constant symbol such as Base (df-base 13093) and N is a fixed integer such as 1. S is a structure, i.e. a specific member of a class of structures. Note: Normally, this theorem shouldn't be used outside of this section, because it requires hard-coded index values. Instead, use strslfv 13132. (Contributed by NM, 9-Sep-2011.) (Revised by Jim Kingdon, 19-Jan-2023.) (New usage is discouraged.)
|- S e. _V   &    |- E = Slot N   &    |- N e. NN   =>    |- ( E ` S ) = ( S ` N )
Theorem	strfvssn 13109	A structure component extractor produces a value which is contained in a set dependent on S, but not E. This is sometimes useful for showing sethood. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Jim Kingdon, 19-Jan-2023.)
|- E = Slot N   &    |- ( ph -> S e. V )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> ( E ` S ) C_ U. ran S )
Theorem	ndxarg 13110	Get the numeric argument from a defined structure component extractor such as df-base 13093. (Contributed by Mario Carneiro, 6-Oct-2013.)
|- E = Slot N   &    |- N e. NN   =>    |- ( E ` ndx ) = N
Theorem	ndxid 13111	A structure component extractor is defined by its own index. This theorem, together with strslfv 13132 below, is useful for avoiding direct reference to the hard-coded numeric index in component extractor definitions, such as the 1 in df-base 13093, making it easier to change should the need arise. (Contributed by NM, 19-Oct-2012.) (Revised by Mario Carneiro, 6-Oct-2013.) (Proof shortened by BJ, 27-Dec-2021.)
|- E = Slot N   &    |- N e. NN   =>    |- E = Slot ( E ` ndx )
Theorem	ndxslid 13112	A structure component extractor is defined by its own index. That the index is a natural number will also be needed in quite a few contexts so it is included in the conclusion of this theorem which can be used as a hypothesis of theorems like strslfv 13132. (Contributed by Jim Kingdon, 29-Jan-2023.)
|- E = Slot N   &    |- N e. NN   =>    |- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )
Theorem	slotslfn 13113	A slot is a function on sets, treated as structures. (Contributed by Mario Carneiro, 22-Sep-2015.) (Revised by Jim Kingdon, 10-Feb-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   =>    |- E Fn _V
Theorem	slotex 13114	Existence of slot value. A corollary of slotslfn 13113. (Contributed by Jim Kingdon, 12-Feb-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   =>    |- ( A e. V -> ( E ` A ) e. _V )
Theorem	strndxid 13115	The value of a structure component extractor is the value of the corresponding slot of the structure. (Contributed by AV, 13-Mar-2020.)
|- ( ph -> S e. V )   &    |- E = Slot N   &    |- N e. NN   =>    |- ( ph -> ( S ` ( E ` ndx ) ) = ( E ` S ) )
Theorem	reldmsets 13116	The structure override operator is a proper operator. (Contributed by Stefan O'Rear, 29-Jan-2015.)
|- Rel dom sSet
Theorem	setsvalg 13117	Value of the structure replacement function. (Contributed by Mario Carneiro, 30-Apr-2015.)
|- ( ( S e. V /\ A e. W ) -> ( S sSet A ) = ( ( S |` ( _V \ dom { A } ) ) u. { A } ) )
Theorem	setsvala 13118	Value of the structure replacement function. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 20-Jan-2023.)
|- ( ( S e. V /\ A e. X /\ B e. W ) -> ( S sSet <. A , B >. ) = ( ( S |` ( _V \ { A } ) ) u. { <. A , B >. } ) )
Theorem	setsex 13119	Applying the structure replacement function yields a set. (Contributed by Jim Kingdon, 22-Jan-2023.)
|- ( ( S e. V /\ A e. X /\ B e. W ) -> ( S sSet <. A , B >. ) e. _V )
Theorem	strsetsid 13120	Value of the structure replacement function. (Contributed by AV, 14-Mar-2020.) (Revised by Jim Kingdon, 30-Jan-2023.)
|- E = Slot ( E ` ndx )   &    |- ( ph -> S Struct <. M , N >. )   &    |- ( ph -> Fun S )   &    |- ( ph -> ( E ` ndx ) e. dom S )   =>    |- ( ph -> S = ( S sSet <. ( E ` ndx ) , ( E ` S ) >. ) )
Theorem	fvsetsid 13121	The value of the structure replacement function for its first argument is its second argument. (Contributed by SO, 12-Jul-2018.)
|- ( ( F e. V /\ X e. W /\ Y e. U ) -> ( ( F sSet <. X , Y >. ) ` X ) = Y )
Theorem	setsfun 13122	A structure with replacement is a function if the original structure is a function. (Contributed by AV, 7-Jun-2021.)
|- ( ( ( G e. V /\ Fun G ) /\ ( I e. U /\ E e. W ) ) -> Fun ( G sSet <. I , E >. ) )
Theorem	setsfun0 13123	A structure with replacement without the empty set is a function if the original structure without the empty set is a function. This variant of setsfun 13122 is useful for proofs based on isstruct2r 13098 which requires Fun ( F \ { (/) } ) for F to be an extensible structure. (Contributed by AV, 7-Jun-2021.)
|- ( ( ( G e. V /\ Fun ( G \ { (/) } ) ) /\ ( I e. U /\ E e. W ) ) -> Fun ( ( G sSet <. I , E >. ) \ { (/) } ) )
Theorem	setsn0fun 13124	The value of the structure replacement function (without the empty set) is a function if the structure (without the empty set) is a function. (Contributed by AV, 7-Jun-2021.) (Revised by AV, 16-Nov-2021.)
|- ( ph -> S Struct X )   &    |- ( ph -> I e. U )   &    |- ( ph -> E e. W )   =>    |- ( ph -> Fun ( ( S sSet <. I , E >. ) \ { (/) } ) )
Theorem	setsresg 13125	The structure replacement function does not affect the value of S away from A. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 22-Jan-2023.)
|- ( ( S e. V /\ A e. W /\ B e. X ) -> ( ( S sSet <. A , B >. ) |` ( _V \ { A } ) ) = ( S |` ( _V \ { A } ) ) )
Theorem	setsabsd 13126	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 13127	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 13128	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 13129	Deduction version of strslfv 13132. (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 13130	Deduction version of strslfv 13132. (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 13131	A variation on strslfv 13132 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 13132	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 13093). By virtue of ndxslid 13112, 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 13133	Variant on strslfv 13132 for large structures. (Contributed by Mario Carneiro, 10-Jan-2017.) (Revised by Jim Kingdon, 30-Jan-2023.)
|- ( ph -> U = S )   &    |- ( ph -> S Struct X )   &    |- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- ( ph -> { <. ( E ` ndx ) , C >. } C_ S )   &    |- ( ph -> C e. V )   &    |- A = ( E ` U )   =>    |- ( ph -> A = C )
Theorem	strslssd 13134	Deduction version of strslss 13135. (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 13135	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 13136	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 13137	The base set of the empty structure. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- (/) = ( Base ` (/) )
Theorem	setsslid 13138	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 13139	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 13140	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 13141	Utility theorem: index-independent form of df-base 13093. (Contributed by NM, 20-Oct-2012.)
|- Base = Slot ( Base ` ndx )
Theorem	basendx 13142	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 13141 and basendxnn 13143. 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 13252. Although we have a few theorems such as basendxnplusgndx 13213, 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 13143	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	bassetsnn 13144	The pair of the base index and another index is a subset of the domain of the structure obtained by replacing/adding a slot at the other index in a structure having a base slot. (Contributed by AV, 7-Jun-2021.) (Revised by AV, 16-Nov-2021.)
|- ( ph -> S Struct X )   &    |- ( ph -> I e. NN )   &    |- ( ph -> E e. W )   &    |- ( ph -> ( Base ` ndx ) e. dom S )   =>    |- ( ph -> { ( Base ` ndx ) , I } C_ dom ( S sSet <. I , E >. ) )
Theorem	baseslid 13145	The base set extractor is a slot. (Contributed by Jim Kingdon, 31-Jan-2023.)
|- ( Base = Slot ( Base ` ndx ) /\ ( Base ` ndx ) e. NN )
Theorem	basfn 13146	The base set extractor is a function on _V. (Contributed by Stefan O'Rear, 8-Jul-2015.)
|- Base Fn _V
Theorem	basmex 13147	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 13148	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	basm 13149*	A structure whose base is inhabited is inhabited. (Contributed by Jim Kingdon, 14-Jun-2025.)
|- B = ( Base ` G )   =>    |- ( A e. B -> E. j j e. G )
Theorem	relelbasov 13150	Utility theorem: reverse closure for any structure defined as a two-argument function. (Contributed by Mario Carneiro, 3-Oct-2015.)
|- Rel dom O   &    |- Rel O   &    |- S = ( X O Y )   &    |- B = ( Base ` S )   =>    |- ( A e. B -> ( X e. _V /\ Y e. _V ) )
Theorem	reldmress 13151	The structure restriction is a proper operator, so it can be used with ovprc1 6055. (Contributed by Stefan O'Rear, 29-Nov-2014.)
|- Rel dom ↾s
Theorem	ressvalsets 13152	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 13153	Existence of structure restriction. (Contributed by Jim Kingdon, 16-Jan-2025.)
|- ( ( W e. X /\ A e. Y ) -> ( W ↾s A ) e. _V )
Theorem	ressval2 13154	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 13155	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 13156	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 13157	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	ressbasid 13158	The trivial structure restriction leaves the base set unchanged. (Contributed by Jim Kingdon, 29-Apr-2025.)
|- B = ( Base ` W )   =>    |- ( W e. V -> ( Base ` ( W ↾s B ) ) = B )
Theorem	strressid 13159	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 13160	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 13161	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 13162	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 13163	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 13164	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 13165	Extend class notation with group (addition) operation.
class +g
Syntax	cmulr 13166	Extend class notation with ring multiplication.
class .r
Syntax	cstv 13167	Extend class notation with involution.
class *r
Syntax	csca 13168	Extend class notation with scalar field.
class Scalar
Syntax	cvsca 13169	Extend class notation with scalar product.
class .s
Syntax	cip 13170	Extend class notation with Hermitian form (inner product).
class .i
Syntax	cts 13171	Extend class notation with the topology component of a topological space.
class TopSet
Syntax	cple 13172	Extend class notation with "less than or equal to" for posets.
class le
Syntax	coc 13173	Extend class notation with the class of orthocomplementation extractors.
class oc
Syntax	cds 13174	Extend class notation with the metric space distance function.
class dist
Syntax	cunif 13175	Extend class notation with the uniform structure.
class UnifSet
Syntax	chom 13176	Extend class notation with the hom-set structure.
class Hom
Syntax	cco 13177	Extend class notation with the composition operation.
class comp
Definition	df-plusg 13178	Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- +g = Slot 2
Definition	df-mulr 13179	Define ring multiplication. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- .r = Slot 3
Definition	df-starv 13180	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 13181	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 13182	Define scalar product. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- .s = Slot 6
Definition	df-ip 13183	Define Hermitian form (inner product). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- .i = Slot 8
Definition	df-tset 13184	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 13185	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 13186	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 13187	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 13188	Define the uniform structure component of a uniform space. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- UnifSet = Slot ; 1 3
Definition	df-hom 13189	Define the hom-set component of a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- Hom = Slot ; 1 4
Definition	df-cco 13190	Define the composition operation of a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- comp = Slot ; 1 5
Theorem	strleund 13191	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 13192	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 13193	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 13194	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 13195	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 13196	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 13197	Index value of the df-plusg 13178 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( +g ` ndx ) = 2
Theorem	plusgid 13198	Utility theorem: index-independent form of df-plusg 13178. (Contributed by NM, 20-Oct-2012.)
|- +g = Slot ( +g ` ndx )
Theorem	plusgndxnn 13199	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 13200	Slot property of +g. (Contributed by Jim Kingdon, 3-Feb-2023.)
|- ( +g = Slot ( +g ` ndx ) /\ ( +g ` ndx ) e. NN )