MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-grpo Structured version   Visualization version   GIF version

Definition df-grpo 26731
Description: Define the class of all group operations. The base set for a group can be determined from its group operation. Based on the definition in Exercise 28 of [Herstein] p. 54. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-grpo GrpOp = {𝑔 ∣ ∃𝑡(𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥𝑡𝑦𝑡𝑧𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢𝑡𝑥𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦𝑡 (𝑦𝑔𝑥) = 𝑢))}
Distinct variable group:   𝑡,𝑔,𝑢,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-grpo
StepHypRef Expression
1 cgr 26727 . 2 class GrpOp
2 vt . . . . . . . 8 setvar 𝑡
32cv 1474 . . . . . . 7 class 𝑡
43, 3cxp 5036 . . . . . 6 class (𝑡 × 𝑡)
5 vg . . . . . . 7 setvar 𝑔
65cv 1474 . . . . . 6 class 𝑔
74, 3, 6wf 5800 . . . . 5 wff 𝑔:(𝑡 × 𝑡)⟶𝑡
8 vx . . . . . . . . . . . 12 setvar 𝑥
98cv 1474 . . . . . . . . . . 11 class 𝑥
10 vy . . . . . . . . . . . 12 setvar 𝑦
1110cv 1474 . . . . . . . . . . 11 class 𝑦
129, 11, 6co 6549 . . . . . . . . . 10 class (𝑥𝑔𝑦)
13 vz . . . . . . . . . . 11 setvar 𝑧
1413cv 1474 . . . . . . . . . 10 class 𝑧
1512, 14, 6co 6549 . . . . . . . . 9 class ((𝑥𝑔𝑦)𝑔𝑧)
1611, 14, 6co 6549 . . . . . . . . . 10 class (𝑦𝑔𝑧)
179, 16, 6co 6549 . . . . . . . . 9 class (𝑥𝑔(𝑦𝑔𝑧))
1815, 17wceq 1475 . . . . . . . 8 wff ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))
1918, 13, 3wral 2896 . . . . . . 7 wff 𝑧𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))
2019, 10, 3wral 2896 . . . . . 6 wff 𝑦𝑡𝑧𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))
2120, 8, 3wral 2896 . . . . 5 wff 𝑥𝑡𝑦𝑡𝑧𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))
22 vu . . . . . . . . . . 11 setvar 𝑢
2322cv 1474 . . . . . . . . . 10 class 𝑢
2423, 9, 6co 6549 . . . . . . . . 9 class (𝑢𝑔𝑥)
2524, 9wceq 1475 . . . . . . . 8 wff (𝑢𝑔𝑥) = 𝑥
2611, 9, 6co 6549 . . . . . . . . . 10 class (𝑦𝑔𝑥)
2726, 23wceq 1475 . . . . . . . . 9 wff (𝑦𝑔𝑥) = 𝑢
2827, 10, 3wrex 2897 . . . . . . . 8 wff 𝑦𝑡 (𝑦𝑔𝑥) = 𝑢
2925, 28wa 383 . . . . . . 7 wff ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦𝑡 (𝑦𝑔𝑥) = 𝑢)
3029, 8, 3wral 2896 . . . . . 6 wff 𝑥𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦𝑡 (𝑦𝑔𝑥) = 𝑢)
3130, 22, 3wrex 2897 . . . . 5 wff 𝑢𝑡𝑥𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦𝑡 (𝑦𝑔𝑥) = 𝑢)
327, 21, 31w3a 1031 . . . 4 wff (𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥𝑡𝑦𝑡𝑧𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢𝑡𝑥𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦𝑡 (𝑦𝑔𝑥) = 𝑢))
3332, 2wex 1695 . . 3 wff 𝑡(𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥𝑡𝑦𝑡𝑧𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢𝑡𝑥𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦𝑡 (𝑦𝑔𝑥) = 𝑢))
3433, 5cab 2596 . 2 class {𝑔 ∣ ∃𝑡(𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥𝑡𝑦𝑡𝑧𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢𝑡𝑥𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦𝑡 (𝑦𝑔𝑥) = 𝑢))}
351, 34wceq 1475 1 wff GrpOp = {𝑔 ∣ ∃𝑡(𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥𝑡𝑦𝑡𝑧𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢𝑡𝑥𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦𝑡 (𝑦𝑔𝑥) = 𝑢))}
Colors of variables: wff setvar class
This definition is referenced by:  isgrpo  26735
  Copyright terms: Public domain W3C validator