Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-asslaw | Structured version Visualization version Unicode version |
Description: The associative law for binary operations, see definitions of laws A1. and M1. in section 1.1 of [Hall] p. 1, or definition 5 in [BourbakiAlg1] p. 4: the value of a binary operation applied the value of the binary operation applied to two operands and a third operand equals the value of the binary operation applied to the first operand and the value of the binary operation applied to the second and third operand. By this definition, the associative law is expressed as binary relation: a binary operation is related to a set by assLaw if the associative 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 FL, 1-Nov-2009.) (Revised by AV, 13-Jan-2020.) |
Ref | Expression |
---|---|
df-asslaw | assLaw |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | casslaw 41820 | . 2 assLaw | |
2 | vx | . . . . . . . . . 10 | |
3 | 2 | cv 1482 | . . . . . . . . 9 |
4 | vy | . . . . . . . . . 10 | |
5 | 4 | cv 1482 | . . . . . . . . 9 |
6 | vo | . . . . . . . . . 10 | |
7 | 6 | cv 1482 | . . . . . . . . 9 |
8 | 3, 5, 7 | co 6650 | . . . . . . . 8 |
9 | vz | . . . . . . . . 9 | |
10 | 9 | cv 1482 | . . . . . . . 8 |
11 | 8, 10, 7 | co 6650 | . . . . . . 7 |
12 | 5, 10, 7 | co 6650 | . . . . . . . 8 |
13 | 3, 12, 7 | co 6650 | . . . . . . 7 |
14 | 11, 13 | wceq 1483 | . . . . . 6 |
15 | vm | . . . . . . 7 | |
16 | 15 | cv 1482 | . . . . . 6 |
17 | 14, 9, 16 | wral 2912 | . . . . 5 |
18 | 17, 4, 16 | wral 2912 | . . . 4 |
19 | 18, 2, 16 | wral 2912 | . . 3 |
20 | 19, 6, 15 | copab 4712 | . 2 |
21 | 1, 20 | wceq 1483 | 1 assLaw |
Colors of variables: wff setvar class |
This definition is referenced by: isasslaw 41828 asslawass 41829 |
Copyright terms: Public domain | W3C validator |