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 ) >. "> >. ) ) } )