Metamath Proof Explorer


Definition df-comlaw

Description: The commutative law for binary operations, see definitions of laws A2. and M2. in section 1.1 of Hall p. 1, or definition 8 in BourbakiAlg1 p. 7: the value of a binary operation applied to two operands equals the value of a binary operation applied to the two operands in reversed order. By this definition, the commutative law is expressed as binary relation: a binary operation is related to a set by comLaw if the commutative law holds for this binary operation regarding this set. Note that the binary operation needs neither to be closed nor to be a function. (Contributed by AV, 7-Jan-2020)

Ref Expression
Assertion df-comlaw comLaw = o m | x m y m x o y = y o x

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccomlaw class comLaw
1 vo setvar o
2 vm setvar m
3 vx setvar x
4 2 cv setvar m
5 vy setvar y
6 3 cv setvar x
7 1 cv setvar o
8 5 cv setvar y
9 6 8 7 co class x o y
10 8 6 7 co class y o x
11 9 10 wceq wff x o y = y o x
12 11 5 4 wral wff y m x o y = y o x
13 12 3 4 wral wff x m y m x o y = y o x
14 13 1 2 copab class o m | x m y m x o y = y o x
15 0 14 wceq wff comLaw = o m | x m y m x o y = y o x