P. 137 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13601-13700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	qusmulval 13601*	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 13602*	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 13603	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 13604	Biconditional version of fnpr2o 13603. (Contributed by Jim Kingdon, 27-Sep-2023.)
|- ( ( A e. _V /\ B e. _V ) <-> { <. (/) , A >. , <. 1o , B >. } Fn 2o )
Theorem	fvpr0o 13605	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 13606	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 13607	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 13608*	Elementhood in the target space of the function F appearing in xpsval 14143. (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 13609	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 13610*	Elementhood in the target space of the function F appearing in xpsval 14143. (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 13611	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 13612*	The value of the function appearing in xpsval 14143. (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 13613*	The function appearing in xpsval 14143 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 13614*	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 13615*	The function appearing in xpsval 14143 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
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 6063, binary operations are defined by a rule, and with df-ov 6061, 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 6061 (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 6061). The definition of magmas (Mgm, see df-mgm 13619) 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 13616	Extend class notation with group addition as a function.
class +f
Syntax	cmgm 13617	Extend class notation with class of all magmas.
class Mgm
Definition	df-plusf 13618*	Define group addition function. Usually we will use +g directly instead of +f, and they have the same behavior in most cases. The main advantage of +f for any magma is that it is a guaranteed function (mgmplusf 13629), while +g only has closure (mgmcl 13622). (Contributed by Mario Carneiro, 14-Aug-2015.)
|- +f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )
Definition	df-mgm 13619*	A magma is a set equipped with an everywhere defined internal operation. Definition 1 in [BourbakiAlg1] p. 1, or definition of a groupoid in section I.1 of [Bruck] p. 1. Note: The term "groupoid" is now widely used to refer to other objects: (small) categories all of whose morphisms are invertible, or groups with a partial function replacing the binary operation. Therefore, we will only use the term "magma" for the present notion in set.mm. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
|- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
Theorem	ismgm 13620*	The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( M e. V -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) )
Theorem	ismgmn0 13621*	The predicate "is a magma" for a structure with a nonempty base set. (Contributed by AV, 29-Jan-2020.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( A e. B -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) )
Theorem	mgmcl 13622	Closure of the operation of a magma. (Contributed by FL, 14-Sep-2010.) (Revised by AV, 13-Jan-2020.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( ( M e. Mgm /\ X e. B /\ Y e. B ) -> ( X .o. Y ) e. B )
Theorem	isnmgm 13623	A condition for a structure not to be a magma. (Contributed by AV, 30-Jan-2020.) (Proof shortened by NM, 5-Feb-2020.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( ( X e. B /\ Y e. B /\ ( X .o. Y ) e/ B ) -> M e/ Mgm )
Theorem	mgmsscl 13624	If the base set of a magma is contained in the base set of another magma, and the group operation of the magma is the restriction of the group operation of the other magma to its base set, then the base set of the magma is closed under the group operation of the other magma. (Contributed by AV, 17-Feb-2024.)
|- B = ( Base ` G )   &    |- S = ( Base ` H )   =>    |- ( ( ( G e. Mgm /\ H e. Mgm ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) /\ ( X e. S /\ Y e. S ) ) -> ( X ( +g ` G ) Y ) e. S )
Theorem	plusffvalg 13625*	The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Proof shortened by AV, 2-Mar-2024.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .+^ = ( +f ` G )   =>    |- ( G e. V -> .+^ = ( x e. B , y e. B |-> ( x .+ y ) ) )
Theorem	plusfvalg 13626	The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .+^ = ( +f ` G )   =>    |- ( ( G e. V /\ X e. B /\ Y e. B ) -> ( X .+^ Y ) = ( X .+ Y ) )
Theorem	plusfeqg 13627	If the addition operation is already a function, the functionalization of it is equal to the original operation. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .+^ = ( +f ` G )   =>    |- ( ( G e. V /\ .+ Fn ( B X. B ) ) -> .+^ = .+ )
Theorem	plusffng 13628	The group addition operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015.)
|- B = ( Base ` G )   &    |- .+^ = ( +f ` G )   =>    |- ( G e. V -> .+^ Fn ( B X. B ) )
Theorem	mgmplusf 13629	The group addition function of a magma is a function into its base set. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revisd by AV, 28-Jan-2020.)
|- B = ( Base ` M )   &    |- .+^ = ( +f ` M )   =>    |- ( M e. Mgm -> .+^ : ( B X. B ) --> B )
Theorem	intopsn 13630	The internal operation for a set is the trivial operation iff the set is a singleton. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 23-Jan-2020.)
|- ( ( .o. : ( B X. B ) --> B /\ Z e. B ) -> ( B = { Z } <-> .o. = { <. <. Z , Z >. , Z >. } ) )
Theorem	mgmb1mgm1 13631	The only magma with a base set consisting of one element is the trivial magma (at least if its operation is an internal binary operation). (Contributed by AV, 23-Jan-2020.) (Revised by AV, 7-Feb-2020.)
|- B = ( Base ` M )   &    |- .+ = ( +g ` M )   =>    |- ( ( M e. Mgm /\ Z e. B /\ .+ Fn ( B X. B ) ) -> ( B = { Z } <-> .+ = { <. <. Z , Z >. , Z >. } ) )
Theorem	mgm0 13632	Any set with an empty base set and any group operation is a magma. (Contributed by AV, 28-Aug-2021.)
|- ( ( M e. V /\ ( Base ` M ) = (/) ) -> M e. Mgm )
Theorem	mgm1 13633	The structure with one element and the only closed internal operation for a singleton is a magma. (Contributed by AV, 10-Feb-2020.)
|- M = { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. }   =>    |- ( I e. V -> M e. Mgm )
Theorem	opifismgmdc 13634*	A structure with a group addition operation expressed by a conditional operator is a magma if both values of the conditional operator are contained in the base set. (Contributed by AV, 9-Feb-2020.)
|- B = ( Base ` M )   &    |- ( +g ` M ) = ( x e. B , y e. B |-> if ( ps , C , D ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> DECID ps )   &    |- ( ph -> E. x x e. B )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> C e. B )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> D e. B )   =>    |- ( ph -> M e. Mgm )
7.1.2  Identity elements According to Wikipedia ("Identity element", 7-Feb-2020, https://en.wikipedia.org/wiki/Identity_element): "In mathematics, an identity element, or neutral element, is a special type of element of a set with respect to a binary operation on that set, which leaves any element of the set unchanged when combined with it.". Or in more detail "... an element e of S is called a left identity if e * a = a for all a in S, and a right identity if a * e = a for all a in S. If e is both a left identity and a right identity, then it is called a two-sided identity, or simply an identity." We concentrate on two-sided identities in the following. The existence of an identity (an identity is unique if it exists, see mgmidmo 13635) is an important property of monoids, and therefore also for groups, but also for magmas not required to be associative. Magmas with an identity element are called "unital magmas" (see Definition 2 in [BourbakiAlg1] p. 12) or, if the magmas are cancellative, "loops" (see definition in [Bruck] p. 15). In the context of extensible structures, the identity element (of any magma M) is defined as "group identity element" ( 0g ` M ), see df-0g 13555. Related theorems which are already valid for magmas are provided in the following.
Theorem	mgmidmo 13635*	A two-sided identity element is unique (if it exists) in any magma. (Contributed by Mario Carneiro, 7-Dec-2014.) (Revised by NM, 17-Jun-2017.)
|- E* u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x )
Theorem	grpidvalg 13636*	The value of the identity element of a group. (Contributed by NM, 20-Aug-2011.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( G e. V -> .0. = ( iota e ( e e. B /\ A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) ) )
Theorem	grpidpropdg 13637*	If two structures have the same base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, they have the same identity element. (Contributed by Mario Carneiro, 27-Nov-2014.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ph -> K e. V )   &    |- ( ph -> L e. W )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   =>    |- ( ph -> ( 0g ` K ) = ( 0g ` L ) )
Theorem	fn0g 13638	The group zero extractor is a function. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- 0g Fn _V
Theorem	0g0 13639	The identity element function evaluates to the empty set on an empty structure. (Contributed by Stefan O'Rear, 2-Oct-2015.)
|- (/) = ( 0g ` (/) )
Theorem	ismgmid 13640*	The identity element of a magma, if it exists, belongs to the base set. (Contributed by Mario Carneiro, 27-Dec-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> E. e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )   =>    |- ( ph -> ( ( U e. B /\ A. x e. B ( ( U .+ x ) = x /\ ( x .+ U ) = x ) ) <-> .0. = U ) )
Theorem	mgmidcl 13641*	The identity element of a magma, if it exists, belongs to the base set. (Contributed by Mario Carneiro, 27-Dec-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> E. e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )   =>    |- ( ph -> .0. e. B )
Theorem	mgmlrid 13642*	The identity element of a magma, if it exists, is a left and right identity. (Contributed by Mario Carneiro, 27-Dec-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> E. e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )   =>    |- ( ( ph /\ X e. B ) -> ( ( .0. .+ X ) = X /\ ( X .+ .0. ) = X ) )
Theorem	ismgmid2 13643*	Show that a given element is the identity element of a magma. (Contributed by Mario Carneiro, 27-Dec-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> U e. B )   &    |- ( ( ph /\ x e. B ) -> ( U .+ x ) = x )   &    |- ( ( ph /\ x e. B ) -> ( x .+ U ) = x )   =>    |- ( ph -> U = .0. )
Theorem	lidrideqd 13644*	If there is a left and right identity element for any binary operation (group operation) .+, both identity elements are equal. Generalization of statement in [Lang] p. 3: it is sufficient that "e" is a left identity element and "e`" is a right identity element instead of both being (two-sided) identity elements. (Contributed by AV, 26-Dec-2023.)
|- ( ph -> L e. B )   &    |- ( ph -> R e. B )   &    |- ( ph -> A. x e. B ( L .+ x ) = x )   &    |- ( ph -> A. x e. B ( x .+ R ) = x )   =>    |- ( ph -> L = R )
Theorem	lidrididd 13645*	If there is a left and right identity element for any binary operation (group operation) .+, the left identity element (and therefore also the right identity element according to lidrideqd 13644) is equal to the two-sided identity element. (Contributed by AV, 26-Dec-2023.)
|- ( ph -> L e. B )   &    |- ( ph -> R e. B )   &    |- ( ph -> A. x e. B ( L .+ x ) = x )   &    |- ( ph -> A. x e. B ( x .+ R ) = x )   &    |- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ph -> L = .0. )
Theorem	grpidd 13646*	Deduce the identity element of a magma from its properties. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> .+ = ( +g ` G ) )   &    |- ( ph -> .0. e. B )   &    |- ( ( ph /\ x e. B ) -> ( .0. .+ x ) = x )   &    |- ( ( ph /\ x e. B ) -> ( x .+ .0. ) = x )   =>    |- ( ph -> .0. = ( 0g ` G ) )
Theorem	mgmidsssn0 13647*	Property of the set of identities of G. Either G has no identities, and O = (/), or it has one and this identity is unique and identified by the 0g function. (Contributed by Mario Carneiro, 7-Dec-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- O = { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) }   =>    |- ( G e. V -> O C_ { .0. } )
Theorem	grpinvalem 13648*	Lemma for grpinva 13649. (Contributed by NM, 9-Aug-2013.)
|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )   &    |- ( ph -> O e. B )   &    |- ( ( ph /\ x e. B ) -> ( O .+ x ) = x )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = O )   &    |- ( ( ph /\ ps ) -> X e. B )   &    |- ( ( ph /\ ps ) -> ( X .+ X ) = X )   =>    |- ( ( ph /\ ps ) -> X = O )
Theorem	grpinva 13649*	Deduce right inverse from left inverse and left identity in an associative structure (such as a group). (Contributed by NM, 10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )   &    |- ( ph -> O e. B )   &    |- ( ( ph /\ x e. B ) -> ( O .+ x ) = x )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = O )   &    |- ( ( ph /\ ps ) -> X e. B )   &    |- ( ( ph /\ ps ) -> N e. B )   &    |- ( ( ph /\ ps ) -> ( N .+ X ) = O )   =>    |- ( ( ph /\ ps ) -> ( X .+ N ) = O )
Theorem	grprida 13650*	Deduce right identity from left inverse and left identity in an associative structure (such as a group). (Contributed by NM, 10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )   &    |- ( ph -> O e. B )   &    |- ( ( ph /\ x e. B ) -> ( O .+ x ) = x )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = O )   =>    |- ( ( ph /\ x e. B ) -> ( x .+ O ) = x )
7.1.3  Iterated sums in a magma The symbol gsumg is mostly used in the context of abelian groups. Therefore, it is usually called "group sum". It can be defined, however, in arbitrary magmas (then it should be called "iterated sum"). If the magma is not required to be commutative or associative, then the order of the summands and the order in which summations are done become important. If the magma is not unital, then one cannot define a meaningful empty sum. See the comment for df-igsum 13556.
Theorem	fngsum 13651	Iterated sum has a universal domain. (Contributed by Jim Kingdon, 28-Jun-2025.)
|- gsumg Fn ( _V X. _V )
Theorem	igsumvalx 13652*	Expand out the substitutions in df-igsum 13556. (Contributed by Mario Carneiro, 18-Sep-2015.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> F e. X )   &    |- ( ph -> dom F = A )   =>    |- ( ph -> ( G gsumg F ) = ( iota x ( ( A = (/) /\ x = .0. ) \/ E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) ) )
Theorem	igsumval 13653*	Expand out the substitutions in df-igsum 13556. (Contributed by Mario Carneiro, 7-Dec-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> A e. X )   &    |- ( ph -> F : A --> B )   =>    |- ( ph -> ( G gsumg F ) = ( iota x ( ( A = (/) /\ x = .0. ) \/ E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) ) )
Theorem	gsumfzval 13654	An expression for gsumg when summing over a finite set of sequential integers. (Contributed by Jim Kingdon, 14-Aug-2025.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> F : ( M ... N ) --> B )   =>    |- ( ph -> ( G gsumg F ) = if ( N < M , .0. , ( seq M ( .+ , F ) ` N ) ) )
Theorem	gsumpropd 13655	The group sum depends only on the base set and additive operation. (Contributed by Stefan O'Rear, 1-Feb-2015.) (Proof shortened by Mario Carneiro, 18-Sep-2015.)
|- ( ph -> F e. V )   &    |- ( ph -> G e. W )   &    |- ( ph -> H e. X )   &    |- ( ph -> ( Base ` G ) = ( Base ` H ) )   &    |- ( ph -> ( +g ` G ) = ( +g ` H ) )   =>    |- ( ph -> ( G gsumg F ) = ( H gsumg F ) )
Theorem	gsumpropd2 13656*	A stronger version of gsumpropd 13655, working for magma, where only the closure of the addition operation on a common base is required, see gsummgmpropd 13657. (Contributed by Thierry Arnoux, 28-Jun-2017.)
|- ( ph -> F e. V )   &    |- ( ph -> G e. W )   &    |- ( ph -> H e. X )   &    |- ( ph -> ( Base ` G ) = ( Base ` H ) )   &    |- ( ( ph /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( s ( +g ` G ) t ) e. ( Base ` G ) )   &    |- ( ( ph /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( s ( +g ` G ) t ) = ( s ( +g ` H ) t ) )   &    |- ( ph -> Fun F )   &    |- ( ph -> ran F C_ ( Base ` G ) )   =>    |- ( ph -> ( G gsumg F ) = ( H gsumg F ) )
Theorem	gsummgmpropd 13657*	A stronger version of gsumpropd 13655 if at least one of the involved structures is a magma, see gsumpropd2 13656. (Contributed by AV, 31-Jan-2020.)
|- ( ph -> F e. V )   &    |- ( ph -> G e. W )   &    |- ( ph -> H e. X )   &    |- ( ph -> ( Base ` G ) = ( Base ` H ) )   &    |- ( ph -> G e. Mgm )   &    |- ( ( ph /\ ( s e. ( Base ` G ) /\ t e. ( Base ` G ) ) ) -> ( s ( +g ` G ) t ) = ( s ( +g ` H ) t ) )   &    |- ( ph -> Fun F )   &    |- ( ph -> ran F C_ ( Base ` G ) )   =>    |- ( ph -> ( G gsumg F ) = ( H gsumg F ) )
Theorem	gsumress 13658*	The group sum in a substructure is the same as the group sum in the original structure. The only requirement on the substructure is that it contain the identity element; neither G nor H need be groups. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- H = ( G ↾s S )   &    |- ( ph -> G e. V )   &    |- ( ph -> A e. X )   &    |- ( ph -> S C_ B )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> .0. e. S )   &    |- ( ( ph /\ x e. B ) -> ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) )   =>    |- ( ph -> ( G gsumg F ) = ( H gsumg F ) )
Theorem	gsum0g 13659	Value of the empty group sum. (Contributed by Mario Carneiro, 7-Dec-2014.)
|- .0. = ( 0g ` G )   =>    |- ( G e. V -> ( G gsumg (/) ) = .0. )
Theorem	gsumval2 13660	Value of the group sum operation over a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Dec-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> F : ( M ... N ) --> B )   =>    |- ( ph -> ( G gsumg F ) = ( seq M ( .+ , F ) ` N ) )
Theorem	gsumsplit1r 13661	Splitting off the rightmost summand of a group sum. This corresponds to the (inductive) definition of a (finite) product in [Lang] p. 4, first formula. (Contributed by AV, 26-Dec-2023.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> F : ( M ... ( N + 1 ) ) --> B )   =>    |- ( ph -> ( G gsumg F ) = ( ( G gsumg ( F |` ( M ... N ) ) ) .+ ( F ` ( N + 1 ) ) ) )
Theorem	gsumprval 13662	Value of the group sum operation over a pair of sequential integers. (Contributed by AV, 14-Dec-2018.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N = ( M + 1 ) )   &    |- ( ph -> F : { M , N } --> B )   =>    |- ( ph -> ( G gsumg F ) = ( ( F ` M ) .+ ( F ` N ) ) )
Theorem	gsumpr12val 13663	Value of the group sum operation over the pair { 1 , 2 }. (Contributed by AV, 14-Dec-2018.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. V )   &    |- ( ph -> F : { 1 , 2 } --> B )   =>    |- ( ph -> ( G gsumg F ) = ( ( F ` 1 ) .+ ( F ` 2 ) ) )
7.1.4  Semigroups A semigroup (Smgrp, see df-sgrp 13665) is a set together with an associative binary operation (see Wikipedia, Semigroup, 8-Jan-2020, https://en.wikipedia.org/wiki/Semigroup 13665). In other words, a semigroup is an associative magma. The notion of semigroup is a generalization of that of group where the existence of an identity or inverses is not required.
Syntax	csgrp 13664	Extend class notation with class of all semigroups.
class Smgrp
Definition	df-sgrp 13665*	A semigroup is a set equipped with an everywhere defined internal operation (so, a magma, see df-mgm 13619), whose operation is associative. Definition in section II.1 of [Bruck] p. 23, or of an "associative magma" in definition 5 of [BourbakiAlg1] p. 4 . (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
|- Smgrp = { g e. Mgm | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b A. z e. b ( ( x o y ) o z ) = ( x o ( y o z ) ) }
Theorem	issgrp 13666*	The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( M e. Smgrp <-> ( M e. Mgm /\ A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )
Theorem	issgrpv 13667*	The predicate "is a semigroup" for a structure which is a set. (Contributed by AV, 1-Feb-2020.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( M e. V -> ( M e. Smgrp <-> A. x e. B A. y e. B ( ( x .o. y ) e. B /\ A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) )
Theorem	issgrpn0 13668*	The predicate "is a semigroup" for a structure with a nonempty base set. (Contributed by AV, 1-Feb-2020.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( A e. B -> ( M e. Smgrp <-> A. x e. B A. y e. B ( ( x .o. y ) e. B /\ A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) )
Theorem	isnsgrp 13669	A condition for a structure not to be a semigroup. (Contributed by AV, 30-Jan-2020.)
|- B = ( Base ` M )   &    |- .o. = ( +g ` M )   =>    |- ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) -> M e/ Smgrp ) )
Theorem	sgrpmgm 13670	A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
|- ( M e. Smgrp -> M e. Mgm )
Theorem	sgrpass 13671	A semigroup operation is associative. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 30-Jan-2020.)
|- B = ( Base ` G )   &    |- .o. = ( +g ` G )   =>    |- ( ( G e. Smgrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) )
Theorem	sgrpcl 13672	Closure of the operation of a semigroup. (Contributed by AV, 15-Feb-2025.)
|- B = ( Base ` G )   &    |- .o. = ( +g ` G )   =>    |- ( ( G e. Smgrp /\ X e. B /\ Y e. B ) -> ( X .o. Y ) e. B )
Theorem	sgrp0 13673	Any set with an empty base set and any group operation is a semigroup. (Contributed by AV, 28-Aug-2021.)
|- ( ( M e. V /\ ( Base ` M ) = (/) ) -> M e. Smgrp )
Theorem	sgrp1 13674	The structure with one element and the only closed internal operation for a singleton is a semigroup. (Contributed by AV, 10-Feb-2020.)
|- M = { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. }   =>    |- ( I e. V -> M e. Smgrp )
Theorem	issgrpd 13675*	Deduce a semigroup from its properties. (Contributed by AV, 13-Feb-2025.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> .+ = ( +g ` G ) )   &    |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ph -> G e. V )   =>    |- ( ph -> G e. Smgrp )
Theorem	sgrppropd 13676*	If two structures are sets, have the same base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, one is a semigroup iff the other one is. (Contributed by AV, 15-Feb-2025.)
|- ( ph -> K e. V )   &    |- ( ph -> L e. W )   &    |- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   =>    |- ( ph -> ( K e. Smgrp <-> L e. Smgrp ) )
7.1.5  Definition and basic properties of monoids According to Wikipedia ("Monoid", https://en.wikipedia.org/wiki/Monoid, 6-Feb-2020,) "In abstract algebra [...] a monoid is an algebraic structure with a single associative binary operation and an identity element. Monoids are semigroups with identity.". In the following, monoids are defined in the second way (as semigroups with identity), see df-mnd 13678, whereas many authors define magmas in the first way (as algebraic structure with a single associative binary operation and an identity element, i.e. without the need of a definition for/knowledge about semigroups), see ismnd 13680. See, for example, the definition in [Lang] p. 3: "A monoid is a set G, with a law of composition which is associative, and having a unit element".
Syntax	cmnd 13677	Extend class notation with class of all monoids.
class Mnd
Definition	df-mnd 13678*	A monoid is a semigroup, which has a two-sided neutral element. Definition 2 in [BourbakiAlg1] p. 12. In other words (according to the definition in [Lang] p. 3), a monoid is a set equipped with an everywhere defined internal operation (see mndcl 13684), whose operation is associative (see mndass 13685) and has a two-sided neutral element (see mndid 13686), see also ismnd 13680. (Contributed by Mario Carneiro, 6-Jan-2015.) (Revised by AV, 1-Feb-2020.)
|- Mnd = { g e. Smgrp | [. ( Base ` g ) / b ]. [. ( +g ` g ) / p ]. E. e e. b A. x e. b ( ( e p x ) = x /\ ( x p e ) = x ) }
Theorem	ismnddef 13679*	The predicate "is a monoid", corresponding 1-to-1 to the definition. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 1-Feb-2020.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. Mnd <-> ( G e. Smgrp /\ E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) )
Theorem	ismnd 13680*	The predicate "is a monoid". This is the defining theorem of a monoid by showing that a set is a monoid if and only if it is a set equipped with a closed, everywhere defined internal operation (so, a magma, see mndcl 13684), whose operation is associative (so, a semigroup, see also mndass 13685) and has a two-sided neutral element (see mndid 13686). (Contributed by Mario Carneiro, 6-Jan-2015.) (Revised by AV, 1-Feb-2020.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. Mnd <-> ( A. a e. B A. b e. B ( ( a .+ b ) e. B /\ A. c e. B ( ( a .+ b ) .+ c ) = ( a .+ ( b .+ c ) ) ) /\ E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) )
Theorem	sgrpidmndm 13681*	A semigroup with an identity element which is inhabited is a monoid. Of course there could be monoids with the empty set as identity element, but these cannot be proven to be monoids with this theorem. (Contributed by AV, 29-Jan-2024.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Smgrp /\ E. e e. B ( E. w w e. e /\ e = .0. ) ) -> G e. Mnd )
Theorem	mndsgrp 13682	A monoid is a semigroup. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) (Proof shortened by AV, 6-Feb-2020.)
|- ( G e. Mnd -> G e. Smgrp )
Theorem	mndmgm 13683	A monoid is a magma. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) (Proof shortened by AV, 6-Feb-2020.)
|- ( M e. Mnd -> M e. Mgm )
Theorem	mndcl 13684	Closure of the operation of a monoid. (Contributed by NM, 14-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Proof shortened by AV, 8-Feb-2020.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Mnd /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
Theorem	mndass 13685	A monoid operation is associative. (Contributed by NM, 14-Aug-2011.) (Proof shortened by AV, 8-Feb-2020.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Mnd /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .+ Z ) = ( X .+ ( Y .+ Z ) ) )
Theorem	mndid 13686*	A monoid has a two-sided identity element. (Contributed by NM, 16-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. Mnd -> E. u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) )
Theorem	mndideu 13687*	The two-sided identity element of a monoid is unique. Lemma 2.2.1(a) of [Herstein] p. 55. (Contributed by Mario Carneiro, 8-Dec-2014.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. Mnd -> E! u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) )
Theorem	mnd32g 13688	Commutative/associative law for monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> ( Y .+ Z ) = ( Z .+ Y ) )   =>    |- ( ph -> ( ( X .+ Y ) .+ Z ) = ( ( X .+ Z ) .+ Y ) )
Theorem	mnd12g 13689	Commutative/associative law for monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> ( X .+ Y ) = ( Y .+ X ) )   =>    |- ( ph -> ( X .+ ( Y .+ Z ) ) = ( Y .+ ( X .+ Z ) ) )
Theorem	mnd4g 13690	Commutative/associative law for commutative monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> W e. B )   &    |- ( ph -> ( Y .+ Z ) = ( Z .+ Y ) )   =>    |- ( ph -> ( ( X .+ Y ) .+ ( Z .+ W ) ) = ( ( X .+ Z ) .+ ( Y .+ W ) ) )
Theorem	mndidcl 13691	The identity element of a monoid belongs to the monoid. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( G e. Mnd -> .0. e. B )
Theorem	mndbn0 13692	The base set of a monoid is not empty. (It is also inhabited, as seen at mndidcl 13691). Statement in [Lang] p. 3. (Contributed by AV, 29-Dec-2023.)
|- B = ( Base ` G )   =>    |- ( G e. Mnd -> B =/= (/) )
Theorem	hashfinmndnn 13693	A finite monoid has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- B = ( Base ` G )   &    |- ( ph -> G e. Mnd )   &    |- ( ph -> B e. Fin )   =>    |- ( ph -> (♯ ` B ) e. NN )
Theorem	mndplusf 13694	The group addition operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Proof shortened by AV, 3-Feb-2020.)
|- B = ( Base ` G )   &    |- .+^ = ( +f ` G )   =>    |- ( G e. Mnd -> .+^ : ( B X. B ) --> B )
Theorem	mndlrid 13695	A monoid's identity element is a two-sided identity. (Contributed by NM, 18-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Mnd /\ X e. B ) -> ( ( .0. .+ X ) = X /\ ( X .+ .0. ) = X ) )
Theorem	mndlid 13696	The identity element of a monoid is a left identity. (Contributed by NM, 18-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Mnd /\ X e. B ) -> ( .0. .+ X ) = X )
Theorem	mndrid 13697	The identity element of a monoid is a right identity. (Contributed by NM, 18-Aug-2011.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ( G e. Mnd /\ X e. B ) -> ( X .+ .0. ) = X )
Theorem	ismndd 13698*	Deduce a monoid from its properties. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> .+ = ( +g ` G ) )   &    |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ph -> .0. e. B )   &    |- ( ( ph /\ x e. B ) -> ( .0. .+ x ) = x )   &    |- ( ( ph /\ x e. B ) -> ( x .+ .0. ) = x )   =>    |- ( ph -> G e. Mnd )
Theorem	mndpfo 13699	The addition operation of a monoid as a function is an onto function. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 11-Oct-2013.) (Revised by AV, 23-Jan-2020.)
|- B = ( Base ` G )   &    |- .+^ = ( +f ` G )   =>    |- ( G e. Mnd -> .+^ : ( B X. B ) -onto-> B )
Theorem	mndfo 13700	The addition operation of a monoid is an onto function (assuming it is a function). (Contributed by Mario Carneiro, 11-Oct-2013.) (Proof shortened by AV, 23-Jan-2020.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Mnd /\ .+ Fn ( B X. B ) ) -> .+ : ( B X. B ) -onto-> B )