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