P. 136 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13501-13600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	srngbased 13501	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 13502	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 13503	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 13504	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 13505	Index value of the df-sca 13447 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- (Scalar ` ndx ) = 5
Theorem	scaid 13506	Utility theorem: index-independent form of scalar df-sca 13447. (Contributed by Mario Carneiro, 19-Jun-2014.)
|- Scalar = Slot (Scalar ` ndx )
Theorem	scaslid 13507	Slot property of Scalar. (Contributed by Jim Kingdon, 5-Feb-2023.)
|- (Scalar = Slot (Scalar ` ndx ) /\ (Scalar ` ndx ) e. NN )
Theorem	scandxnbasendx 13508	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 13509	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 13510	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 13511	Index value of the df-vsca 13448 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( .s ` ndx ) = 6
Theorem	vscaid 13512	Utility theorem: index-independent form of scalar product df-vsca 13448. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- .s = Slot ( .s ` ndx )
Theorem	vscandxnbasendx 13513	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 13514	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 13515	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 13516	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 13517	Slot property of .s. (Contributed by Jim Kingdon, 5-Feb-2023.)
|- ( .s = Slot ( .s ` ndx ) /\ ( .s ` ndx ) e. NN )
Theorem	lmodstrd 13518	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 13519	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 13520	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 13521	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 13522	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 13523	Index value of the df-ip 13449 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( .i ` ndx ) = 8
Theorem	ipid 13524	Utility theorem: index-independent form of df-ip 13449. (Contributed by Mario Carneiro, 6-Oct-2013.)
|- .i = Slot ( .i ` ndx )
Theorem	ipslid 13525	Slot property of .i. (Contributed by Jim Kingdon, 7-Feb-2023.)
|- ( .i = Slot ( .i ` ndx ) /\ ( .i ` ndx ) e. NN )
Theorem	ipndxnbasendx 13526	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 13527	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 13528	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 13529	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 13530	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 13531	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 13532	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 13533	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 13534	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 13535	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 13536	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 13537	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 13538	.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 13539	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 13540	Index value of the df-tset 13450 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- (TopSet ` ndx ) = 9
Theorem	tsetid 13541	Utility theorem: index-independent form of df-tset 13450. (Contributed by NM, 20-Oct-2012.)
|- TopSet = Slot (TopSet ` ndx )
Theorem	tsetslid 13542	Slot property of TopSet. (Contributed by Jim Kingdon, 9-Feb-2023.)
|- (TopSet = Slot (TopSet ` ndx ) /\ (TopSet ` ndx ) e. NN )
Theorem	tsetndxnn 13543	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 13544	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 13545	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 13546	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 13547	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 13548	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 13549	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 13550	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 13551	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 13552	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 13553	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 13554	Index value of the df-ple 13451 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.)
|- ( le ` ndx ) = ; 1 0
Theorem	pleid 13555	Utility theorem: self-referencing, index-independent form of df-ple 13451. (Contributed by NM, 9-Nov-2012.) (Revised by AV, 9-Sep-2021.)
|- le = Slot ( le ` ndx )
Theorem	pleslid 13556	Slot property of le. (Contributed by Jim Kingdon, 9-Feb-2023.)
|- ( le = Slot ( le ` ndx ) /\ ( le ` ndx ) e. NN )
Theorem	plendxnn 13557	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 13558	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 13559	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 13560	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 13561	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 13562	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 13563	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 13564	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 13565	Index value of the df-ocomp 13452 slot. (Contributed by Mario Carneiro, 25-Oct-2015.) (New usage is discouraged.)
|- ( oc ` ndx ) = ; 1 1
Theorem	ocid 13566	Utility theorem: index-independent form of df-ocomp 13452. (Contributed by Mario Carneiro, 25-Oct-2015.)
|- oc = Slot ( oc ` ndx )
Theorem	basendxnocndx 13567	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 13568	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 13569	Index value of the df-ds 13453 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( dist ` ndx ) = ; 1 2
Theorem	dsid 13570	Utility theorem: index-independent form of df-ds 13453. (Contributed by Mario Carneiro, 23-Dec-2013.)
|- dist = Slot ( dist ` ndx )
Theorem	dsslid 13571	Slot property of dist. (Contributed by Jim Kingdon, 6-May-2023.)
|- ( dist = Slot ( dist ` ndx ) /\ ( dist ` ndx ) e. NN )
Theorem	dsndxnn 13572	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
Theorem	basendxltdsndx 13573	The index of the slot for the base set is less then the index of the slot for the distance in an extensible structure. (Contributed by AV, 28-Oct-2024.)
|- ( Base ` ndx ) < ( dist ` ndx )
Theorem	dsndxnbasendx 13574	The slot for the distance is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 28-Oct-2024.)
|- ( dist ` ndx ) =/= ( Base ` ndx )
Theorem	dsndxnplusgndx 13575	The slot for the distance function is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.)
|- ( dist ` ndx ) =/= ( +g ` ndx )
Theorem	dsndxnmulrndx 13576	The slot for the distance function is not the slot for the ring multiplication operation in an extensible structure. (Contributed by AV, 31-Oct-2024.)
|- ( dist ` ndx ) =/= ( .r ` ndx )
Theorem	slotsdnscsi 13577	The slots Scalar, .s and .i are different from the slot dist. (Contributed by AV, 29-Oct-2024.)
|- ( ( dist ` ndx ) =/= (Scalar ` ndx ) /\ ( dist ` ndx ) =/= ( .s ` ndx ) /\ ( dist ` ndx ) =/= ( .i ` ndx ) )
Theorem	dsndxntsetndx 13578	The slot for the distance function is not the slot for the topology in an extensible structure. (Contributed by AV, 29-Oct-2024.)
|- ( dist ` ndx ) =/= (TopSet ` ndx )
Theorem	slotsdifdsndx 13579	The index of the slot for the distance is not the index of other slots. (Contributed by AV, 11-Nov-2024.)
|- ( ( *r ` ndx ) =/= ( dist ` ndx ) /\ ( le ` ndx ) =/= ( dist ` ndx ) )
Theorem	unifndx 13580	Index value of the df-unif 13454 slot. (Contributed by Thierry Arnoux, 17-Dec-2017.) (New usage is discouraged.)
|- ( UnifSet ` ndx ) = ; 1 3
Theorem	unifid 13581	Utility theorem: index-independent form of df-unif 13454. (Contributed by Thierry Arnoux, 17-Dec-2017.)
|- UnifSet = Slot ( UnifSet ` ndx )
Theorem	unifndxnn 13582	The index of the slot for the uniform set in an extensible structure is a positive integer. (Contributed by AV, 28-Oct-2024.)
|- ( UnifSet ` ndx ) e. NN
Theorem	basendxltunifndx 13583	The index of the slot for the base set is less then the index of the slot for the uniform set in an extensible structure. (Contributed by AV, 28-Oct-2024.)
|- ( Base ` ndx ) < ( UnifSet ` ndx )
Theorem	unifndxnbasendx 13584	The slot for the uniform set is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.)
|- ( UnifSet ` ndx ) =/= ( Base ` ndx )
Theorem	unifndxntsetndx 13585	The slot for the uniform set is not the slot for the topology in an extensible structure. (Contributed by AV, 28-Oct-2024.)
|- ( UnifSet ` ndx ) =/= (TopSet ` ndx )
Theorem	slotsdifunifndx 13586	The index of the slot for the uniform set is not the index of other slots. (Contributed by AV, 10-Nov-2024.)
|- ( ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) /\ ( *r ` ndx ) =/= ( UnifSet ` ndx ) ) /\ ( ( le ` ndx ) =/= ( UnifSet ` ndx ) /\ ( dist ` ndx ) =/= ( UnifSet ` ndx ) ) )
Theorem	homndx 13587	Index value of the df-hom 13455 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.)
|- ( Hom ` ndx ) = ; 1 4
Theorem	homid 13588	Utility theorem: index-independent form of df-hom 13455. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- Hom = Slot ( Hom ` ndx )
Theorem	homslid 13589	Slot property of Hom. (Contributed by Jim Kingdon, 20-Mar-2025.)
|- ( Hom = Slot ( Hom ` ndx ) /\ ( Hom ` ndx ) e. NN )
Theorem	ccondx 13590	Index value of the df-cco 13456 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.)
|- (comp ` ndx ) = ; 1 5
Theorem	ccoid 13591	Utility theorem: index-independent form of df-cco 13456. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- comp = Slot (comp ` ndx )
Theorem	ccoslid 13592	Slot property of comp. (Contributed by Jim Kingdon, 20-Mar-2025.)
|- (comp = Slot (comp ` ndx ) /\ (comp ` ndx ) e. NN )
6.1.3  Various definitions used by the structure product
Syntax	crest 13593	Extend class notation with the function returning a subspace topology.
class ↾t
Syntax	ctopn 13594	Extend class notation with the topology extractor function.
class TopOpen
Definition	df-rest 13595*	Function returning the subspace topology induced by the topology y and the set x. (Contributed by FL, 20-Sep-2010.) (Revised by Mario Carneiro, 1-May-2015.)
|- ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
Definition	df-topn 13596	Define the topology extractor function. This differs from df-tset 13450 when a structure has been restricted using df-iress 13360; in this case the TopSet component will still have a topology over the larger set, and this function fixes this by restricting the topology as well. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- TopOpen = ( w e. _V |-> ( (TopSet ` w ) ↾t ( Base ` w ) ) )
Theorem	restfn 13597	The subspace topology operator is a function on pairs. (Contributed by Mario Carneiro, 1-May-2015.)
|- ↾t Fn ( _V X. _V )
Theorem	topnfn 13598	The topology extractor function is a function on the universe. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- TopOpen Fn _V
Theorem	restval 13599*	The subspace topology induced by the topology J on the set A. (Contributed by FL, 20-Sep-2010.) (Revised by Mario Carneiro, 1-May-2015.)
|- ( ( J e. V /\ A e. W ) -> ( J ↾t A ) = ran ( x e. J |-> ( x i^i A ) ) )
Theorem	elrest 13600*	The predicate "is an open set of a subspace topology". (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
|- ( ( J e. V /\ B e. W ) -> ( A e. ( J ↾t B ) <-> E. x e. J A = ( x i^i B ) ) )