P. 147 of Theorem List - Metamath Proof Explorer

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

Theorem List for Metamath Proof Explorer - 14601-14700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	psss 14601	Any subset of a partially ordered set is partially ordered. (Contributed by FL, 24-Jan-2010.)
|- ( R e. PosetRel -> ( R i^i ( A X. A ) ) e. PosetRel )
Theorem	psssdm2 14602	Field of a subposet. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- X = dom R   =>    |- ( R e. PosetRel -> dom ( R i^i ( A X. A ) ) = ( X i^i A ) )
Theorem	psssdm 14603	Field of a subposet. (Contributed by FL, 19-Sep-2011.) (Revised by Mario Carneiro, 9-Sep-2015.)
|- X = dom R   =>    |- ( ( R e. PosetRel /\ A C_ X ) -> dom ( R i^i ( A X. A ) ) = A )
Theorem	istsr 14604	The predicate is a toset. (Contributed by FL, 1-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- X = dom R   =>    |- ( R e. TosetRel <-> ( R e. PosetRel /\ ( X X. X ) C_ ( R u. `' R ) ) )
Theorem	istsr2 14605*	The predicate is a toset. (Contributed by FL, 1-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- X = dom R   =>    |- ( R e. TosetRel <-> ( R e. PosetRel /\ A. x e. X A. y e. X ( x R y \/ y R x ) ) )
Theorem	tsrlin 14606	A toset is a linear order. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- X = dom R   =>    |- ( ( R e. TosetRel /\ A e. X /\ B e. X ) -> ( A R B \/ B R A ) )
Theorem	tsrlemax 14607	Two ways of saying a number is less than or equal to the maximum of two others. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- X = dom R   =>    |- ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A R if ( B R C , C , B ) <-> ( A R B \/ A R C ) ) )
Theorem	tsrps 14608	A toset is a poset. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- ( R e. TosetRel -> R e. PosetRel )
Theorem	cnvtsr 14609	The converse of a toset is a toset. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- ( R e. TosetRel -> `' R e. TosetRel )
Theorem	tsrss 14610	Any subset of a totally ordered set is totally ordered. (Contributed by FL, 24-Jan-2010.) (Proof shortened by Mario Carneiro, 21-Nov-2013.)
|- ( R e. TosetRel -> ( R i^i ( A X. A ) ) e. TosetRel )
Theorem	spwval2 14611*	Value of supremum under a weak ordering. Read R sup w A as "the R-supremum of A." U. U. R is the field of a relation R by relfld 5354. Unlike df-sup 7404 for strong orderings, the supremum exists iff R sup w A belongs to the field. (Contributed by NM, 13-May-2008.) (Revised by Mario Carneiro, 20-Nov-2013.)
|- X = U. U. R   =>    |- ( ( R e. PosetRel /\ A e. V ) -> ( R sup w A ) = ( iota_ x e. X ( A. y e. A y R x /\ A. y e. X ( A. z e. A z R y -> x R y ) ) ) )
Theorem	spwval 14612*	Value of supremum under a weak ordering. Read R sup w A as "the R-supremum of A." U. U. R is the field of a relation R by relfld 5354. Unlike df-sup 7404 for strong orderings, the supremum exists iff R sup w A belongs to the field. (Contributed by NM, 13-May-2008.) (Revised by Mario Carneiro, 20-Nov-2013.)
|- X = dom R   =>    |- ( ( R e. PosetRel /\ A e. V ) -> ( R sup w A ) = ( iota_ x e. X ( A. y e. A y R x /\ A. y e. X ( A. z e. A z R y -> x R y ) ) ) )
Theorem	spwmo 14613*	A poset has at most one supremum. (Contributed by NM, 13-May-2008.) (Revised by NM, 16-Jun-2017.)
|- ( ph <-> ( A. y e. A y R x /\ A. y e. X ( A. z e. A z R y -> x R y ) ) )   =>    |- ( R e. PosetRel -> E* x e. X ph )
Theorem	spweu 14614*	A supremum is unique. (Contributed by NM, 15-May-2008.)
|- ( ph <-> ( A. y e. A y R x /\ A. y e. X ( A. z e. A z R y -> x R y ) ) )   =>    |- ( ( R e. PosetRel /\ E. x e. X ph ) -> E! x e. X ph )
Theorem	spwpr2 14615*	Property of supremum defining condition for an unordered pair. (Contributed by NM, 24-Jun-2008.)
|- ( ph <-> ( A. y e. A y R x /\ A. y e. X ( A. z e. A z R y -> x R y ) ) )   =>    |- ( ( ( R e. T /\ A = { B , C } ) /\ ( B e. U /\ C e. W ) ) -> ( ph <-> ( ( B R x /\ C R x ) /\ A. y e. X ( ( B R y /\ C R y ) -> x R y ) ) ) )
Theorem	spwex 14616*	A supremum exists iff R sup w A belongs to the domain of R. (Contributed by NM, 15-May-2008.) (Revised by Mario Carneiro, 20-Nov-2013.)
|- X = dom R   &    |- ( ph <-> ( A. y e. A y R x /\ A. y e. X ( A. z e. A z R y -> x R y ) ) )   =>    |- ( ( R e. PosetRel /\ A e. V ) -> ( E. x e. X ph <-> ( R sup w A ) e. X ) )
Theorem	spwcl 14617*	Closure of a supremum. (Contributed by NM, 15-May-2008.) (Revised by Mario Carneiro, 20-Nov-2013.)
|- X = dom R   &    |- ( ph <-> ( A. y e. A y R x /\ A. y e. X ( A. z e. A z R y -> x R y ) ) )   =>    |- ( ( R e. PosetRel /\ A e. V /\ E. x e. X ph ) -> ( R sup w A ) e. X )
Theorem	spwpr4 14618*	Supremum of an unordered pair. (Contributed by NM, 7-Jul-2008.) (Revised by Mario Carneiro, 20-Nov-2013.)
|- X = dom R   =>    |- ( ( R e. PosetRel /\ ( A R C /\ B R C ) /\ A. x e. X ( ( A R x /\ B R x ) -> C R x ) ) -> ( R sup w { A , B } ) = C )
Theorem	spwpr4c 14619	Supremum of an unordered pair of comparable elements. (Contributed by NM, 7-Jul-2008.)
|- ( ( R e. PosetRel /\ A R B ) -> ( R sup w { A , B } ) = B )
Theorem	isla 14620*	The predicate "is a lattice" i.e. a poset in which any two elements have upper and lower bounds. (Contributed by NM, 12-Jun-2008.)
|- X = dom R   =>    |- ( R e. LatRel <-> ( R e. PosetRel /\ A. x e. X A. y e. X ( ( R sup w { x , y } ) e. X /\ ( R inf w { x , y } ) e. X ) ) )
Theorem	laspwcl 14621	Closure of the supremum (join) of two lattice elements. (Contributed by NM, 12-Jun-2008.)
|- X = dom R   =>    |- ( ( R e. LatRel /\ A e. X /\ B e. X ) -> ( R sup w { A , B } ) e. X )
Theorem	lanfwcl 14622	Closure of the infimum (meet) of two lattice elements. (Contributed by NM, 20-Jun-2008.)
|- X = dom R   =>    |- ( ( R e. LatRel /\ A e. X /\ B e. X ) -> ( R inf w { A , B } ) e. X )
Theorem	laps 14623	A lattice is a poset. (Contributed by NM, 12-Jun-2008.)
|- ( R e. LatRel -> R e. PosetRel )
Theorem	ledm 14624	domain of <_ is RR*. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 4-May-2015.)
|- RR* = dom <_
Theorem	lern 14625	The range of <_ is RR*. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 3-Sep-2015.)
|- RR* = ran <_
Theorem	lefld 14626	The field of the 'less or equal to' relationship on the extended real. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 4-May-2015.)
|- RR* = U. U. <_
Theorem	letsr 14627	The "less than or equal to" relationship on the extended reals is a toset. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 3-Sep-2015.)
|- <_ e. TosetRel
9.2.7  Directed sets, nets
Syntax	cdir 14628	Extend class notation with the class of all directed sets.
class DirRel
Syntax	ctail 14629	Extend class notation with the tail function.
class tail
Definition	df-dir 14630	Define the class of all directed sets/directions. (Contributed by Jeff Hankins, 25-Nov-2009.)
|- DirRel = { r | ( ( Rel r /\ ( _I |` U. U. r ) C_ r ) /\ ( ( r o. r ) C_ r /\ ( U. U. r X. U. U. r ) C_ ( `' r o. r ) ) ) }
Definition	df-tail 14631*	Define the tail function for directed sets. (Contributed by Jeff Hankins, 25-Nov-2009.)
|- tail = ( r e. DirRel |-> ( x e. U. U. r |-> ( r " { x } ) ) )
Theorem	isdir 14632	A condition for a relation to be a direction. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- A = U. U. R   =>    |- ( R e. V -> ( R e. DirRel <-> ( ( Rel R /\ ( _I |` A ) C_ R ) /\ ( ( R o. R ) C_ R /\ ( A X. A ) C_ ( `' R o. R ) ) ) ) )
Theorem	reldir 14633	A direction is a relation. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- ( R e. DirRel -> Rel R )
Theorem	dirdm 14634	A direction's domain is equal to its field. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- ( R e. DirRel -> dom R = U. U. R )
Theorem	dirref 14635	A direction is reflexive. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- X = dom R   =>    |- ( ( R e. DirRel /\ A e. X ) -> A R A )
Theorem	dirtr 14636	A direction is transitive. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- ( ( ( R e. DirRel /\ C e. V ) /\ ( A R B /\ B R C ) ) -> A R C )
Theorem	dirge 14637*	For any two elements of a directed set, there exists a third element greater than or equal to both. (Note that this does not say that the two elements have a least upper bound.) (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- X = dom R   =>    |- ( ( R e. DirRel /\ A e. X /\ B e. X ) -> E. x e. X ( A R x /\ B R x ) )
Theorem	tsrdir 14638	A totally ordered set is a directed set. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
|- ( A e. TosetRel -> A e. DirRel )
PART 10  BASIC ALGEBRAIC STRUCTURES
10.1  Monoids
10.1.1  Definition and basic properties
Syntax	cmnd 14639	Extend class notation with class of all monoids.
class Mnd
Syntax	cgrp 14640	Extend class notation with class of all groups.
class Grp
Syntax	cminusg 14641	Extend class notation with inverse of group element.
class inv g
Syntax	cplusf 14642	Extend class notation with group addition as a function.
class + f
Syntax	csg 14643	Extend class notation with group subtraction (or division) operation.
class -g
Syntax	cmg 14644	Extend class notation with a function mapping a group operation to the power operation for the group.
class .g
Definition	df-mnd 14645*	Definition of a monoid. A monoid is a set equipped with an everywhere defined internal operation (so, a magma, see mndcl 14650), whose operation is associative (so, a semigroup, see mndass 14651) and has a two-sided neutral element (see mndid 14652). (Contributed by Mario Carneiro, 6-Jan-2015.)
|- Mnd = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / p ]. ( A. x e. b A. y e. b A. z e. b ( ( x p y ) e. b /\ ( ( x p y ) p z ) = ( x p ( y p z ) ) ) /\ E. e e. b A. x e. b ( ( e p x ) = x /\ ( x p e ) = x ) ) }
Definition	df-plusf 14646*	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 is that it is a guaranteed function (mndplusf 14661), while +g only has closure (mndcl 14650). (Contributed by Mario Carneiro, 14-Aug-2015.)
|- + f = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( +g ` g ) y ) ) )
Theorem	ismnd 14647*	The predicate "is a monoid." (Contributed by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. Mnd <-> ( A. a e. B A. b e. B A. c e. B ( ( a .+ b ) e. B /\ ( ( a .+ b ) .+ c ) = ( a .+ ( b .+ c ) ) ) /\ E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) )
Theorem	mgmidmo 14648*	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	mndlem1 14649	Lemma for monoid properties. (Contributed by NM, 14-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Mnd /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) e. B /\ ( ( X .+ Y ) .+ Z ) = ( X .+ ( Y .+ Z ) ) ) )
Theorem	mndcl 14650	Closure of the operation of a monoid. (Contributed by NM, 14-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Mnd /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
Theorem	mndass 14651	A monoid operation is associative. (Contributed by NM, 14-Aug-2011.)
|- 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 14652*	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 14653*	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 14654	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 14655	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 14656	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	plusffval 14657*	The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .+^ = ( + f ` G )   =>    |- .+^ = ( x e. B , y e. B |-> ( x .+ y ) )
Theorem	plusfval 14658	The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .+^ = ( + f ` G )   =>    |- ( ( X e. B /\ Y e. B ) -> ( X .+^ Y ) = ( X .+ Y ) )
Theorem	plusfeq 14659	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 )   =>    |- ( .+ Fn ( B X. B ) -> .+^ = .+ )
Theorem	plusffn 14660	The group addition operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015.)
|- B = ( Base ` G )   &    |- .+^ = ( + f ` G )   =>    |- .+^ Fn ( B X. B )
Theorem	mndplusf 14661	The group addition operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- B = ( Base ` G )   &    |- .+^ = ( + f ` G )   =>    |- ( G e. Mnd -> .+^ : ( B X. B ) --> B )
Theorem	grpidval 14662*	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 )   =>    |- .0. = ( iota e ( e e. B /\ A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) )
Theorem	fn0g 14663	The group zero extractor is a function. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- 0g Fn _V
Theorem	0g0 14664	The identity element function evaluates to the empty set on an empty structure. (Contributed by Stefan O'Rear, 2-Oct-2015.)
|- (/) = ( 0g ` (/) )
Theorem	ismgmid 14665*	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 14666*	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 14667*	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 14668*	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	mndidcl 14669	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	mndlrid 14670	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 14671	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 14672	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	grpidd 14673*	Deduce the identity element of a monoid 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	ismndd 14674*	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	mndfo 14675	The addition operation of a monoid is an onto function (assuming it is a function). (Contributed by Mario Carneiro, 11-Oct-2013.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Mnd /\ .+ Fn ( B X. B ) ) -> .+ : ( B X. B ) -onto-> B )
Theorem	mndpropd 14676*	If two structures have the same group components (properties), one is a monoid iff the other one is. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- ( 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. Mnd <-> L e. Mnd ) )
Theorem	grpidpropd 14677*	If two structures have the same group components (properties), they have the same identity element. (Contributed by Mario Carneiro, 27-Nov-2014.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   =>    |- ( ph -> ( 0g ` K ) = ( 0g ` L ) )
Theorem	mndprop 14678	If two structures have the same group components (properties), one is a group iff the other one is. (Contributed by Mario Carneiro, 11-Oct-2013.)
|- ( Base ` K ) = ( Base ` L )   &    |- ( +g ` K ) = ( +g ` L )   =>    |- ( K e. Mnd <-> L e. Mnd )
Theorem	issubmnd 14679*	Characterize a submonoid by closure properties. (Contributed by Mario Carneiro, 10-Jan-2015.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- H = ( G ↾s S )   =>    |- ( ( G e. Mnd /\ S C_ B /\ .0. e. S ) -> ( H e. Mnd <-> A. x e. S A. y e. S ( x .+ y ) e. S ) )
Theorem	submnd0 14680	The zero of a submonoid is the same as the zero in the parent monoid. (Note that we must add the condition that the zero of the parent monoid is actually contained in the submonoid, because it is possible to have "subsets that are monoids" which are not submonoids because they have a different identity element.) (Contributed by Mario Carneiro, 10-Jan-2015.)
|- B = ( Base ` G )   &    |- .0. = ( 0g ` G )   &    |- H = ( G ↾s S )   =>    |- ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S ) ) -> .0. = ( 0g ` H ) )
Theorem	prdsplusgcl 14681	Structure product pointwise sums are closed when the factors are monoids. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- .+ = ( +g ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R : I --> Mnd )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   =>    |- ( ph -> ( F .+ G ) e. B )
Theorem	prdsidlem 14682*	Characterization of identity in a structure product. (Contributed by Mario Carneiro, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- .+ = ( +g ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R : I --> Mnd )   &    |- .0. = ( 0g o. R )   =>    |- ( ph -> ( .0. e. B /\ A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) )
Theorem	prdsmndd 14683	The product of a family of monoids is a monoid. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- ( ph -> I e. W )   &    |- ( ph -> S e. V )   &    |- ( ph -> R : I --> Mnd )   =>    |- ( ph -> Y e. Mnd )
Theorem	prds0g 14684	Zero in a product of monoids. (Contributed by Stefan O'Rear, 10-Jan-2015.)
|- Y = ( S X_s R )   &    |- ( ph -> I e. W )   &    |- ( ph -> S e. V )   &    |- ( ph -> R : I --> Mnd )   =>    |- ( ph -> ( 0g o. R ) = ( 0g ` Y ) )
Theorem	pwsmnd 14685	The structure power of a monoid is a monoid. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   =>    |- ( ( R e. Mnd /\ I e. V ) -> Y e. Mnd )
Theorem	pws0g 14686	Zero in a product of monoids. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- Y = ( R ^s I )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Mnd /\ I e. V ) -> ( I X. { .0. } ) = ( 0g ` Y ) )
Theorem	imasmnd2 14687*	The image structure of a monoid is a monoid. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- .+ = ( +g ` R )   &    |- ( 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 .+ b ) ) = ( F ` ( p .+ q ) ) ) )   &    |- ( ph -> R e. W )   &    |- ( ( ph /\ x e. V /\ y e. V ) -> ( x .+ y ) e. V )   &    |- ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( F ` ( ( x .+ y ) .+ z ) ) = ( F ` ( x .+ ( y .+ z ) ) ) )   &    |- ( ph -> .0. e. V )   &    |- ( ( ph /\ x e. V ) -> ( F ` ( .0. .+ x ) ) = ( F ` x ) )   &    |- ( ( ph /\ x e. V ) -> ( F ` ( x .+ .0. ) ) = ( F ` x ) )   =>    |- ( ph -> ( U e. Mnd /\ ( F ` .0. ) = ( 0g ` U ) ) )
Theorem	imasmnd 14688*	The image structure of a monoid is a monoid. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- .+ = ( +g ` R )   &    |- ( 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 .+ b ) ) = ( F ` ( p .+ q ) ) ) )   &    |- ( ph -> R e. Mnd )   &    |- .0. = ( 0g ` R )   =>    |- ( ph -> ( U e. Mnd /\ ( F ` .0. ) = ( 0g ` U ) ) )
Theorem	imasmndf1 14689	The image of a monoid under an injection is a monoid. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- U = ( F "s R )   &    |- V = ( Base ` R )   =>    |- ( ( F : V -1-1-> B /\ R e. Mnd ) -> U e. Mnd )
Theorem	xpsmnd 14690	The binary product of monoids is a monoid. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- T = ( R X.s S )   =>    |- ( ( R e. Mnd /\ S e. Mnd ) -> T e. Mnd )
10.1.2  Monoid homomorphisms and submonoids
Syntax	cmhm 14691	Hom-set generator class for monoids.
class MndHom
Syntax	csubmnd 14692	Class function taking a monoid to its lattice of submonoids.
class SubMnd
Definition	df-mhm 14693*	A monoid homomorphism is a function on the base sets which preserves the binary operation and the identity. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- MndHom = ( s e. Mnd , t e. Mnd |-> { f e. ( ( Base ` t ) ^m ( Base ` s ) ) | ( A. x e. ( Base ` s ) A. y e. ( Base ` s ) ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) ) /\ ( f ` ( 0g ` s ) ) = ( 0g ` t ) ) } )
Definition	df-submnd 14694*	A submonoid is a subset of a monoid which contains the identity and is closed under the operation. Such subsets are themselves monoids with the same identity. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- SubMnd = ( s e. Mnd |-> { t e. ~P ( Base ` s ) | ( ( 0g ` s ) e. t /\ A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t ) } )
Theorem	ismhm 14695*	Property of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- B = ( Base ` S )   &    |- C = ( Base ` T )   &    |- .+ = ( +g ` S )   &    |- .+^ = ( +g ` T )   &    |- .0. = ( 0g ` S )   &    |- Y = ( 0g ` T )   =>    |- ( F e. ( S MndHom T ) <-> ( ( S e. Mnd /\ T e. Mnd ) /\ ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` .0. ) = Y ) ) )
Theorem	mhmrcl1 14696	Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- ( F e. ( S MndHom T ) -> S e. Mnd )
Theorem	mhmrcl2 14697	Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- ( F e. ( S MndHom T ) -> T e. Mnd )
Theorem	mhmf 14698	A monoid homomorphism is a function. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- B = ( Base ` S )   &    |- C = ( Base ` T )   =>    |- ( F e. ( S MndHom T ) -> F : B --> C )
Theorem	mhmpropd 14699*	Monoid homomorphism depends only on the monoidal attributes of structures. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 7-Nov-2015.)
|- ( ph -> B = ( Base ` J ) )   &    |- ( ph -> C = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ph -> C = ( Base ` M ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` J ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` M ) y ) )   =>    |- ( ph -> ( J MndHom K ) = ( L MndHom M ) )
Theorem	mhmlin 14700	A monoid homomorphism commutes with composition. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- B = ( Base ` S )   &    |- .+ = ( +g ` S )   &    |- .+^ = ( +g ` T )   =>    |- ( ( F e. ( S MndHom T ) /\ X e. B /\ Y e. B ) -> ( F ` ( X .+ Y ) ) = ( ( F ` X ) .+^ ( F ` Y ) ) )