Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-com1 Unicode version

Definition df-com1 25332
 Description: A device to add commutativity to magmas, semi-groups, monoids and so on. A commutative group is composed of 5 properties (internal operation, commutativity, associativity, existence of a neutral element and an inverse). If we switch on or off those four properties we get 32 structures. Instead of giving a name to those 32 structures, I suggest we use intersected classes and speak of or . (Contributed by FL, 5-Sep-2010.)
Assertion
Ref Expression
df-com1
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-com1
StepHypRef Expression
1 ccm1 25331 . 2
2 vx . . . . . . . 8
32cv 1622 . . . . . . 7
4 vy . . . . . . . 8
54cv 1622 . . . . . . 7
6 vg . . . . . . . 8
76cv 1622 . . . . . . 7
83, 5, 7co 5858 . . . . . 6
95, 3, 7co 5858 . . . . . 6
108, 9wceq 1623 . . . . 5
117cdm 4689 . . . . . 6
1211cdm 4689 . . . . 5
1310, 4, 12wral 2543 . . . 4
1413, 2, 12wral 2543 . . 3
1514, 6cab 2269 . 2
161, 15wceq 1623 1
 Colors of variables: wff set class This definition is referenced by:  iscom  25333
 Copyright terms: Public domain W3C validator