This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∖ 𝑧 ) ⟩ ”⟩ ⟩ ) ) } )