Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-frgp | Structured version Visualization version GIF version |
Description: Define the free group on a set 𝐼 of generators, defined as the quotient of the free monoid on 𝐼 × 2𝑜 (representing the generator elements and their formal inverses) by the free group equivalence relation df-efg 18122. (Contributed by Mario Carneiro, 1-Oct-2015.) |
Ref | Expression |
---|---|
df-frgp | ⊢ freeGrp = (𝑖 ∈ V ↦ ((freeMnd‘(𝑖 × 2𝑜)) /s ( ~FG ‘𝑖))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cfrgp 18120 | . 2 class freeGrp | |
2 | vi | . . 3 setvar 𝑖 | |
3 | cvv 3200 | . . 3 class V | |
4 | 2 | cv 1482 | . . . . . 6 class 𝑖 |
5 | c2o 7554 | . . . . . 6 class 2𝑜 | |
6 | 4, 5 | cxp 5112 | . . . . 5 class (𝑖 × 2𝑜) |
7 | cfrmd 17384 | . . . . 5 class freeMnd | |
8 | 6, 7 | cfv 5888 | . . . 4 class (freeMnd‘(𝑖 × 2𝑜)) |
9 | cefg 18119 | . . . . 5 class ~FG | |
10 | 4, 9 | cfv 5888 | . . . 4 class ( ~FG ‘𝑖) |
11 | cqus 16165 | . . . 4 class /s | |
12 | 8, 10, 11 | co 6650 | . . 3 class ((freeMnd‘(𝑖 × 2𝑜)) /s ( ~FG ‘𝑖)) |
13 | 2, 3, 12 | cmpt 4729 | . 2 class (𝑖 ∈ V ↦ ((freeMnd‘(𝑖 × 2𝑜)) /s ( ~FG ‘𝑖))) |
14 | 1, 13 | wceq 1483 | 1 wff freeGrp = (𝑖 ∈ V ↦ ((freeMnd‘(𝑖 × 2𝑜)) /s ( ~FG ‘𝑖))) |
Colors of variables: wff setvar class |
This definition is referenced by: frgpval 18171 |
Copyright terms: Public domain | W3C validator |