Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-asslaw Structured version   Visualization version   GIF version

Definition df-asslaw 42393
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.)
Assertion
Ref Expression
df-asslaw assLaw = {⟨𝑜, 𝑚⟩ ∣ ∀𝑥𝑚𝑦𝑚𝑧𝑚 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))}
Distinct variable group:   𝑚,𝑜,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-asslaw
StepHypRef Expression
1 casslaw 42389 . 2 class assLaw
2 vx . . . . . . . . . 10 setvar 𝑥
32cv 1636 . . . . . . . . 9 class 𝑥
4 vy . . . . . . . . . 10 setvar 𝑦
54cv 1636 . . . . . . . . 9 class 𝑦
6 vo . . . . . . . . . 10 setvar 𝑜
76cv 1636 . . . . . . . . 9 class 𝑜
83, 5, 7co 6877 . . . . . . . 8 class (𝑥𝑜𝑦)
9 vz . . . . . . . . 9 setvar 𝑧
109cv 1636 . . . . . . . 8 class 𝑧
118, 10, 7co 6877 . . . . . . 7 class ((𝑥𝑜𝑦)𝑜𝑧)
125, 10, 7co 6877 . . . . . . . 8 class (𝑦𝑜𝑧)
133, 12, 7co 6877 . . . . . . 7 class (𝑥𝑜(𝑦𝑜𝑧))
1411, 13wceq 1637 . . . . . 6 wff ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))
15 vm . . . . . . 7 setvar 𝑚
1615cv 1636 . . . . . 6 class 𝑚
1714, 9, 16wral 3103 . . . . 5 wff 𝑧𝑚 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))
1817, 4, 16wral 3103 . . . 4 wff 𝑦𝑚𝑧𝑚 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))
1918, 2, 16wral 3103 . . 3 wff 𝑥𝑚𝑦𝑚𝑧𝑚 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))
2019, 6, 15copab 4913 . 2 class {⟨𝑜, 𝑚⟩ ∣ ∀𝑥𝑚𝑦𝑚𝑧𝑚 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))}
211, 20wceq 1637 1 wff assLaw = {⟨𝑜, 𝑚⟩ ∣ ∀𝑥𝑚𝑦𝑚𝑧𝑚 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))}
Colors of variables: wff setvar class
This definition is referenced by:  isasslaw  42397  asslawass  42398
  Copyright terms: Public domain W3C validator