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

Definition df-frgp 17946
 Description: Define the free group on a set 𝐼 of generators, defined as the quotient of the free monoid on 𝐼 × 2𝑜 (representing the generator elements and their formal inverses) by the free group equivalence relation df-efg 17945. (Contributed by Mario Carneiro, 1-Oct-2015.)
Assertion
Ref Expression
df-frgp freeGrp = (𝑖 ∈ V ↦ ((freeMnd‘(𝑖 × 2𝑜)) /s ( ~FG𝑖)))

Detailed syntax breakdown of Definition df-frgp
StepHypRef Expression
1 cfrgp 17943 . 2 class freeGrp
2 vi . . 3 setvar 𝑖
3 cvv 3173 . . 3 class V
42cv 1474 . . . . . 6 class 𝑖
5 c2o 7441 . . . . . 6 class 2𝑜
64, 5cxp 5036 . . . . 5 class (𝑖 × 2𝑜)
7 cfrmd 17207 . . . . 5 class freeMnd
86, 7cfv 5804 . . . 4 class (freeMnd‘(𝑖 × 2𝑜))
9 cefg 17942 . . . . 5 class ~FG
104, 9cfv 5804 . . . 4 class ( ~FG𝑖)
11 cqus 15988 . . . 4 class /s
128, 10, 11co 6549 . . 3 class ((freeMnd‘(𝑖 × 2𝑜)) /s ( ~FG𝑖))
132, 3, 12cmpt 4643 . 2 class (𝑖 ∈ V ↦ ((freeMnd‘(𝑖 × 2𝑜)) /s ( ~FG𝑖)))
141, 13wceq 1475 1 wff freeGrp = (𝑖 ∈ V ↦ ((freeMnd‘(𝑖 × 2𝑜)) /s ( ~FG𝑖)))
 Colors of variables: wff setvar class This definition is referenced by:  frgpval  17994
 Copyright terms: Public domain W3C validator