df-mgm

Description: Amagma 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)

		Ref	Expression
	Assertion	df-mgm	\|- Mgm = { g \| [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmgm	\|- Mgm
1		vg	\|- g
2		cbs	\|- Base
3	1	cv	\|- g
4	3 2	cfv	\|- ( Base ` g )
5		vb	\|- b
6		cplusg	\|- +g
7	3 6	cfv	\|- ( +g ` g )
8		vo	\|- o
9		vx	\|- x
10	5	cv	\|- b
11		vy	\|- y
12	9	cv	\|- x
13	8	cv	\|- o
14	11	cv	\|- y
15	12 14 13	co	\|- ( x o y )
16	15 10	wcel	\|- ( x o y ) e. b
17	16 11 10	wral	\|- A. y e. b ( x o y ) e. b
18	17 9 10	wral	\|- A. x e. b A. y e. b ( x o y ) e. b
19	18 8 7	wsbc	\|- [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b
20	19 5 4	wsbc	\|- [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b
21	20 1	cab	\|- { g \| [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
22	0 21	wceq	\|- Mgm = { g \| [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }

Metamath Proof Explorer

Definition df-mgm

Detailed syntax breakdown