Theorem frgpinv

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

	Ref	Expression
Hypotheses	frgpadd.w	$$⊢W=\mathrm{I}\left(\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)$$
	frgpadd.g	$$⊢G=\mathrm{freeGrp}\left(I\right)$$
	frgpadd.r	$$⊢\underset{\dot{}}{\sim }={~}_{\mathit{FG}}\left(I\right)$$
	frgpinv.n	$$⊢N={inv}_g\left(G\right)$$
	frgpinv.m	$$⊢M=\left(y\in I,z\in 2_{𝑜}⟼⟨y,1_{𝑜}\setminus z⟩\right)$$
Assertion	frgpinv	$$⊢A\in W\to N\left(\left[A\right]\underset{\dot{}}{\sim }\right)=\left[\left(M\circ \mathrm{reverse}\left(A\right)\right)\right]\underset{\dot{}}{\sim }$$

Proof

Step	Hyp	Ref	Expression
1		frgpadd.w	$$⊢W=\mathrm{I}\left(\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)$$
2		frgpadd.g	$$⊢G=\mathrm{freeGrp}\left(I\right)$$
3		frgpadd.r	$$⊢\underset{\dot{}}{\sim }={~}_{\mathit{FG}}\left(I\right)$$
4		frgpinv.n	$$⊢N={inv}_g\left(G\right)$$
5		frgpinv.m	$$⊢M=\left(y\in I,z\in 2_{𝑜}⟼⟨y,1_{𝑜}\setminus z⟩\right)$$
6		fviss	$$⊢\mathrm{I}\left(\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)\subseteq \mathrm{Word}\left(I\times 2_{𝑜}\right)$$
7	1 6	eqsstri	$$⊢W\subseteq \mathrm{Word}\left(I\times 2_{𝑜}\right)$$
8	7	sseli	$$⊢A\in W\to A\in \mathrm{Word}\left(I\times 2_{𝑜}\right)$$
9		revcl	$$⊢A\in \mathrm{Word}\left(I\times 2_{𝑜}\right)\to \mathrm{reverse}\left(A\right)\in \mathrm{Word}\left(I\times 2_{𝑜}\right)$$
10	8 9	syl	$$⊢A\in W\to \mathrm{reverse}\left(A\right)\in \mathrm{Word}\left(I\times 2_{𝑜}\right)$$
11	5	efgmf	$$⊢M:I\times 2_{𝑜}⟶I\times 2_{𝑜}$$
12		wrdco	$$⊢\left(\mathrm{reverse}\left(A\right)\in \mathrm{Word}\left(I\times 2_{𝑜}\right)\wedge M:I\times 2_{𝑜}⟶I\times 2_{𝑜}\right)\to M\circ \mathrm{reverse}\left(A\right)\in \mathrm{Word}\left(I\times 2_{𝑜}\right)$$
13	10 11 12	sylancl	$$⊢A\in W\to M\circ \mathrm{reverse}\left(A\right)\in \mathrm{Word}\left(I\times 2_{𝑜}\right)$$
14	1	efgrcl	$$⊢A\in W\to \left(I\in \mathrm{V}\wedge W=\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)$$
15	14	simprd	$$⊢A\in W\to W=\mathrm{Word}\left(I\times 2_{𝑜}\right)$$
16	13 15	eleqtrrd	$$⊢A\in W\to M\circ \mathrm{reverse}\left(A\right)\in W$$
17		eqid	$$⊢{+}_G={+}_G$$
18	1 2 3 17	frgpadd	$$⊢\left(A\in W\wedge M\circ \mathrm{reverse}\left(A\right)\in W\right)\to \left[A\right]\underset{\dot{}}{\sim }{+}_G\left[\left(M\circ \mathrm{reverse}\left(A\right)\right)\right]\underset{\dot{}}{\sim }=\left[\left(A\mathrm{++}\left(M\circ \mathrm{reverse}\left(A\right)\right)\right)\right]\underset{\dot{}}{\sim }$$
19	16 18	mpdan	$$⊢A\in W\to \left[A\right]\underset{\dot{}}{\sim }{+}_G\left[\left(M\circ \mathrm{reverse}\left(A\right)\right)\right]\underset{\dot{}}{\sim }=\left[\left(A\mathrm{++}\left(M\circ \mathrm{reverse}\left(A\right)\right)\right)\right]\underset{\dot{}}{\sim }$$
20	1 3	efger	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}W$$
21	20	a1i	$$⊢A\in W\to \underset{\dot{}}{\sim }\mathrm{Er}W$$
22		eqid	$$⊢\left(v\in W⟼\left(n\in \left(0\dots \left|v\right|\right),w\in \left(I\times 2_{𝑜}\right)⟼v\mathrm{splice}⟨n,n,⟨“wM\left(w\right)”⟩⟩\right)\right)=\left(v\in W⟼\left(n\in \left(0\dots \left|v\right|\right),w\in \left(I\times 2_{𝑜}\right)⟼v\mathrm{splice}⟨n,n,⟨“wM\left(w\right)”⟩⟩\right)\right)$$
23	1 3 5 22	efginvrel2	$$⊢A\in W\to \left(A\mathrm{++}\left(M\circ \mathrm{reverse}\left(A\right)\right)\right)\underset{\dot{}}{\sim }\varnothing$$
24	21 23	erthi	$$⊢A\in W\to \left[\left(A\mathrm{++}\left(M\circ \mathrm{reverse}\left(A\right)\right)\right)\right]\underset{\dot{}}{\sim }=\left[\varnothing \right]\underset{\dot{}}{\sim }$$
25	2 3	frgp0	$$⊢I\in \mathrm{V}\to \left(G\in \mathrm{Grp}\wedge \left[\varnothing \right]\underset{\dot{}}{\sim }=0_G\right)$$
26	25	adantr	$$⊢\left(I\in \mathrm{V}\wedge W=\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)\to \left(G\in \mathrm{Grp}\wedge \left[\varnothing \right]\underset{\dot{}}{\sim }=0_G\right)$$
27	14 26	syl	$$⊢A\in W\to \left(G\in \mathrm{Grp}\wedge \left[\varnothing \right]\underset{\dot{}}{\sim }=0_G\right)$$
28	27	simprd	$$⊢A\in W\to \left[\varnothing \right]\underset{\dot{}}{\sim }=0_G$$
29	19 24 28	3eqtrd	$$⊢A\in W\to \left[A\right]\underset{\dot{}}{\sim }{+}_G\left[\left(M\circ \mathrm{reverse}\left(A\right)\right)\right]\underset{\dot{}}{\sim }=0_G$$
30	27	simpld	$$⊢A\in W\to G\in \mathrm{Grp}$$
31		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
32	2 3 1 31	frgpeccl	$$⊢A\in W\to \left[A\right]\underset{\dot{}}{\sim }\in {\mathrm{Base}}_G$$
33	2 3 1 31	frgpeccl	$$⊢M\circ \mathrm{reverse}\left(A\right)\in W\to \left[\left(M\circ \mathrm{reverse}\left(A\right)\right)\right]\underset{\dot{}}{\sim }\in {\mathrm{Base}}_G$$
34	16 33	syl	$$⊢A\in W\to \left[\left(M\circ \mathrm{reverse}\left(A\right)\right)\right]\underset{\dot{}}{\sim }\in {\mathrm{Base}}_G$$
35		eqid	$$⊢0_G=0_G$$
36	31 17 35 4	grpinvid1	$$⊢\left(G\in \mathrm{Grp}\wedge \left[A\right]\underset{\dot{}}{\sim }\in {\mathrm{Base}}_G\wedge \left[\left(M\circ \mathrm{reverse}\left(A\right)\right)\right]\underset{\dot{}}{\sim }\in {\mathrm{Base}}_G\right)\to \left(N\left(\left[A\right]\underset{\dot{}}{\sim }\right)=\left[\left(M\circ \mathrm{reverse}\left(A\right)\right)\right]\underset{\dot{}}{\sim }\leftrightarrow \left[A\right]\underset{\dot{}}{\sim }{+}_G\left[\left(M\circ \mathrm{reverse}\left(A\right)\right)\right]\underset{\dot{}}{\sim }=0_G\right)$$
37	30 32 34 36	syl3anc	$$⊢A\in W\to \left(N\left(\left[A\right]\underset{\dot{}}{\sim }\right)=\left[\left(M\circ \mathrm{reverse}\left(A\right)\right)\right]\underset{\dot{}}{\sim }\leftrightarrow \left[A\right]\underset{\dot{}}{\sim }{+}_G\left[\left(M\circ \mathrm{reverse}\left(A\right)\right)\right]\underset{\dot{}}{\sim }=0_G\right)$$
38	29 37	mpbird	$$⊢A\in W\to N\left(\left[A\right]\underset{\dot{}}{\sim }\right)=\left[\left(M\circ \mathrm{reverse}\left(A\right)\right)\right]\underset{\dot{}}{\sim }$$