Metamath Proof Explorer

Definition df-efg

Description: Define the free group equivalence relation, which is the smallest equivalence relation ~ such that for any words A , B and formal symbol x with inverse invg x , A B ~A x ( invg x ) B . (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Assertion df-efg 
|- ~FG = ( i e. _V |-> |^| { r | ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cefg 
 |-  ~FG
1 vi 
 |-  i
2 cvv 
 |-  _V
3 vr 
 |-  r
4 3 cv 
 |-  r
5 1 cv 
 |-  i
6 c2o 
 |-  2o
7 5 6 cxp 
 |-  ( i X. 2o )
8 7 cword 
 |-  Word ( i X. 2o )
9 8 4 wer 
 |-  r Er Word ( i X. 2o )
10 vx 
 |-  x
11 vn 
 |-  n
12 cc0 
 |-  0
13 cfz 
 |-  ...
14 chash 
 |-  #
15 10 cv 
 |-  x
16 15 14 cfv 
 |-  ( # ` x )
17 12 16 13 co 
 |-  ( 0 ... ( # ` x ) )
18 vy 
 |-  y
19 vz 
 |-  z
20 csplice 
 |-  splice
21 11 cv 
 |-  n
22 18 cv 
 |-  y
23 19 cv 
 |-  z
24 22 23 cop 
 |-  <. y , z >.
25 c1o 
 |-  1o
26 25 23 cdif 
 |-  ( 1o \ z )
27 22 26 cop 
 |-  <. y , ( 1o \ z ) >.
28 24 27 cs2 
 |-  <" <. y , z >. <. y , ( 1o \ z ) >. ">
29 21 21 28 cotp 
 |-  <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >.
30 15 29 20 co 
 |-  ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. )
31 15 30 4 wbr 
 |-  x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. )
32 31 19 6 wral 
 |-  A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. )
33 32 18 5 wral 
 |-  A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. )
34 33 11 17 wral 
 |-  A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. )
35 34 10 8 wral 
 |-  A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. )
36 9 35 wa 
 |-  ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) )
37 36 3 cab 
 |-  { r | ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) }
38 37 cint 
 |-  |^| { r | ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) }
39 1 2 38 cmpt 
 |-  ( i e. _V |-> |^| { r | ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } )
40 0 39 wceq 
 |-  ~FG = ( i e. _V |-> |^| { r | ( r Er Word ( i X. 2o ) /\ A. x e. Word ( i X. 2o ) A. n e. ( 0 ... ( # ` x ) ) A. y e. i A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) } )