Metamath Proof Explorer


Table of Contents - 20.43.17. Magmas and internal binary operations (alternate approach)

With df-mpo, binary operations are defined by a rule, and with df-ov, 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/Binaryoperation (19-Jan-2020), "... a binary operation on a set is a mapping of the elements of the Cartesian product to 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 internal binary operations, see df-intop. If, in addition, the result is also contained in the set , the operation is called closed internal binary operation, see df-clintop. Therefore, a "binary operation on a set " 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 and df-assintop), and on the other hand to define the common algebraic structures like magmas, groups, rings, etc. Internal binary operations, which obey 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 alternate definition df-cllaw for an internal binary operation is provided, which does not require function-ness, but only closure. Therefore, this definition could be used as binary operation (Slot 2) defined for a magma as extensible structure, see mgmplusgiopALT, or for an alternate definition df-mgm2 for a magma as extensible structure. Similar results are obtained for an associative operation (defining semigroups).

  1. Laws for internal binary operations
    1. ccllaw
    2. casslaw
    3. ccomlaw
    4. df-cllaw
    5. df-comlaw
    6. df-asslaw
    7. iscllaw
    8. iscomlaw
    9. clcllaw
    10. isasslaw
    11. asslawass
    12. mgmplusgiopALT
    13. sgrpplusgaopALT
  2. Internal binary operations
    1. cintop
    2. cclintop
    3. cassintop
    4. df-intop
    5. df-clintop
    6. df-assintop
    7. intopval
    8. intop
    9. clintopval
    10. assintopval
    11. assintopmap
    12. isclintop
    13. clintop
    14. assintop
    15. isassintop
    16. clintopcllaw
    17. assintopcllaw
    18. assintopasslaw
    19. assintopass
  3. Alternative definitions for magmas and semigroups
    1. cmgm2
    2. ccmgm2
    3. csgrp2
    4. ccsgrp2
    5. df-mgm2
    6. df-cmgm2
    7. df-sgrp2
    8. df-csgrp2
    9. ismgmALT
    10. iscmgmALT
    11. issgrpALT
    12. iscsgrpALT
    13. mgm2mgm
    14. sgrp2sgrp