P. 127 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12601-12700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	starvslid 12601	Slot property of *r. (Contributed by Jim Kingdon, 4-Feb-2023.)
|- ( *r = Slot ( *r ` ndx ) /\ ( *r ` ndx ) e. NN )
Theorem	starvndxnbasendx 12602	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 12603	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 12604	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 12605	.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 12606	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 12607	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 12608	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 12609	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 12610	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 12611	Index value of the df-sca 12554 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- (Scalar ` ndx ) = 5
Theorem	scaid 12612	Utility theorem: index-independent form of scalar df-sca 12554. (Contributed by Mario Carneiro, 19-Jun-2014.)
|- Scalar = Slot (Scalar ` ndx )
Theorem	scaslid 12613	Slot property of Scalar. (Contributed by Jim Kingdon, 5-Feb-2023.)
|- (Scalar = Slot (Scalar ` ndx ) /\ (Scalar ` ndx ) e. NN )
Theorem	scandxnbasendx 12614	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 12615	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 12616	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 12617	Index value of the df-vsca 12555 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( .s ` ndx ) = 6
Theorem	vscaid 12618	Utility theorem: index-independent form of scalar product df-vsca 12555. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- .s = Slot ( .s ` ndx )
Theorem	vscandxnbasendx 12619	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 12620	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 12621	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 12622	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 12623	Slot property of .s. (Contributed by Jim Kingdon, 5-Feb-2023.)
|- ( .s = Slot ( .s ` ndx ) /\ ( .s ` ndx ) e. NN )
Theorem	lmodstrd 12624	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 12625	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 12626	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 12627	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 12628	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 12629	Index value of the df-ip 12556 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( .i ` ndx ) = 8
Theorem	ipid 12630	Utility theorem: index-independent form of df-ip 12556. (Contributed by Mario Carneiro, 6-Oct-2013.)
|- .i = Slot ( .i ` ndx )
Theorem	ipslid 12631	Slot property of .i. (Contributed by Jim Kingdon, 7-Feb-2023.)
|- ( .i = Slot ( .i ` ndx ) /\ ( .i ` ndx ) e. NN )
Theorem	ipndxnbasendx 12632	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 12633	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 12634	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 12635	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 12636	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 12637	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 12638	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 12639	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 12640	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 12641	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 12642	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 12643	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 12644	.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 12645	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 12646	Index value of the df-tset 12557 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- (TopSet ` ndx ) = 9
Theorem	tsetid 12647	Utility theorem: index-independent form of df-tset 12557. (Contributed by NM, 20-Oct-2012.)
|- TopSet = Slot (TopSet ` ndx )
Theorem	tsetslid 12648	Slot property of TopSet. (Contributed by Jim Kingdon, 9-Feb-2023.)
|- (TopSet = Slot (TopSet ` ndx ) /\ (TopSet ` ndx ) e. NN )
Theorem	tsetndxnn 12649	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 12650	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 12651	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 12652	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 12653	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 12654	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 12655	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 12656	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 12657	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 12658	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 12659	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 12660	Index value of the df-ple 12558 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.)
|- ( le ` ndx ) = ; 1 0
Theorem	pleid 12661	Utility theorem: self-referencing, index-independent form of df-ple 12558. (Contributed by NM, 9-Nov-2012.) (Revised by AV, 9-Sep-2021.)
|- le = Slot ( le ` ndx )
Theorem	pleslid 12662	Slot property of le. (Contributed by Jim Kingdon, 9-Feb-2023.)
|- ( le = Slot ( le ` ndx ) /\ ( le ` ndx ) e. NN )
Theorem	plendxnn 12663	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 12664	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 12665	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 12666	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 12667	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 12668	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 12669	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 12670	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	dsndx 12671	Index value of the df-ds 12560 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( dist ` ndx ) = ; 1 2
Theorem	dsid 12672	Utility theorem: index-independent form of df-ds 12560. (Contributed by Mario Carneiro, 23-Dec-2013.)
|- dist = Slot ( dist ` ndx )
Theorem	dsslid 12673	Slot property of dist. (Contributed by Jim Kingdon, 6-May-2023.)
|- ( dist = Slot ( dist ` ndx ) /\ ( dist ` ndx ) e. NN )
Theorem	dsndxnn 12674	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 12675	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 12676	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 12677	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 12678	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 12679	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 12680	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 12681	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 12682	Index value of the df-unif 12561 slot. (Contributed by Thierry Arnoux, 17-Dec-2017.) (New usage is discouraged.)
|- ( UnifSet ` ndx ) = ; 1 3
Theorem	unifid 12683	Utility theorem: index-independent form of df-unif 12561. (Contributed by Thierry Arnoux, 17-Dec-2017.)
|- UnifSet = Slot ( UnifSet ` ndx )
Theorem	unifndxnn 12684	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 12685	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 12686	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 12687	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 12688	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	homid 12689	Utility theorem: index-independent form of df-hom 12562. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- Hom = Slot ( Hom ` ndx )
Theorem	homslid 12690	Slot property of Hom. (Contributed by Jim Kingdon, 20-Mar-2025.)
|- ( Hom = Slot ( Hom ` ndx ) /\ ( Hom ` ndx ) e. NN )
Theorem	ccoid 12691	Utility theorem: index-independent form of df-cco 12563. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- comp = Slot (comp ` ndx )
Theorem	ccoslid 12692	Slot property of comp. (Contributed by Jim Kingdon, 20-Mar-2025.)
|- (comp = Slot (comp ` ndx ) /\ (comp ` ndx ) e. NN )
6.1.3  Definition of the structure product
Syntax	crest 12693	Extend class notation with the function returning a subspace topology.
class ↾t
Syntax	ctopn 12694	Extend class notation with the topology extractor function.
class TopOpen
Definition	df-rest 12695*	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 12696	Define the topology extractor function. This differs from df-tset 12557 when a structure has been restricted using df-iress 12472; 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 12697	The subspace topology operator is a function on pairs. (Contributed by Mario Carneiro, 1-May-2015.)
|- ↾t Fn ( _V X. _V )
Theorem	topnfn 12698	The topology extractor function is a function on the universe. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- TopOpen Fn _V
Theorem	restval 12699*	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 12700*	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 ) ) )