P. 135 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13401-13500   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cpt 13401	Extend class notation with a function whose value is a product topology.
class Xt_
Syntax	c0g 13402	Extend class notation with group identity element.
class 0g
Syntax	cgsu 13403	Extend class notation to include finitely supported group sums.
class gsumg
Definition	df-0g 13404*	Define group identity element. Remark: this definition is required here because the symbol 0g is already used in df-igsum 13405. 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 13405*	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 13406*	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 13407*	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 13408*	The topology generated by a basis. See also tgval2 14845 and tgval3 14852. (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 13409	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 13410	Existence of the product topology. (Contributed by Jim Kingdon, 19-Mar-2025.)
|- ( F e. V -> ( Xt_ ` F ) e. _V )
Syntax	cprds 13411	The function constructing structure products.
class X_s
Syntax	cpws 13412	The function constructing structure powers.
class ^s
Definition	df-prds 13413*	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 13414	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 13415	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 13416	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 13417	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 13418*	Lemma for prdsval 13419. (Contributed by Stefan O'Rear, 3-Jan-2015.) Extracted from the former proof of prdsval 13419, dependency on df-hom 13247 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 13419*	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 13420	Lemma for prdsbas 13422 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 13421	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 13422*	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 13423*	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 13424*	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 13425*	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 13426*	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 13427	Points in the structure product are functions; use this with dffn5im 5700 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 13428	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 13429*	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 13430	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 13431*	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 13432	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 13433*	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 13434*	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 13435*	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 13436*	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 13437	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 13438	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 13439	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 13440	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 13441	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 13442	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 13443	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 13444*	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 13445	Image structure function.
class "s
Syntax	cqus 13446	Quotient structure function.
class /.s
Syntax	cxps 13447	Binary product structure function.
class X.s
Definition	df-iimas 13448*	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 4744, 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 4743) and/or R ( with df-iress 13153) 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 13449*	Define a quotient ring (or quotient group), which is a special case of an image structure df-iimas 13448 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 13450*	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 13451	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 13452*	Value of an image structure. The is a lemma for the theorems imasbas 13453, imasplusg 13454, and imasmulr 13455 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 13453	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 13454*	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 13455*	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 13456	Lemma for f1ocpbl 13457. (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 13457	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 13458	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 13459	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 13460*	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 13461*	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 13462*	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 13463*	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 13464*	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 13465*	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 13466*	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 13467*	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 13468*	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 13469*	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 13470*	The function in qusval 13469 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 13471	Existence of a quotient structure. (Contributed by Jim Kingdon, 25-Apr-2025.)
|- ( ( R e. V /\ .~ e. W ) -> ( R /.s .~ ) e. _V )
Theorem	qusin 13472	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 ) ) ) )
Theorem	qusbas 13473	Base set of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ e. W )   &    |- ( ph -> R e. Z )   =>    |- ( ph -> ( V /. .~ ) = ( Base ` U ) )
Theorem	divsfval 13474*	Value of the function in qusval 13469. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
|- ( ph -> .~ Er V )   &    |- ( ph -> V e. W )   &    |- F = ( x e. V |-> [ x ] .~ )   =>    |- ( ph -> ( F ` A ) = [ A ] .~ )
Theorem	divsfvalg 13475*	Value of the function in qusval 13469. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
|- ( ph -> .~ Er V )   &    |- ( ph -> V e. W )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> A e. V )   =>    |- ( ph -> ( F ` A ) = [ A ] .~ )
Theorem	ercpbllemg 13476*	Lemma for ercpbl 13477. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by AV, 12-Jul-2024.)
|- ( ph -> .~ Er V )   &    |- ( ph -> V e. W )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. V )   =>    |- ( ph -> ( ( F ` A ) = ( F ` B ) <-> A .~ B ) )
Theorem	ercpbl 13477*	Translate the function compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
|- ( ph -> .~ Er V )   &    |- ( ph -> V e. W )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( a .+ b ) e. V )   &    |- ( ph -> ( ( A .~ C /\ B .~ D ) -> ( A .+ B ) .~ ( C .+ D ) ) )   =>    |- ( ( 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	erlecpbl 13478*	Translate the relation compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
|- ( ph -> .~ Er V )   &    |- ( ph -> V e. W )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> ( ( A .~ C /\ B .~ D ) -> ( A N B <-> C N D ) ) )   =>    |- ( ( 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	qusaddvallemg 13479*	Value of an operation defined on a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ Er V )   &    |- ( ph -> R e. Z )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )   &    |- ( ph -> .x. e. W )   =>    |- ( ( ph /\ X e. V /\ Y e. V ) -> ( [ X ] .~ .xb [ Y ] .~ ) = [ ( X .x. Y ) ] .~ )
Theorem	qusaddflemg 13480*	The operation of a quotient structure is a function. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ Er V )   &    |- ( ph -> R e. Z )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   &    |- F = ( x e. V |-> [ x ] .~ )   &    |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )   &    |- ( ph -> .x. e. W )   =>    |- ( ph -> .xb : ( ( V /. .~ ) X. ( V /. .~ ) ) --> ( V /. .~ ) )
Theorem	qusaddval 13481*	The addition in a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ Er V )   &    |- ( ph -> R e. Z )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   &    |- .x. = ( +g ` R )   &    |- .xb = ( +g ` U )   =>    |- ( ( ph /\ X e. V /\ Y e. V ) -> ( [ X ] .~ .xb [ Y ] .~ ) = [ ( X .x. Y ) ] .~ )
Theorem	qusaddf 13482*	The addition in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ Er V )   &    |- ( ph -> R e. Z )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   &    |- .x. = ( +g ` R )   &    |- .xb = ( +g ` U )   =>    |- ( ph -> .xb : ( ( V /. .~ ) X. ( V /. .~ ) ) --> ( V /. .~ ) )
Theorem	qusmulval 13483*	The multiplication in a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ Er V )   &    |- ( ph -> R e. Z )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` U )   =>    |- ( ( ph /\ X e. V /\ Y e. V ) -> ( [ X ] .~ .xb [ Y ] .~ ) = [ ( X .x. Y ) ] .~ )
Theorem	qusmulf 13484*	The multiplication in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- ( ph -> .~ Er V )   &    |- ( ph -> R e. Z )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )   &    |- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` U )   =>    |- ( ph -> .xb : ( ( V /. .~ ) X. ( V /. .~ ) ) --> ( V /. .~ ) )
Theorem	fnpr2o 13485	Function with a domain of 2o. (Contributed by Jim Kingdon, 25-Sep-2023.)
|- ( ( A e. V /\ B e. W ) -> { <. (/) , A >. , <. 1o , B >. } Fn 2o )
Theorem	fnpr2ob 13486	Biconditional version of fnpr2o 13485. (Contributed by Jim Kingdon, 27-Sep-2023.)
|- ( ( A e. _V /\ B e. _V ) <-> { <. (/) , A >. , <. 1o , B >. } Fn 2o )
Theorem	fvpr0o 13487	The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.)
|- ( A e. V -> ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) = A )
Theorem	fvpr1o 13488	The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.)
|- ( B e. V -> ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) = B )
Theorem	fvprif 13489	The value of the pair function at an element of 2o. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( ( A e. V /\ B e. W /\ C e. 2o ) -> ( { <. (/) , A >. , <. 1o , B >. } ` C ) = if ( C = (/) , A , B ) )
Theorem	xpsfrnel 13490*	Elementhood in the target space of the function F appearing in xpsval 13498. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( G e. X_ k e. 2o if ( k = (/) , A , B ) <-> ( G Fn 2o /\ ( G ` (/) ) e. A /\ ( G ` 1o ) e. B ) )
Theorem	xpsfeq 13491	A function on 2o is determined by its values at zero and one. (Contributed by Mario Carneiro, 27-Aug-2015.)
|- ( G Fn 2o -> { <. (/) , ( G ` (/) ) >. , <. 1o , ( G ` 1o ) >. } = G )
Theorem	xpsfrnel2 13492*	Elementhood in the target space of the function F appearing in xpsval 13498. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- ( { <. (/) , X >. , <. 1o , Y >. } e. X_ k e. 2o if ( k = (/) , A , B ) <-> ( X e. A /\ Y e. B ) )
Theorem	xpscf 13493	Equivalent condition for the pair function to be a proper function on A. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( { <. (/) , X >. , <. 1o , Y >. } : 2o --> A <-> ( X e. A /\ Y e. A ) )
Theorem	xpsfval 13494*	The value of the function appearing in xpsval 13498. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- F = ( x e. A , y e. B |-> { <. (/) , x >. , <. 1o , y >. } )   =>    |- ( ( X e. A /\ Y e. B ) -> ( X F Y ) = { <. (/) , X >. , <. 1o , Y >. } )
Theorem	xpsff1o 13495*	The function appearing in xpsval 13498 is a bijection from the cartesian product to the indexed cartesian product indexed on the pair 2o = { (/) , 1o }. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- F = ( x e. A , y e. B |-> { <. (/) , x >. , <. 1o , y >. } )   =>    |- F : ( A X. B ) -1-1-onto-> X_ k e. 2o if ( k = (/) , A , B )
Theorem	xpsfrn 13496*	A short expression for the indexed cartesian product on two indices. (Contributed by Mario Carneiro, 15-Aug-2015.)
|- F = ( x e. A , y e. B |-> { <. (/) , x >. , <. 1o , y >. } )   =>    |- ran F = X_ k e. 2o if ( k = (/) , A , B )
Theorem	xpsff1o2 13497*	The function appearing in xpsval 13498 is a bijection from the cartesian product to the indexed cartesian product indexed on the pair 2o = { (/) , 1o }. (Contributed by Mario Carneiro, 24-Jan-2015.)
|- F = ( x e. A , y e. B |-> { <. (/) , x >. , <. 1o , y >. } )   =>    |- F : ( A X. B ) -1-1-onto-> ran F
Theorem	xpsval 13498*	Value of the binary structure product function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.)
|- T = ( R X.s S )   &    |- X = ( Base ` R )   &    |- Y = ( Base ` S )   &    |- ( ph -> R e. V )   &    |- ( ph -> S e. W )   &    |- F = ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } )   &    |- G = (Scalar ` R )   &    |- U = ( G X_s { <. (/) , R >. , <. 1o , S >. } )   =>    |- ( ph -> T = ( `' F "s U ) )
PART 7  BASIC ALGEBRAIC STRUCTURES
7.1  Monoids
7.1.1  Magmas According to Wikipedia ("Magma (algebra)", 08-Jan-2020, https://en.wikipedia.org/wiki/magma_(algebra)) "In abstract algebra, a magma [...] is a basic kind of algebraic structure. Specifically, a magma consists of a set equipped with a single binary operation. The binary operation must be closed by definition but no other properties are imposed.". Since the concept of a "binary operation" is used in different variants, these differences are explained in more detail in the following: With df-mpo 6033, binary operations are defined by a rule, and with df-ov 6031, the value of a binary operation applied to two operands can be expressed. In both cases, the two operands can belong to different sets, and the result can be an element of a third set. However, according to Wikipedia "Binary operation", see https://en.wikipedia.org/wiki/Binary_operation 6031 (19-Jan-2020), "... a binary operation on a set S is a mapping of the elements of the Cartesian product S X. S to S: f : S X. S --> S. Because the result of performing the operation on a pair of elements of S is again an element of S, the operation is called a closed binary operation on S (or sometimes expressed as having the property of closure).". To distinguish this more restrictive definition (in Wikipedia and most of the literature) from the general case, binary operations mapping the elements of the Cartesian product S X. S are more precisely called internal binary operations. If, in addition, the result is also contained in the set S, the operation should be called closed internal binary operation. Therefore, a "binary operation on a set S" according to Wikipedia is a "closed internal binary operation" in a more precise terminology. If the sets are different, the operation is explicitly called external binary operation (see Wikipedia https://en.wikipedia.org/wiki/Binary_operation#External_binary_operations 6031). The definition of magmas (Mgm, see df-mgm 13502) concentrates on the closure property of the associated operation, and poses no additional restrictions on it. In this way, it is most general and flexible.
Syntax	cplusf 13499	Extend class notation with group addition as a function.
class +f
Syntax	cmgm 13500	Extend class notation with class of all magmas.
class Mgm