P. 137 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 13601-13700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	resshom 13601	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 13602	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 ) )
7.1.3  Definition of the structure product
Syntax	crest 13603	Extend class notation with the function returning a subspace topology.
class ↾t
Syntax	ctopn 13604	Extend class notation with the topology extractor function.
class TopOpen
Definition	df-rest 13605*	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 13606	Define the topology extractor function. This differs from df-tset 13503 when a structure has been restricted using df-ress 13431; 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 13607	The subspace topology operator is a function on pairs. (Contributed by Mario Carneiro, 1-May-2015.)
|- ↾t Fn ( _V X. _V )
Theorem	topnfn 13608	The topology extractor function is a function on the universe. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- TopOpen Fn _V
Theorem	restval 13609*	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 13610*	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 13611	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 13612	Value of the structure restriction when the topology input is empty. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- ( (/) ↾t A ) = (/)
Theorem	restid2 13613	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 13614	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 13615	The finite intersections operator commutes with restriction. (Contributed by Mario Carneiro, 30-Aug-2015.)
|- ( fi ` ( J ↾t A ) ) = ( ( fi ` J ) ↾t A )
Theorem	restid 13616	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 13617	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 13618	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 13619	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 13620	Extend class notation with a function that converts a basis to its corresponding topology.
class topGen
Syntax	cpt 13621	Extend class notation with a function whose value is a product topology.
class Xt_
Definition	df-topgen 13622*	Define a function that converts a basis to its corresponding topology. Equivalent to the definition of a topology generated by a basis in [Munkres] p. 78 (see tgval2 16976). See tgval3 16983 for an alternate expression for the value. (Contributed by NM, 16-Jul-2006.)
|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
Definition	df-pt 13623*	Define the product topology on a collection of topologies. For convenience, it is defined on arbitrary collections of sets, expressed as a function from some index set to the subbases of each factor space. (Contributed by Mario Carneiro, 3-Feb-2015.)
|- Xt_ = ( f e. _V |-> ( topGen ` { x | E. g ( ( g Fn dom f /\ A. y e. dom f ( g ` y ) e. ( f ` y ) /\ E. z e. Fin A. y e. ( dom f \ z ) ( g ` y ) = U. ( f ` y ) ) /\ x = X_ y e. dom f ( g ` y ) ) } ) )
Syntax	cprds 13624	The function constructing structure products.
class X_s
Syntax	cpws 13625	The function constructing structure powers.
class ^s
Definition	df-prds 13626*	Define a structure product. This can be a product of groups, rings, modules, or ordered topological fields; any unused components will have garbage in them but this usually not relevant for the purpose of inheriting the structures present in the factors. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- X_s = ( s e. _V , r e. _V |-> [_ X_ x e. dom r ( Base ` ( r ` x ) ) / v ]_ [_ ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) ) / h ]_ ( ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) ) ) >. } u. { <. (Scalar ` ndx ) , s >. , <. ( .s ` ndx ) , ( f e. ( Base ` s ) , g e. v |-> ( x e. dom r |-> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) ) ) >. } ) u. ( { <. (TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. r ) ) >. , <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ v /\ A. x e. dom r ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) ) } >. , <. ( dist ` ndx ) , ( f e. v , g e. v |-> sup ( ( ran ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. } u. { <. ( Hom ` ndx ) , h >. , <. (comp ` ndx ) , ( a e. ( v X. v ) , c e. v |-> ( d e. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. (comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) ) )
Theorem	reldmprds 13627	The structure product is a well-behaved binary operator. (Contributed by Stefan O'Rear, 7-Jan-2015.)
|- Rel dom X_s
Definition	df-pws 13628*	Define a structure power, which is just a structure product where all the factors are the same. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- ^s = ( r e. _V , i e. _V |-> ( (Scalar ` r ) X_s ( i X. { r } ) ) )
Theorem	prdsbasex 13629*	Lemma for structure products. (Contributed by Mario Carneiro, 3-Jan-2015.)
|- B = X_ x e. dom R ( Base ` ( R ` x ) )   =>    |- B e. _V
Theorem	imasvalstr 13630	Structure product value is a structure. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- U = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } ) u. { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , L >. , <. ( dist ` ndx ) , D >. } )   =>    |- U Struct <. 1 , ; 1 2 >.
Theorem	prdsvalstr 13631	Structure product value is a structure. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } ) u. ( { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , L >. , <. ( dist ` ndx ) , D >. } u. { <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .xb >. } ) ) Struct <. 1 , ; 1 5 >.
Theorem	prdsvallem 13632	Lemma for prdsbas 13635 and similar theorems. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- ( ph -> U = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } ) u. ( { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , L >. , <. ( dist ` ndx ) , D >. } u. { <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .xb >. } ) ) )   &    |- A = ( E ` U )   &    |- E = Slot ( E ` ndx )   &    |- ( ph -> T e. _V )   &    |- { <. ( E ` ndx ) , T >. } C_ ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } ) u. ( { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , L >. , <. ( dist ` ndx ) , D >. } u. { <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .xb >. } ) )   =>    |- ( ph -> A = T )
Theorem	prdsval 13633*	Value of the structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 7-Jan-2017.)
|- P = ( S X_s R )   &    |- K = ( Base ` S )   &    |- ( ph -> dom R = I )   &    |- ( ph -> B = X_ x e. I ( Base ` ( R ` x ) ) )   &    |- ( ph -> .+ = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) )   &    |- ( ph -> .X. = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) )   &    |- ( ph -> .x. = ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) )   &    |- ( ph -> O = ( Xt_ ` ( TopOpen o. R ) ) )   &    |- ( ph -> .<_ = { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } )   &    |- ( ph -> D = ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) )   &    |- ( ph -> H = ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) )   &    |- ( ph -> .xb = ( a e. ( B X. B ) , c e. B |-> ( d e. ( c H ( 2nd ` a ) ) , e e. ( H ` a ) |-> ( x e. I |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. (comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) )   &    |- ( ph -> S e. W )   &    |- ( ph -> R e. Z )   =>    |- ( ph -> P = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } ) u. ( { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } u. { <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .xb >. } ) ) )
Theorem	prdssca 13634	Scalar ring of a structure product. (Contributed by Stefan O'Rear, 5-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.)
|- P = ( S X_s R )   &    |- ( ph -> S e. V )   &    |- ( ph -> R e. W )   =>    |- ( ph -> S = (Scalar ` P ) )
Theorem	prdsbas 13635*	Base set of a structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.)
|- P = ( S X_s R )   &    |- ( ph -> S e. V )   &    |- ( ph -> R e. W )   &    |- B = ( Base ` P )   &    |- ( ph -> dom R = I )   =>    |- ( ph -> B = X_ x e. I ( Base ` ( R ` x ) ) )
Theorem	prdsplusg 13636*	Addition in a structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.)
|- P = ( S X_s R )   &    |- ( ph -> S e. V )   &    |- ( ph -> R e. W )   &    |- B = ( Base ` P )   &    |- ( ph -> dom R = I )   &    |- .+ = ( +g ` P )   =>    |- ( ph -> .+ = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) )
Theorem	prdsmulr 13637*	Multiplication in a structure product. (Contributed by Mario Carneiro, 11-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.)
|- P = ( S X_s R )   &    |- ( ph -> S e. V )   &    |- ( ph -> R e. W )   &    |- B = ( Base ` P )   &    |- ( ph -> dom R = I )   &    |- .x. = ( .r ` P )   =>    |- ( ph -> .x. = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) )
Theorem	prdsvsca 13638*	Scalar multiplication in a structure product. (Contributed by Stefan O'Rear, 5-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.)
|- P = ( S X_s R )   &    |- ( ph -> S e. V )   &    |- ( ph -> R e. W )   &    |- B = ( Base ` P )   &    |- ( ph -> dom R = I )   &    |- K = ( Base ` S )   &    |- .x. = ( .s ` P )   =>    |- ( ph -> .x. = ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) )
Theorem	prdsle 13639*	Structure product weak ordering. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- P = ( S X_s R )   &    |- ( ph -> S e. V )   &    |- ( ph -> R e. W )   &    |- B = ( Base ` P )   &    |- ( ph -> dom R = I )   &    |- .<_ = ( le ` P )   =>    |- ( ph -> .<_ = { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } )
Theorem	prdsless 13640	Closure of the order relation on a structure product. (Contributed by Mario Carneiro, 16-Aug-2015.)
|- P = ( S X_s R )   &    |- ( ph -> S e. V )   &    |- ( ph -> R e. W )   &    |- B = ( Base ` P )   &    |- ( ph -> dom R = I )   &    |- .<_ = ( le ` P )   =>    |- ( ph -> .<_ C_ ( B X. B ) )
Theorem	prdsds 13641*	Structure product distance function. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- P = ( S X_s R )   &    |- ( ph -> S e. V )   &    |- ( ph -> R e. W )   &    |- B = ( Base ` P )   &    |- ( ph -> dom R = I )   &    |- D = ( dist ` P )   =>    |- ( ph -> D = ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) )
Theorem	prdsdsfn 13642	Structure product distance function. (Contributed by Mario Carneiro, 15-Sep-2015.)
|- P = ( S X_s R )   &    |- ( ph -> S e. V )   &    |- ( ph -> R e. W )   &    |- B = ( Base ` P )   &    |- ( ph -> dom R = I )   &    |- D = ( dist ` P )   =>    |- ( ph -> D Fn ( B X. B ) )
Theorem	prdstset 13643	Structure product topology. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- P = ( S X_s R )   &    |- ( ph -> S e. V )   &    |- ( ph -> R e. W )   &    |- B = ( Base ` P )   &    |- ( ph -> dom R = I )   &    |- O = (TopSet ` P )   =>    |- ( ph -> O = ( Xt_ ` ( TopOpen o. R ) ) )
Theorem	prdshom 13644*	Structure product hom-sets. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- P = ( S X_s R )   &    |- ( ph -> S e. V )   &    |- ( ph -> R e. W )   &    |- B = ( Base ` P )   &    |- ( ph -> dom R = I )   &    |- H = ( Hom ` P )   =>    |- ( ph -> H = ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) )
Theorem	prdsco 13645*	Structure product composition operation. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- P = ( S X_s R )   &    |- ( ph -> S e. V )   &    |- ( ph -> R e. W )   &    |- B = ( Base ` P )   &    |- ( ph -> dom R = I )   &    |- H = ( Hom ` P )   &    |- .xb = (comp ` P )   =>    |- ( ph -> .xb = ( a e. ( B X. B ) , c e. B |-> ( d e. ( c H ( 2nd ` a ) ) , e e. ( H ` a ) |-> ( x e. I |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. (comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) )
Theorem	prdsbas2 13646*	The base set of a structure product is an indexed set product. (Contributed by Stefan O'Rear, 10-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R Fn I )   =>    |- ( ph -> B = X_ x e. I ( Base ` ( R ` x ) ) )
Theorem	prdsbasmpt 13647*	A constructed tuple is a point in a structure product iff each coordinate is in the proper base set. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R Fn I )   =>    |- ( ph -> ( ( x e. I |-> U ) e. B <-> A. x e. I U e. ( Base ` ( R ` x ) ) ) )
Theorem	prdsbasfn 13648	Points in the structure product are functions; use this with dffn5 5731 to establish equalities. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R Fn I )   &    |- ( ph -> T e. B )   =>    |- ( ph -> T Fn I )
Theorem	prdsbasprj 13649	Each point in a structure product restricts on each coordinate to the relevant base set. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R Fn I )   &    |- ( ph -> T e. B )   &    |- ( ph -> J e. I )   =>    |- ( ph -> ( T ` J ) e. ( Base ` ( R ` J ) ) )
Theorem	prdsplusgval 13650*	Value of a componentwise sum in a structure product. (Contributed by Stefan O'Rear, 10-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R Fn I )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- .+ = ( +g ` Y )   =>    |- ( ph -> ( F .+ G ) = ( x e. I |-> ( ( F ` x ) ( +g ` ( R ` x ) ) ( G ` x ) ) ) )
Theorem	prdsplusgfval 13651	Value of a structure product sum at a single coordinate. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R Fn I )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- .+ = ( +g ` Y )   &    |- ( ph -> J e. I )   =>    |- ( ph -> ( ( F .+ G ) ` J ) = ( ( F ` J ) ( +g ` ( R ` J ) ) ( G ` J ) ) )
Theorem	prdsmulrval 13652*	Value of a componentwise ring product in a structure product. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R Fn I )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- .x. = ( .r ` Y )   =>    |- ( ph -> ( F .x. G ) = ( x e. I |-> ( ( F ` x ) ( .r ` ( R ` x ) ) ( G ` x ) ) ) )
Theorem	prdsmulrfval 13653	Value of a structure product's ring product at a single coordinate. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R Fn I )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- .x. = ( .r ` Y )   &    |- ( ph -> J e. I )   =>    |- ( ph -> ( ( F .x. G ) ` J ) = ( ( F ` J ) ( .r ` ( R ` J ) ) ( G ` J ) ) )
Theorem	prdsleval 13654*	Value of the product ordering in a structure product. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R Fn I )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- .<_ = ( le ` Y )   =>    |- ( ph -> ( F .<_ G <-> A. x e. I ( F ` x ) ( le ` ( R ` x ) ) ( G ` x ) ) )
Theorem	prdsdsval 13655*	Value of the metric in a structure product. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R Fn I )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- D = ( dist ` Y )   =>    |- ( ph -> ( F D G ) = sup ( ( ran ( x e. I |-> ( ( F ` x ) ( dist ` ( R ` x ) ) ( G ` x ) ) ) u. { 0 } ) , RR* , < ) )
Theorem	prdsvscaval 13656*	Scalar multiplication in a structure product is pointwise. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- .x. = ( .s ` Y )   &    |- K = ( Base ` S )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R Fn I )   &    |- ( ph -> F e. K )   &    |- ( ph -> G e. B )   =>    |- ( ph -> ( F .x. G ) = ( x e. I |-> ( F ( .s ` ( R ` x ) ) ( G ` x ) ) ) )
Theorem	prdsvscafval 13657	Scalar multiplication of a single coordinate in a structure product. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- .x. = ( .s ` Y )   &    |- K = ( Base ` S )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R Fn I )   &    |- ( ph -> F e. K )   &    |- ( ph -> G e. B )   &    |- ( ph -> J e. I )   =>    |- ( ph -> ( ( F .x. G ) ` J ) = ( F ( .s ` ( R ` J ) ) ( G ` J ) ) )
Theorem	prdsbas3 13658*	The base set of an indexed structure product. (Contributed by Mario Carneiro, 13-Sep-2015.)
|- Y = ( S X_s ( x e. I |-> R ) )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> A. x e. I R e. X )   &    |- K = ( Base ` R )   =>    |- ( ph -> B = X_ x e. I K )
Theorem	prdsbasmpt2 13659*	A constructed tuple is a point in a structure product iff each coordinate is in the proper base set. (Contributed by Mario Carneiro, 3-Jul-2015.) (Revised by Mario Carneiro, 13-Sep-2015.)
|- Y = ( S X_s ( x e. I |-> R ) )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> A. x e. I R e. X )   &    |- K = ( Base ` R )   =>    |- ( ph -> ( ( x e. I |-> U ) e. B <-> A. x e. I U e. K ) )
Theorem	prdsbascl 13660*	An element of the base has projections closed in the factors. (Contributed by Mario Carneiro, 27-Aug-2015.)
|- Y = ( S X_s ( x e. I |-> R ) )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> A. x e. I R e. X )   &    |- K = ( Base ` R )   &    |- ( ph -> F e. B )   =>    |- ( ph -> A. x e. I ( F ` x ) e. K )
Theorem	prdsdsval2 13661*	Value of the metric in a structure product. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- Y = ( S X_s ( x e. I |-> R ) )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> A. x e. I R e. X )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- E = ( dist ` R )   &    |- D = ( dist ` Y )   =>    |- ( ph -> ( F D G ) = sup ( ( ran ( x e. I |-> ( ( F ` x ) E ( G ` x ) ) ) u. { 0 } ) , RR* , < ) )
Theorem	prdsdsval3 13662*	Value of the metric in a structure product. (Contributed by Mario Carneiro, 27-Aug-2015.)
|- Y = ( S X_s ( x e. I |-> R ) )   &    |- B = ( Base ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> A. x e. I R e. X )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- K = ( Base ` R )   &    |- E = ( ( dist ` R ) |` ( K X. K ) )   &    |- D = ( dist ` Y )   =>    |- ( ph -> ( F D G ) = sup ( ( ran ( x e. I |-> ( ( F ` x ) E ( G ` x ) ) ) u. { 0 } ) , RR* , < ) )
Theorem	pwsval 13663	Value of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   &    |- F = (Scalar ` R )   =>    |- ( ( R e. V /\ I e. W ) -> Y = ( F X_s ( I X. { R } ) ) )
Theorem	pwsbas 13664	Base set of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` R )   =>    |- ( ( R e. V /\ I e. W ) -> ( B ^m I ) = ( Base ` Y ) )
Theorem	pwselbasb 13665	Membership in the base set of a structure product. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` R )   &    |- V = ( Base ` Y )   =>    |- ( ( R e. W /\ I e. Z ) -> ( X e. V <-> X : I --> B ) )
Theorem	pwselbas 13666	An element of a structure power is a function from the index set to the base set of the structure. (Contributed by Mario Carneiro, 11-Jan-2015.) (Revised by Mario Carneiro, 5-Jun-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` R )   &    |- V = ( Base ` Y )   &    |- ( ph -> R e. W )   &    |- ( ph -> I e. Z )   &    |- ( ph -> X e. V )   =>    |- ( ph -> X : I --> B )
Theorem	pwsplusgval 13667	Value of addition in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` Y )   &    |- ( ph -> R e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- .+ = ( +g ` R )   &    |- .+b = ( +g ` Y )   =>    |- ( ph -> ( F .+b G ) = ( F o F .+ G ) )
Theorem	pwsmulrval 13668	Value of multiplication in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` Y )   &    |- ( ph -> R e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` Y )   =>    |- ( ph -> ( F .xb G ) = ( F o F .x. G ) )
Theorem	pwsle 13669	Ordering in a structure power. (Contributed by Mario Carneiro, 16-Aug-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` Y )   &    |- O = ( le ` R )   &    |- .<_ = ( le ` Y )   =>    |- ( ( R e. V /\ I e. W ) -> .<_ = ( o R O i^i ( B X. B ) ) )
Theorem	pwsleval 13670*	Ordering in a structure power. (Contributed by Mario Carneiro, 16-Aug-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` Y )   &    |- O = ( le ` R )   &    |- .<_ = ( le ` Y )   &    |- ( ph -> R e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   =>    |- ( ph -> ( F .<_ G <-> A. x e. I ( F ` x ) O ( G ` x ) ) )
Theorem	pwsvscafval 13671	Scalar multiplication in a structure power is pointwise. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` Y )   &    |- .x. = ( .s ` R )   &    |- .xb = ( .s ` Y )   &    |- F = (Scalar ` R )   &    |- K = ( Base ` F )   &    |- ( ph -> R e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> A e. K )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( A .xb X ) = ( ( I X. { A } ) o F .x. X ) )
Theorem	pwsvscaval 13672	Scalar multiplication of a single coordinate in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` Y )   &    |- .x. = ( .s ` R )   &    |- .xb = ( .s ` Y )   &    |- F = (Scalar ` R )   &    |- K = ( Base ` F )   &    |- ( ph -> R e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> A e. K )   &    |- ( ph -> X e. B )   &    |- ( ph -> J e. I )   =>    |- ( ph -> ( ( A .xb X ) ` J ) = ( A .x. ( X ` J ) ) )
Theorem	pwssca 13673	The ring of scalars of a structure product. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- Y = ( R ^s I )   &    |- S = (Scalar ` R )   =>    |- ( ( R e. V /\ I e. W ) -> S = (Scalar ` Y ) )
Theorem	pwsdiagel 13674	Membership of diagonal elements in the structure power base set. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` R )   &    |- C = ( Base ` Y )   =>    |- ( ( ( R e. V /\ I e. W ) /\ A e. B ) -> ( I X. { A } ) e. C )
Theorem	pwssnf1o 13675*	Triviality of singleton powers: set equipollence. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- Y = ( R ^s { I } )   &    |- B = ( Base ` R )   &    |- F = ( x e. B |-> ( { I } X. { x } ) )   &    |- C = ( Base ` Y )   =>    |- ( ( R e. V /\ I e. W ) -> F : B -1-1-onto-> C )
7.1.4  Definition of the structure quotient
Syntax	cordt 13676	Extend class notation with the order topology.
class ordTop
Syntax	cxrs 13677	Extend class notation with the extended real number structure.
class RR* s
Syntax	c0g 13678	Extend class notation with group identity element.
class 0g
Syntax	cgsu 13679	Extend class notation to include finitely supported group sums.
class gsumg
Definition	df-ordt 13680*	Define the order topology, given an order <_, written as r below. A closed subbasis for the order topology is given by the closed rays [ y , +oo ) = { z e. X | y <_ z } and ( -oo , y ] = { z e. X | z <_ y }, along with ( -oo , +oo ) = X itself. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- ordTop = ( r e. _V |-> ( topGen ` ( fi ` ( { dom r } u. ran ( ( x e. dom r |-> { y e. dom r | -. y r x } ) u. ( x e. dom r |-> { y e. dom r | -. x r y } ) ) ) ) ) )
Definition	df-xrs 13681*	The extended real number structure. Unlike df-cnfld 16659, the extended real numbers do not have good algebraic properties, so this is not actually a group or anything higher, even though it has just as many operations as df-cnfld 16659. The main interest in this structure is in its ordering, which is complete and compact. The metric described here is an extension of the absolute value metric, but it is not itself a metric because +oo is infinitely far from all other points. The topology is based on the order and not the extended metric (which would make +oo an isolated point since there is nothing else in the 1 -ball around it). All components of this structure agree with ℂfld when restricted to RR. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- RR* s = ( { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , + e >. , <. ( .r ` ndx ) , x e >. } u. { <. (TopSet ` ndx ) , (ordTop ` <_ ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y + e - e x ) , ( x + e - e y ) ) ) >. } )
Definition	df-0g 13682*	Define group identity element. (Contributed by NM, 20-Aug-2011.)
|- 0g = ( g e. _V |-> ( iota e ( e e. ( Base ` g ) /\ A. x e. ( Base ` g ) ( ( e ( +g ` g ) x ) = x /\ ( x ( +g ` g ) e ) = x ) ) ) )
Definition	df-gsum 13683*	Define the group sum for the structure G of a finite sequence of elements whose values are defined by the expression B and whose set of indices is A. It may be viewed as a product (if G is a multiplication), a sum (if G is an addition) or whatever. The variable k is normally a free variable in B ( i.e. B can be thought of as B ( k )). The definition is meaningful in three contexts, depending on the size of the index set A and each demanding different properties of G. 1. If A = (/) and G has an identity element, then the sum equals this identity. 2. If A = ( M ... N ) and G is any magma, then the sum is the sum of the elements, evaluated left-to-right, i.e. ( B ( 1 ) + B ( 2 ) ) + B ( 3 ) etc. 3. If A is a finite set (or is non-zero for finitely many indices) and G is a commutative monoid, then the sum adds up these elements in some order, which is then uniquely defined. 4. If A is an infinite set and G is a Hausdorff topological group, then there is a meaningful sum, but gsumg cannot handle this case. See df-tsms 18109. (Contributed by FL, 5-Sep-2010.) (Revised by FL, 17-Oct-2011.) (Revised by Mario Carneiro, 7-Dec-2014.)
|- gsumg = ( w e. _V , f e. _V |-> [_ { x e. ( Base ` w ) | A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) } / o ]_ if ( ran f C_ o , ( 0g ` w ) , if ( dom f e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) ) , ( iota x E. g [. ( `' f " ( _V \ o ) ) / y ]. ( g : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( f o. g ) ) ` ( # ` y ) ) ) ) ) ) )
Syntax	cqtop 13684	Extend class notation with the quotient topology function.
class qTop
Syntax	cimas 13685	Image structure function.
class "s
Syntax	cqus 13686	Quotient structure function.
class /.s
Syntax	cxps 13687	Binary product structure function.
class X.s
Definition	df-qtop 13688*	Define the quotient topology given a function f and topology j on the domain of f. (Contributed by Mario Carneiro, 23-Mar-2015.)
|- qTop = ( j e. _V , f e. _V |-> { s e. ~P ( f " U. j ) | ( ( `' f " s ) i^i U. j ) e. j } )
Definition	df-imas 13689*	Define an image structure, which takes a structure and a function on the base set, and maps all the operations via the function. For this to work properly f must either be injective or satisfy the well-definedness condition f ( a ) = f ( c ) /\ f ( b ) = f ( d ) -> f ( a + b ) = f ( c + d ) for each relevant operation. Note that although we call this an "image" by association to df-ima 4850, in order to keep the definition simple we consider only the case when the domain of F is equal to the base set of R. Other cases can be achieved by restricting F (with df-res 4849) and/or R ( with df-ress 13431) to their common domain. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- "s = ( f e. _V , r e. _V |-> [_ ( Base ` r ) / v ]_ ( ( { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. } u. { <. (Scalar ` ndx ) , (Scalar ` r ) >. , <. ( .s ` ndx ) , U_ q e. v ( p e. ( Base ` (Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) >. } ) u. { <. (TopSet ` ndx ) , ( ( TopOpen ` r ) qTop f ) >. , <. ( le ` ndx ) , ( ( f o. ( le ` r ) ) o. `' f ) >. , <. ( dist ` ndx ) , ( x e. ran f , y e. ran f |-> sup ( U_ n e. NN ran ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR* s gsumg ( ( dist ` r ) o. g ) ) ) , RR* , `' < ) ) >. } ) )
Definition	df-divs 13690*	Define a quotient ring (or quotient group), which is a special case of an image structure df-imas 13689 where the image function is x |-> [ x ] e. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- /.s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )
Definition	df-xps 13691*	Define a binary product on structures. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- X.s = ( r e. _V , s e. _V |-> ( `' ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> `' ( { x } +c { y } ) ) "s ( (Scalar ` r ) X_s `' ( { r } +c { s } ) ) ) )
Theorem	imasval 13692*	Value of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- .+ = ( +g ` R )   &    |- .X. = ( .r ` R )   &    |- G = (Scalar ` R )   &    |- K = ( Base ` G )   &    |- .x. = ( .s ` R )   &    |- J = ( TopOpen ` R )   &    |- E = ( dist ` R )   &    |- N = ( le ` R )   &    |- ( ph -> .+b = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } )   &    |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } )   &    |- ( ph -> .(x) = U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> O = ( J qTop F ) )   &    |- ( ph -> D = ( x e. B , y e. B |-> sup ( U_ n e. NN ran ( g e. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR* s gsumg ( E o. g ) ) ) , RR* , `' < ) ) )   &    |- ( ph -> .<_ = ( ( F o. N ) o. `' F ) )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ph -> R e. Z )   =>    |- ( ph -> U = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } u. { <. (Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. } ) u. { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } ) )
Theorem	imasbas 13693	The base set of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ph -> R e. Z )   =>    |- ( ph -> B = ( Base ` U ) )
Theorem	imasds 13694*	The distance function of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ph -> R e. Z )   &    |- E = ( dist ` R )   &    |- D = ( dist ` U )   =>    |- ( ph -> D = ( x e. B , y e. B |-> sup ( U_ n e. NN ran ( g e. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR* s gsumg ( E o. g ) ) ) , RR* , `' < ) ) )
Theorem	imasdsfn 13695	The distance function is a function on the base set. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ph -> R e. Z )   &    |- E = ( dist ` R )   &    |- D = ( dist ` U )   =>    |- ( ph -> D Fn ( B X. B ) )
Theorem	imasdsval 13696*	The distance function of an image structure. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ph -> R e. Z )   &    |- E = ( dist ` R )   &    |- D = ( dist ` U )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- S = { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = X /\ ( F ` ( 2nd ` ( h ` n ) ) ) = Y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) }   =>    |- ( ph -> ( X D Y ) = sup ( U_ n e. NN ran ( g e. S |-> ( RR* s gsumg ( E o. g ) ) ) , RR* , `' < ) )
Theorem	imasdsval2 13697*	The distance function of an image structure. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ph -> R e. Z )   &    |- E = ( dist ` R )   &    |- D = ( dist ` U )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- S = { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = X /\ ( F ` ( 2nd ` ( h ` n ) ) ) = Y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) }   &    |- T = ( E |` ( V X. V ) )   =>    |- ( ph -> ( X D Y ) = sup ( U_ n e. NN ran ( g e. S |-> ( RR* s gsumg ( T o. g ) ) ) , RR* , `' < ) )
Theorem	imasplusg 13698*	The group operation in an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ph -> R e. Z )   &    |- .+ = ( +g ` R )   &    |- .+b = ( +g ` U )   =>    |- ( ph -> .+b = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } )
Theorem	imasmulr 13699*	The ring multiplication in an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ph -> R e. Z )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` U )   =>    |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
Theorem	imassca 13700	The scalar field of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ph -> R e. Z )   &    |- G = (Scalar ` R )   =>    |- ( ph -> G = (Scalar ` U ) )