Theorem frgpinv

Description: The inverse of an element of the free group. (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	frgpadd.w	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
	frgpadd.g	⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
	frgpadd.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
	frgpinv.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
	frgpinv.m	⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
Assertion	frgpinv	⊢ ( 𝐴 ∈ 𝑊 → ( 𝑁 ‘ [ 𝐴 ] ∼ ) = [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] ∼ )

Proof

Step	Hyp	Ref	Expression
1		frgpadd.w	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
2		frgpadd.g	⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
3		frgpadd.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
4		frgpinv.n	⊢ 𝑁 = ( invg ‘ 𝐺 )
5		frgpinv.m	⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
6		fviss	⊢ ( I ‘ Word ( 𝐼 × 2o ) ) ⊆ Word ( 𝐼 × 2o )
7	1 6	eqsstri	⊢ 𝑊 ⊆ Word ( 𝐼 × 2o )
8	7	sseli	⊢ ( 𝐴 ∈ 𝑊 → 𝐴 ∈ Word ( 𝐼 × 2o ) )
9		revcl	⊢ ( 𝐴 ∈ Word ( 𝐼 × 2o ) → ( reverse ‘ 𝐴 ) ∈ Word ( 𝐼 × 2o ) )
10	8 9	syl	⊢ ( 𝐴 ∈ 𝑊 → ( reverse ‘ 𝐴 ) ∈ Word ( 𝐼 × 2o ) )
11	5	efgmf	⊢ 𝑀 : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o )
12		wrdco	⊢ ( ( ( reverse ‘ 𝐴 ) ∈ Word ( 𝐼 × 2o ) ∧ 𝑀 : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o ) ) → ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ∈ Word ( 𝐼 × 2o ) )
13	10 11 12	sylancl	⊢ ( 𝐴 ∈ 𝑊 → ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ∈ Word ( 𝐼 × 2o ) )
14	1	efgrcl	⊢ ( 𝐴 ∈ 𝑊 → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) )
15	14	simprd	⊢ ( 𝐴 ∈ 𝑊 → 𝑊 = Word ( 𝐼 × 2o ) )
16	13 15	eleqtrrd	⊢ ( 𝐴 ∈ 𝑊 → ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ∈ 𝑊 )
17		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
18	1 2 3 17	frgpadd	⊢ ( ( 𝐴 ∈ 𝑊 ∧ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ∈ 𝑊 ) → ( [ 𝐴 ] ∼ ( +g ‘ 𝐺 ) [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] ∼ ) = [ ( 𝐴 ++ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ) ] ∼ )
19	16 18	mpdan	⊢ ( 𝐴 ∈ 𝑊 → ( [ 𝐴 ] ∼ ( +g ‘ 𝐺 ) [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] ∼ ) = [ ( 𝐴 ++ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ) ] ∼ )
20	1 3	efger	⊢ ∼ Er 𝑊
21	20	a1i	⊢ ( 𝐴 ∈ 𝑊 → ∼ Er 𝑊 )
22		eqid	⊢ ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) ) = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
23	1 3 5 22	efginvrel2	⊢ ( 𝐴 ∈ 𝑊 → ( 𝐴 ++ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ) ∼ ∅ )
24	21 23	erthi	⊢ ( 𝐴 ∈ 𝑊 → [ ( 𝐴 ++ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ) ] ∼ = [ ∅ ] ∼ )
25	2 3	frgp0	⊢ ( 𝐼 ∈ V → ( 𝐺 ∈ Grp ∧ [ ∅ ] ∼ = ( 0g ‘ 𝐺 ) ) )
26	25	adantr	⊢ ( ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) → ( 𝐺 ∈ Grp ∧ [ ∅ ] ∼ = ( 0g ‘ 𝐺 ) ) )
27	14 26	syl	⊢ ( 𝐴 ∈ 𝑊 → ( 𝐺 ∈ Grp ∧ [ ∅ ] ∼ = ( 0g ‘ 𝐺 ) ) )
28	27	simprd	⊢ ( 𝐴 ∈ 𝑊 → [ ∅ ] ∼ = ( 0g ‘ 𝐺 ) )
29	19 24 28	3eqtrd	⊢ ( 𝐴 ∈ 𝑊 → ( [ 𝐴 ] ∼ ( +g ‘ 𝐺 ) [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] ∼ ) = ( 0g ‘ 𝐺 ) )
30	27	simpld	⊢ ( 𝐴 ∈ 𝑊 → 𝐺 ∈ Grp )
31		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
32	2 3 1 31	frgpeccl	⊢ ( 𝐴 ∈ 𝑊 → [ 𝐴 ] ∼ ∈ ( Base ‘ 𝐺 ) )
33	2 3 1 31	frgpeccl	⊢ ( ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ∈ 𝑊 → [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] ∼ ∈ ( Base ‘ 𝐺 ) )
34	16 33	syl	⊢ ( 𝐴 ∈ 𝑊 → [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] ∼ ∈ ( Base ‘ 𝐺 ) )
35		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
36	31 17 35 4	grpinvid1	⊢ ( ( 𝐺 ∈ Grp ∧ [ 𝐴 ] ∼ ∈ ( Base ‘ 𝐺 ) ∧ [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] ∼ ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑁 ‘ [ 𝐴 ] ∼ ) = [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] ∼ ↔ ( [ 𝐴 ] ∼ ( +g ‘ 𝐺 ) [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] ∼ ) = ( 0g ‘ 𝐺 ) ) )
37	30 32 34 36	syl3anc	⊢ ( 𝐴 ∈ 𝑊 → ( ( 𝑁 ‘ [ 𝐴 ] ∼ ) = [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] ∼ ↔ ( [ 𝐴 ] ∼ ( +g ‘ 𝐺 ) [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] ∼ ) = ( 0g ‘ 𝐺 ) ) )
38	29 37	mpbird	⊢ ( 𝐴 ∈ 𝑊 → ( 𝑁 ‘ [ 𝐴 ] ∼ ) = [ ( 𝑀 ∘ ( reverse ‘ 𝐴 ) ) ] ∼ )