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 ∈ V ⟼ freeMnd ⁡ i × 2 𝑜 / 𝑠 ~ FG ⁡ i

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfrgp class freeGrp
1 vi setvar i
2 cvv class V
3 cfrmd class freeMnd
4 1 cv setvar i
5 c2o class 2 𝑜
6 4 5 cxp class i × 2 𝑜
7 6 3 cfv class freeMnd ⁡ i × 2 𝑜
8 cqus class / 𝑠
9 cefg class ~ FG
10 4 9 cfv class ~ FG ⁡ i
11 7 10 8 co class freeMnd ⁡ i × 2 𝑜 / 𝑠 ~ FG ⁡ i
12 1 2 11 cmpt class i ∈ V ⟼ freeMnd ⁡ i × 2 𝑜 / 𝑠 ~ FG ⁡ i
13 0 12 wceq wff freeGrp = i ∈ V ⟼ freeMnd ⁡ i × 2 𝑜 / 𝑠 ~ FG ⁡ i