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 = ( 𝑖 ∈ V ↦ { 𝑟 ∣ ( 𝑟 Er Word ( 𝑖 × 2o ) ∧ ∀ 𝑥 ∈ Word ( 𝑖 × 2o ) ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦𝑖𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o𝑧 ) ⟩ ”⟩ ⟩ ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cefg ~FG
1 vi 𝑖
2 cvv V
3 vr 𝑟
4 3 cv 𝑟
5 1 cv 𝑖
6 c2o 2o
7 5 6 cxp ( 𝑖 × 2o )
8 7 cword Word ( 𝑖 × 2o )
9 8 4 wer 𝑟 Er Word ( 𝑖 × 2o )
10 vx 𝑥
11 vn 𝑛
12 cc0 0
13 cfz ...
14 chash
15 10 cv 𝑥
16 15 14 cfv ( ♯ ‘ 𝑥 )
17 12 16 13 co ( 0 ... ( ♯ ‘ 𝑥 ) )
18 vy 𝑦
19 vz 𝑧
20 csplice splice
21 11 cv 𝑛
22 18 cv 𝑦
23 19 cv 𝑧
24 22 23 cop 𝑦 , 𝑧
25 c1o 1o
26 25 23 cdif ( 1o𝑧 )
27 22 26 cop 𝑦 , ( 1o𝑧 ) ⟩
28 24 27 cs2 ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o𝑧 ) ⟩ ”⟩
29 21 21 28 cotp 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o𝑧 ) ⟩ ”⟩ ⟩
30 15 29 20 co ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o𝑧 ) ⟩ ”⟩ ⟩ )
31 15 30 4 wbr 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o𝑧 ) ⟩ ”⟩ ⟩ )
32 31 19 6 wral 𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o𝑧 ) ⟩ ”⟩ ⟩ )
33 32 18 5 wral 𝑦𝑖𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o𝑧 ) ⟩ ”⟩ ⟩ )
34 33 11 17 wral 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦𝑖𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o𝑧 ) ⟩ ”⟩ ⟩ )
35 34 10 8 wral 𝑥 ∈ Word ( 𝑖 × 2o ) ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦𝑖𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o𝑧 ) ⟩ ”⟩ ⟩ )
36 9 35 wa ( 𝑟 Er Word ( 𝑖 × 2o ) ∧ ∀ 𝑥 ∈ Word ( 𝑖 × 2o ) ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦𝑖𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o𝑧 ) ⟩ ”⟩ ⟩ ) )
37 36 3 cab { 𝑟 ∣ ( 𝑟 Er Word ( 𝑖 × 2o ) ∧ ∀ 𝑥 ∈ Word ( 𝑖 × 2o ) ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦𝑖𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o𝑧 ) ⟩ ”⟩ ⟩ ) ) }
38 37 cint { 𝑟 ∣ ( 𝑟 Er Word ( 𝑖 × 2o ) ∧ ∀ 𝑥 ∈ Word ( 𝑖 × 2o ) ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦𝑖𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o𝑧 ) ⟩ ”⟩ ⟩ ) ) }
39 1 2 38 cmpt ( 𝑖 ∈ V ↦ { 𝑟 ∣ ( 𝑟 Er Word ( 𝑖 × 2o ) ∧ ∀ 𝑥 ∈ Word ( 𝑖 × 2o ) ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦𝑖𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o𝑧 ) ⟩ ”⟩ ⟩ ) ) } )
40 0 39 wceq ~FG = ( 𝑖 ∈ V ↦ { 𝑟 ∣ ( 𝑟 Er Word ( 𝑖 × 2o ) ∧ ∀ 𝑥 ∈ Word ( 𝑖 × 2o ) ∀ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑦𝑖𝑧 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑛 , 𝑛 , ⟨“ ⟨ 𝑦 , 𝑧 ⟩ ⟨ 𝑦 , ( 1o𝑧 ) ⟩ ”⟩ ⟩ ) ) } )