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 = ( 𝑖 ∈ V ↦ ( ( freeMnd ‘ ( 𝑖 × 2o ) ) /s ( ~FG𝑖 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfrgp freeGrp
1 vi 𝑖
2 cvv V
3 cfrmd freeMnd
4 1 cv 𝑖
5 c2o 2o
6 4 5 cxp ( 𝑖 × 2o )
7 6 3 cfv ( freeMnd ‘ ( 𝑖 × 2o ) )
8 cqus /s
9 cefg ~FG
10 4 9 cfv ( ~FG𝑖 )
11 7 10 8 co ( ( freeMnd ‘ ( 𝑖 × 2o ) ) /s ( ~FG𝑖 ) )
12 1 2 11 cmpt ( 𝑖 ∈ V ↦ ( ( freeMnd ‘ ( 𝑖 × 2o ) ) /s ( ~FG𝑖 ) ) )
13 0 12 wceq freeGrp = ( 𝑖 ∈ V ↦ ( ( freeMnd ‘ ( 𝑖 × 2o ) ) /s ( ~FG𝑖 ) ) )