P. 133 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13201-13300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	2strstrg 13201	A constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.) Use 2strstrndx 13200 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 13202	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 13203	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 13204	A constructed two-slot structure. Version of 2strstrg 13201 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 13205	The base set of a constructed two-slot structure. Version of 2strbasg 13202 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 13206	The other slot of a constructed two-slot structure. Version of 2stropg 13203 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 13207	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 13208	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 13209	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 13210	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 13211	+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 13212	Index value of the df-mulr 13173 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( .r ` ndx ) = 3
Theorem	mulridx 13213	Utility theorem: index-independent form of df-mulr 13173. (Contributed by Mario Carneiro, 8-Jun-2013.)
|- .r = Slot ( .r ` ndx )
Theorem	mulrslid 13214	Slot property of .r. (Contributed by Jim Kingdon, 3-Feb-2023.)
|- ( .r = Slot ( .r ` ndx ) /\ ( .r ` ndx ) e. NN )
Theorem	plusgndxnmulrndx 13215	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 13216	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 13217	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 13218	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 13219	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 13220	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 13221	Index value of the df-starv 13174 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( *r ` ndx ) = 4
Theorem	starvid 13222	Utility theorem: index-independent form of df-starv 13174. (Contributed by Mario Carneiro, 6-Oct-2013.)
|- *r = Slot ( *r ` ndx )
Theorem	starvslid 13223	Slot property of *r. (Contributed by Jim Kingdon, 4-Feb-2023.)
|- ( *r = Slot ( *r ` ndx ) /\ ( *r ` ndx ) e. NN )
Theorem	starvndxnbasendx 13224	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 13225	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 13226	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 13227	.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 13228	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 13229	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 13230	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 13231	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 13232	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 13233	Index value of the df-sca 13175 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- (Scalar ` ndx ) = 5
Theorem	scaid 13234	Utility theorem: index-independent form of scalar df-sca 13175. (Contributed by Mario Carneiro, 19-Jun-2014.)
|- Scalar = Slot (Scalar ` ndx )
Theorem	scaslid 13235	Slot property of Scalar. (Contributed by Jim Kingdon, 5-Feb-2023.)
|- (Scalar = Slot (Scalar ` ndx ) /\ (Scalar ` ndx ) e. NN )
Theorem	scandxnbasendx 13236	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 13237	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 13238	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 13239	Index value of the df-vsca 13176 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( .s ` ndx ) = 6
Theorem	vscaid 13240	Utility theorem: index-independent form of scalar product df-vsca 13176. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- .s = Slot ( .s ` ndx )
Theorem	vscandxnbasendx 13241	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 13242	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 13243	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 13244	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 13245	Slot property of .s. (Contributed by Jim Kingdon, 5-Feb-2023.)
|- ( .s = Slot ( .s ` ndx ) /\ ( .s ` ndx ) e. NN )
Theorem	lmodstrd 13246	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 13247	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 13248	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 13249	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 13250	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 13251	Index value of the df-ip 13177 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( .i ` ndx ) = 8
Theorem	ipid 13252	Utility theorem: index-independent form of df-ip 13177. (Contributed by Mario Carneiro, 6-Oct-2013.)
|- .i = Slot ( .i ` ndx )
Theorem	ipslid 13253	Slot property of .i. (Contributed by Jim Kingdon, 7-Feb-2023.)
|- ( .i = Slot ( .i ` ndx ) /\ ( .i ` ndx ) e. NN )
Theorem	ipndxnbasendx 13254	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 13255	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 13256	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 13257	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 13258	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 13259	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 13260	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 13261	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 13262	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 13263	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 13264	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 13265	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 13266	.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 13267	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 13268	Index value of the df-tset 13178 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- (TopSet ` ndx ) = 9
Theorem	tsetid 13269	Utility theorem: index-independent form of df-tset 13178. (Contributed by NM, 20-Oct-2012.)
|- TopSet = Slot (TopSet ` ndx )
Theorem	tsetslid 13270	Slot property of TopSet. (Contributed by Jim Kingdon, 9-Feb-2023.)
|- (TopSet = Slot (TopSet ` ndx ) /\ (TopSet ` ndx ) e. NN )
Theorem	tsetndxnn 13271	The index of the slot for the group operation in an extensible structure is a positive integer. (Contributed by AV, 31-Oct-2024.)
|- (TopSet ` ndx ) e. NN
Theorem	basendxlttsetndx 13272	The index of the slot for the base set is less then the index of the slot for the topology in an extensible structure. (Contributed by AV, 31-Oct-2024.)
|- ( Base ` ndx ) < (TopSet ` ndx )
Theorem	tsetndxnbasendx 13273	The slot for the topology is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 31-Oct-2024.)
|- (TopSet ` ndx ) =/= ( Base ` ndx )
Theorem	tsetndxnplusgndx 13274	The slot for the topology is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.)
|- (TopSet ` ndx ) =/= ( +g ` ndx )
Theorem	tsetndxnmulrndx 13275	The slot for the topology is not the slot for the ring multiplication operation in an extensible structure. (Contributed by AV, 31-Oct-2024.)
|- (TopSet ` ndx ) =/= ( .r ` ndx )
Theorem	tsetndxnstarvndx 13276	The slot for the topology is not the slot for the involution in an extensible structure. (Contributed by AV, 11-Nov-2024.)
|- (TopSet ` ndx ) =/= ( *r ` ndx )
Theorem	slotstnscsi 13277	The slots Scalar, .s and .i are different from the slot TopSet. (Contributed by AV, 29-Oct-2024.)
|- ( (TopSet ` ndx ) =/= (Scalar ` ndx ) /\ (TopSet ` ndx ) =/= ( .s ` ndx ) /\ (TopSet ` ndx ) =/= ( .i ` ndx ) )
Theorem	topgrpstrd 13278	A constructed topological group is a structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.)
|- W = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (TopSet ` ndx ) , J >. }   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> J e. X )   =>    |- ( ph -> W Struct <. 1 , 9 >. )
Theorem	topgrpbasd 13279	The base set of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.)
|- W = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (TopSet ` ndx ) , J >. }   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> J e. X )   =>    |- ( ph -> B = ( Base ` W ) )
Theorem	topgrpplusgd 13280	The additive operation of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.)
|- W = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (TopSet ` ndx ) , J >. }   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> J e. X )   =>    |- ( ph -> .+ = ( +g ` W ) )
Theorem	topgrptsetd 13281	The topology of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.)
|- W = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (TopSet ` ndx ) , J >. }   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> J e. X )   =>    |- ( ph -> J = (TopSet ` W ) )
Theorem	plendx 13282	Index value of the df-ple 13179 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.)
|- ( le ` ndx ) = ; 1 0
Theorem	pleid 13283	Utility theorem: self-referencing, index-independent form of df-ple 13179. (Contributed by NM, 9-Nov-2012.) (Revised by AV, 9-Sep-2021.)
|- le = Slot ( le ` ndx )
Theorem	pleslid 13284	Slot property of le. (Contributed by Jim Kingdon, 9-Feb-2023.)
|- ( le = Slot ( le ` ndx ) /\ ( le ` ndx ) e. NN )
Theorem	plendxnn 13285	The index value of the order slot 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, 30-Oct-2024.)
|- ( le ` ndx ) e. NN
Theorem	basendxltplendx 13286	The index value of the Base slot is less than the index value of the le slot. (Contributed by AV, 30-Oct-2024.)
|- ( Base ` ndx ) < ( le ` ndx )
Theorem	plendxnbasendx 13287	The slot for the order is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 30-Oct-2024.)
|- ( le ` ndx ) =/= ( Base ` ndx )
Theorem	plendxnplusgndx 13288	The slot for the "less than or equal to" ordering is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.)
|- ( le ` ndx ) =/= ( +g ` ndx )
Theorem	plendxnmulrndx 13289	The slot for the "less than or equal to" ordering is not the slot for the ring multiplication operation in an extensible structure. (Contributed by AV, 1-Nov-2024.)
|- ( le ` ndx ) =/= ( .r ` ndx )
Theorem	plendxnscandx 13290	The slot for the "less than or equal to" ordering is not the slot for the scalar in an extensible structure. (Contributed by AV, 1-Nov-2024.)
|- ( le ` ndx ) =/= (Scalar ` ndx )
Theorem	plendxnvscandx 13291	The slot for the "less than or equal to" ordering is not the slot for the scalar product in an extensible structure. (Contributed by AV, 1-Nov-2024.)
|- ( le ` ndx ) =/= ( .s ` ndx )
Theorem	slotsdifplendx 13292	The index of the slot for the distance is not the index of other slots. (Contributed by AV, 11-Nov-2024.)
|- ( ( *r ` ndx ) =/= ( le ` ndx ) /\ (TopSet ` ndx ) =/= ( le ` ndx ) )
Theorem	ocndx 13293	Index value of the df-ocomp 13180 slot. (Contributed by Mario Carneiro, 25-Oct-2015.) (New usage is discouraged.)
|- ( oc ` ndx ) = ; 1 1
Theorem	ocid 13294	Utility theorem: index-independent form of df-ocomp 13180. (Contributed by Mario Carneiro, 25-Oct-2015.)
|- oc = Slot ( oc ` ndx )
Theorem	basendxnocndx 13295	The slot for the orthocomplementation is not the slot for the base set in an extensible structure. (Contributed by AV, 11-Nov-2024.)
|- ( Base ` ndx ) =/= ( oc ` ndx )
Theorem	plendxnocndx 13296	The slot for the orthocomplementation is not the slot for the order in an extensible structure. (Contributed by AV, 11-Nov-2024.)
|- ( le ` ndx ) =/= ( oc ` ndx )
Theorem	dsndx 13297	Index value of the df-ds 13181 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( dist ` ndx ) = ; 1 2
Theorem	dsid 13298	Utility theorem: index-independent form of df-ds 13181. (Contributed by Mario Carneiro, 23-Dec-2013.)
|- dist = Slot ( dist ` ndx )
Theorem	dsslid 13299	Slot property of dist. (Contributed by Jim Kingdon, 6-May-2023.)
|- ( dist = Slot ( dist ` ndx ) /\ ( dist ` ndx ) e. NN )
Theorem	dsndxnn 13300	The index of the slot for the distance in an extensible structure is a positive integer. (Contributed by AV, 28-Oct-2024.)
|- ( dist ` ndx ) e. NN