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

Definition df-frgp 15342
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 15341. (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 15339 . 2  class freeGrp
2 vi . . 3  set  i
3 cvv 2956 . . 3  class  _V
42cv 1651 . . . . . 6  class  i
5 c2o 6718 . . . . . 6  class  2o
64, 5cxp 4876 . . . . 5  class  ( i  X.  2o )
7 cfrmd 14792 . . . . 5  class freeMnd
86, 7cfv 5454 . . . 4  class  (freeMnd `  (
i  X.  2o ) )
9 cefg 15338 . . . . 5  class ~FG
104, 9cfv 5454 . . . 4  class  ( ~FG  `  i
)
11 cqus 13731 . . . 4  class  /.s
128, 10, 11co 6081 . . 3  class  ( (freeMnd `  ( i  X.  2o ) )  /.s  ( ~FG  `  i ) )
132, 3, 12cmpt 4266 . 2  class  ( i  e.  _V  |->  ( (freeMnd `  ( i  X.  2o ) )  /.s  ( ~FG  `  i ) ) )
141, 13wceq 1652 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  15390
  Copyright terms: Public domain W3C validator