efginvrel2 - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > efginvrel2		Structured version Unicode version

Theorem efginvrel2 16215

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.)

**Hypotheses**
Ref	Expression
efgval.w	Word
efgval.r	~_FG
efgval2.m	$\$
efgval2.t	splice

**Assertion**
Ref	Expression
efginvrel2	concat reverse

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

Proof of Theorem efginvrel2 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		efgval.w	. . . 4 Word
2		fviss 5744	. . . 4 Word Word
3	1, 2	eqsstri 3381	. . 3 Word
4	3	sseli 3347	. 2 Word
5		id 22	. . . . . 6
6		fveq2 5686	. . . . . . . . 9 reverse reverse
7		rev0 12396	. . . . . . . . 9 reverse
8	6, 7	syl6eq 2486	. . . . . . . 8 reverse
9	8	coeq2d 4997	. . . . . . 7 reverse
10		co02 5346	. . . . . . 7
11	9, 10	syl6eq 2486	. . . . . 6 reverse
12	5, 11	oveq12d 6104	. . . . 5 concat reverse concat
13	12	breq1d 4297	. . . 4 concat reverse concat
14	13	imbi2d 316	. . 3 concat reverse concat
15		id 22	. . . . . 6
16		fveq2 5686	. . . . . . 7 reverse reverse
17	16	coeq2d 4997	. . . . . 6 reverse reverse
18	15, 17	oveq12d 6104	. . . . 5 concat reverse concat reverse
19	18	breq1d 4297	. . . 4 concat reverse concat reverse
20	19	imbi2d 316	. . 3 concat reverse concat reverse
21		id 22	. . . . . 6 concat concat
22		fveq2 5686	. . . . . . 7 concat reverse reverse concat
23	22	coeq2d 4997	. . . . . 6 concat reverse reverse concat
24	21, 23	oveq12d 6104	. . . . 5 concat concat reverse concat concat reverse concat
25	24	breq1d 4297	. . . 4 concat concat reverse concat concat reverse concat
26	25	imbi2d 316	. . 3 concat concat reverse concat concat reverse concat
27		id 22	. . . . . 6
28		fveq2 5686	. . . . . . 7 reverse reverse
29	28	coeq2d 4997	. . . . . 6 reverse reverse
30	27, 29	oveq12d 6104	. . . . 5 concat reverse concat reverse
31	30	breq1d 4297	. . . 4 concat reverse concat reverse
32	31	imbi2d 316	. . 3 concat reverse concat reverse
33		wrd0 12244	. . . . 5 Word
34		ccatlid 12276	. . . . 5 Word concat
35	33, 34	ax-mp 5	. . . 4 concat
36		efgval.r	. . . . . . 7 ~_FG
37	1, 36	efger 16206	. . . . . 6
38	37	a1i 11	. . . . 5
39	1	efgrcl 16203	. . . . . . 7 $/\$ Word
40	39	simprd 463	. . . . . 6 Word
41	33, 40	syl5eleqr 2525	. . . . 5
42	38, 41	erref 7113	. . . 4
43	35, 42	syl5eqbr 4320	. . 3 concat
44	37	a1i 11	. . . . . . 7 $/\$ Word $/\$
45		simprl 755	. . . . . . . . . 10 $/\$ Word $/\$ Word
46		revcl 12393	. . . . . . . . . . . 12 Word reverse Word
47	46	ad2antrl 727	. . . . . . . . . . 11 $/\$ Word $/\$ reverse Word
48		efgval2.m	. . . . . . . . . . . 12 $\$
49	48	efgmf 16201	. . . . . . . . . . 11
50		wrdco 12451	. . . . . . . . . . 11 reverse Word $/\$ reverse Word
51	47, 49, 50	sylancl 662	. . . . . . . . . 10 $/\$ Word $/\$ reverse Word
52		ccatcl 12266	. . . . . . . . . 10 Word $/\$ reverse Word concat reverse Word
53	45, 51, 52	syl2anc 661	. . . . . . . . 9 $/\$ Word $/\$ concat reverse Word
54	40	adantr 465	. . . . . . . . 9 $/\$ Word $/\$ Word
55	53, 54	eleqtrrd 2515	. . . . . . . 8 $/\$ Word $/\$ concat reverse
56		lencl 12241	. . . . . . . . . . . . . 14 Word
57	56	ad2antrl 727	. . . . . . . . . . . . 13 $/\$ Word $/\$
58		nn0uz 10887	. . . . . . . . . . . . 13
59	57, 58	syl6eleq 2528	. . . . . . . . . . . 12 $/\$ Word $/\$
60		ccatlen 12267	. . . . . . . . . . . . . 14 Word $/\$ reverse Word concat reverse reverse
61	45, 51, 60	syl2anc 661	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat reverse reverse
62	57	nn0zd 10737	. . . . . . . . . . . . . . 15 $/\$ Word $/\$
63		uzid 10867	. . . . . . . . . . . . . . 15
64	62, 63	syl 16	. . . . . . . . . . . . . 14 $/\$ Word $/\$
65		lencl 12241	. . . . . . . . . . . . . . 15 reverse Word reverse
66	51, 65	syl 16	. . . . . . . . . . . . . 14 $/\$ Word $/\$ reverse
67		uzaddcl 10903	. . . . . . . . . . . . . 14 $/\$ reverse reverse
68	64, 66, 67	syl2anc 661	. . . . . . . . . . . . 13 $/\$ Word $/\$ reverse
69	61, 68	eqeltrd 2512	. . . . . . . . . . . 12 $/\$ Word $/\$ concat reverse
70		elfzuzb 11439	. . . . . . . . . . . 12 concat reverse $/\$ concat reverse
71	59, 69, 70	sylanbrc 664	. . . . . . . . . . 11 $/\$ Word $/\$ concat reverse
72		simprr 756	. . . . . . . . . . 11 $/\$ Word $/\$
73		efgval2.t	. . . . . . . . . . . 12 splice
74	1, 36, 48, 73	efgtval 16211	. . . . . . . . . . 11 concat reverse $/\$ concat reverse $/\$ concat reverse concat reverse splice
75	55, 71, 72, 74	syl3anc 1218	. . . . . . . . . 10 $/\$ Word $/\$ concat reverse concat reverse splice
76	33	a1i 11	. . . . . . . . . . 11 $/\$ Word $/\$ Word
77	49	ffvelrni 5837	. . . . . . . . . . . . 13
78	72, 77	syl 16	. . . . . . . . . . . 12 $/\$ Word $/\$
79	72, 78	s2cld 12488	. . . . . . . . . . 11 $/\$ Word $/\$ Word
80		ccatrid 12277	. . . . . . . . . . . . . 14 Word concat
81	80	ad2antrl 727	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat
82	81	eqcomd 2443	. . . . . . . . . . . 12 $/\$ Word $/\$ concat
83	82	oveq1d 6101	. . . . . . . . . . 11 $/\$ Word $/\$ concat reverse concat concat reverse
84		eqidd 2439	. . . . . . . . . . 11 $/\$ Word $/\$
85		hash0 12127	. . . . . . . . . . . . 13
86	85	oveq2i 6097	. . . . . . . . . . . 12
87	57	nn0cnd 10630	. . . . . . . . . . . . 13 $/\$ Word $/\$
88	87	addid1d 9561	. . . . . . . . . . . 12 $/\$ Word $/\$
89	86, 88	syl5req 2483	. . . . . . . . . . 11 $/\$ Word $/\$
90	45, 76, 51, 79, 83, 84, 89	splval2 12391	. . . . . . . . . 10 $/\$ Word $/\$ concat reverse splice concat concat reverse
91	72	s1cld 12286	. . . . . . . . . . . . . . . 16 $/\$ Word $/\$ Word
92		revccat 12398	. . . . . . . . . . . . . . . 16 Word $/\$ Word reverse concat reverse concat reverse
93	45, 91, 92	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ Word $/\$ reverse concat reverse concat reverse
94		revs1 12397	. . . . . . . . . . . . . . . 16 reverse
95	94	oveq1i 6096	. . . . . . . . . . . . . . 15 reverse concat reverse concat reverse
96	93, 95	syl6eq 2486	. . . . . . . . . . . . . 14 $/\$ Word $/\$ reverse concat concat reverse
97	96	coeq2d 4997	. . . . . . . . . . . . 13 $/\$ Word $/\$ reverse concat concat reverse
98	49	a1i 11	. . . . . . . . . . . . . 14 $/\$ Word $/\$
99		ccatco 12455	. . . . . . . . . . . . . 14 Word $/\$ reverse Word $/\$ concat reverse concat reverse
100	91, 47, 98, 99	syl3anc 1218	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat reverse concat reverse
101		s1co 12453	. . . . . . . . . . . . . . 15 $/\$
102	72, 49, 101	sylancl 662	. . . . . . . . . . . . . 14 $/\$ Word $/\$
103	102	oveq1d 6101	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat reverse concat reverse
104	97, 100, 103	3eqtrd 2474	. . . . . . . . . . . 12 $/\$ Word $/\$ reverse concat concat reverse
105	104	oveq2d 6102	. . . . . . . . . . 11 $/\$ Word $/\$ concat concat reverse concat concat concat concat reverse
106		ccatcl 12266	. . . . . . . . . . . . 13 Word $/\$ Word concat Word
107	45, 91, 106	syl2anc 661	. . . . . . . . . . . 12 $/\$ Word $/\$ concat Word
108	78	s1cld 12286	. . . . . . . . . . . 12 $/\$ Word $/\$ Word
109		ccatass 12278	. . . . . . . . . . . 12 concat Word $/\$ Word $/\$ reverse Word concat concat concat reverse concat concat concat reverse
110	107, 108, 51, 109	syl3anc 1218	. . . . . . . . . . 11 $/\$ Word $/\$ concat concat concat reverse concat concat concat reverse
111		ccatass 12278	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ Word concat concat concat concat
112	45, 91, 108, 111	syl3anc 1218	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat concat concat concat
113		df-s2 12467	. . . . . . . . . . . . . 14 concat
114	113	oveq2i 6097	. . . . . . . . . . . . 13 concat concat concat
115	112, 114	syl6eqr 2488	. . . . . . . . . . . 12 $/\$ Word $/\$ concat concat concat
116	115	oveq1d 6101	. . . . . . . . . . 11 $/\$ Word $/\$ concat concat concat reverse concat concat reverse
117	105, 110, 116	3eqtr2rd 2477	. . . . . . . . . 10 $/\$ Word $/\$ concat concat reverse concat concat reverse concat
118	75, 90, 117	3eqtrd 2474	. . . . . . . . 9 $/\$ Word $/\$ concat reverse concat concat reverse concat
119	1, 36, 48, 73	efgtf 16210	. . . . . . . . . . . 12 concat reverse concat reverse concat reverse concat reverse splice $/\$ concat reverse concat reverse
120	119	simprd 463	. . . . . . . . . . 11 concat reverse concat reverse concat reverse
121		ffn 5554	. . . . . . . . . . 11 concat reverse concat reverse concat reverse concat reverse
122	55, 120, 121	3syl 20	. . . . . . . . . 10 $/\$ Word $/\$ concat reverse concat reverse
123		fnovrn 6233	. . . . . . . . . 10 concat reverse concat reverse $/\$ concat reverse $/\$ concat reverse concat reverse
124	122, 71, 72, 123	syl3anc 1218	. . . . . . . . 9 $/\$ Word $/\$ concat reverse concat reverse
125	118, 124	eqeltrrd 2513	. . . . . . . 8 $/\$ Word $/\$ concat concat reverse concat concat reverse
126	1, 36, 48, 73	efgi2 16213	. . . . . . . 8 concat reverse $/\$ concat concat reverse concat concat reverse concat reverse concat concat reverse concat
127	55, 125, 126	syl2anc 661	. . . . . . 7 $/\$ Word $/\$ concat reverse concat concat reverse concat
128	44, 127	ersym 7105	. . . . . 6 $/\$ Word $/\$ concat concat reverse concat concat reverse
129	44	ertr 7108	. . . . . 6 $/\$ Word $/\$ concat concat reverse concat concat reverse $/\$ concat reverse concat concat reverse concat
130	128, 129	mpand 675	. . . . 5 $/\$ Word $/\$ concat reverse concat concat reverse concat
131	130	expcom 435	. . . 4 Word $/\$ concat reverse concat concat reverse concat
132	131	a2d 26	. . 3 Word $/\$ concat reverse concat concat reverse concat
133	14, 20, 26, 32, 43, 132	wrdind 12363	. 2 Word concat reverse
134	4, 133	mpcom 36	1 concat reverse

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 369

wceq 1369

wcel 1756

cvv 2967 $\$ cdif 3320

c0 3632

cop 3878

cotp 3880 class class class wbr 4287

cmpt 4345

cid 4626

cxp 4833

crn 4836

ccom 4839

wfn 5408

wf 5409

cfv 5413 (class class class)co 6086

cmpt2 6088

c1o 6905

c2o 6906

wer 7090

cc0 9274

caddc 9277

cn0 10571

cz 10638

cuz 10853

cfz 11429

chash 12095 Word cword 12213 concat cconcat 12215

cs1 12216 splice csplice 12218 reversecreverse 12219

cs2 12460 ~_FG cefg 16194

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367 ax-cnex 9330 ax-resscn 9331 ax-1cn 9332 ax-icn 9333 ax-addcl 9334 ax-addrcl 9335 ax-mulcl 9336 ax-mulrcl 9337 ax-mulcom 9338 ax-addass 9339 ax-mulass 9340 ax-distr 9341 ax-i2m1 9342 ax-1ne0 9343 ax-1rid 9344 ax-rnegex 9345 ax-rrecex 9346 ax-cnre 9347 ax-pre-lttri 9348 ax-pre-lttrn 9349 ax-pre-ltadd 9350 ax-pre-mulgt0 9351

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2715 df-rex 2716 df-reu 2717 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-pss 3339 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-tp 3877 df-op 3879 df-ot 3881 df-uni 4087 df-int 4124 df-iun 4168 df-iin 4169 df-br 4288 df-opab 4346 df-mpt 4347 df-tr 4381 df-eprel 4627 df-id 4631 df-po 4636 df-so 4637 df-fr 4674 df-we 4676 df-ord 4717 df-on 4718 df-lim 4719 df-suc 4720 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-riota 6047 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-om 6472 df-1st 6572 df-2nd 6573 df-recs 6824 df-rdg 6858 df-1o 6912 df-2o 6913 df-oadd 6916 df-er 7093 df-ec 7095 df-map 7208 df-pm 7209 df-en 7303 df-dom 7304 df-sdom 7305 df-fin 7306 df-card 8101 df-pnf 9412 df-mnf 9413 df-xr 9414 df-ltxr 9415 df-le 9416 df-sub 9589 df-neg 9590 df-nn 10315 df-n0 10572 df-z 10639 df-uz 10854 df-fz 11430 df-fzo 11541 df-hash 12096 df-word 12221 df-concat 12223 df-s1 12224 df-substr 12225 df-splice 12226 df-reverse 12227 df-s2 12467 df-efg 16197

This theorem is referenced by: efginvrel1 16216 frgpinv 16252

W3C validator