P. 131 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13001-13100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	unifid 13001	Utility theorem: index-independent form of df-unif 12874. (Contributed by Thierry Arnoux, 17-Dec-2017.)
|- UnifSet = Slot ( UnifSet ` ndx )
Theorem	unifndxnn 13002	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 13003	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 13004	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 13005	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 13006	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 13007	Index value of the df-hom 12875 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.)
|- ( Hom ` ndx ) = ; 1 4
Theorem	homid 13008	Utility theorem: index-independent form of df-hom 12875. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- Hom = Slot ( Hom ` ndx )
Theorem	homslid 13009	Slot property of Hom. (Contributed by Jim Kingdon, 20-Mar-2025.)
|- ( Hom = Slot ( Hom ` ndx ) /\ ( Hom ` ndx ) e. NN )
Theorem	ccondx 13010	Index value of the df-cco 12876 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.)
|- (comp ` ndx ) = ; 1 5
Theorem	ccoid 13011	Utility theorem: index-independent form of df-cco 12876. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- comp = Slot (comp ` ndx )
Theorem	ccoslid 13012	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 13013	Extend class notation with the function returning a subspace topology.
class ↾t
Syntax	ctopn 13014	Extend class notation with the topology extractor function.
class TopOpen
Definition	df-rest 13015*	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 13016	Define the topology extractor function. This differs from df-tset 12870 when a structure has been restricted using df-iress 12782; 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 13017	The subspace topology operator is a function on pairs. (Contributed by Mario Carneiro, 1-May-2015.)
|- ↾t Fn ( _V X. _V )
Theorem	topnfn 13018	The topology extractor function is a function on the universe. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- TopOpen Fn _V
Theorem	restval 13019*	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 13020*	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 13021	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	restid2 13022	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 13023	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	restid 13024	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	topnvalg 13025	Value of the topology extractor function. (Contributed by Mario Carneiro, 13-Aug-2015.) (Revised by Jim Kingdon, 11-Feb-2023.)
|- B = ( Base ` W )   &    |- J = (TopSet ` W )   =>    |- ( W e. V -> ( J ↾t B ) = ( TopOpen ` W ) )
Theorem	topnidg 13026	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 )   =>    |- ( ( W e. V /\ J C_ ~P B ) -> J = ( TopOpen ` W ) )
Theorem	topnpropgd 13027	The topology extractor function depends only on the base and topology components. (Contributed by NM, 18-Jul-2006.) (Revised by Jim Kingdon, 13-Feb-2023.)
|- ( ph -> ( Base ` K ) = ( Base ` L ) )   &    |- ( ph -> (TopSet ` K ) = (TopSet ` L ) )   &    |- ( ph -> K e. V )   &    |- ( ph -> L e. W )   =>    |- ( ph -> ( TopOpen ` K ) = ( TopOpen ` L ) )
Syntax	ctg 13028	Extend class notation with a function that converts a basis to its corresponding topology.
class topGen
Syntax	cpt 13029	Extend class notation with a function whose value is a product topology.
class Xt_
Syntax	c0g 13030	Extend class notation with group identity element.
class 0g
Syntax	cgsu 13031	Extend class notation to include finitely supported group sums.
class gsumg
Definition	df-0g 13032*	Define group identity element. Remark: this definition is required here because the symbol 0g is already used in df-igsum 13033. The related theorems will be provided later. (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-igsum 13033*	Define a finite group sum (also called "iterated sum") of a structure. Given G gsumg F where F : A --> ( Base ` G ), the set of indices is A and the values are given by F at each index. A group sum over a multiplicative group may be viewed as a product. The definition is meaningful in different 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., ( ( F ` 1 ) + ( F ` 2 ) ) + ( F ` 3 ), etc. 3. This definition does not handle other cases. (Contributed by FL, 5-Sep-2010.) (Revised by Mario Carneiro, 7-Dec-2014.) (Revised by Jim Kingdon, 27-Jun-2025.)
|- gsumg = ( w e. _V , f e. _V |-> ( iota x ( ( dom f = (/) /\ x = ( 0g ` w ) ) \/ E. m E. n e. ( ZZ>= ` m ) ( dom f = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , f ) ` n ) ) ) ) )
Definition	df-topgen 13034*	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. (Contributed by NM, 16-Jul-2006.)
|- topGen = ( x e. _V |-> { y | y C_ U. ( x i^i ~P y ) } )
Definition	df-pt 13035*	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 ) ) } ) )
Theorem	tgval 13036*	The topology generated by a basis. See also tgval2 14465 and tgval3 14472. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
|- ( B e. V -> ( topGen ` B ) = { x | x C_ U. ( B i^i ~P x ) } )
Theorem	tgvalex 13037	The topology generated by a basis is a set. (Contributed by Jim Kingdon, 4-Mar-2023.)
|- ( B e. V -> ( topGen ` B ) e. _V )
Theorem	ptex 13038	Existence of the product topology. (Contributed by Jim Kingdon, 19-Mar-2025.)
|- ( F e. V -> ( Xt_ ` F ) e. _V )
Syntax	cprds 13039	The function constructing structure products.
class X_s
Syntax	cpws 13040	The function constructing structure powers.
class ^s
Definition	df-prds 13041*	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 is usually not relevant for the purpose of inheriting the structures present in the factors. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
|- 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 ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. v , g e. v |-> ( s gsumg ( x e. dom r |-> ( ( f ` x ) ( .i ` ( 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. ( ( 2nd ` a ) h c ) , 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 13042	The structure product is a well-behaved binary operator. (Contributed by Stefan O'Rear, 7-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.)
|- Rel dom X_s
Theorem	prdsex 13043	Existence of the structure product. (Contributed by Jim Kingdon, 18-Mar-2025.)
|- ( ( S e. V /\ R e. W ) -> ( S X_s R ) e. _V )
Theorem	imasvalstrd 13044	An image structure value is a structure. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
|- U = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) u. { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , L >. , <. ( dist ` ndx ) , D >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> .X. e. X )   &    |- ( ph -> S e. Y )   &    |- ( ph -> .x. e. Z )   &    |- ( ph -> ., e. P )   &    |- ( ph -> O e. Q )   &    |- ( ph -> L e. R )   &    |- ( ph -> D e. A )   =>    |- ( ph -> U Struct <. 1 , ; 1 2 >. )
Theorem	prdsvalstrd 13045	Structure product value is a structure. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
|- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> .X. e. X )   &    |- ( ph -> S e. Y )   &    |- ( ph -> .x. e. Z )   &    |- ( ph -> ., e. P )   &    |- ( ph -> O e. Q )   &    |- ( ph -> L e. R )   &    |- ( ph -> D e. A )   &    |- ( ph -> H e. T )   &    |- ( ph -> .xb e. U )   =>    |- ( ph -> ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) u. ( { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , L >. , <. ( dist ` ndx ) , D >. } u. { <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .xb >. } ) ) Struct <. 1 , ; 1 5 >. )
Theorem	prdsvallem 13046*	Lemma for prdsval 13047. (Contributed by Stefan O'Rear, 3-Jan-2015.) Extracted from the former proof of prdsval 13047, dependency on df-hom 12875 removed. (Revised by AV, 13-Oct-2024.)
|- ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) ) e. _V
Theorem	prdsval 13047*	Value of the structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
|- 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 -> ., = ( f e. B , g e. B |-> ( S gsumg ( x e. I |-> ( ( f ` x ) ( .i ` ( 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. ( ( 2nd ` a ) H c ) , 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. >. , <. ( .i ` ndx ) , ., >. } ) u. ( { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } u. { <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .xb >. } ) ) )
Theorem	prdsbaslemss 13048	Lemma for prdsbas 13050 and similar theorems. (Contributed by Jim Kingdon, 10-Nov-2025.)
|- P = ( S X_s R )   &    |- ( ph -> S e. V )   &    |- ( ph -> R e. W )   &    |- A = ( E ` P )   &    |- E = Slot ( E ` ndx )   &    |- ( E ` ndx ) e. NN   &    |- ( ph -> T e. X )   &    |- ( ph -> { <. ( E ` ndx ) , T >. } C_ P )   =>    |- ( ph -> A = T )
Theorem	prdssca 13049	Scalar ring of a structure product. (Contributed by Stefan O'Rear, 5-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
|- P = ( S X_s R )   &    |- ( ph -> S e. V )   &    |- ( ph -> R e. W )   =>    |- ( ph -> S = (Scalar ` P ) )
Theorem	prdsbas 13050*	Base set of a structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
|- 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 13051*	Addition in a structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
|- 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 13052*	Multiplication in a structure product. (Contributed by Mario Carneiro, 11-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
|- 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	prdsbas2 13053*	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 13054*	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 13055	Points in the structure product are functions; use this with dffn5im 5623 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 13056	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 13057*	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 13058	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 13059*	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 13060	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	prdsbas3 13061*	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 13062*	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 13063*	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 )
Definition	df-pws 13064*	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	pwsval 13065	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 13066	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 13067	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 13068	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 13069	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 oF .+ G ) )
Theorem	pwsmulrval 13070	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 oF .x. G ) )
Theorem	pwsdiagel 13071	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 13072*	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 )
6.1.4  Definition of the structure quotient
Syntax	cimas 13073	Image structure function.
class "s
Syntax	cqus 13074	Quotient structure function.
class /.s
Syntax	cxps 13075	Binary product structure function.
class X.s
Definition	df-iimas 13076*	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 4687, 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 4686) and/or R ( with df-iress 12782) to their common domain. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by AV, 6-Oct-2020.)
|- "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 ) ) >. } >. } )
Definition	df-qus 13077*	Define a quotient ring (or quotient group), which is a special case of an image structure df-iimas 13076 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 13078*	Define a binary product on structures. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.)
|- X.s = ( r e. _V , s e. _V |-> ( `' ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( (Scalar ` r ) X_s { <. (/) , r >. , <. 1o , s >. } ) ) )
Theorem	imasex 13079	Existence of the image structure. (Contributed by Jim Kingdon, 13-Mar-2025.)
|- ( ( F e. V /\ R e. W ) -> ( F "s R ) e. _V )
Theorem	imasival 13080*	Value of an image structure. The is a lemma for the theorems imasbas 13081, imasplusg 13082, and imasmulr 13083 and should not be needed once they are proved. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Jim Kingdon, 11-Mar-2025.) (New usage is discouraged.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- .+ = ( +g ` R )   &    |- .X. = ( .r ` R )   &    |- .x. = ( .s ` 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 -> F : V -onto-> B )   &    |- ( ph -> R e. Z )   =>    |- ( ph -> U = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } )
Theorem	imasbas 13081	The base set of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 6-Oct-2020.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ph -> R e. Z )   =>    |- ( ph -> B = ( Base ` U ) )
Theorem	imasplusg 13082*	The group operation in an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
|- ( 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 13083*	The ring multiplication in an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
|- ( 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	f1ocpbllem 13084	Lemma for f1ocpbl 13085. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> F : V -1-1-onto-> X )   =>    |- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( ( F ` A ) = ( F ` C ) /\ ( F ` B ) = ( F ` D ) ) <-> ( A = C /\ B = D ) ) )
Theorem	f1ocpbl 13085	An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> F : V -1-1-onto-> X )   =>    |- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( ( F ` A ) = ( F ` C ) /\ ( F ` B ) = ( F ` D ) ) -> ( F ` ( A .+ B ) ) = ( F ` ( C .+ D ) ) ) )
Theorem	f1ovscpbl 13086	An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- ( ph -> F : V -1-1-onto-> X )   =>    |- ( ( ph /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( ( F ` B ) = ( F ` C ) -> ( F ` ( A .+ B ) ) = ( F ` ( A .+ C ) ) ) )
Theorem	f1olecpbl 13087	An injection is compatible with any relations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> F : V -1-1-onto-> X )   =>    |- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( ( F ` A ) = ( F ` C ) /\ ( F ` B ) = ( F ` D ) ) -> ( A N B <-> C N D ) ) )
Theorem	imasaddfnlemg 13088*	The image structure operation is a function if the original operation is compatible with the function. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )   &    |- ( ph -> V e. W )   &    |- ( ph -> .x. e. C )   =>    |- ( ph -> .xb Fn ( B X. B ) )
Theorem	imasaddvallemg 13089*	The operation of an image structure is defined to distribute over the mapping function. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )   &    |- ( ph -> V e. W )   &    |- ( ph -> .x. e. C )   =>    |- ( ( ph /\ X e. V /\ Y e. V ) -> ( ( F ` X ) .xb ( F ` Y ) ) = ( F ` ( X .x. Y ) ) )
Theorem	imasaddflemg 13090*	The image set operations are closed if the original operation is. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )   &    |- ( ph -> V e. W )   &    |- ( ph -> .x. e. C )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   =>    |- ( ph -> .xb : ( B X. B ) --> B )
Theorem	imasaddfn 13091*	The image structure's group operation is a function. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 10-Jul-2015.)
|- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> R e. Z )   &    |- .x. = ( +g ` R )   &    |- .xb = ( +g ` U )   =>    |- ( ph -> .xb Fn ( B X. B ) )
Theorem	imasaddval 13092*	The value of an image structure's group operation. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> R e. Z )   &    |- .x. = ( +g ` R )   &    |- .xb = ( +g ` U )   =>    |- ( ( ph /\ X e. V /\ Y e. V ) -> ( ( F ` X ) .xb ( F ` Y ) ) = ( F ` ( X .x. Y ) ) )
Theorem	imasaddf 13093*	The image structure's group operation is closed in the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> R e. Z )   &    |- .x. = ( +g ` R )   &    |- .xb = ( +g ` U )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   =>    |- ( ph -> .xb : ( B X. B ) --> B )
Theorem	imasmulfn 13094*	The image structure's ring multiplication is a function. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> R e. Z )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` U )   =>    |- ( ph -> .xb Fn ( B X. B ) )
Theorem	imasmulval 13095*	The value of an image structure's ring multiplication. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> R e. Z )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` U )   =>    |- ( ( ph /\ X e. V /\ Y e. V ) -> ( ( F ` X ) .xb ( F ` Y ) ) = ( F ` ( X .x. Y ) ) )
Theorem	imasmulf 13096*	The image structure's ring multiplication is closed in the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> R e. Z )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` U )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   =>    |- ( ph -> .xb : ( B X. B ) --> B )
Theorem	qusval 13097*	Value of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> .~ e. W )   &    |- ( ph -> R e. Z )   =>    |- ( ph -> U = ( F "s R ) )
Theorem	quslem 13098*	The function in qusval 13097 is a surjection onto a quotient set. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> .~ e. W )   &    |- ( ph -> R e. Z )   =>    |- ( ph -> F : V -onto-> ( V /. .~ ) )
Theorem	qusex 13099	Existence of a quotient structure. (Contributed by Jim Kingdon, 25-Apr-2025.)
|- ( ( R e. V /\ .~ e. W ) -> ( R /.s .~ ) e. _V )
Theorem	qusin 13100	Restrict the equivalence relation in a quotient structure to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ e. W )   &    |- ( ph -> R e. Z )   &    |- ( ph -> ( .~ " V ) C_ V )   =>    |- ( ph -> U = ( R /.s ( .~ i^i ( V X. V ) ) ) )