![]() |
Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-comlaw | Structured version Visualization version GIF version |
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 |
---|---|
df-comlaw | ⊢ comLaw = {〈𝑜, 𝑚〉 ∣ ∀𝑥 ∈ 𝑚 ∀𝑦 ∈ 𝑚 (𝑥𝑜𝑦) = (𝑦𝑜𝑥)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ccomlaw 44797 | . 2 class comLaw | |
2 | vx | . . . . . . . 8 setvar 𝑥 | |
3 | 2 | cv 1538 | . . . . . . 7 class 𝑥 |
4 | vy | . . . . . . . 8 setvar 𝑦 | |
5 | 4 | cv 1538 | . . . . . . 7 class 𝑦 |
6 | vo | . . . . . . . 8 setvar 𝑜 | |
7 | 6 | cv 1538 | . . . . . . 7 class 𝑜 |
8 | 3, 5, 7 | co 7143 | . . . . . 6 class (𝑥𝑜𝑦) |
9 | 5, 3, 7 | co 7143 | . . . . . 6 class (𝑦𝑜𝑥) |
10 | 8, 9 | wceq 1539 | . . . . 5 wff (𝑥𝑜𝑦) = (𝑦𝑜𝑥) |
11 | vm | . . . . . 6 setvar 𝑚 | |
12 | 11 | cv 1538 | . . . . 5 class 𝑚 |
13 | 10, 4, 12 | wral 3068 | . . . 4 wff ∀𝑦 ∈ 𝑚 (𝑥𝑜𝑦) = (𝑦𝑜𝑥) |
14 | 13, 2, 12 | wral 3068 | . . 3 wff ∀𝑥 ∈ 𝑚 ∀𝑦 ∈ 𝑚 (𝑥𝑜𝑦) = (𝑦𝑜𝑥) |
15 | 14, 6, 11 | copab 5087 | . 2 class {〈𝑜, 𝑚〉 ∣ ∀𝑥 ∈ 𝑚 ∀𝑦 ∈ 𝑚 (𝑥𝑜𝑦) = (𝑦𝑜𝑥)} |
16 | 1, 15 | wceq 1539 | 1 wff comLaw = {〈𝑜, 𝑚〉 ∣ ∀𝑥 ∈ 𝑚 ∀𝑦 ∈ 𝑚 (𝑥𝑜𝑦) = (𝑦𝑜𝑥)} |
Colors of variables: wff setvar class |
This definition is referenced by: iscomlaw 44802 |
Copyright terms: Public domain | W3C validator |