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 of generators, defined as the quotient of the free monoid on (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 freeMnd s ~FG

Detailed syntax breakdown of Definition df-frgp
StepHypRef Expression
1 cfrgp 15339 . 2 freeGrp
2 vi . . 3
3 cvv 2956 . . 3
42cv 1651 . . . . . 6
5 c2o 6718 . . . . . 6
64, 5cxp 4876 . . . . 5
7 cfrmd 14792 . . . . 5 freeMnd
86, 7cfv 5454 . . . 4 freeMnd
9 cefg 15338 . . . . 5 ~FG
104, 9cfv 5454 . . . 4 ~FG
11 cqus 13731 . . . 4 s
128, 10, 11co 6081 . . 3 freeMnd s ~FG
132, 3, 12cmpt 4266 . 2 freeMnd s ~FG
141, 13wceq 1652 1 freeGrp freeMnd s ~FG
 Colors of variables: wff set class This definition is referenced by:  frgpval  15390
 Copyright terms: Public domain W3C validator