efginvrel1

Description: The inverse of the reverse of a word composed with the word relates to the identity. (This provides an explicit expression for the representation of the group inverse, given a representative of the free group equivalence class.) (Contributed by Mario Carneiro, 1-Oct-2015)

	Ref	Expression
Hypotheses	efgval.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
	efgval.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
	efgval2.m	$⊢ M = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
	efgval2.t	$⊢ T = (v \in W ⟼ (n \in (0 \dots \|v\|), w \in (I \times 2_{𝑜}) ⟼ v splice ⟨n, n, ⟨“ w M (w) ”⟩⟩))$
Assertion	efginvrel1	$⊢ A \in W \to ((M \circ reverse (A)) ++ A) \underset{˙}{\sim} \emptyset$

Proof

Step	Hyp	Ref	Expression
1		efgval.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
2		efgval.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
3		efgval2.m	$⊢ M = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
4		efgval2.t	$⊢ T = (v \in W ⟼ (n \in (0 \dots \|v\|), w \in (I \times 2_{𝑜}) ⟼ v splice ⟨n, n, ⟨“ w M (w) ”⟩⟩))$
5		fviss	$⊢ I (Word (I \times 2_{𝑜})) \subseteq Word (I \times 2_{𝑜})$
6	1 5	eqsstri	$⊢ W \subseteq Word (I \times 2_{𝑜})$
7	6	sseli	$⊢ A \in W \to A \in Word (I \times 2_{𝑜})$
8		revcl	$⊢ A \in Word (I \times 2_{𝑜}) \to reverse (A) \in Word (I \times 2_{𝑜})$
9	7 8	syl	$⊢ A \in W \to reverse (A) \in Word (I \times 2_{𝑜})$
10	3	efgmf	$⊢ M : I \times 2_{𝑜} ⟶ I \times 2_{𝑜}$
11		revco	$⊢ (reverse (A) \in Word (I \times 2_{𝑜}) \land M : I \times 2_{𝑜} ⟶ I \times 2_{𝑜}) \to M \circ reverse (reverse (A)) = reverse (M \circ reverse (A))$
12	9 10 11	sylancl	$⊢ A \in W \to M \circ reverse (reverse (A)) = reverse (M \circ reverse (A))$
13		revrev	$⊢ A \in Word (I \times 2_{𝑜}) \to reverse (reverse (A)) = A$
14	7 13	syl	$⊢ A \in W \to reverse (reverse (A)) = A$
15	14	coeq2d	$⊢ A \in W \to M \circ reverse (reverse (A)) = M \circ A$
16	12 15	eqtr3d	$⊢ A \in W \to reverse (M \circ reverse (A)) = M \circ A$
17	16	coeq2d	$⊢ A \in W \to M \circ reverse (M \circ reverse (A)) = M \circ (M \circ A)$
18		wrdf	$⊢ A \in Word (I \times 2_{𝑜}) \to A : (0 ..^\|A\|) ⟶ I \times 2_{𝑜}$
19	7 18	syl	$⊢ A \in W \to A : (0 ..^\|A\|) ⟶ I \times 2_{𝑜}$
20	19	ffvelcdmda	$⊢ (A \in W \land c \in (0 ..^\|A\|)) \to A (c) \in (I \times 2_{𝑜})$
21	3	efgmnvl	$⊢ A (c) \in (I \times 2_{𝑜}) \to M (M (A (c))) = A (c)$
22	20 21	syl	$⊢ (A \in W \land c \in (0 ..^\|A\|)) \to M (M (A (c))) = A (c)$
23	22	mpteq2dva	$⊢ A \in W \to (c \in (0 ..^\|A\|) ⟼ M (M (A (c)))) = (c \in (0 ..^\|A\|) ⟼ A (c))$
24	10	ffvelcdmi	$⊢ A (c) \in (I \times 2_{𝑜}) \to M (A (c)) \in (I \times 2_{𝑜})$
25	20 24	syl	$⊢ (A \in W \land c \in (0 ..^\|A\|)) \to M (A (c)) \in (I \times 2_{𝑜})$
26		fcompt	$⊢ (M : I \times 2_{𝑜} ⟶ I \times 2_{𝑜} \land A : (0 ..^\|A\|) ⟶ I \times 2_{𝑜}) \to M \circ A = (c \in (0 ..^\|A\|) ⟼ M (A (c)))$
27	10 19 26	sylancr	$⊢ A \in W \to M \circ A = (c \in (0 ..^\|A\|) ⟼ M (A (c)))$
28	10	a1i	$⊢ A \in W \to M : I \times 2_{𝑜} ⟶ I \times 2_{𝑜}$
29	28	feqmptd	$⊢ A \in W \to M = (a \in (I \times 2_{𝑜}) ⟼ M (a))$
30		fveq2	$⊢ a = M (A (c)) \to M (a) = M (M (A (c)))$
31	25 27 29 30	fmptco	$⊢ A \in W \to M \circ (M \circ A) = (c \in (0 ..^\|A\|) ⟼ M (M (A (c))))$
32	19	feqmptd	$⊢ A \in W \to A = (c \in (0 ..^\|A\|) ⟼ A (c))$
33	23 31 32	3eqtr4d	$⊢ A \in W \to M \circ (M \circ A) = A$
34	17 33	eqtrd	$⊢ A \in W \to M \circ reverse (M \circ reverse (A)) = A$
35	34	oveq2d	$⊢ A \in W \to (M \circ reverse (A)) ++ (M \circ reverse (M \circ reverse (A))) = (M \circ reverse (A)) ++ A$
36		wrdco	$⊢ (reverse (A) \in Word (I \times 2_{𝑜}) \land M : I \times 2_{𝑜} ⟶ I \times 2_{𝑜}) \to M \circ reverse (A) \in Word (I \times 2_{𝑜})$
37	9 10 36	sylancl	$⊢ A \in W \to M \circ reverse (A) \in Word (I \times 2_{𝑜})$
38	1	efgrcl	$⊢ A \in W \to (I \in V \land W = Word (I \times 2_{𝑜}))$
39	38	simprd	$⊢ A \in W \to W = Word (I \times 2_{𝑜})$
40	37 39	eleqtrrd	$⊢ A \in W \to M \circ reverse (A) \in W$
41	1 2 3 4	efginvrel2	$⊢ M \circ reverse (A) \in W \to ((M \circ reverse (A)) ++ (M \circ reverse (M \circ reverse (A)))) \underset{˙}{\sim} \emptyset$
42	40 41	syl	$⊢ A \in W \to ((M \circ reverse (A)) ++ (M \circ reverse (M \circ reverse (A)))) \underset{˙}{\sim} \emptyset$
43	35 42	eqbrtrrd	$⊢ A \in W \to ((M \circ reverse (A)) ++ A) \underset{˙}{\sim} \emptyset$

Metamath Proof Explorer

Theorem efginvrel1

Proof