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