P. 128 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12701-12800   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	csca 12701	Extend class notation with scalar field.
class Scalar
Syntax	cvsca 12702	Extend class notation with scalar product.
class .s
Syntax	cip 12703	Extend class notation with Hermitian form (inner product).
class .i
Syntax	cts 12704	Extend class notation with the topology component of a topological space.
class TopSet
Syntax	cple 12705	Extend class notation with "less than or equal to" for posets.
class le
Syntax	coc 12706	Extend class notation with the class of orthocomplementation extractors.
class oc
Syntax	cds 12707	Extend class notation with the metric space distance function.
class dist
Syntax	cunif 12708	Extend class notation with the uniform structure.
class UnifSet
Syntax	chom 12709	Extend class notation with the hom-set structure.
class Hom
Syntax	cco 12710	Extend class notation with the composition operation.
class comp
Definition	df-plusg 12711	Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- +g = Slot 2
Definition	df-mulr 12712	Define ring multiplication. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- .r = Slot 3
Definition	df-starv 12713	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 12714	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 12715	Define scalar product. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- .s = Slot 6
Definition	df-ip 12716	Define Hermitian form (inner product). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- .i = Slot 8
Definition	df-tset 12717	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 12718	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 12719	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 12720	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 12721	Define the uniform structure component of a uniform space. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- UnifSet = Slot ; 1 3
Definition	df-hom 12722	Define the hom-set component of a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- Hom = Slot ; 1 4
Definition	df-cco 12723	Define the composition operation of a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- comp = Slot ; 1 5
Theorem	strleund 12724	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 12725	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 12726	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 12727	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 12728	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 12729	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 12730	Index value of the df-plusg 12711 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( +g ` ndx ) = 2
Theorem	plusgid 12731	Utility theorem: index-independent form of df-plusg 12711. (Contributed by NM, 20-Oct-2012.)
|- +g = Slot ( +g ` ndx )
Theorem	plusgndxnn 12732	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 12733	Slot property of +g. (Contributed by Jim Kingdon, 3-Feb-2023.)
|- ( +g = Slot ( +g ` ndx ) /\ ( +g ` ndx ) e. NN )
Theorem	basendxltplusgndx 12734	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 12735	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 12736	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 12737	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 12738	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 12739	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 12740	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 12741	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 12742	A constructed two-slot structure. Version of 2strstrg 12739 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 12743	The base set of a constructed two-slot structure. Version of 2strbasg 12740 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 12744	The other slot of a constructed two-slot structure. Version of 2stropg 12741 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 12745	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 12746	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 12747	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 12748	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 12749	+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 12750	Index value of the df-mulr 12712 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( .r ` ndx ) = 3
Theorem	mulridx 12751	Utility theorem: index-independent form of df-mulr 12712. (Contributed by Mario Carneiro, 8-Jun-2013.)
|- .r = Slot ( .r ` ndx )
Theorem	mulrslid 12752	Slot property of .r. (Contributed by Jim Kingdon, 3-Feb-2023.)
|- ( .r = Slot ( .r ` ndx ) /\ ( .r ` ndx ) e. NN )
Theorem	plusgndxnmulrndx 12753	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 12754	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 12755	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 12756	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 12757	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 12758	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 12759	Index value of the df-starv 12713 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( *r ` ndx ) = 4
Theorem	starvid 12760	Utility theorem: index-independent form of df-starv 12713. (Contributed by Mario Carneiro, 6-Oct-2013.)
|- *r = Slot ( *r ` ndx )
Theorem	starvslid 12761	Slot property of *r. (Contributed by Jim Kingdon, 4-Feb-2023.)
|- ( *r = Slot ( *r ` ndx ) /\ ( *r ` ndx ) e. NN )
Theorem	starvndxnbasendx 12762	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 12763	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 12764	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 12765	.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 12766	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 12767	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 12768	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 12769	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 12770	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 12771	Index value of the df-sca 12714 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- (Scalar ` ndx ) = 5
Theorem	scaid 12772	Utility theorem: index-independent form of scalar df-sca 12714. (Contributed by Mario Carneiro, 19-Jun-2014.)
|- Scalar = Slot (Scalar ` ndx )
Theorem	scaslid 12773	Slot property of Scalar. (Contributed by Jim Kingdon, 5-Feb-2023.)
|- (Scalar = Slot (Scalar ` ndx ) /\ (Scalar ` ndx ) e. NN )
Theorem	scandxnbasendx 12774	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 12775	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 12776	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 12777	Index value of the df-vsca 12715 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( .s ` ndx ) = 6
Theorem	vscaid 12778	Utility theorem: index-independent form of scalar product df-vsca 12715. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- .s = Slot ( .s ` ndx )
Theorem	vscandxnbasendx 12779	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 12780	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 12781	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 12782	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 12783	Slot property of .s. (Contributed by Jim Kingdon, 5-Feb-2023.)
|- ( .s = Slot ( .s ` ndx ) /\ ( .s ` ndx ) e. NN )
Theorem	lmodstrd 12784	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 12785	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 12786	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 12787	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 12788	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 12789	Index value of the df-ip 12716 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( .i ` ndx ) = 8
Theorem	ipid 12790	Utility theorem: index-independent form of df-ip 12716. (Contributed by Mario Carneiro, 6-Oct-2013.)
|- .i = Slot ( .i ` ndx )
Theorem	ipslid 12791	Slot property of .i. (Contributed by Jim Kingdon, 7-Feb-2023.)
|- ( .i = Slot ( .i ` ndx ) /\ ( .i ` ndx ) e. NN )
Theorem	ipndxnbasendx 12792	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 12793	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 12794	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 12795	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 12796	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 12797	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 12798	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 12799	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 12800	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 ) )