efginvrel2

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	efginvrel2	$⊢ A \in W \to (A ++ (M \circ reverse (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		id	$⊢ c = \emptyset \to c = \emptyset$
9		fveq2	$⊢ c = \emptyset \to reverse (c) = reverse (\emptyset)$
10		rev0	$⊢ reverse (\emptyset) = \emptyset$
11	9 10	eqtrdi	$⊢ c = \emptyset \to reverse (c) = \emptyset$
12	11	coeq2d	$⊢ c = \emptyset \to M \circ reverse (c) = M \circ \emptyset$
13		co02	$⊢ M \circ \emptyset = \emptyset$
14	12 13	eqtrdi	$⊢ c = \emptyset \to M \circ reverse (c) = \emptyset$
15	8 14	oveq12d	$⊢ c = \emptyset \to c ++ (M \circ reverse (c)) = \emptyset ++ \emptyset$
16	15	breq1d	$⊢ c = \emptyset \to ((c ++ (M \circ reverse (c))) \underset{˙}{\sim} \emptyset \leftrightarrow (\emptyset ++ \emptyset) \underset{˙}{\sim} \emptyset)$
17	16	imbi2d	$⊢ c = \emptyset \to ((A \in W \to (c ++ (M \circ reverse (c))) \underset{˙}{\sim} \emptyset) \leftrightarrow (A \in W \to (\emptyset ++ \emptyset) \underset{˙}{\sim} \emptyset))$
18		id	$⊢ c = a \to c = a$
19		fveq2	$⊢ c = a \to reverse (c) = reverse (a)$
20	19	coeq2d	$⊢ c = a \to M \circ reverse (c) = M \circ reverse (a)$
21	18 20	oveq12d	$⊢ c = a \to c ++ (M \circ reverse (c)) = a ++ (M \circ reverse (a))$
22	21	breq1d	$⊢ c = a \to ((c ++ (M \circ reverse (c))) \underset{˙}{\sim} \emptyset \leftrightarrow (a ++ (M \circ reverse (a))) \underset{˙}{\sim} \emptyset)$
23	22	imbi2d	$⊢ c = a \to ((A \in W \to (c ++ (M \circ reverse (c))) \underset{˙}{\sim} \emptyset) \leftrightarrow (A \in W \to (a ++ (M \circ reverse (a))) \underset{˙}{\sim} \emptyset))$
24		id	$⊢ c = a ++ ⟨“ b ”⟩ \to c = a ++ ⟨“ b ”⟩$
25		fveq2	$⊢ c = a ++ ⟨“ b ”⟩ \to reverse (c) = reverse (a ++ ⟨“ b ”⟩)$
26	25	coeq2d	$⊢ c = a ++ ⟨“ b ”⟩ \to M \circ reverse (c) = M \circ reverse (a ++ ⟨“ b ”⟩)$
27	24 26	oveq12d	$⊢ c = a ++ ⟨“ b ”⟩ \to c ++ (M \circ reverse (c)) = (a ++ ⟨“ b ”⟩) ++ (M \circ reverse (a ++ ⟨“ b ”⟩))$
28	27	breq1d	$⊢ c = a ++ ⟨“ b ”⟩ \to ((c ++ (M \circ reverse (c))) \underset{˙}{\sim} \emptyset \leftrightarrow ((a ++ ⟨“ b ”⟩) ++ (M \circ reverse (a ++ ⟨“ b ”⟩))) \underset{˙}{\sim} \emptyset)$
29	28	imbi2d	$⊢ c = a ++ ⟨“ b ”⟩ \to ((A \in W \to (c ++ (M \circ reverse (c))) \underset{˙}{\sim} \emptyset) \leftrightarrow (A \in W \to ((a ++ ⟨“ b ”⟩) ++ (M \circ reverse (a ++ ⟨“ b ”⟩))) \underset{˙}{\sim} \emptyset))$
30		id	$⊢ c = A \to c = A$
31		fveq2	$⊢ c = A \to reverse (c) = reverse (A)$
32	31	coeq2d	$⊢ c = A \to M \circ reverse (c) = M \circ reverse (A)$
33	30 32	oveq12d	$⊢ c = A \to c ++ (M \circ reverse (c)) = A ++ (M \circ reverse (A))$
34	33	breq1d	$⊢ c = A \to ((c ++ (M \circ reverse (c))) \underset{˙}{\sim} \emptyset \leftrightarrow (A ++ (M \circ reverse (A))) \underset{˙}{\sim} \emptyset)$
35	34	imbi2d	$⊢ c = A \to ((A \in W \to (c ++ (M \circ reverse (c))) \underset{˙}{\sim} \emptyset) \leftrightarrow (A \in W \to (A ++ (M \circ reverse (A))) \underset{˙}{\sim} \emptyset))$
36		ccatidid	$⊢ \emptyset ++ \emptyset = \emptyset$
37	1 2	efger	$⊢ \underset{˙}{\sim} Er W$
38	37	a1i	$⊢ A \in W \to \underset{˙}{\sim} Er W$
39		wrd0	$⊢ \emptyset \in Word (I \times 2_{𝑜})$
40	1	efgrcl	$⊢ A \in W \to (I \in V \land W = Word (I \times 2_{𝑜}))$
41	40	simprd	$⊢ A \in W \to W = Word (I \times 2_{𝑜})$
42	39 41	eleqtrrid	$⊢ A \in W \to \emptyset \in W$
43	38 42	erref	$⊢ A \in W \to \emptyset \underset{˙}{\sim} \emptyset$
44	36 43	eqbrtrid	$⊢ A \in W \to (\emptyset ++ \emptyset) \underset{˙}{\sim} \emptyset$
45	37	a1i	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to \underset{˙}{\sim} Er W$
46		simprl	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to a \in Word (I \times 2_{𝑜})$
47		revcl	$⊢ a \in Word (I \times 2_{𝑜}) \to reverse (a) \in Word (I \times 2_{𝑜})$
48	47	ad2antrl	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to reverse (a) \in Word (I \times 2_{𝑜})$
49	3	efgmf	$⊢ M : I \times 2_{𝑜} ⟶ I \times 2_{𝑜}$
50		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_{𝑜})$
51	48 49 50	sylancl	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to M \circ reverse (a) \in Word (I \times 2_{𝑜})$
52		ccatcl	$⊢ (a \in Word (I \times 2_{𝑜}) \land M \circ reverse (a) \in Word (I \times 2_{𝑜})) \to a ++ (M \circ reverse (a)) \in Word (I \times 2_{𝑜})$
53	46 51 52	syl2anc	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to a ++ (M \circ reverse (a)) \in Word (I \times 2_{𝑜})$
54	41	adantr	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to W = Word (I \times 2_{𝑜})$
55	53 54	eleqtrrd	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to a ++ (M \circ reverse (a)) \in W$
56		lencl	$⊢ a \in Word (I \times 2_{𝑜}) \to \|a\| \in ℕ_{0}$
57	56	ad2antrl	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to \|a\| \in ℕ_{0}$
58		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
59	57 58	eleqtrdi	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to \|a\| \in ℤ_{\geq 0}$
60		ccatlen	$⊢ (a \in Word (I \times 2_{𝑜}) \land M \circ reverse (a) \in Word (I \times 2_{𝑜})) \to \|a ++ (M \circ reverse (a))\| = \|a\| + \|M \circ reverse (a)\|$
61	46 51 60	syl2anc	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to \|a ++ (M \circ reverse (a))\| = \|a\| + \|M \circ reverse (a)\|$
62	57	nn0zd	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to \|a\| \in ℤ$
63	62	uzidd	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to \|a\| \in ℤ_{\geq \|a\|}$
64		lencl	$⊢ M \circ reverse (a) \in Word (I \times 2_{𝑜}) \to \|M \circ reverse (a)\| \in ℕ_{0}$
65	51 64	syl	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to \|M \circ reverse (a)\| \in ℕ_{0}$
66		uzaddcl	$⊢ (\|a\| \in ℤ_{\geq \|a\|} \land \|M \circ reverse (a)\| \in ℕ_{0}) \to \|a\| + \|M \circ reverse (a)\| \in ℤ_{\geq \|a\|}$
67	63 65 66	syl2anc	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to \|a\| + \|M \circ reverse (a)\| \in ℤ_{\geq \|a\|}$
68	61 67	eqeltrd	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to \|a ++ (M \circ reverse (a))\| \in ℤ_{\geq \|a\|}$
69		elfzuzb	$⊢ \|a\| \in (0 \dots \|a ++ (M \circ reverse (a))\|) \leftrightarrow (\|a\| \in ℤ_{\geq 0} \land \|a ++ (M \circ reverse (a))\| \in ℤ_{\geq \|a\|})$
70	59 68 69	sylanbrc	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to \|a\| \in (0 \dots \|a ++ (M \circ reverse (a))\|)$
71		simprr	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to b \in (I \times 2_{𝑜})$
72	1 2 3 4	efgtval	$⊢ (a ++ (M \circ reverse (a)) \in W \land \|a\| \in (0 \dots \|a ++ (M \circ reverse (a))\|) \land b \in (I \times 2_{𝑜})) \to \|a\| T (a ++ (M \circ reverse (a))) b = (a ++ (M \circ reverse (a))) splice ⟨\|a\|, \|a\|, ⟨“ b M (b) ”⟩⟩$
73	55 70 71 72	syl3anc	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to \|a\| T (a ++ (M \circ reverse (a))) b = (a ++ (M \circ reverse (a))) splice ⟨\|a\|, \|a\|, ⟨“ b M (b) ”⟩⟩$
74	39	a1i	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to \emptyset \in Word (I \times 2_{𝑜})$
75	49	ffvelcdmi	$⊢ b \in (I \times 2_{𝑜}) \to M (b) \in (I \times 2_{𝑜})$
76	75	ad2antll	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to M (b) \in (I \times 2_{𝑜})$
77	71 76	s2cld	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to ⟨“ b M (b) ”⟩ \in Word (I \times 2_{𝑜})$
78		ccatrid	$⊢ a \in Word (I \times 2_{𝑜}) \to a ++ \emptyset = a$
79	78	ad2antrl	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to a ++ \emptyset = a$
80	79	eqcomd	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to a = a ++ \emptyset$
81	80	oveq1d	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to a ++ (M \circ reverse (a)) = (a ++ \emptyset) ++ (M \circ reverse (a))$
82		eqidd	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to \|a\| = \|a\|$
83		hash0	$⊢ \|\emptyset\| = 0$
84	83	oveq2i	$⊢ \|a\| + \|\emptyset\| = \|a\| + 0$
85	57	nn0cnd	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to \|a\| \in ℂ$
86	85	addridd	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to \|a\| + 0 = \|a\|$
87	84 86	eqtr2id	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to \|a\| = \|a\| + \|\emptyset\|$
88	46 74 51 77 81 82 87	splval2	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to (a ++ (M \circ reverse (a))) splice ⟨\|a\|, \|a\|, ⟨“ b M (b) ”⟩⟩ = (a ++ ⟨“ b M (b) ”⟩) ++ (M \circ reverse (a))$
89	71	s1cld	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to ⟨“ b ”⟩ \in Word (I \times 2_{𝑜})$
90		revccat	$⊢ (a \in Word (I \times 2_{𝑜}) \land ⟨“ b ”⟩ \in Word (I \times 2_{𝑜})) \to reverse (a ++ ⟨“ b ”⟩) = reverse (⟨“ b ”⟩) ++ reverse (a)$
91	46 89 90	syl2anc	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to reverse (a ++ ⟨“ b ”⟩) = reverse (⟨“ b ”⟩) ++ reverse (a)$
92		revs1	$⊢ reverse (⟨“ b ”⟩) = ⟨“ b ”⟩$
93	92	oveq1i	$⊢ reverse (⟨“ b ”⟩) ++ reverse (a) = ⟨“ b ”⟩ ++ reverse (a)$
94	91 93	eqtrdi	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to reverse (a ++ ⟨“ b ”⟩) = ⟨“ b ”⟩ ++ reverse (a)$
95	94	coeq2d	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to M \circ reverse (a ++ ⟨“ b ”⟩) = M \circ (⟨“ b ”⟩ ++ reverse (a))$
96	49	a1i	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to M : I \times 2_{𝑜} ⟶ I \times 2_{𝑜}$
97		ccatco	$⊢ (⟨“ b ”⟩ \in Word (I \times 2_{𝑜}) \land reverse (a) \in Word (I \times 2_{𝑜}) \land M : I \times 2_{𝑜} ⟶ I \times 2_{𝑜}) \to M \circ (⟨“ b ”⟩ ++ reverse (a)) = (M \circ ⟨“ b ”⟩) ++ (M \circ reverse (a))$
98	89 48 96 97	syl3anc	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to M \circ (⟨“ b ”⟩ ++ reverse (a)) = (M \circ ⟨“ b ”⟩) ++ (M \circ reverse (a))$
99		s1co	$⊢ (b \in (I \times 2_{𝑜}) \land M : I \times 2_{𝑜} ⟶ I \times 2_{𝑜}) \to M \circ ⟨“ b ”⟩ = ⟨“ M (b) ”⟩$
100	71 49 99	sylancl	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to M \circ ⟨“ b ”⟩ = ⟨“ M (b) ”⟩$
101	100	oveq1d	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to (M \circ ⟨“ b ”⟩) ++ (M \circ reverse (a)) = ⟨“ M (b) ”⟩ ++ (M \circ reverse (a))$
102	95 98 101	3eqtrd	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to M \circ reverse (a ++ ⟨“ b ”⟩) = ⟨“ M (b) ”⟩ ++ (M \circ reverse (a))$
103	102	oveq2d	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to (a ++ ⟨“ b ”⟩) ++ (M \circ reverse (a ++ ⟨“ b ”⟩)) = (a ++ ⟨“ b ”⟩) ++ (⟨“ M (b) ”⟩ ++ (M \circ reverse (a)))$
104		ccatcl	$⊢ (a \in Word (I \times 2_{𝑜}) \land ⟨“ b ”⟩ \in Word (I \times 2_{𝑜})) \to a ++ ⟨“ b ”⟩ \in Word (I \times 2_{𝑜})$
105	46 89 104	syl2anc	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to a ++ ⟨“ b ”⟩ \in Word (I \times 2_{𝑜})$
106	76	s1cld	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to ⟨“ M (b) ”⟩ \in Word (I \times 2_{𝑜})$
107		ccatass	$⊢ (a ++ ⟨“ b ”⟩ \in Word (I \times 2_{𝑜}) \land ⟨“ M (b) ”⟩ \in Word (I \times 2_{𝑜}) \land M \circ reverse (a) \in Word (I \times 2_{𝑜})) \to ((a ++ ⟨“ b ”⟩) ++ ⟨“ M (b) ”⟩) ++ (M \circ reverse (a)) = (a ++ ⟨“ b ”⟩) ++ (⟨“ M (b) ”⟩ ++ (M \circ reverse (a)))$
108	105 106 51 107	syl3anc	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to ((a ++ ⟨“ b ”⟩) ++ ⟨“ M (b) ”⟩) ++ (M \circ reverse (a)) = (a ++ ⟨“ b ”⟩) ++ (⟨“ M (b) ”⟩ ++ (M \circ reverse (a)))$
109		ccatass	$⊢ (a \in Word (I \times 2_{𝑜}) \land ⟨“ b ”⟩ \in Word (I \times 2_{𝑜}) \land ⟨“ M (b) ”⟩ \in Word (I \times 2_{𝑜})) \to (a ++ ⟨“ b ”⟩) ++ ⟨“ M (b) ”⟩ = a ++ (⟨“ b ”⟩ ++ ⟨“ M (b) ”⟩)$
110	46 89 106 109	syl3anc	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to (a ++ ⟨“ b ”⟩) ++ ⟨“ M (b) ”⟩ = a ++ (⟨“ b ”⟩ ++ ⟨“ M (b) ”⟩)$
111		df-s2	$⊢ ⟨“ b M (b) ”⟩ = ⟨“ b ”⟩ ++ ⟨“ M (b) ”⟩$
112	111	oveq2i	$⊢ a ++ ⟨“ b M (b) ”⟩ = a ++ (⟨“ b ”⟩ ++ ⟨“ M (b) ”⟩)$
113	110 112	eqtr4di	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to (a ++ ⟨“ b ”⟩) ++ ⟨“ M (b) ”⟩ = a ++ ⟨“ b M (b) ”⟩$
114	113	oveq1d	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to ((a ++ ⟨“ b ”⟩) ++ ⟨“ M (b) ”⟩) ++ (M \circ reverse (a)) = (a ++ ⟨“ b M (b) ”⟩) ++ (M \circ reverse (a))$
115	103 108 114	3eqtr2rd	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to (a ++ ⟨“ b M (b) ”⟩) ++ (M \circ reverse (a)) = (a ++ ⟨“ b ”⟩) ++ (M \circ reverse (a ++ ⟨“ b ”⟩))$
116	73 88 115	3eqtrd	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to \|a\| T (a ++ (M \circ reverse (a))) b = (a ++ ⟨“ b ”⟩) ++ (M \circ reverse (a ++ ⟨“ b ”⟩))$
117	1 2 3 4	efgtf	$⊢ a ++ (M \circ reverse (a)) \in W \to (T (a ++ (M \circ reverse (a))) = (m \in (0 \dots \|a ++ (M \circ reverse (a))\|), u \in (I \times 2_{𝑜}) ⟼ (a ++ (M \circ reverse (a))) splice ⟨m, m, ⟨“ u M (u) ”⟩⟩) \land T (a ++ (M \circ reverse (a))) : (0 \dots \|a ++ (M \circ reverse (a))\|) \times (I \times 2_{𝑜}) ⟶ W)$
118	117	simprd	$⊢ a ++ (M \circ reverse (a)) \in W \to T (a ++ (M \circ reverse (a))) : (0 \dots \|a ++ (M \circ reverse (a))\|) \times (I \times 2_{𝑜}) ⟶ W$
119	55 118	syl	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to T (a ++ (M \circ reverse (a))) : (0 \dots \|a ++ (M \circ reverse (a))\|) \times (I \times 2_{𝑜}) ⟶ W$
120	119	ffnd	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to T (a ++ (M \circ reverse (a))) Fn ((0 \dots \|a ++ (M \circ reverse (a))\|) \times (I \times 2_{𝑜}))$
121		fnovrn	$⊢ (T (a ++ (M \circ reverse (a))) Fn ((0 \dots \|a ++ (M \circ reverse (a))\|) \times (I \times 2_{𝑜})) \land \|a\| \in (0 \dots \|a ++ (M \circ reverse (a))\|) \land b \in (I \times 2_{𝑜})) \to \|a\| T (a ++ (M \circ reverse (a))) b \in ran T (a ++ (M \circ reverse (a)))$
122	120 70 71 121	syl3anc	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to \|a\| T (a ++ (M \circ reverse (a))) b \in ran T (a ++ (M \circ reverse (a)))$
123	116 122	eqeltrrd	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to (a ++ ⟨“ b ”⟩) ++ (M \circ reverse (a ++ ⟨“ b ”⟩)) \in ran T (a ++ (M \circ reverse (a)))$
124	1 2 3 4	efgi2	$⊢ (a ++ (M \circ reverse (a)) \in W \land (a ++ ⟨“ b ”⟩) ++ (M \circ reverse (a ++ ⟨“ b ”⟩)) \in ran T (a ++ (M \circ reverse (a)))) \to (a ++ (M \circ reverse (a))) \underset{˙}{\sim} ((a ++ ⟨“ b ”⟩) ++ (M \circ reverse (a ++ ⟨“ b ”⟩)))$
125	55 123 124	syl2anc	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to (a ++ (M \circ reverse (a))) \underset{˙}{\sim} ((a ++ ⟨“ b ”⟩) ++ (M \circ reverse (a ++ ⟨“ b ”⟩)))$
126	45 125	ersym	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to ((a ++ ⟨“ b ”⟩) ++ (M \circ reverse (a ++ ⟨“ b ”⟩))) \underset{˙}{\sim} (a ++ (M \circ reverse (a)))$
127	45	ertr	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to ((((a ++ ⟨“ b ”⟩) ++ (M \circ reverse (a ++ ⟨“ b ”⟩))) \underset{˙}{\sim} (a ++ (M \circ reverse (a))) \land (a ++ (M \circ reverse (a))) \underset{˙}{\sim} \emptyset) \to ((a ++ ⟨“ b ”⟩) ++ (M \circ reverse (a ++ ⟨“ b ”⟩))) \underset{˙}{\sim} \emptyset)$
128	126 127	mpand	$⊢ (A \in W \land (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜}))) \to ((a ++ (M \circ reverse (a))) \underset{˙}{\sim} \emptyset \to ((a ++ ⟨“ b ”⟩) ++ (M \circ reverse (a ++ ⟨“ b ”⟩))) \underset{˙}{\sim} \emptyset)$
129	128	expcom	$⊢ (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜})) \to (A \in W \to ((a ++ (M \circ reverse (a))) \underset{˙}{\sim} \emptyset \to ((a ++ ⟨“ b ”⟩) ++ (M \circ reverse (a ++ ⟨“ b ”⟩))) \underset{˙}{\sim} \emptyset))$
130	129	a2d	$⊢ (a \in Word (I \times 2_{𝑜}) \land b \in (I \times 2_{𝑜})) \to ((A \in W \to (a ++ (M \circ reverse (a))) \underset{˙}{\sim} \emptyset) \to (A \in W \to ((a ++ ⟨“ b ”⟩) ++ (M \circ reverse (a ++ ⟨“ b ”⟩))) \underset{˙}{\sim} \emptyset))$
131	17 23 29 35 44 130	wrdind	$⊢ A \in Word (I \times 2_{𝑜}) \to (A \in W \to (A ++ (M \circ reverse (A))) \underset{˙}{\sim} \emptyset)$
132	7 131	mpcom	$⊢ A \in W \to (A ++ (M \circ reverse (A))) \underset{˙}{\sim} \emptyset$

Metamath Proof Explorer

Theorem efginvrel2

Proof