This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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