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
Syntax	chom 13301	Extend class notation with the hom-set structure.
class Hom
Syntax	cco 13302	Extend class notation with the composition operation.
class comp
Definition	df-plusg 13303	Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- +g = Slot 2
Definition	df-mulr 13304	Define ring multiplication. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- .r = Slot 3
Definition	df-starv 13305	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 13306	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 13307	Define scalar product. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- .s = Slot 6
Definition	df-ip 13308	Define Hermitian form (inner product). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- .i = Slot 8
Definition	df-tset 13309	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 13310	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 13311	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 13312	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 13313	Define the uniform structure component of a uniform space. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- UnifSet = Slot ; 1 3
Definition	df-hom 13314	Define the hom-set component of a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- Hom = Slot ; 1 4
Definition	df-cco 13315	Define the composition operation of a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- comp = Slot ; 1 5
Theorem	strleund 13316	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 13317	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 13318	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 13319	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 13320	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 13321	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 13322	Index value of the df-plusg 13303 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( +g ` ndx ) = 2
Theorem	plusgid 13323	Utility theorem: index-independent form of df-plusg 13303. (Contributed by NM, 20-Oct-2012.)
|- +g = Slot ( +g ` ndx )
Theorem	plusgndxnn 13324	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 13325	Slot property of +g. (Contributed by Jim Kingdon, 3-Feb-2023.)
|- ( +g = Slot ( +g ` ndx ) /\ ( +g ` ndx ) e. NN )
Theorem	basendxltplusgndx 13326	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 13327	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 13328	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 13329	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 13330	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	2strstrndx 13331	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.)
|- G = { <. ( Base ` ndx ) , B >. , <. N , .+ >. }   &    |- ( Base ` ndx ) < N   &    |- N e. NN   =>    |- ( ( B e. V /\ .+ e. W ) -> G Struct <. ( Base ` ndx ) , N >. )
Theorem	2strstrg 13332	A constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.) Use 2strstrndx 13331 instead. (New usage is discouraged.)
|- 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 13333	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 13334	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 13335	A constructed two-slot structure. Version of 2strstrg 13332 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 13336	The base set of a constructed two-slot structure. Version of 2strbasg 13333 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 13337	The other slot of a constructed two-slot structure. Version of 2stropg 13334 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 13338	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 13339	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 13340	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 13341	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 13342	+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 13343	Index value of the df-mulr 13304 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( .r ` ndx ) = 3
Theorem	mulridx 13344	Utility theorem: index-independent form of df-mulr 13304. (Contributed by Mario Carneiro, 8-Jun-2013.)
|- .r = Slot ( .r ` ndx )
Theorem	mulrslid 13345	Slot property of .r. (Contributed by Jim Kingdon, 3-Feb-2023.)
|- ( .r = Slot ( .r ` ndx ) /\ ( .r ` ndx ) e. NN )
Theorem	plusgndxnmulrndx 13346	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 13347	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 13348	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 13349	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 13350	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 13351	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 13352	Index value of the df-starv 13305 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( *r ` ndx ) = 4
Theorem	starvid 13353	Utility theorem: index-independent form of df-starv 13305. (Contributed by Mario Carneiro, 6-Oct-2013.)
|- *r = Slot ( *r ` ndx )
Theorem	starvslid 13354	Slot property of *r. (Contributed by Jim Kingdon, 4-Feb-2023.)
|- ( *r = Slot ( *r ` ndx ) /\ ( *r ` ndx ) e. NN )
Theorem	starvndxnbasendx 13355	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 )
Theorem	starvndxnplusgndx 13356	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 ) =/= ( +g ` ndx )
Theorem	starvndxnmulrndx 13357	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 ) =/= ( .r ` ndx )
Theorem	ressmulrg 13358	.r is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- S = ( R ↾s A )   &    |- .x. = ( .r ` R )   =>    |- ( ( A e. V /\ R e. W ) -> .x. = ( .r ` S ) )
Theorem	srngstrd 13359	A constructed star ring is a structure. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Jim Kingdon, 5-Feb-2023.)
|- R = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. ( *r ` ndx ) , .* >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> .x. e. X )   &    |- ( ph -> .* e. Y )   =>    |- ( ph -> R Struct <. 1 , 4 >. )
Theorem	srngbased 13360	The base set of a constructed star ring. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Jim Kingdon, 5-Feb-2023.)
|- R = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. ( *r ` ndx ) , .* >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> .x. e. X )   &    |- ( ph -> .* e. Y )   =>    |- ( ph -> B = ( Base ` R ) )
Theorem	srngplusgd 13361	The addition operation of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.) (Revised by Jim Kingdon, 5-Feb-2023.)
|- R = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. ( *r ` ndx ) , .* >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> .x. e. X )   &    |- ( ph -> .* e. Y )   =>    |- ( ph -> .+ = ( +g ` R ) )
Theorem	srngmulrd 13362	The multiplication operation of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- R = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. ( *r ` ndx ) , .* >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> .x. e. X )   &    |- ( ph -> .* e. Y )   =>    |- ( ph -> .x. = ( .r ` R ) )
Theorem	srnginvld 13363	The involution function of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- R = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. ( *r ` ndx ) , .* >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> .x. e. X )   &    |- ( ph -> .* e. Y )   =>    |- ( ph -> .* = ( *r ` R ) )
Theorem	scandx 13364	Index value of the df-sca 13306 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- (Scalar ` ndx ) = 5
Theorem	scaid 13365	Utility theorem: index-independent form of scalar df-sca 13306. (Contributed by Mario Carneiro, 19-Jun-2014.)
|- Scalar = Slot (Scalar ` ndx )
Theorem	scaslid 13366	Slot property of Scalar. (Contributed by Jim Kingdon, 5-Feb-2023.)
|- (Scalar = Slot (Scalar ` ndx ) /\ (Scalar ` ndx ) e. NN )
Theorem	scandxnbasendx 13367	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 13368	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 13369	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 13370	Index value of the df-vsca 13307 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( .s ` ndx ) = 6
Theorem	vscaid 13371	Utility theorem: index-independent form of scalar product df-vsca 13307. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- .s = Slot ( .s ` ndx )
Theorem	vscandxnbasendx 13372	The slot for the scalar product is not the slot for the base set in an extensible structure. (Contributed by AV, 18-Oct-2024.)
|- ( .s ` ndx ) =/= ( Base ` ndx )
Theorem	vscandxnplusgndx 13373	The slot for the scalar product is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.)
|- ( .s ` ndx ) =/= ( +g ` ndx )
Theorem	vscandxnmulrndx 13374	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.)
|- ( .s ` ndx ) =/= ( .r ` ndx )
Theorem	vscandxnscandx 13375	The slot for the scalar product is not the slot for the scalar field in an extensible structure. (Contributed by AV, 18-Oct-2024.)
|- ( .s ` ndx ) =/= (Scalar ` ndx )
Theorem	vscaslid 13376	Slot property of .s. (Contributed by Jim Kingdon, 5-Feb-2023.)
|- ( .s = Slot ( .s ` ndx ) /\ ( .s ` ndx ) e. NN )
Theorem	lmodstrd 13377	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.)
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (Scalar ` ndx ) , F >. } u. { <. ( .s ` ndx ) , .x. >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. X )   &    |- ( ph -> F e. Y )   &    |- ( ph -> .x. e. Z )   =>    |- ( ph -> W Struct <. 1 , 6 >. )
Theorem	lmodbased 13378	The base set of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 6-Feb-2023.)
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (Scalar ` ndx ) , F >. } u. { <. ( .s ` ndx ) , .x. >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. X )   &    |- ( ph -> F e. Y )   &    |- ( ph -> .x. e. Z )   =>    |- ( ph -> B = ( Base ` W ) )
Theorem	lmodplusgd 13379	The additive operation of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 6-Feb-2023.)
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (Scalar ` ndx ) , F >. } u. { <. ( .s ` ndx ) , .x. >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. X )   &    |- ( ph -> F e. Y )   &    |- ( ph -> .x. e. Z )   =>    |- ( ph -> .+ = ( +g ` W ) )
Theorem	lmodscad 13380	The set of scalars of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 6-Feb-2023.)
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (Scalar ` ndx ) , F >. } u. { <. ( .s ` ndx ) , .x. >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. X )   &    |- ( ph -> F e. Y )   &    |- ( ph -> .x. e. Z )   =>    |- ( ph -> F = (Scalar ` W ) )
Theorem	lmodvscad 13381	The scalar product operation of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 7-Feb-2023.)
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (Scalar ` ndx ) , F >. } u. { <. ( .s ` ndx ) , .x. >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. X )   &    |- ( ph -> F e. Y )   &    |- ( ph -> .x. e. Z )   =>    |- ( ph -> .x. = ( .s ` W ) )
Theorem	ipndx 13382	Index value of the df-ip 13308 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( .i ` ndx ) = 8
Theorem	ipid 13383	Utility theorem: index-independent form of df-ip 13308. (Contributed by Mario Carneiro, 6-Oct-2013.)
|- .i = Slot ( .i ` ndx )
Theorem	ipslid 13384	Slot property of .i. (Contributed by Jim Kingdon, 7-Feb-2023.)
|- ( .i = Slot ( .i ` ndx ) /\ ( .i ` ndx ) e. NN )
Theorem	ipndxnbasendx 13385	The slot for the inner product is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.)
|- ( .i ` ndx ) =/= ( Base ` ndx )
Theorem	ipndxnplusgndx 13386	The slot for the inner product is not the slot for the group operation in an extensible structure. (Contributed by AV, 29-Oct-2024.)
|- ( .i ` ndx ) =/= ( +g ` ndx )
Theorem	ipndxnmulrndx 13387	The slot for the inner product is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 29-Oct-2024.)
|- ( .i ` ndx ) =/= ( .r ` ndx )
Theorem	slotsdifipndx 13388	The slot for the scalar is not the index of other slots. (Contributed by AV, 12-Nov-2024.)
|- ( ( .s ` ndx ) =/= ( .i ` ndx ) /\ (Scalar ` ndx ) =/= ( .i ` ndx ) )
Theorem	ipsstrd 13389	A constructed inner product space is a structure. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> .X. e. X )   &    |- ( ph -> S e. Y )   &    |- ( ph -> .x. e. Q )   &    |- ( ph -> I e. Z )   =>    |- ( ph -> A Struct <. 1 , 8 >. )
Theorem	ipsbased 13390	The base set of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> .X. e. X )   &    |- ( ph -> S e. Y )   &    |- ( ph -> .x. e. Q )   &    |- ( ph -> I e. Z )   =>    |- ( ph -> B = ( Base ` A ) )
Theorem	ipsaddgd 13391	The additive operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> .X. e. X )   &    |- ( ph -> S e. Y )   &    |- ( ph -> .x. e. Q )   &    |- ( ph -> I e. Z )   =>    |- ( ph -> .+ = ( +g ` A ) )
Theorem	ipsmulrd 13392	The multiplicative operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> .X. e. X )   &    |- ( ph -> S e. Y )   &    |- ( ph -> .x. e. Q )   &    |- ( ph -> I e. Z )   =>    |- ( ph -> .X. = ( .r ` A ) )
Theorem	ipsscad 13393	The set of scalars of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 8-Feb-2023.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> .X. e. X )   &    |- ( ph -> S e. Y )   &    |- ( ph -> .x. e. Q )   &    |- ( ph -> I e. Z )   =>    |- ( ph -> S = (Scalar ` A ) )
Theorem	ipsvscad 13394	The scalar product operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 8-Feb-2023.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> .X. e. X )   &    |- ( ph -> S e. Y )   &    |- ( ph -> .x. e. Q )   &    |- ( ph -> I e. Z )   =>    |- ( ph -> .x. = ( .s ` A ) )
Theorem	ipsipd 13395	The multiplicative operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 8-Feb-2023.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> .X. e. X )   &    |- ( ph -> S e. Y )   &    |- ( ph -> .x. e. Q )   &    |- ( ph -> I e. Z )   =>    |- ( ph -> I = ( .i ` A ) )
Theorem	ressscag 13396	Scalar is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.)
|- H = ( G ↾s A )   &    |- F = (Scalar ` G )   =>    |- ( ( G e. X /\ A e. V ) -> F = (Scalar ` H ) )
Theorem	ressvscag 13397	.s is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.)
|- H = ( G ↾s A )   &    |- .x. = ( .s ` G )   =>    |- ( ( G e. X /\ A e. V ) -> .x. = ( .s ` H ) )
Theorem	ressipg 13398	The inner product is unaffected by restriction. (Contributed by Thierry Arnoux, 16-Jun-2019.)
|- H = ( G ↾s A )   &    |- ., = ( .i ` G )   =>    |- ( ( G e. X /\ A e. V ) -> ., = ( .i ` H ) )
Theorem	tsetndx 13399	Index value of the df-tset 13309 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- (TopSet ` ndx ) = 9
Theorem	tsetid 13400	Utility theorem: index-independent form of df-tset 13309. (Contributed by NM, 20-Oct-2012.)
|- TopSet = Slot (TopSet ` ndx )