efginvrel2 - Metamath Proof Explorer

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

Theorem efginvrel2 16344

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 5857	. . . 4 Word Word
3	1, 2	eqsstri 3493	. . 3 Word
4	3	sseli 3459	. 2 Word
5		id 22	. . . . . 6
6		fveq2 5798	. . . . . . . . 9 reverse reverse
7		rev0 12521	. . . . . . . . 9 reverse
8	6, 7	syl6eq 2511	. . . . . . . 8 reverse
9	8	coeq2d 5109	. . . . . . 7 reverse
10		co02 5458	. . . . . . 7
11	9, 10	syl6eq 2511	. . . . . 6 reverse
12	5, 11	oveq12d 6217	. . . . 5 concat reverse concat
13	12	breq1d 4409	. . . 4 concat reverse concat
14	13	imbi2d 316	. . 3 concat reverse concat
15		id 22	. . . . . 6
16		fveq2 5798	. . . . . . 7 reverse reverse
17	16	coeq2d 5109	. . . . . 6 reverse reverse
18	15, 17	oveq12d 6217	. . . . 5 concat reverse concat reverse
19	18	breq1d 4409	. . . 4 concat reverse concat reverse
20	19	imbi2d 316	. . 3 concat reverse concat reverse
21		id 22	. . . . . 6 concat concat
22		fveq2 5798	. . . . . . 7 concat reverse reverse concat
23	22	coeq2d 5109	. . . . . 6 concat reverse reverse concat
24	21, 23	oveq12d 6217	. . . . 5 concat concat reverse concat concat reverse concat
25	24	breq1d 4409	. . . 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 5798	. . . . . . 7 reverse reverse
29	28	coeq2d 5109	. . . . . 6 reverse reverse
30	27, 29	oveq12d 6217	. . . . 5 concat reverse concat reverse
31	30	breq1d 4409	. . . 4 concat reverse concat reverse
32	31	imbi2d 316	. . 3 concat reverse concat reverse
33		wrd0 12369	. . . . 5 Word
34		ccatlid 12401	. . . . 5 Word concat
35	33, 34	ax-mp 5	. . . 4 concat
36		efgval.r	. . . . . . 7 ~_FG
37	1, 36	efger 16335	. . . . . 6
38	37	a1i 11	. . . . 5
39	1	efgrcl 16332	. . . . . . 7 $/\$ Word
40	39	simprd 463	. . . . . 6 Word
41	33, 40	syl5eleqr 2549	. . . . 5
42	38, 41	erref 7230	. . . 4
43	35, 42	syl5eqbr 4432	. . 3 concat
44	37	a1i 11	. . . . . . 7 $/\$ Word $/\$
45		simprl 755	. . . . . . . . . 10 $/\$ Word $/\$ Word
46		revcl 12518	. . . . . . . . . . . 12 Word reverse Word
47	46	ad2antrl 727	. . . . . . . . . . 11 $/\$ Word $/\$ reverse Word
48		efgval2.m	. . . . . . . . . . . 12 $\$
49	48	efgmf 16330	. . . . . . . . . . 11
50		wrdco 12576	. . . . . . . . . . 11 reverse Word $/\$ reverse Word
51	47, 49, 50	sylancl 662	. . . . . . . . . 10 $/\$ Word $/\$ reverse Word
52		ccatcl 12391	. . . . . . . . . 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 2545	. . . . . . . 8 $/\$ Word $/\$ concat reverse
56		lencl 12366	. . . . . . . . . . . . . 14 Word
57	56	ad2antrl 727	. . . . . . . . . . . . 13 $/\$ Word $/\$
58		nn0uz 11005	. . . . . . . . . . . . 13
59	57, 58	syl6eleq 2552	. . . . . . . . . . . 12 $/\$ Word $/\$
60		ccatlen 12392	. . . . . . . . . . . . . 14 Word $/\$ reverse Word concat reverse reverse
61	45, 51, 60	syl2anc 661	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat reverse reverse
62	57	nn0zd 10855	. . . . . . . . . . . . . . 15 $/\$ Word $/\$
63		uzid 10985	. . . . . . . . . . . . . . 15
64	62, 63	syl 16	. . . . . . . . . . . . . 14 $/\$ Word $/\$
65		lencl 12366	. . . . . . . . . . . . . . 15 reverse Word reverse
66	51, 65	syl 16	. . . . . . . . . . . . . 14 $/\$ Word $/\$ reverse
67		uzaddcl 11021	. . . . . . . . . . . . . 14 $/\$ reverse reverse
68	64, 66, 67	syl2anc 661	. . . . . . . . . . . . 13 $/\$ Word $/\$ reverse
69	61, 68	eqeltrd 2542	. . . . . . . . . . . 12 $/\$ Word $/\$ concat reverse
70		elfzuzb 11563	. . . . . . . . . . . 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 16340	. . . . . . . . . . 11 concat reverse $/\$ concat reverse $/\$ concat reverse concat reverse splice
75	55, 71, 72, 74	syl3anc 1219	. . . . . . . . . 10 $/\$ Word $/\$ concat reverse concat reverse splice
76	33	a1i 11	. . . . . . . . . . 11 $/\$ Word $/\$ Word
77	49	ffvelrni 5950	. . . . . . . . . . . . 13
78	72, 77	syl 16	. . . . . . . . . . . 12 $/\$ Word $/\$
79	72, 78	s2cld 12613	. . . . . . . . . . 11 $/\$ Word $/\$ Word
80		ccatrid 12402	. . . . . . . . . . . . . 14 Word concat
81	80	ad2antrl 727	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat
82	81	eqcomd 2462	. . . . . . . . . . . 12 $/\$ Word $/\$ concat
83	82	oveq1d 6214	. . . . . . . . . . 11 $/\$ Word $/\$ concat reverse concat concat reverse
84		eqidd 2455	. . . . . . . . . . 11 $/\$ Word $/\$
85		hash0 12251	. . . . . . . . . . . . 13
86	85	oveq2i 6210	. . . . . . . . . . . 12
87	57	nn0cnd 10748	. . . . . . . . . . . . 13 $/\$ Word $/\$
88	87	addid1d 9679	. . . . . . . . . . . 12 $/\$ Word $/\$
89	86, 88	syl5req 2508	. . . . . . . . . . 11 $/\$ Word $/\$
90	45, 76, 51, 79, 83, 84, 89	splval2 12516	. . . . . . . . . 10 $/\$ Word $/\$ concat reverse splice concat concat reverse
91	72	s1cld 12411	. . . . . . . . . . . . . . . 16 $/\$ Word $/\$ Word
92		revccat 12523	. . . . . . . . . . . . . . . 16 Word $/\$ Word reverse concat reverse concat reverse
93	45, 91, 92	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ Word $/\$ reverse concat reverse concat reverse
94		revs1 12522	. . . . . . . . . . . . . . . 16 reverse
95	94	oveq1i 6209	. . . . . . . . . . . . . . 15 reverse concat reverse concat reverse
96	93, 95	syl6eq 2511	. . . . . . . . . . . . . 14 $/\$ Word $/\$ reverse concat concat reverse
97	96	coeq2d 5109	. . . . . . . . . . . . 13 $/\$ Word $/\$ reverse concat concat reverse
98	49	a1i 11	. . . . . . . . . . . . . 14 $/\$ Word $/\$
99		ccatco 12580	. . . . . . . . . . . . . 14 Word $/\$ reverse Word $/\$ concat reverse concat reverse
100	91, 47, 98, 99	syl3anc 1219	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat reverse concat reverse
101		s1co 12578	. . . . . . . . . . . . . . 15 $/\$
102	72, 49, 101	sylancl 662	. . . . . . . . . . . . . 14 $/\$ Word $/\$
103	102	oveq1d 6214	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat reverse concat reverse
104	97, 100, 103	3eqtrd 2499	. . . . . . . . . . . 12 $/\$ Word $/\$ reverse concat concat reverse
105	104	oveq2d 6215	. . . . . . . . . . 11 $/\$ Word $/\$ concat concat reverse concat concat concat concat reverse
106		ccatcl 12391	. . . . . . . . . . . . 13 Word $/\$ Word concat Word
107	45, 91, 106	syl2anc 661	. . . . . . . . . . . 12 $/\$ Word $/\$ concat Word
108	78	s1cld 12411	. . . . . . . . . . . 12 $/\$ Word $/\$ Word
109		ccatass 12403	. . . . . . . . . . . 12 concat Word $/\$ Word $/\$ reverse Word concat concat concat reverse concat concat concat reverse
110	107, 108, 51, 109	syl3anc 1219	. . . . . . . . . . 11 $/\$ Word $/\$ concat concat concat reverse concat concat concat reverse
111		ccatass 12403	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ Word concat concat concat concat
112	45, 91, 108, 111	syl3anc 1219	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat concat concat concat
113		df-s2 12592	. . . . . . . . . . . . . 14 concat
114	113	oveq2i 6210	. . . . . . . . . . . . 13 concat concat concat
115	112, 114	syl6eqr 2513	. . . . . . . . . . . 12 $/\$ Word $/\$ concat concat concat
116	115	oveq1d 6214	. . . . . . . . . . 11 $/\$ Word $/\$ concat concat concat reverse concat concat reverse
117	105, 110, 116	3eqtr2rd 2502	. . . . . . . . . 10 $/\$ Word $/\$ concat concat reverse concat concat reverse concat
118	75, 90, 117	3eqtrd 2499	. . . . . . . . 9 $/\$ Word $/\$ concat reverse concat concat reverse concat
119	1, 36, 48, 73	efgtf 16339	. . . . . . . . . . . 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 5666	. . . . . . . . . . 11 concat reverse concat reverse concat reverse concat reverse
122	55, 120, 121	3syl 20	. . . . . . . . . 10 $/\$ Word $/\$ concat reverse concat reverse
123		fnovrn 6347	. . . . . . . . . 10 concat reverse concat reverse $/\$ concat reverse $/\$ concat reverse concat reverse
124	122, 71, 72, 123	syl3anc 1219	. . . . . . . . 9 $/\$ Word $/\$ concat reverse concat reverse
125	118, 124	eqeltrrd 2543	. . . . . . . 8 $/\$ Word $/\$ concat concat reverse concat concat reverse
126	1, 36, 48, 73	efgi2 16342	. . . . . . . 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 7222	. . . . . 6 $/\$ Word $/\$ concat concat reverse concat concat reverse
129	44	ertr 7225	. . . . . 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 12488	. 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 1370

wcel 1758

cvv 3076 $\$ cdif 3432

c0 3744

cop 3990

cotp 3992 class class class wbr 4399

cmpt 4457

cid 4738

cxp 4945

crn 4948

ccom 4951

wfn 5520

wf 5521

cfv 5525 (class class class)co 6199

cmpt2 6201

c1o 7022

c2o 7023

wer 7207

cc0 9392

caddc 9395

cn0 10689

cz 10756

cuz 10971

cfz 11553

chash 12219 Word cword 12338 concat cconcat 12340

cs1 12341 splice csplice 12343 reversecreverse 12344

cs2 12585 ~_FG cefg 16323

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-rep 4510 ax-sep 4520 ax-nul 4528 ax-pow 4577 ax-pr 4638 ax-un 6481 ax-cnex 9448 ax-resscn 9449 ax-1cn 9450 ax-icn 9451 ax-addcl 9452 ax-addrcl 9453 ax-mulcl 9454 ax-mulrcl 9455 ax-mulcom 9456 ax-addass 9457 ax-mulass 9458 ax-distr 9459 ax-i2m1 9460 ax-1ne0 9461 ax-1rid 9462 ax-rnegex 9463 ax-rrecex 9464 ax-cnre 9465 ax-pre-lttri 9466 ax-pre-lttrn 9467 ax-pre-ltadd 9468 ax-pre-mulgt0 9469

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2649 df-nel 2650 df-ral 2803 df-rex 2804 df-reu 2805 df-rab 2807 df-v 3078 df-sbc 3293 df-csb 3395 df-dif 3438 df-un 3440 df-in 3442 df-ss 3449 df-pss 3451 df-nul 3745 df-if 3899 df-pw 3969 df-sn 3985 df-pr 3987 df-tp 3989 df-op 3991 df-ot 3993 df-uni 4199 df-int 4236 df-iun 4280 df-iin 4281 df-br 4400 df-opab 4458 df-mpt 4459 df-tr 4493 df-eprel 4739 df-id 4743 df-po 4748 df-so 4749 df-fr 4786 df-we 4788 df-ord 4829 df-on 4830 df-lim 4831 df-suc 4832 df-xp 4953 df-rel 4954 df-cnv 4955 df-co 4956 df-dm 4957 df-rn 4958 df-res 4959 df-ima 4960 df-iota 5488 df-fun 5527 df-fn 5528 df-f 5529 df-f1 5530 df-fo 5531 df-f1o 5532 df-fv 5533 df-riota 6160 df-ov 6202 df-oprab 6203 df-mpt2 6204 df-om 6586 df-1st 6686 df-2nd 6687 df-recs 6941 df-rdg 6975 df-1o 7029 df-2o 7030 df-oadd 7033 df-er 7210 df-ec 7212 df-map 7325 df-pm 7326 df-en 7420 df-dom 7421 df-sdom 7422 df-fin 7423 df-card 8219 df-pnf 9530 df-mnf 9531 df-xr 9532 df-ltxr 9533 df-le 9534 df-sub 9707 df-neg 9708 df-nn 10433 df-n0 10690 df-z 10757 df-uz 10972 df-fz 11554 df-fzo 11665 df-hash 12220 df-word 12346 df-concat 12348 df-s1 12349 df-substr 12350 df-splice 12351 df-reverse 12352 df-s2 12592 df-efg 16326

This theorem is referenced by: efginvrel1 16345 frgpinv 16381

W3C validator