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

Definition df-frgp 15035
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 15034. (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 15032 . 2  class freeGrp
2 vi . . 3  set  i
3 cvv 2801 . . 3  class  _V
42cv 1631 . . . . . 6  class  i
5 c2o 6489 . . . . . 6  class  2o
64, 5cxp 4703 . . . . 5  class  ( i  X.  2o )
7 cfrmd 14485 . . . . 5  class freeMnd
86, 7cfv 5271 . . . 4  class  (freeMnd `  (
i  X.  2o ) )
9 cefg 15031 . . . . 5  class ~FG
104, 9cfv 5271 . . . 4  class  ( ~FG  `  i
)
11 cqus 13424 . . . 4  class  /.s
128, 10, 11co 5874 . . 3  class  ( (freeMnd `  ( i  X.  2o ) )  /.s  ( ~FG  `  i ) )
132, 3, 12cmpt 4093 . 2  class  ( i  e.  _V  |->  ( (freeMnd `  ( i  X.  2o ) )  /.s  ( ~FG  `  i ) ) )
141, 13wceq 1632 1  wff freeGrp  =  ( i  e.  _V  |->  ( (freeMnd `  ( i  X.  2o ) )  /.s  ( ~FG  `  i
) ) )
Colors of variables: wff set class
This definition is referenced by:  frgpval  15083
  Copyright terms: Public domain W3C validator