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

Definition df-frgp 18044
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 18043. (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 18041 . 2 class freeGrp
2 vi . . 3 setvar 𝑖
3 cvv 3186 . . 3 class V
42cv 1479 . . . . . 6 class 𝑖
5 c2o 7499 . . . . . 6 class 2𝑜
64, 5cxp 5072 . . . . 5 class (𝑖 × 2𝑜)
7 cfrmd 17305 . . . . 5 class freeMnd
86, 7cfv 5847 . . . 4 class (freeMnd‘(𝑖 × 2𝑜))
9 cefg 18040 . . . . 5 class ~FG
104, 9cfv 5847 . . . 4 class ( ~FG𝑖)
11 cqus 16086 . . . 4 class /s
128, 10, 11co 6604 . . 3 class ((freeMnd‘(𝑖 × 2𝑜)) /s ( ~FG𝑖))
132, 3, 12cmpt 4673 . 2 class (𝑖 ∈ V ↦ ((freeMnd‘(𝑖 × 2𝑜)) /s ( ~FG𝑖)))
141, 13wceq 1480 1 wff freeGrp = (𝑖 ∈ V ↦ ((freeMnd‘(𝑖 × 2𝑜)) /s ( ~FG𝑖)))
Colors of variables: wff setvar class
This definition is referenced by:  frgpval  18092
  Copyright terms: Public domain W3C validator