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

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

Detailed syntax breakdown of Definition df-frgp
StepHypRef Expression
1 cfrgp 18833 . 2 class freeGrp
2 vi . . 3 setvar 𝑖
3 cvv 3480 . . 3 class V
42cv 1537 . . . . . 6 class 𝑖
5 c2o 8092 . . . . . 6 class 2o
64, 5cxp 5540 . . . . 5 class (𝑖 × 2o)
7 cfrmd 18012 . . . . 5 class freeMnd
86, 7cfv 6343 . . . 4 class (freeMnd‘(𝑖 × 2o))
9 cefg 18832 . . . . 5 class ~FG
104, 9cfv 6343 . . . 4 class ( ~FG𝑖)
11 cqus 16778 . . . 4 class /s
128, 10, 11co 7149 . . 3 class ((freeMnd‘(𝑖 × 2o)) /s ( ~FG𝑖))
132, 3, 12cmpt 5132 . 2 class (𝑖 ∈ V ↦ ((freeMnd‘(𝑖 × 2o)) /s ( ~FG𝑖)))
141, 13wceq 1538 1 wff freeGrp = (𝑖 ∈ V ↦ ((freeMnd‘(𝑖 × 2o)) /s ( ~FG𝑖)))
 Colors of variables: wff setvar class This definition is referenced by:  frgpval  18884
 Copyright terms: Public domain W3C validator