P. 329 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32801-32900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	usgedgnlp 32801*	An edge of a graph is not a loop. (Contributed by AV, 9-Jan-2020.)
|- E = ( Edges ` G )   =>    |- ( ( G e. USGrph /\ C e. E ) -> -. E. v C = { v } )
Theorem	usgvad2edg 32802*	If a vertex is adjacent to two different vertices in a simple graph, there are more than one edges starting at this vertex, analogous to usgra2edg 24587. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 9-Jan-2020.)
|- E = ( Edges ` G )   =>    |- ( ( ( G e. USGrph /\ B =/= C ) /\ ( { N , B } e. E /\ { C , N } e. E ) ) -> E. x e. E E. y e. E ( x =/= y /\ N e. x /\ N e. y ) )
Theorem	usg2edgneu 32803*	If a vertex is adjacent to two different vertices in a simple graph, there is not only one edge starting at this vertex, analogous to usgra2edg1 24588. Lemma for theorems about friendship graphs. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 9-Jan-2020.)
|- E = ( Edges ` G )   =>    |- ( ( ( G e. USGrph /\ B =/= C ) /\ ( { N , B } e. E /\ { C , N } e. E ) ) -> -. E! x e. E N e. x )
Theorem	usgedgvadf1lem1 32804*	Lemma 1 for usgedgvadf1 32806. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 9-Jan-2020.)
|- V = ( Vtx ` G )   &    |- E = ( Edges ` G )   &    |- A = { e e. E | N e. e }   =>    |- ( ( G e. USGrph /\ C e. A ) -> ( iota_ m e. V C = { m , N } ) e. V )
Theorem	usgedgvadf1lem2 32805*	Lemma 2 for usgedgvadf1 32806. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 9-Jan-2020.)
|- V = ( Vtx ` G )   &    |- E = ( Edges ` G )   &    |- A = { e e. E | N e. e }   =>    |- ( ( G e. USGrph /\ C e. A ) -> ( M = ( iota_ m e. V C = { m , N } ) -> C = { M , N } ) )
Theorem	usgedgvadf1 32806*	The mapping of edges containing a given vertex into the set of vertices is 1-1, analogous to usgraidx2v 24598. The edge is mapped to the other vertex of the edge containing the vertex N. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 9-Jan-2020.)
|- V = ( Vtx ` G )   &    |- E = ( Edges ` G )   &    |- A = { e e. E | N e. e }   &    |- F = ( e e. A |-> ( iota_ m e. V e = { m , N } ) )   =>    |- ( ( G e. USGrph /\ N e. V ) -> F : A -1-1-> V )
Theorem	usgedgvadf1ALTlem1 32807*	Lemma 1 for usgedgvadf1 32806. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 9-Jan-2020.)
|- V = ( 1st ` G )   &    |- E = ( Edges ` G )   &    |- A = { e e. E | N e. e }   =>    |- ( ( G e. USGrph /\ C e. A ) -> ( iota_ m e. V C = { m , N } ) e. V )
Theorem	usgedgvadf1ALTlem2 32808*	Lemma 2 for usgedgvadf1 32806. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 9-Jan-2020.)
|- V = ( 1st ` G )   &    |- E = ( Edges ` G )   &    |- A = { e e. E | N e. e }   =>    |- ( ( G e. USGrph /\ C e. A ) -> ( M = ( iota_ m e. V C = { m , N } ) -> C = { M , N } ) )
Theorem	usgedgvadf1ALT 32809*	The mapping of edges containing a given vertex into the set of vertices is 1-1, analogous to usgraidx2v 24598. The edge is mapped to the other vertex of the edge containing the vertex N. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 9-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- V = ( 1st ` G )   &    |- E = ( Edges ` G )   &    |- A = { e e. E | N e. e }   &    |- F = ( e e. A |-> ( iota_ m e. V e = { m , N } ) )   =>    |- ( ( G e. USGrph /\ N e. V ) -> F : A -1-1-> V )
Theorem	usgedgleord 32810*	In a graph, the number of edges which contain a given vertex is not greater than the number of vertices, analogous to usgraedgleord 24599. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 9-Jan-2020.)
|- V = ( Vtx ` G )   &    |- E = ( Edges ` G )   =>    |- ( ( G e. USGrph /\ N e. V ) -> ( # ` { e e. E | N e. e } ) <_ ( GrOrder ` G ) )
Theorem	usgedgleordALT 32811*	Alternate version of usgedgleord 32810 with a shorter proof. In a graph, the number of edges which contain a given vertex is not greater than the order of the graph, i. e. the number of its vertices, analogous to usgraedgleord 24599. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 12-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- V = ( 1st ` G )   &    |- E = ( Edges ` G )   &    |- O = ( # ` V )   =>    |- ( ( G e. USGrph /\ N e. V ) -> ( # ` { e e. E | N e. e } ) <_ O )
21.24.6.8  Finite undirected simple graphs without loops
Syntax	cfusg 32812	Extend class notation with finite graphs.
class FinUSGrph
Definition	df-fusg 32813*	Define the class of all finite undirected simple graphs without loops. Such a finite graph is an undirected simple graph without loops <. V , E >. of finite order, i.e. where V is finite. (Contributed by AV, 3-Jan-2020.)
|- FinUSGrph = { <. v , e >. | ( e : dom e -1-1-> { x e. ~P v | ( # ` x ) = 2 } /\ v e. Fin ) }
Theorem	relfusgra 32814	The class of all finite undirected simple graph without loops is a relation. (Contributed by AV, 3-Jan-2020.)
|- Rel FinUSGrph
Theorem	isfusgra 32815*	The property of being a finite undirected simple graph without loops. (Contributed by AV, 3-Jan-2020.)
|- ( ( V e. W /\ E e. X ) -> ( V FinUSGrph E <-> ( E : dom E -1-1-> { x e. ~P V | ( # ` x ) = 2 } /\ V e. Fin ) ) )
Theorem	isfusgra0 32816	The property of being a finite undirected simple graph without loops. (Contributed by AV, 3-Jan-2020.)
|- ( ( V e. W /\ E e. X ) -> ( V FinUSGrph E <-> ( V USGrph E /\ V e. Fin ) ) )
Theorem	isfusgracl 32817	The property of being a finite undirected simple graph without loops. (Contributed by AV, 3-Jan-2020.)
|- ( G e. ( W X. X ) -> ( G e. FinUSGrph <-> ( G e. USGrph /\ ( GrOrder ` G ) e. NN0 ) ) )
Theorem	fusgraimpcl 32818	The implications of a finite undirected simple graph without loops. (Contributed by AV, 4-Jan-2020.)
|- ( G e. FinUSGrph -> ( G e. USGrph /\ ( GrOrder ` G ) e. NN0 ) )
Theorem	isfusgraclALT 32819	The property of being a finite undirected simple graph without loops. (Contributed by AV, 15-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- V = ( 1st ` G )   =>    |- ( G e. ( W X. X ) -> ( G e. FinUSGrph <-> ( G e. USGrph /\ V e. Fin ) ) )
Theorem	fusgraimpclALT 32820	The implications of a finite undirected simple graph without loops. (Contributed by AV, 15-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- V = ( 1st ` G )   =>    |- ( G e. FinUSGrph -> ( G e. USGrph /\ V e. Fin ) )
Theorem	fusgusg 32821	A finite undirected simple graph without loops is a undirected simple graph without loops. (Contributed by AV, 16-Jan-2020.)
|- ( G e. FinUSGrph -> G e. USGrph )
Theorem	fusgraimpclALT2 32822	The implications of a finite undirected simple graph without loops. (Contributed by AV, 12-Jan-2020.) (Proof modification is discouraged.)
|- ( G e. FinUSGrph -> ( G e. USGrph /\ ( 1st ` G ) e. Fin ) )
Theorem	fiusgedgfi 32823*	In a finite graph the number of edges which contain a given vertex is also finite, analogous to fiusgraedgfi 24612. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 9-Jan-2020.)
|- V = ( Vtx ` G )   &    |- E = ( Edges ` G )   =>    |- ( ( G e. FinUSGrph /\ N e. V ) -> { e e. E | N e. e } e. Fin )
Theorem	fiusgedgfiALT 32824*	In a finite graph the number of edges which contain a given vertex is also finite, analogous to fiusgraedgfi 24612. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 15-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- V = ( 1st ` G )   &    |- E = ( Edges ` G )   =>    |- ( ( G e. FinUSGrph /\ N e. V ) -> { e e. E | N e. e } e. Fin )
21.24.6.9  Finite undirected simple graphs (extension)
Theorem	usgedgffibi 32825	The number of edges in a graph is finite iff its edge function is finite. (Contributed by AV, 10-Jan-2020.)
|- ( V USGrph E -> ( E e. Fin <-> ( V Edges E ) e. Fin ) )
Theorem	usgo0s0 32826	The size of a graph of order 0 (i.e. with 0 vertices) is 0, analogous to usgrafisindb0 24613. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 4-Jan-2020.)
|- ( ( G e. USGrph /\ ( GrOrder ` G ) = 0 ) -> ( GrSize ` G ) = 0 )
Theorem	usgo0s0ALT 32827	The size of a graph of order 0 (i.e. with 0 vertices) is 0, analogous to usgrafisindb0 24613. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 15-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- O = ( # ` ( 1st ` G ) )   &    |- S = ( # ` ( 2nd ` G ) )   =>    |- ( ( G e. USGrph /\ O = 0 ) -> S = 0 )
Theorem	usgo1s0ALT 32828	The size of a graph of order 1 (i.e. with 1 vertex) is 0, analogous to usgrafisindb1 24614. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 15-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- O = ( # ` ( 1st ` G ) )   &    |- S = ( # ` ( 2nd ` G ) )   =>    |- ( ( G e. USGrph /\ O = 1 ) -> S = 0 )
Theorem	usgo0fis 32829	A graph of order 0 (i.e. with 0 vertices) has a finite set of edges, analogous to usgrafisbase 24619. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 10-Jan-2020.)
|- ( ( G e. USGrph /\ ( GrOrder ` G ) = 0 ) -> ( Edges ` G ) e. Fin )
Theorem	usgo0fisALT 32830	A graph of order 0 (i.e. with 0 vertices) has a finite set of edges, analogous to usgrafisbase 24619. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 15-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- O = ( # ` ( 1st ` G ) )   =>    |- ( ( G e. USGrph /\ O = 0 ) -> ( Edges ` G ) e. Fin )
Theorem	usgrafisbaseALT 32831	Alternate version of usgrafisbase 24619, not depending on usgrafisindb0 24613. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 10-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( V USGrph E /\ ( # ` V ) = 0 ) -> E e. Fin )
Theorem	usgrafisbaseALT2 32832	Alternate version of usgrafisbase 24619, not depending on usgrafisindb0 24613. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 10-Jan-2020.) (Proof modification is discouraged.)
|- ( ( V USGrph E /\ ( # ` V ) = 0 ) -> E e. Fin )
Theorem	usgo1s0 32833	The size of a graph of order 1 (i.e. with 1 vertex) is 0, analogous to usgrafisindb1 24614. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 4-Jan-2020.)
|- ( ( G e. USGrph /\ ( GrOrder ` G ) = 1 ) -> ( GrSize ` G ) = 0 )
Theorem	usgresvm1 32834*	Restricting an undirected simple graph by removing one vertex (and all edges ending at this vertex), analogous to usgrares1 24615. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 10-Jan-2020.)
|- V = ( Vtx ` G )   &    |- E = ( Edges ` G )   &    |- F = { e e. E | N e/ e }   =>    |- ( ( G e. USGrph /\ N e. V ) -> ( V \ { N } ) USGrph ( _I |` F ) )
Theorem	usgfislem1 32835*	Lemma 1 for usgfis 32837: The set of edges is the union of the edges containing a specific vertex and the edges not containing this vertex. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 10-Jan-2020.)
|- V = ( Vtx ` G )   &    |- E = ( Edges ` G )   &    |- F = { e e. E | N e/ e }   =>    |- E = ( F u. { e e. E | N e. e } )
Theorem	usgfislem2 32836*	Lemma 2 for usgfis 32837: In a graph of finite order (i.e. with a finite number of vertices), the number of edges is finite if and only if the number of edges not containing one of the vertices is finite. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 9-Jan-2020.)
|- V = ( Vtx ` G )   &    |- E = ( Edges ` G )   &    |- F = { e e. E | N e/ e }   =>    |- ( ( G e. FinUSGrph /\ N e. V ) -> ( E e. Fin <-> F e. Fin ) )
Theorem	usgfis 32837	An undirected simple graph of finite order (i.e. with a finite number of vertices) is of finite size, i.e. it has also only a finite number of edges, analogous to usgrafis 24620. Remark: The proof of this theorem is very long compared with usgrafis 24620, because the theorem brfi1ind 12520 to perform the finite induction is taylored for binary relations, so that the theorem itself and the used lemmas must be transformed accordingly. Maybe a variant of brfi1ind 12520 could be provided, which is better suitable for this theorem. (Contributed by Alexander van der Vekens, 6-Jan-2018.) (Revised by AV, 11-Jan-2018.) (Proof modification is discouraged.)
|- ( G e. FinUSGrph -> ( GrSize ` G ) e. NN0 )
Theorem	usgresvm1ALT 32838*	Restricting an undirected simple graph by removing one vertex (and all edges ending at this vertex), analogous to usgrares1 24615. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 15-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- V = ( 1st ` G )   &    |- E = ( Edges ` G )   &    |- F = { e e. E | N e/ e }   =>    |- ( ( G e. USGrph /\ N e. V ) -> ( V \ { N } ) USGrph ( _I |` F ) )
Theorem	usgfisALTlem1 32839*	Lemma 1 for usgfisALT 32841: The set of edges is the union of the edges containing a specific vertex and the edges not containing this vertex. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 15-Jan-2020.)
|- V = ( 1st ` G )   &    |- E = ( Edges ` G )   &    |- F = { e e. E | N e/ e }   =>    |- E = ( F u. { e e. E | N e. e } )
Theorem	usgfisALTlem2 32840*	Lemma 2 for usgfis 32837: In a graph of finite order (i.e. with a finite number of vertices), the number of edges is finite if and only if the number of edges not containing one of the vertices is finite. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 15-Jan-2020.)
|- V = ( 1st ` G )   &    |- E = ( Edges ` G )   &    |- F = { e e. E | N e/ e }   =>    |- ( ( G e. FinUSGrph /\ N e. V ) -> ( E e. Fin <-> F e. Fin ) )
Theorem	usgfisALT 32841	An undirected simple graph of finite order (i.e. with a finite number of vertices) is of finite size, i.e. it has also only a finite number of edges, analogous to usgrafis 24620. Remark: The proof of this theorem is very long compared with usgrafis 24620, because the theorem brfi1ind 12520 to perform the finite induction is taylored for binary relations, so that the theorem itself and the used lemmas must be transformed accordingly. Maybe a variant of brfi1ind 12520 could be provided, which is better suitable for this theorem. (Contributed by Alexander van der Vekens, 6-Jan-2018.) (Revised by AV, 15-Jan-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( G e. FinUSGrph -> ( Edges ` G ) e. Fin )
Theorem	usgrafiedgALT 32842	A simple undirected graph with a finite number of vertices has also only a finite number of edges. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 4-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( G e. FinUSGrph -> ( Edges ` G ) e. Fin )
21.24.7  Monoids (extension)
21.24.7.1  Auxiliary theorems
Theorem	ovn0dmfun 32843	If a class' operation value for two operands is not the empty set, the operands are contained in the domain of the class, and the class restricted to the operands is a function, analogous to fvfundmfvn0 5880. (Contributed by AV, 27-Jan-2020.)
|- ( ( A F B ) =/= (/) -> ( <. A , B >. e. dom F /\ Fun ( F |` { <. A , B >. } ) ) )
Theorem	xpsnopab 32844*	A Cartesian product with a singleton expressed as ordered-pair class abstraction. (Contributed by AV, 27-Jan-2020.)
|- ( { X } X. C ) = { <. a , b >. | ( a = X /\ b e. C ) }
Theorem	xpiun 32845*	A Cartesian product expressed as indexed union of ordered-pair class abstractions. (Contributed by AV, 27-Jan-2020.)
|- ( B X. C ) = U_ x e. B { <. a , b >. | ( a = x /\ b e. C ) }
Theorem	ovn0ssdmfun 32846*	If a class' operation value for two operands is not the empty set, the operands are contained in the domain of the class, and the class restricted to the operands is a function, analogous to fvfundmfvn0 5880. (Contributed by AV, 27-Jan-2020.)
|- ( A. a e. D A. b e. E ( a F b ) =/= (/) -> ( ( D X. E ) C_ dom F /\ Fun ( F |` ( D X. E ) ) ) )
Theorem	fnxpdmdm 32847	The domain of the domain of a function over a Cartesian square. (Contributed by AV, 13-Jan-2020.)
|- ( F Fn ( A X. A ) -> dom dom F = A )
Theorem	cnfldsrngbas 32848	The base set of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.)
|- R = (ℂfld ↾s S )   =>    |- ( S C_ CC -> S = ( Base ` R ) )
Theorem	cnfldsrngadd 32849	The group addition operation of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.)
|- R = (ℂfld ↾s S )   =>    |- ( S e. V -> + = ( +g ` R ) )
Theorem	cnfldsrngmul 32850	The ring multiplication operation of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020.)
|- R = (ℂfld ↾s S )   =>    |- ( S e. V -> x. = ( .r ` R ) )
21.24.7.2  Magmas and Semigroups (extension)
Theorem	plusfreseq 32851	If the empty set is not contained in the range of the group addition function of an extensible structure (not necessarily a magma), the restriction of the addition operation to (the Cartesian square of) the base set is the functionalization of it. (Contributed by AV, 28-Jan-2020.)
|- B = ( Base ` M )   &    |- .+ = ( +g ` M )   &    |- .+^ = ( +f ` M )   =>    |- ( (/) e/ ran .+^ -> ( .+ |` ( B X. B ) ) = .+^ )
Theorem	mgmplusfreseq 32852	If the empty set is not contained in the base set of a magma, the restriction of the addition operation to (the Cartesian square of) the base set is the functionalization of it. (Contributed by AV, 28-Jan-2020.)
|- B = ( Base ` M )   &    |- .+ = ( +g ` M )   &    |- .+^ = ( +f ` M )   =>    |- ( ( M e. Mgm /\ (/) e/ B ) -> ( .+ |` ( B X. B ) ) = .+^ )
Theorem	0mgm 32853	A set with an empty base set is always a magma". (Contributed by AV, 25-Feb-2020.)
|- ( Base ` M ) = (/)   =>    |- ( M e. V -> M e. Mgm )
Theorem	mgmpropd 32854*	If two structures have the same (nonempty) base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, one is a magma iff the other one is. (Contributed by AV, 25-Feb-2020.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ph -> B =/= (/) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   =>    |- ( ph -> ( K e. Mgm <-> L e. Mgm ) )
Theorem	ismgmd 32855*	Deduce a magma from its properties. (Contributed by AV, 25-Feb-2020.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> G e. V )   &    |- ( ph -> .+ = ( +g ` G ) )   &    |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )   =>    |- ( ph -> G e. Mgm )
21.24.7.3  Magma homomorphisms and submagmas
Syntax	cmgmhm 32856	Hom-set generator class for magmas.
class MgmHom
Syntax	csubmgm 32857	Class function taking a magma to its lattice of submagmas.
class SubMgm
Definition	df-mgmhm 32858*	A magma homomorphism is a function on the base sets which preserves the binary operation. (Contributed by AV, 24-Feb-2020.)
|- MgmHom = ( s e. Mgm , t e. Mgm |-> { 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 ) ) } )
Definition	df-submgm 32859*	A submagma is a subset of a magma which is closed under the operation. Such subsets are themselves magmas. (Contributed by AV, 24-Feb-2020.)
|- SubMgm = ( s e. Mgm |-> { t e. ~P ( Base ` s ) | A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t } )
Theorem	mgmhmrcl 32860	Reverse closure of a magma homomorphism. (Contributed by AV, 24-Feb-2020.)
|- ( F e. ( S MgmHom T ) -> ( S e. Mgm /\ T e. Mgm ) )
Theorem	submgmrcl 32861	Reverse closure for submagmas. (Contributed by AV, 24-Feb-2020.)
|- ( S e. (SubMgm ` M ) -> M e. Mgm )
Theorem	ismgmhm 32862*	Property of a magma homomorphism. (Contributed by AV, 25-Feb-2020.)
|- B = ( Base ` S )   &    |- C = ( Base ` T )   &    |- .+ = ( +g ` S )   &    |- .+^ = ( +g ` T )   =>    |- ( F e. ( S MgmHom T ) <-> ( ( S e. Mgm /\ T e. Mgm ) /\ ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) ) )
Theorem	mgmhmf 32863	A magma homomorphism is a function. (Contributed by AV, 25-Feb-2020.)
|- B = ( Base ` S )   &    |- C = ( Base ` T )   =>    |- ( F e. ( S MgmHom T ) -> F : B --> C )
Theorem	mgmhmpropd 32864*	Magma homomorphism depends only on the operation of structures. (Contributed by AV, 25-Feb-2020.)
|- ( ph -> B = ( Base ` J ) )   &    |- ( ph -> C = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ph -> C = ( Base ` M ) )   &    |- ( ph -> B =/= (/) )   &    |- ( ph -> C =/= (/) )   &    |- ( ( 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 MgmHom K ) = ( L MgmHom M ) )
Theorem	mgmhmlin 32865	A magma homomorphism preserves the binary operation. (Contributed by AV, 25-Feb-2020.)
|- B = ( Base ` S )   &    |- .+ = ( +g ` S )   &    |- .+^ = ( +g ` T )   =>    |- ( ( F e. ( S MgmHom T ) /\ X e. B /\ Y e. B ) -> ( F ` ( X .+ Y ) ) = ( ( F ` X ) .+^ ( F ` Y ) ) )
Theorem	mgmhmf1o 32866	A magma homomorphism is bijective iff its converse is also a magma homomorphism. (Contributed by AV, 25-Feb-2020.)
|- B = ( Base ` R )   &    |- C = ( Base ` S )   =>    |- ( F e. ( R MgmHom S ) -> ( F : B -1-1-onto-> C <-> `' F e. ( S MgmHom R ) ) )
Theorem	idmgmhm 32867	The identity homomorphism on a magma. (Contributed by AV, 27-Feb-2020.)
|- B = ( Base ` M )   =>    |- ( M e. Mgm -> ( _I |` B ) e. ( M MgmHom M ) )
Theorem	issubmgm 32868*	Expand definition of a submagma. (Contributed by AV, 25-Feb-2020.)
|- B = ( Base ` M )   &    |- .+ = ( +g ` M )   =>    |- ( M e. Mgm -> ( S e. (SubMgm ` M ) <-> ( S C_ B /\ A. x e. S A. y e. S ( x .+ y ) e. S ) ) )
Theorem	issubmgm2 32869	Submagmas are subsets that are also magmas. (Contributed by AV, 25-Feb-2020.)
|- B = ( Base ` M )   &    |- H = ( M ↾s S )   =>    |- ( M e. Mgm -> ( S e. (SubMgm ` M ) <-> ( S C_ B /\ H e. Mgm ) ) )
Theorem	rabsubmgmd 32870*	Deduction for proving that a restricted class abstraction is a submagma. (Contributed by AV, 26-Feb-2020.)
|- B = ( Base ` M )   &    |- .+ = ( +g ` M )   &    |- ( ph -> M e. Mgm )   &    |- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( th /\ ta ) ) ) -> et )   &    |- ( z = x -> ( ps <-> th ) )   &    |- ( z = y -> ( ps <-> ta ) )   &    |- ( z = ( x .+ y ) -> ( ps <-> et ) )   =>    |- ( ph -> { z e. B | ps } e. (SubMgm ` M ) )
Theorem	submgmss 32871	Submagmas are subsets of the base set. (Contributed by AV, 26-Feb-2020.)
|- B = ( Base ` M )   =>    |- ( S e. (SubMgm ` M ) -> S C_ B )
Theorem	submgmid 32872	Every magma is trivially a submagma of itself. (Contributed by AV, 26-Feb-2020.)
|- B = ( Base ` M )   =>    |- ( M e. Mgm -> B e. (SubMgm ` M ) )
Theorem	submgmcl 32873	Submagmas are closed under the monoid operation. (Contributed by AV, 26-Feb-2020.)
|- .+ = ( +g ` M )   =>    |- ( ( S e. (SubMgm ` M ) /\ X e. S /\ Y e. S ) -> ( X .+ Y ) e. S )
Theorem	submgmmgm 32874	Submagmas are themselves magmas under the given operation. (Contributed by AV, 26-Feb-2020.)
|- H = ( M ↾s S )   =>    |- ( S e. (SubMgm ` M ) -> H e. Mgm )
Theorem	submgmbas 32875	The base set of a submagma. (Contributed by AV, 26-Feb-2020.)
|- H = ( M ↾s S )   =>    |- ( S e. (SubMgm ` M ) -> S = ( Base ` H ) )
Theorem	subsubmgm 32876	A submagma of a submagma is a submagma. (Contributed by AV, 26-Feb-2020.)
|- H = ( G ↾s S )   =>    |- ( S e. (SubMgm ` G ) -> ( A e. (SubMgm ` H ) <-> ( A e. (SubMgm ` G ) /\ A C_ S ) ) )
Theorem	resmgmhm 32877	Restriction of a magma homomorphism to a submagma is a homomorphism. (Contributed by AV, 26-Feb-2020.)
|- U = ( S ↾s X )   =>    |- ( ( F e. ( S MgmHom T ) /\ X e. (SubMgm ` S ) ) -> ( F |` X ) e. ( U MgmHom T ) )
Theorem	resmgmhm2 32878	One direction of resmgmhm2b 32879. (Contributed by AV, 26-Feb-2020.)
|- U = ( T ↾s X )   =>    |- ( ( F e. ( S MgmHom U ) /\ X e. (SubMgm ` T ) ) -> F e. ( S MgmHom T ) )
Theorem	resmgmhm2b 32879	Restriction of the codomain of a homomorphism. (Contributed by AV, 26-Feb-2020.)
|- U = ( T ↾s X )   =>    |- ( ( X e. (SubMgm ` T ) /\ ran F C_ X ) -> ( F e. ( S MgmHom T ) <-> F e. ( S MgmHom U ) ) )
Theorem	mgmhmco 32880	The composition of magma homomorphisms is a homomorphism. (Contributed by AV, 27-Feb-2020.)
|- ( ( F e. ( T MgmHom U ) /\ G e. ( S MgmHom T ) ) -> ( F o. G ) e. ( S MgmHom U ) )
Theorem	mgmhmima 32881	The homomorphic image of a submagma is a submagma. (Contributed by AV, 27-Feb-2020.)
|- ( ( F e. ( M MgmHom N ) /\ X e. (SubMgm ` M ) ) -> ( F " X ) e. (SubMgm ` N ) )
Theorem	mgmhmeql 32882	The equalizer of two magma homomorphisms is a submagma. (Contributed by AV, 27-Feb-2020.)
|- ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom T ) ) -> dom ( F i^i G ) e. (SubMgm ` S ) )
Theorem	submgmacs 32883	Submagmas are an algebraic closure system. (Contributed by AV, 27-Feb-2020.)
|- B = ( Base ` G )   =>    |- ( G e. Mgm -> (SubMgm ` G ) e. (ACS ` B ) )
Theorem	ismhm0 32884	Property of a monoid homomorphism, expressed by a magma homomorphism. (Contributed by AV, 17-Apr-2020.)
|- 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 e. ( S MgmHom T ) /\ ( F ` .0. ) = Y ) ) )
Theorem	mhmismgmhm 32885	Each monoid homomorphism is a magma homomorphism. (Contributed by AV, 29-Feb-2020.)
|- ( F e. ( R MndHom S ) -> F e. ( R MgmHom S ) )
21.24.7.4  Examples and counterexamples for magmas, semigroups and monoids (extension)
Theorem	opmpt2ismgm 32886*	A structure with a group addition operation in maps-to notation is a magma if the operation value is contained in the base set. (Contributed by AV, 16-Feb-2020.)
|- B = ( Base ` M )   &    |- ( +g ` M ) = ( x e. B , y e. B |-> C )   &    |- ( ph -> B =/= (/) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> C e. B )   =>    |- ( ph -> M e. Mgm )
Theorem	copissgrp 32887*	A structure with a constant group addition operation is a semigroup if the constant is contained in the base set. (Contributed by AV, 16-Feb-2020.)
|- B = ( Base ` M )   &    |- ( +g ` M ) = ( x e. B , y e. B |-> C )   &    |- ( ph -> B =/= (/) )   &    |- ( ph -> C e. B )   =>    |- ( ph -> M e. SGrp )
Theorem	copisnmnd 32888*	A structure with a constant group addition operation and at least two elements is not a monoid. (Contributed by AV, 16-Feb-2020.)
|- B = ( Base ` M )   &    |- ( +g ` M ) = ( x e. B , y e. B |-> C )   &    |- ( ph -> C e. B )   &    |- ( ph -> 1 < ( # ` B ) )   =>    |- ( ph -> M e/ Mnd )
Theorem	0nodd 32889*	0 is not an odd integer. (Contributed by AV, 3-Feb-2020.)
|- O = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }   =>    |- 0 e/ O
Theorem	1odd 32890*	1 is an odd integer. (Contributed by AV, 3-Feb-2020.)
|- O = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }   =>    |- 1 e. O
Theorem	2nodd 32891*	2 is not an odd integer. (Contributed by AV, 3-Feb-2020.)
|- O = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }   =>    |- 2 e/ O
Theorem	oddibas 32892*	Lemma 1 for oddinmgm 32894: The base set of M is the set of all odd integers. (Contributed by AV, 3-Feb-2020.)
|- O = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }   &    |- M = (ℂfld ↾s O )   =>    |- O = ( Base ` M )
Theorem	oddiadd 32893*	Lemma 2 for oddinmgm 32894: The group addition operation of M is the addition of complex numbers. (Contributed by AV, 3-Feb-2020.)
|- O = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }   &    |- M = (ℂfld ↾s O )   =>    |- + = ( +g ` M )
Theorem	oddinmgm 32894*	The structure of all odd integers together with the addition of complex numbers is not a magma. Remark: the structure of the complementary subset of the set of integers, the even integers, is a magma, actually an abelian group, see 2zrngaabl 33023, and even a non-unital ring, see 2zrng 33014. (Contributed by AV, 3-Feb-2020.)
|- O = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }   &    |- M = (ℂfld ↾s O )   =>    |- M e/ Mgm
Theorem	nnsgrpmgm 32895	The structure of positive integers together with the addition of complex numbers is a magma. (Contributed by AV, 4-Feb-2020.)
|- M = (ℂfld ↾s NN )   =>    |- M e. Mgm
Theorem	nnsgrp 32896	The structure of positive integers together with the addition of complex numbers is a semigroup. (Contributed by AV, 4-Feb-2020.)
|- M = (ℂfld ↾s NN )   =>    |- M e. SGrp
Theorem	nnsgrpnmnd 32897	The structure of positive integers together with the addition of complex numbers is not a monoid. (Contributed by AV, 4-Feb-2020.)
|- M = (ℂfld ↾s NN )   =>    |- M e/ Mnd
21.24.8  Magmas and internal binary operations (alternate approach) With df-mpt2 6275, binary operations are defined by a rule, and with df-ov 6273, 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 (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, we call binary operations mapping the elements of the Cartesian product S X. S internal binary operations, see df-intop 32914. If, in addition, the result is also contained in the set S, the operation is called closed internal binary operation, see df-clintop 32915. Therefore, a "binary operation on a set S" according to Wikipedia is a "closed internal binary operation" in our 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 ). Taking a step back, we define "laws" applicable for "binary operations" (which even need not to be functions), according to the definition in [Hall] p. 1 and [BourbakiAlg1] p. 1, p. 4 and p. 7. These laws are used, on the one hand, to specialize internal binary operations (see df-clintop 32915 and df-assintop 32916), and on the other hand to define the common algebraic structures like magmas, groups, rings, etc. Internal binary operations, which obeys these laws, are defined afterwards. Notice that in [BourbakiAlg1] p. 1, p. 4 and p. 7, these operations are called "laws" by themselves. In the following, an alternative definition df-cllaw 32901 for an internal binary operation is provided, which does not require to be a function, but only closure. Therefore, this definition could be used as binary operation (slot 2) defined for a magma as extensible structure, see mgmplusgiopALT 32909, or for an alternative definition df-mgm2 32934 for a magma as extensible structure. Similar results are obtained for an associative operation resp. semigroups.
21.24.8.1  Laws for internal binary operations In this subsection, the "laws" applicable for "binary operations" according to the definition in [Hall] p. 1 and [BourbakiAlg1] p. 1, p. 4 and p. 7 are defined. These laws are called "internal laws" in [BourbakiAlg1] p. xxi.
Syntax	ccllaw 32898	Extend class notation for the closure law.
class clLaw
Syntax	casslaw 32899	Extend class notation for the associative law.
class assLaw
Syntax	ccomlaw 32900	Extend class notation for the commutative law.
class comLaw