efginvrel2 - Metamath Proof Explorer

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

Theorem efginvrel2 15314

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 5743	. . . 4 Word Word
3	1, 2	eqsstri 3338	. . 3 Word
4	3	sseli 3304	. 2 Word
5		id 20	. . . . . 6
6		fveq2 5687	. . . . . . . . 9 reverse reverse
7		rev0 11751	. . . . . . . . 9 reverse
8	6, 7	syl6eq 2452	. . . . . . . 8 reverse
9	8	coeq2d 4994	. . . . . . 7 reverse
10		co02 5342	. . . . . . 7
11	9, 10	syl6eq 2452	. . . . . 6 reverse
12	5, 11	oveq12d 6058	. . . . 5 concat reverse concat
13	12	breq1d 4182	. . . 4 concat reverse concat
14	13	imbi2d 308	. . 3 concat reverse concat
15		id 20	. . . . . 6
16		fveq2 5687	. . . . . . 7 reverse reverse
17	16	coeq2d 4994	. . . . . 6 reverse reverse
18	15, 17	oveq12d 6058	. . . . 5 concat reverse concat reverse
19	18	breq1d 4182	. . . 4 concat reverse concat reverse
20	19	imbi2d 308	. . 3 concat reverse concat reverse
21		id 20	. . . . . 6 concat concat
22		fveq2 5687	. . . . . . 7 concat reverse reverse concat
23	22	coeq2d 4994	. . . . . 6 concat reverse reverse concat
24	21, 23	oveq12d 6058	. . . . 5 concat concat reverse concat concat reverse concat
25	24	breq1d 4182	. . . 4 concat concat reverse concat concat reverse concat
26	25	imbi2d 308	. . 3 concat concat reverse concat concat reverse concat
27		id 20	. . . . . 6
28		fveq2 5687	. . . . . . 7 reverse reverse
29	28	coeq2d 4994	. . . . . 6 reverse reverse
30	27, 29	oveq12d 6058	. . . . 5 concat reverse concat reverse
31	30	breq1d 4182	. . . 4 concat reverse concat reverse
32	31	imbi2d 308	. . 3 concat reverse concat reverse
33		wrd0 11687	. . . . 5 Word
34		ccatlid 11703	. . . . 5 Word concat
35	33, 34	ax-mp 8	. . . 4 concat
36		efgval.r	. . . . . . 7 ~_FG
37	1, 36	efger 15305	. . . . . 6
38	37	a1i 11	. . . . 5
39	1	efgrcl 15302	. . . . . . 7 $/\$ Word
40	39	simprd 450	. . . . . 6 Word
41	33, 40	syl5eleqr 2491	. . . . 5
42	38, 41	erref 6884	. . . 4
43	35, 42	syl5eqbr 4205	. . 3 concat
44	37	a1i 11	. . . . . . 7 $/\$ Word $/\$
45		simprl 733	. . . . . . . . . 10 $/\$ Word $/\$ Word
46		revcl 11748	. . . . . . . . . . . 12 Word reverse Word
47	46	ad2antrl 709	. . . . . . . . . . 11 $/\$ Word $/\$ reverse Word
48		efgval2.m	. . . . . . . . . . . 12 $\$
49	48	efgmf 15300	. . . . . . . . . . 11
50		wrdco 11755	. . . . . . . . . . 11 reverse Word $/\$ reverse Word
51	47, 49, 50	sylancl 644	. . . . . . . . . 10 $/\$ Word $/\$ reverse Word
52		ccatcl 11698	. . . . . . . . . 10 Word $/\$ reverse Word concat reverse Word
53	45, 51, 52	syl2anc 643	. . . . . . . . 9 $/\$ Word $/\$ concat reverse Word
54	40	adantr 452	. . . . . . . . 9 $/\$ Word $/\$ Word
55	53, 54	eleqtrrd 2481	. . . . . . . 8 $/\$ Word $/\$ concat reverse
56		lencl 11690	. . . . . . . . . . . . . 14 Word
57	56	ad2antrl 709	. . . . . . . . . . . . 13 $/\$ Word $/\$
58		nn0uz 10476	. . . . . . . . . . . . 13
59	57, 58	syl6eleq 2494	. . . . . . . . . . . 12 $/\$ Word $/\$
60		ccatlen 11699	. . . . . . . . . . . . . 14 Word $/\$ reverse Word concat reverse reverse
61	45, 51, 60	syl2anc 643	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat reverse reverse
62	57	nn0zd 10329	. . . . . . . . . . . . . . 15 $/\$ Word $/\$
63		uzid 10456	. . . . . . . . . . . . . . 15
64	62, 63	syl 16	. . . . . . . . . . . . . 14 $/\$ Word $/\$
65		lencl 11690	. . . . . . . . . . . . . . 15 reverse Word reverse
66	51, 65	syl 16	. . . . . . . . . . . . . 14 $/\$ Word $/\$ reverse
67		uzaddcl 10489	. . . . . . . . . . . . . 14 $/\$ reverse reverse
68	64, 66, 67	syl2anc 643	. . . . . . . . . . . . 13 $/\$ Word $/\$ reverse
69	61, 68	eqeltrd 2478	. . . . . . . . . . . 12 $/\$ Word $/\$ concat reverse
70		elfzuzb 11009	. . . . . . . . . . . 12 concat reverse $/\$ concat reverse
71	59, 69, 70	sylanbrc 646	. . . . . . . . . . 11 $/\$ Word $/\$ concat reverse
72		simprr 734	. . . . . . . . . . 11 $/\$ Word $/\$
73		efgval2.t	. . . . . . . . . . . 12 splice
74	1, 36, 48, 73	efgtval 15310	. . . . . . . . . . 11 concat reverse $/\$ concat reverse $/\$ concat reverse concat reverse splice
75	55, 71, 72, 74	syl3anc 1184	. . . . . . . . . 10 $/\$ Word $/\$ concat reverse concat reverse splice
76	33	a1i 11	. . . . . . . . . . 11 $/\$ Word $/\$ Word
77	49	ffvelrni 5828	. . . . . . . . . . . . 13
78	72, 77	syl 16	. . . . . . . . . . . 12 $/\$ Word $/\$
79	72, 78	s2cld 11788	. . . . . . . . . . 11 $/\$ Word $/\$ Word
80		ccatrid 11704	. . . . . . . . . . . . . 14 Word concat
81	80	ad2antrl 709	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat
82	81	eqcomd 2409	. . . . . . . . . . . 12 $/\$ Word $/\$ concat
83	82	oveq1d 6055	. . . . . . . . . . 11 $/\$ Word $/\$ concat reverse concat concat reverse
84		eqidd 2405	. . . . . . . . . . 11 $/\$ Word $/\$
85		hash0 11601	. . . . . . . . . . . . 13
86	85	oveq2i 6051	. . . . . . . . . . . 12
87	57	nn0cnd 10232	. . . . . . . . . . . . 13 $/\$ Word $/\$
88	87	addid1d 9222	. . . . . . . . . . . 12 $/\$ Word $/\$
89	86, 88	syl5req 2449	. . . . . . . . . . 11 $/\$ Word $/\$
90	45, 76, 51, 79, 83, 84, 89	splval2 11741	. . . . . . . . . 10 $/\$ Word $/\$ concat reverse splice concat concat reverse
91	72	s1cld 11711	. . . . . . . . . . . . . . . 16 $/\$ Word $/\$ Word
92		revccat 11753	. . . . . . . . . . . . . . . 16 Word $/\$ Word reverse concat reverse concat reverse
93	45, 91, 92	syl2anc 643	. . . . . . . . . . . . . . 15 $/\$ Word $/\$ reverse concat reverse concat reverse
94		revs1 11752	. . . . . . . . . . . . . . . 16 reverse
95	94	oveq1i 6050	. . . . . . . . . . . . . . 15 reverse concat reverse concat reverse
96	93, 95	syl6eq 2452	. . . . . . . . . . . . . 14 $/\$ Word $/\$ reverse concat concat reverse
97	96	coeq2d 4994	. . . . . . . . . . . . 13 $/\$ Word $/\$ reverse concat concat reverse
98	49	a1i 11	. . . . . . . . . . . . . 14 $/\$ Word $/\$
99		ccatco 11759	. . . . . . . . . . . . . 14 Word $/\$ reverse Word $/\$ concat reverse concat reverse
100	91, 47, 98, 99	syl3anc 1184	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat reverse concat reverse
101		s1co 11757	. . . . . . . . . . . . . . 15 $/\$
102	72, 49, 101	sylancl 644	. . . . . . . . . . . . . 14 $/\$ Word $/\$
103	102	oveq1d 6055	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat reverse concat reverse
104	97, 100, 103	3eqtrd 2440	. . . . . . . . . . . 12 $/\$ Word $/\$ reverse concat concat reverse
105	104	oveq2d 6056	. . . . . . . . . . 11 $/\$ Word $/\$ concat concat reverse concat concat concat concat reverse
106		ccatcl 11698	. . . . . . . . . . . . 13 Word $/\$ Word concat Word
107	45, 91, 106	syl2anc 643	. . . . . . . . . . . 12 $/\$ Word $/\$ concat Word
108	78	s1cld 11711	. . . . . . . . . . . 12 $/\$ Word $/\$ Word
109		ccatass 11705	. . . . . . . . . . . 12 concat Word $/\$ Word $/\$ reverse Word concat concat concat reverse concat concat concat reverse
110	107, 108, 51, 109	syl3anc 1184	. . . . . . . . . . 11 $/\$ Word $/\$ concat concat concat reverse concat concat concat reverse
111		ccatass 11705	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ Word concat concat concat concat
112	45, 91, 108, 111	syl3anc 1184	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat concat concat concat
113		df-s2 11767	. . . . . . . . . . . . . 14 concat
114	113	oveq2i 6051	. . . . . . . . . . . . 13 concat concat concat
115	112, 114	syl6eqr 2454	. . . . . . . . . . . 12 $/\$ Word $/\$ concat concat concat
116	115	oveq1d 6055	. . . . . . . . . . 11 $/\$ Word $/\$ concat concat concat reverse concat concat reverse
117	105, 110, 116	3eqtr2rd 2443	. . . . . . . . . 10 $/\$ Word $/\$ concat concat reverse concat concat reverse concat
118	75, 90, 117	3eqtrd 2440	. . . . . . . . 9 $/\$ Word $/\$ concat reverse concat concat reverse concat
119	1, 36, 48, 73	efgtf 15309	. . . . . . . . . . . 12 concat reverse concat reverse concat reverse concat reverse splice $/\$ concat reverse concat reverse
120	119	simprd 450	. . . . . . . . . . 11 concat reverse concat reverse concat reverse
121		ffn 5550	. . . . . . . . . . 11 concat reverse concat reverse concat reverse concat reverse
122	55, 120, 121	3syl 19	. . . . . . . . . 10 $/\$ Word $/\$ concat reverse concat reverse
123		fnovrn 6180	. . . . . . . . . 10 concat reverse concat reverse $/\$ concat reverse $/\$ concat reverse concat reverse
124	122, 71, 72, 123	syl3anc 1184	. . . . . . . . 9 $/\$ Word $/\$ concat reverse concat reverse
125	118, 124	eqeltrrd 2479	. . . . . . . 8 $/\$ Word $/\$ concat concat reverse concat concat reverse
126	1, 36, 48, 73	efgi2 15312	. . . . . . . 8 concat reverse $/\$ concat concat reverse concat concat reverse concat reverse concat concat reverse concat
127	55, 125, 126	syl2anc 643	. . . . . . 7 $/\$ Word $/\$ concat reverse concat concat reverse concat
128	44, 127	ersym 6876	. . . . . 6 $/\$ Word $/\$ concat concat reverse concat concat reverse
129	44	ertr 6879	. . . . . 6 $/\$ Word $/\$ concat concat reverse concat concat reverse $/\$ concat reverse concat concat reverse concat
130	128, 129	mpand 657	. . . . 5 $/\$ Word $/\$ concat reverse concat concat reverse concat
131	130	expcom 425	. . . 4 Word $/\$ concat reverse concat concat reverse concat
132	131	a2d 24	. . 3 Word $/\$ concat reverse concat concat reverse concat
133	14, 20, 26, 32, 43, 132	wrdind 11746	. 2 Word concat reverse
134	4, 133	mpcom 34	1 concat reverse

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 359

wceq 1649

wcel 1721

cvv 2916 $\$ cdif 3277

c0 3588

cop 3777

cotp 3778 class class class wbr 4172

cmpt 4226

cid 4453

cxp 4835

crn 4838

ccom 4841

wfn 5408

wf 5409

cfv 5413 (class class class)co 6040

cmpt2 6042

c1o 6676

c2o 6677

wer 6861

cc0 8946

caddc 8949

cn0 10177

cz 10238

cuz 10444

cfz 10999

chash 11573 Word cword 11672 concat cconcat 11673

cs1 11674 splice csplice 11676 reversecreverse 11677

cs2 11760 ~_FG cefg 15293

This theorem is referenced by: efginvrel1 15315 frgpinv 15351

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-ot 3784 df-uni 3976 df-int 4011 df-iun 4055 df-iin 4056 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-2o 6684 df-oadd 6687 df-er 6864 df-ec 6866 df-map 6979 df-pm 6980 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-card 7782 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-nn 9957 df-n0 10178 df-z 10239 df-uz 10445 df-fz 11000 df-fzo 11091 df-hash 11574 df-word 11678 df-concat 11679 df-s1 11680 df-substr 11681 df-splice 11682 df-reverse 11683 df-s2 11767 df-efg 15296

W3C validator