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