Metamath Proof Explorer


Definition df-frgp

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 . (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Assertion df-frgp
|- freeGrp = ( i e. _V |-> ( ( freeMnd ` ( i X. 2o ) ) /s ( ~FG ` i ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfrgp
 |-  freeGrp
1 vi
 |-  i
2 cvv
 |-  _V
3 cfrmd
 |-  freeMnd
4 1 cv
 |-  i
5 c2o
 |-  2o
6 4 5 cxp
 |-  ( i X. 2o )
7 6 3 cfv
 |-  ( freeMnd ` ( i X. 2o ) )
8 cqus
 |-  /s
9 cefg
 |-  ~FG
10 4 9 cfv
 |-  ( ~FG ` i )
11 7 10 8 co
 |-  ( ( freeMnd ` ( i X. 2o ) ) /s ( ~FG ` i ) )
12 1 2 11 cmpt
 |-  ( i e. _V |-> ( ( freeMnd ` ( i X. 2o ) ) /s ( ~FG ` i ) ) )
13 0 12 wceq
 |-  freeGrp = ( i e. _V |-> ( ( freeMnd ` ( i X. 2o ) ) /s ( ~FG ` i ) ) )