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 \in V ⟼ freeMnd (i \times 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 \times 2_{𝑜})$
7	6 3	cfv	$class freeMnd (i \times 2_{𝑜})$
8		cqus	$class /_{𝑠}$
9		cefg	$class ~_{FG}$
10	4 9	cfv	$class ~_{FG} (i)$
11	7 10 8	co	$class (freeMnd (i \times 2_{𝑜}) /_{𝑠} ~_{FG} (i))$
12	1 2 11	cmpt	$class (i \in V ⟼ freeMnd (i \times 2_{𝑜}) /_{𝑠} ~_{FG} (i))$
13	0 12	wceq	$wff freeGrp = (i \in V ⟼ freeMnd (i \times 2_{𝑜}) /_{𝑠} ~_{FG} (i))$

Metamath Proof Explorer

Definition df-frgp

Detailed syntax breakdown