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

Definition df-frgp 16601
Description: Define the free group on a set  I of generators, defined as the quotient of the free monoid on  I  X.  2o (representing the generator elements and their formal inverses) by the free group equivalence relation df-efg 16600. (Contributed by Mario Carneiro, 1-Oct-2015.)
Assertion
Ref Expression
df-frgp  |- freeGrp  =  ( i  e.  _V  |->  ( (freeMnd `  ( i  X.  2o ) )  /.s  ( ~FG  `  i
) ) )

Detailed syntax breakdown of Definition df-frgp
StepHypRef Expression
1 cfrgp 16598 . 2  class freeGrp
2 vi . . 3  setvar  i
3 cvv 3118 . . 3  class  _V
42cv 1378 . . . . . 6  class  i
5 c2o 7136 . . . . . 6  class  2o
64, 5cxp 5003 . . . . 5  class  ( i  X.  2o )
7 cfrmd 15887 . . . . 5  class freeMnd
86, 7cfv 5594 . . . 4  class  (freeMnd `  (
i  X.  2o ) )
9 cefg 16597 . . . . 5  class ~FG
104, 9cfv 5594 . . . 4  class  ( ~FG  `  i
)
11 cqus 14777 . . . 4  class  /.s
128, 10, 11co 6295 . . 3  class  ( (freeMnd `  ( i  X.  2o ) )  /.s  ( ~FG  `  i ) )
132, 3, 12cmpt 4511 . 2  class  ( i  e.  _V  |->  ( (freeMnd `  ( i  X.  2o ) )  /.s  ( ~FG  `  i ) ) )
141, 13wceq 1379 1  wff freeGrp  =  ( i  e.  _V  |->  ( (freeMnd `  ( i  X.  2o ) )  /.s  ( ~FG  `  i
) ) )
Colors of variables: wff setvar class
This definition is referenced by:  frgpval  16649
  Copyright terms: Public domain W3C validator