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 ) ) ) |
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 ) ) ) |