P. 134 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13301-13400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	basendxnocndx 13301	The slot for the orthocomplementation is not the slot for the base set in an extensible structure. (Contributed by AV, 11-Nov-2024.)
|- ( Base ` ndx ) =/= ( oc ` ndx )
Theorem	plendxnocndx 13302	The slot for the orthocomplementation is not the slot for the order in an extensible structure. (Contributed by AV, 11-Nov-2024.)
|- ( le ` ndx ) =/= ( oc ` ndx )
Theorem	dsndx 13303	Index value of the df-ds 13187 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( dist ` ndx ) = ; 1 2
Theorem	dsid 13304	Utility theorem: index-independent form of df-ds 13187. (Contributed by Mario Carneiro, 23-Dec-2013.)
|- dist = Slot ( dist ` ndx )
Theorem	dsslid 13305	Slot property of dist. (Contributed by Jim Kingdon, 6-May-2023.)
|- ( dist = Slot ( dist ` ndx ) /\ ( dist ` ndx ) e. NN )
Theorem	dsndxnn 13306	The index of the slot for the distance in an extensible structure is a positive integer. (Contributed by AV, 28-Oct-2024.)
|- ( dist ` ndx ) e. NN
Theorem	basendxltdsndx 13307	The index of the slot for the base set is less then the index of the slot for the distance in an extensible structure. (Contributed by AV, 28-Oct-2024.)
|- ( Base ` ndx ) < ( dist ` ndx )
Theorem	dsndxnbasendx 13308	The slot for the distance is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 28-Oct-2024.)
|- ( dist ` ndx ) =/= ( Base ` ndx )
Theorem	dsndxnplusgndx 13309	The slot for the distance function is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.)
|- ( dist ` ndx ) =/= ( +g ` ndx )
Theorem	dsndxnmulrndx 13310	The slot for the distance function is not the slot for the ring multiplication operation in an extensible structure. (Contributed by AV, 31-Oct-2024.)
|- ( dist ` ndx ) =/= ( .r ` ndx )
Theorem	slotsdnscsi 13311	The slots Scalar, .s and .i are different from the slot dist. (Contributed by AV, 29-Oct-2024.)
|- ( ( dist ` ndx ) =/= (Scalar ` ndx ) /\ ( dist ` ndx ) =/= ( .s ` ndx ) /\ ( dist ` ndx ) =/= ( .i ` ndx ) )
Theorem	dsndxntsetndx 13312	The slot for the distance function is not the slot for the topology in an extensible structure. (Contributed by AV, 29-Oct-2024.)
|- ( dist ` ndx ) =/= (TopSet ` ndx )
Theorem	slotsdifdsndx 13313	The index of the slot for the distance is not the index of other slots. (Contributed by AV, 11-Nov-2024.)
|- ( ( *r ` ndx ) =/= ( dist ` ndx ) /\ ( le ` ndx ) =/= ( dist ` ndx ) )
Theorem	unifndx 13314	Index value of the df-unif 13188 slot. (Contributed by Thierry Arnoux, 17-Dec-2017.) (New usage is discouraged.)
|- ( UnifSet ` ndx ) = ; 1 3
Theorem	unifid 13315	Utility theorem: index-independent form of df-unif 13188. (Contributed by Thierry Arnoux, 17-Dec-2017.)
|- UnifSet = Slot ( UnifSet ` ndx )
Theorem	unifndxnn 13316	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 13317	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 13318	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 13319	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 13320	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 13321	Index value of the df-hom 13189 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.)
|- ( Hom ` ndx ) = ; 1 4
Theorem	homid 13322	Utility theorem: index-independent form of df-hom 13189. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- Hom = Slot ( Hom ` ndx )
Theorem	homslid 13323	Slot property of Hom. (Contributed by Jim Kingdon, 20-Mar-2025.)
|- ( Hom = Slot ( Hom ` ndx ) /\ ( Hom ` ndx ) e. NN )
Theorem	ccondx 13324	Index value of the df-cco 13190 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.)
|- (comp ` ndx ) = ; 1 5
Theorem	ccoid 13325	Utility theorem: index-independent form of df-cco 13190. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- comp = Slot (comp ` ndx )
Theorem	ccoslid 13326	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 13327	Extend class notation with the function returning a subspace topology.
class ↾t
Syntax	ctopn 13328	Extend class notation with the topology extractor function.
class TopOpen
Definition	df-rest 13329*	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 13330	Define the topology extractor function. This differs from df-tset 13184 when a structure has been restricted using df-iress 13095; 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 13331	The subspace topology operator is a function on pairs. (Contributed by Mario Carneiro, 1-May-2015.)
|- ↾t Fn ( _V X. _V )
Theorem	topnfn 13332	The topology extractor function is a function on the universe. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- TopOpen Fn _V
Theorem	restval 13333*	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 13334*	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 13335	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 13336	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 13337	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 13338	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 13339	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 13340	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 13341	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 13342	Extend class notation with a function that converts a basis to its corresponding topology.
class topGen
Syntax	cpt 13343	Extend class notation with a function whose value is a product topology.
class Xt_
Syntax	c0g 13344	Extend class notation with group identity element.
class 0g
Syntax	cgsu 13345	Extend class notation to include finitely supported group sums.
class gsumg
Definition	df-0g 13346*	Define group identity element. Remark: this definition is required here because the symbol 0g is already used in df-igsum 13347. 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 13347*	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 13348*	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 13349*	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 13350*	The topology generated by a basis. See also tgval2 14781 and tgval3 14788. (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 13351	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 13352	Existence of the product topology. (Contributed by Jim Kingdon, 19-Mar-2025.)
|- ( F e. V -> ( Xt_ ` F ) e. _V )
Syntax	cprds 13353	The function constructing structure products.
class X_s
Syntax	cpws 13354	The function constructing structure powers.
class ^s
Definition	df-prds 13355*	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 13356	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 13357	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 13358	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 13359	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 13360*	Lemma for prdsval 13361. (Contributed by Stefan O'Rear, 3-Jan-2015.) Extracted from the former proof of prdsval 13361, dependency on df-hom 13189 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 13361*	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 13362	Lemma for prdsbas 13364 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 13363	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 13364*	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 13365*	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 13366*	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 13367*	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 13368*	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 13369	Points in the structure product are functions; use this with dffn5im 5691 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 13370	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 13371*	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 13372	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 13373*	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 13374	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 13375*	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 13376*	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 13377*	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 13378*	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 13379	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 13380	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 13381	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 13382	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 13383	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 13384	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 13385	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 13386*	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 13387	Image structure function.
class "s
Syntax	cqus 13388	Quotient structure function.
class /.s
Syntax	cxps 13389	Binary product structure function.
class X.s
Definition	df-iimas 13390*	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 4738, 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 4737) and/or R ( with df-iress 13095) 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 13391*	Define a quotient ring (or quotient group), which is a special case of an image structure df-iimas 13390 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 13392*	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 13393	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 13394*	Value of an image structure. The is a lemma for the theorems imasbas 13395, imasplusg 13396, and imasmulr 13397 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 13395	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 13396*	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 13397*	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 13398	Lemma for f1ocpbl 13399. (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 13399	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 13400	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 ) ) ) )