P. 161 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 16001-16100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rngbase 16001	The base set 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 -> B = ( Base ` R ) )
Theorem	rngplusg 16002	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. >. }   =>    |- ( .+ e. V -> .+ = ( +g ` R ) )
Theorem	rngmulr 16003	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. >. }   =>    |- ( .x. e. V -> .x. = ( .r ` R ) )
Theorem	starvndx 16004	Index value of the df-starv 15956 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( *r ` ndx ) = 4
Theorem	starvid 16005	Utility theorem: index-independent form of df-starv 15956. (Contributed by Mario Carneiro, 6-Oct-2013.)
|- *r = Slot ( *r ` ndx )
Theorem	ressmulr 16006	.r is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- S = ( R ↾s A )   &    |- .x. = ( .r ` R )   =>    |- ( A e. V -> .x. = ( .r ` S ) )
Theorem	ressstarv 16007	*r is unaffected by restriction. (Contributed by Mario Carneiro, 9-Oct-2015.)
|- S = ( R ↾s A )   &    |- .* = ( *r ` R )   =>    |- ( A e. V -> .* = ( *r ` S ) )
Theorem	srngfn 16008	A constructed star ring is a function with domain contained in 1 thru 4. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- R = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. ( *r ` ndx ) , .* >. } )   =>    |- R Struct <. 1 , 4 >.
Theorem	srngbase 16009	The base set of a constructed star ring. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Mario Carneiro, 6-May-2015.)
|- R = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. ( *r ` ndx ) , .* >. } )   =>    |- ( B e. X -> B = ( Base ` R ) )
Theorem	srngplusg 16010	The addition 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 ) , .* >. } )   =>    |- ( .+ e. X -> .+ = ( +g ` R ) )
Theorem	srngmulr 16011	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 ) , .* >. } )   =>    |- ( .x. e. X -> .x. = ( .r ` R ) )
Theorem	srnginvl 16012	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 ) , .* >. } )   =>    |- ( .* e. X -> .* = ( *r ` R ) )
Theorem	scandx 16013	Index value of the df-sca 15957 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- (Scalar ` ndx ) = 5
Theorem	scaid 16014	Utility theorem: index-independent form of scalar df-sca 15957. (Contributed by Mario Carneiro, 19-Jun-2014.)
|- Scalar = Slot (Scalar ` ndx )
Theorem	vscandx 16015	Index value of the df-vsca 15958 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( .s ` ndx ) = 6
Theorem	vscaid 16016	Utility theorem: index-independent form of scalar product df-vsca 15958. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- .s = Slot ( .s ` ndx )
Theorem	lmodstr 16017	A constructed left module or left vector space is a function. (Contributed by Mario Carneiro, 1-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.)
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (Scalar ` ndx ) , F >. } u. { <. ( .s ` ndx ) , .x. >. } )   =>    |- W Struct <. 1 , 6 >.
Theorem	lmodbase 16018	The base set of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.)
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (Scalar ` ndx ) , F >. } u. { <. ( .s ` ndx ) , .x. >. } )   =>    |- ( B e. X -> B = ( Base ` W ) )
Theorem	lmodplusg 16019	The additive operation of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.)
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (Scalar ` ndx ) , F >. } u. { <. ( .s ` ndx ) , .x. >. } )   =>    |- ( .+ e. X -> .+ = ( +g ` W ) )
Theorem	lmodsca 16020	The set of scalars of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.)
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (Scalar ` ndx ) , F >. } u. { <. ( .s ` ndx ) , .x. >. } )   =>    |- ( F e. X -> F = (Scalar ` W ) )
Theorem	lmodvsca 16021	The scalar product operation of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.)
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (Scalar ` ndx ) , F >. } u. { <. ( .s ` ndx ) , .x. >. } )   =>    |- ( .x. e. X -> .x. = ( .s ` W ) )
Theorem	ipndx 16022	Index value of the df-ip 15959 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( .i ` ndx ) = 8
Theorem	ipid 16023	Utility theorem: index-independent form of df-ip 15959. (Contributed by Mario Carneiro, 6-Oct-2013.)
|- .i = Slot ( .i ` ndx )
Theorem	ipsstr 16024	Lemma to shorten proofs of ipsbase 16025 through ipsvsca 16029. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } )   =>    |- A Struct <. 1 , 8 >.
Theorem	ipsbase 16025	The base set of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } )   =>    |- ( B e. V -> B = ( Base ` A ) )
Theorem	ipsaddg 16026	The additive operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } )   =>    |- ( .+ e. V -> .+ = ( +g ` A ) )
Theorem	ipsmulr 16027	The multiplicative operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } )   =>    |- ( .X. e. V -> .X. = ( .r ` A ) )
Theorem	ipssca 16028	The set of scalars of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } )   =>    |- ( S e. V -> S = (Scalar ` A ) )
Theorem	ipsvsca 16029	The scalar product operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } )   =>    |- ( .x. e. V -> .x. = ( .s ` A ) )
Theorem	ipsip 16030	The multiplicative operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } )   =>    |- ( I e. V -> I = ( .i ` A ) )
Theorem	resssca 16031	Scalar is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.)
|- H = ( G ↾s A )   &    |- F = (Scalar ` G )   =>    |- ( A e. V -> F = (Scalar ` H ) )
Theorem	ressvsca 16032	.s is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.)
|- H = ( G ↾s A )   &    |- .x. = ( .s ` G )   =>    |- ( A e. V -> .x. = ( .s ` H ) )
Theorem	ressip 16033	The inner product is unaffected by restriction. (Contributed by Thierry Arnoux, 16-Jun-2019.)
|- H = ( G ↾s A )   &    |- ., = ( .i ` G )   =>    |- ( A e. V -> ., = ( .i ` H ) )
Theorem	phlstr 16034	A constructed pre-Hilbert space is a structure. Starting from lmodstr 16017 (which has 4 members), we chain strleun 15972 once more, adding an ordered pair to the function, to get all 5 members. (Contributed by Mario Carneiro, 1-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.)
|- H = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (Scalar ` ndx ) , T >. } u. { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } )   =>    |- H Struct <. 1 , 8 >.
Theorem	phlbase 16035	The base set of a constructed pre-Hilbert space. (Contributed by Mario Carneiro, 6-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.)
|- H = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (Scalar ` ndx ) , T >. } u. { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } )   =>    |- ( B e. X -> B = ( Base ` H ) )
Theorem	phlplusg 16036	The additive operation of a constructed pre-Hilbert space. (Contributed by Mario Carneiro, 6-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.)
|- H = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (Scalar ` ndx ) , T >. } u. { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } )   =>    |- ( .+ e. X -> .+ = ( +g ` H ) )
Theorem	phlsca 16037	The ring of scalars of a constructed pre-Hilbert space. (Contributed by Mario Carneiro, 6-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.)
|- H = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (Scalar ` ndx ) , T >. } u. { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } )   =>    |- ( T e. X -> T = (Scalar ` H ) )
Theorem	phlvsca 16038	The scalar product operation of a constructed pre-Hilbert space. (Contributed by Mario Carneiro, 6-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.)
|- H = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (Scalar ` ndx ) , T >. } u. { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } )   =>    |- ( .x. e. X -> .x. = ( .s ` H ) )
Theorem	phlip 16039	The inner product (Hermitian form) operation of a constructed pre-Hilbert space. (Contributed by Mario Carneiro, 6-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.)
|- H = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (Scalar ` ndx ) , T >. } u. { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } )   =>    |- ( ., e. X -> ., = ( .i ` H ) )
Theorem	tsetndx 16040	Index value of the df-tset 15960 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- (TopSet ` ndx ) = 9
Theorem	tsetid 16041	Utility theorem: index-independent form of df-tset 15960. (Contributed by NM, 20-Oct-2012.)
|- TopSet = Slot (TopSet ` ndx )
Theorem	topgrpstr 16042	A constructed topological group is a structure. (Contributed by Mario Carneiro, 29-Aug-2015.)
|- W = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (TopSet ` ndx ) , J >. }   =>    |- W Struct <. 1 , 9 >.
Theorem	topgrpbas 16043	The base set of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.)
|- W = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (TopSet ` ndx ) , J >. }   =>    |- ( B e. X -> B = ( Base ` W ) )
Theorem	topgrpplusg 16044	The additive operation of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.)
|- W = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (TopSet ` ndx ) , J >. }   =>    |- ( .+ e. X -> .+ = ( +g ` W ) )
Theorem	topgrptset 16045	The topology of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.)
|- W = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (TopSet ` ndx ) , J >. }   =>    |- ( J e. X -> J = (TopSet ` W ) )
Theorem	resstset 16046	TopSet is unaffected by restriction. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- H = ( G ↾s A )   &    |- J = (TopSet ` G )   =>    |- ( A e. V -> J = (TopSet ` H ) )
Theorem	plendx 16047	Index value of the df-ple 15961 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.)
|- ( le ` ndx ) = ; 1 0
Theorem	plendxOLD 16048	Obsolete version of df-ple 15961 as of 9-Sep-2021. (Contributed by Mario Carneiro, 14-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( le ` ndx ) = 10
Theorem	pleid 16049	Utility theorem: self-referencing, index-independent form of df-ple 15961. (Contributed by NM, 9-Nov-2012.) (Revised by AV, 9-Sep-2021.)
|- le = Slot ( le ` ndx )
Theorem	pleidOLD 16050	Obsolete version of otpsstr 16051 as of 9-Sep-2021. (Contributed by Mario Carneiro, 9-Nov-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- le = Slot ( le ` ndx )
Theorem	otpsstr 16051	Functionality of a topological ordered space. (Contributed by Mario Carneiro, 12-Nov-2015.) (Revised by AV, 9-Sep-2021.)
|- K = { <. ( Base ` ndx ) , B >. , <. (TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. }   =>    |- K Struct <. 1 , ; 1 0 >.
Theorem	otpsbas 16052	The base set of a topological ordered space. (Contributed by Mario Carneiro, 12-Nov-2015.) (Revised by AV, 9-Sep-2021.)
|- K = { <. ( Base ` ndx ) , B >. , <. (TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. }   =>    |- ( B e. V -> B = ( Base ` K ) )
Theorem	otpstset 16053	The open sets of a topological ordered space. (Contributed by Mario Carneiro, 12-Nov-2015.) (Revised by AV, 9-Sep-2021.)
|- K = { <. ( Base ` ndx ) , B >. , <. (TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. }   =>    |- ( J e. V -> J = (TopSet ` K ) )
Theorem	otpsle 16054	The order of a topological ordered space. (Contributed by Mario Carneiro, 12-Nov-2015.) (Revised by AV, 9-Sep-2021.)
|- K = { <. ( Base ` ndx ) , B >. , <. (TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. }   =>    |- ( .<_ e. V -> .<_ = ( le ` K ) )
Theorem	otpsstrOLD 16055	Obsolete version of otpsstr 16051 as of 9-Sep-2021. (Contributed by Mario Carneiro, 12-Nov-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- K = { <. ( Base ` ndx ) , B >. , <. (TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. }   =>    |- K Struct <. 1 , 10 >.
Theorem	otpsbasOLD 16056	Obsolete version of otpsbas 16052 as of 9-Sep-2021. (Contributed by Mario Carneiro, 12-Nov-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- K = { <. ( Base ` ndx ) , B >. , <. (TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. }   =>    |- ( B e. V -> B = ( Base ` K ) )
Theorem	otpstsetOLD 16057	Obsolete version of otpstset 16053 as of 9-Sep-2021. (Contributed by Mario Carneiro, 12-Nov-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- K = { <. ( Base ` ndx ) , B >. , <. (TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. }   =>    |- ( J e. V -> J = (TopSet ` K ) )
Theorem	otpsleOLD 16058	Obsolete version of otpsle 16054 as of 9-Sep-2021. (Contributed by Mario Carneiro, 12-Nov-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- K = { <. ( Base ` ndx ) , B >. , <. (TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. }   =>    |- ( .<_ e. V -> .<_ = ( le ` K ) )
Theorem	ressle 16059	le is unaffected by restriction. (Contributed by Mario Carneiro, 3-Nov-2015.)
|- W = ( K ↾s A )   &    |- .<_ = ( le ` K )   =>    |- ( A e. V -> .<_ = ( le ` W ) )
Theorem	ocndx 16060	Index value of the df-ocomp 15963 slot. (Contributed by Mario Carneiro, 25-Oct-2015.)
|- ( oc ` ndx ) = ; 1 1
Theorem	ocid 16061	Utility theorem: index-independent form of df-ocomp 15963. (Contributed by Mario Carneiro, 25-Oct-2015.)
|- oc = Slot ( oc ` ndx )
Theorem	dsndx 16062	Index value of the df-ds 15964 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( dist ` ndx ) = ; 1 2
Theorem	dsid 16063	Utility theorem: index-independent form of df-ds 15964. (Contributed by Mario Carneiro, 23-Dec-2013.)
|- dist = Slot ( dist ` ndx )
Theorem	unifndx 16064	Index value of the df-unif 15965 slot. (Contributed by Thierry Arnoux, 17-Dec-2017.)
|- ( UnifSet ` ndx ) = ; 1 3
Theorem	unifid 16065	Utility theorem: index-independent form of df-unif 15965. (Contributed by Thierry Arnoux, 17-Dec-2017.)
|- UnifSet = Slot ( UnifSet ` ndx )
Theorem	odrngstr 16066	Functionality of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015.) (Proof shortened by AV, 15-Sep-2021.)
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. (TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } )   =>    |- W Struct <. 1 , ; 1 2 >.
Theorem	odrngbas 16067	The base set of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. (TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } )   =>    |- ( B e. V -> B = ( Base ` W ) )
Theorem	odrngplusg 16068	The addition operation of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. (TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } )   =>    |- ( .+ e. V -> .+ = ( +g ` W ) )
Theorem	odrngmulr 16069	The multiplication operation of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. (TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } )   =>    |- ( .x. e. V -> .x. = ( .r ` W ) )
Theorem	odrngtset 16070	The open sets of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. (TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } )   =>    |- ( J e. V -> J = (TopSet ` W ) )
Theorem	odrngle 16071	The order of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. (TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } )   =>    |- ( .<_ e. V -> .<_ = ( le ` W ) )
Theorem	odrngds 16072	The metric of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .x. >. } u. { <. (TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } )   =>    |- ( D e. V -> D = ( dist ` W ) )
Theorem	ressds 16073	dist is unaffected by restriction. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- H = ( G ↾s A )   &    |- D = ( dist ` G )   =>    |- ( A e. V -> D = ( dist ` H ) )
Theorem	homndx 16074	Index value of the df-hom 15966 slot. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- ( Hom ` ndx ) = ; 1 4
Theorem	homid 16075	Utility theorem: index-independent form of df-hom 15966. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- Hom = Slot ( Hom ` ndx )
Theorem	ccondx 16076	Index value of the df-cco 15967 slot. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- (comp ` ndx ) = ; 1 5
Theorem	ccoid 16077	Utility theorem: index-independent form of df-cco 15967. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- comp = Slot (comp ` ndx )
Theorem	resshom 16078	Hom is unaffected by restriction. (Contributed by Mario Carneiro, 5-Jan-2017.)
|- D = ( C ↾s A )   &    |- H = ( Hom ` C )   =>    |- ( A e. V -> H = ( Hom ` D ) )
Theorem	ressco 16079	comp is unaffected by restriction. (Contributed by Mario Carneiro, 5-Jan-2017.)
|- D = ( C ↾s A )   &    |- .x. = (comp ` C )   =>    |- ( A e. V -> .x. = (comp ` D ) )
Theorem	slotsbhcdif 16080	The slots Base, Hom and comp are different. (Contributed by AV, 5-Mar-2020.)
|- ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= (comp ` ndx ) /\ ( Hom ` ndx ) =/= (comp ` ndx ) )
7.1.3  Definition of the structure product
Syntax	crest 16081	Extend class notation with the function returning a subspace topology.
class ↾t
Syntax	ctopn 16082	Extend class notation with the topology extractor function.
class TopOpen
Definition	df-rest 16083*	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 16084	Define the topology extractor function. This differs from df-tset 15960 when a structure has been restricted using df-ress 15865; 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 16085	The subspace topology operator is a function on pairs. (Contributed by Mario Carneiro, 1-May-2015.)
|- ↾t Fn ( _V X. _V )
Theorem	topnfn 16086	The topology extractor function is a function on the universe. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- TopOpen Fn _V
Theorem	restval 16087*	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 16088*	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 ) ) )
Theorem	elrestr 16089	Sufficient condition for being an open set in a subspace. (Contributed by Jeff Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
|- ( ( J e. V /\ S e. W /\ A e. J ) -> ( A i^i S ) e. ( J ↾t S ) )
Theorem	0rest 16090	Value of the structure restriction when the topology input is empty. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- ( (/) ↾t A ) = (/)
Theorem	restid2 16091	The subspace topology over a subset of the base set is the original topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- ( ( A e. V /\ J C_ ~P A ) -> ( J ↾t A ) = J )
Theorem	restsspw 16092	The subspace topology is a collection of subsets of the restriction set. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- ( J ↾t A ) C_ ~P A
Theorem	firest 16093	The finite intersections operator commutes with restriction. (Contributed by Mario Carneiro, 30-Aug-2015.)
|- ( fi ` ( J ↾t A ) ) = ( ( fi ` J ) ↾t A )
Theorem	restid 16094	The subspace topology of the base set is the original topology. (Contributed by Jeff Hankins, 9-Jul-2009.) (Revised by Mario Carneiro, 13-Aug-2015.)
|- X = U. J   =>    |- ( J e. V -> ( J ↾t X ) = J )
Theorem	topnval 16095	Value of the topology extractor function. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- B = ( Base ` W )   &    |- J = (TopSet ` W )   =>    |- ( J ↾t B ) = ( TopOpen ` W )
Theorem	topnid 16096	Value of the topology extractor function when the topology is defined over the same set as the base. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- B = ( Base ` W )   &    |- J = (TopSet ` W )   =>    |- ( J C_ ~P B -> J = ( TopOpen ` W ) )
Theorem	topnpropd 16097	The topology extractor function depends only on the base and topology components. (Contributed by NM, 18-Jul-2006.)
|- ( ph -> ( Base ` K ) = ( Base ` L ) )   &    |- ( ph -> (TopSet ` K ) = (TopSet ` L ) )   =>    |- ( ph -> ( TopOpen ` K ) = ( TopOpen ` L ) )
Syntax	ctg 16098	Extend class notation with a function that converts a basis to its corresponding topology.
class topGen
Syntax	cpt 16099	Extend class notation with a function whose value is a product topology.
class Xt_
Syntax	c0g 16100	Extend class notation with group identity element.
class 0g