efginvrel2 - Metamath Proof Explorer

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

Theorem efginvrel2 16551

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 5925	. . . 4 Word Word
3	1, 2	eqsstri 3534	. . 3 Word
4	3	sseli 3500	. 2 Word
5		id 22	. . . . . 6
6		fveq2 5866	. . . . . . . . 9 reverse reverse
7		rev0 12701	. . . . . . . . 9 reverse
8	6, 7	syl6eq 2524	. . . . . . . 8 reverse
9	8	coeq2d 5165	. . . . . . 7 reverse
10		co02 5521	. . . . . . 7
11	9, 10	syl6eq 2524	. . . . . 6 reverse
12	5, 11	oveq12d 6302	. . . . 5 concat reverse concat
13	12	breq1d 4457	. . . 4 concat reverse concat
14	13	imbi2d 316	. . 3 concat reverse concat
15		id 22	. . . . . 6
16		fveq2 5866	. . . . . . 7 reverse reverse
17	16	coeq2d 5165	. . . . . 6 reverse reverse
18	15, 17	oveq12d 6302	. . . . 5 concat reverse concat reverse
19	18	breq1d 4457	. . . 4 concat reverse concat reverse
20	19	imbi2d 316	. . 3 concat reverse concat reverse
21		id 22	. . . . . 6 concat concat
22		fveq2 5866	. . . . . . 7 concat reverse reverse concat
23	22	coeq2d 5165	. . . . . 6 concat reverse reverse concat
24	21, 23	oveq12d 6302	. . . . 5 concat concat reverse concat concat reverse concat
25	24	breq1d 4457	. . . 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 5866	. . . . . . 7 reverse reverse
29	28	coeq2d 5165	. . . . . 6 reverse reverse
30	27, 29	oveq12d 6302	. . . . 5 concat reverse concat reverse
31	30	breq1d 4457	. . . 4 concat reverse concat reverse
32	31	imbi2d 316	. . 3 concat reverse concat reverse
33		wrd0 12531	. . . . 5 Word
34		ccatlid 12568	. . . . 5 Word concat
35	33, 34	ax-mp 5	. . . 4 concat
36		efgval.r	. . . . . . 7 ~_FG
37	1, 36	efger 16542	. . . . . 6
38	37	a1i 11	. . . . 5
39	1	efgrcl 16539	. . . . . . 7 $/\$ Word
40	39	simprd 463	. . . . . 6 Word
41	33, 40	syl5eleqr 2562	. . . . 5
42	38, 41	erref 7331	. . . 4
43	35, 42	syl5eqbr 4480	. . 3 concat
44	37	a1i 11	. . . . . . 7 $/\$ Word $/\$
45		simprl 755	. . . . . . . . . 10 $/\$ Word $/\$ Word
46		revcl 12698	. . . . . . . . . . . 12 Word reverse Word
47	46	ad2antrl 727	. . . . . . . . . . 11 $/\$ Word $/\$ reverse Word
48		efgval2.m	. . . . . . . . . . . 12 $\$
49	48	efgmf 16537	. . . . . . . . . . 11
50		wrdco 12760	. . . . . . . . . . 11 reverse Word $/\$ reverse Word
51	47, 49, 50	sylancl 662	. . . . . . . . . 10 $/\$ Word $/\$ reverse Word
52		ccatcl 12558	. . . . . . . . . 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 2558	. . . . . . . 8 $/\$ Word $/\$ concat reverse
56		lencl 12528	. . . . . . . . . . . . . 14 Word
57	56	ad2antrl 727	. . . . . . . . . . . . 13 $/\$ Word $/\$
58		nn0uz 11116	. . . . . . . . . . . . 13
59	57, 58	syl6eleq 2565	. . . . . . . . . . . 12 $/\$ Word $/\$
60		ccatlen 12559	. . . . . . . . . . . . . 14 Word $/\$ reverse Word concat reverse reverse
61	45, 51, 60	syl2anc 661	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat reverse reverse
62	57	nn0zd 10964	. . . . . . . . . . . . . . 15 $/\$ Word $/\$
63		uzid 11096	. . . . . . . . . . . . . . 15
64	62, 63	syl 16	. . . . . . . . . . . . . 14 $/\$ Word $/\$
65		lencl 12528	. . . . . . . . . . . . . . 15 reverse Word reverse
66	51, 65	syl 16	. . . . . . . . . . . . . 14 $/\$ Word $/\$ reverse
67		uzaddcl 11137	. . . . . . . . . . . . . 14 $/\$ reverse reverse
68	64, 66, 67	syl2anc 661	. . . . . . . . . . . . 13 $/\$ Word $/\$ reverse
69	61, 68	eqeltrd 2555	. . . . . . . . . . . 12 $/\$ Word $/\$ concat reverse
70		elfzuzb 11682	. . . . . . . . . . . 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 16547	. . . . . . . . . . 11 concat reverse $/\$ concat reverse $/\$ concat reverse concat reverse splice
75	55, 71, 72, 74	syl3anc 1228	. . . . . . . . . 10 $/\$ Word $/\$ concat reverse concat reverse splice
76	33	a1i 11	. . . . . . . . . . 11 $/\$ Word $/\$ Word
77	49	ffvelrni 6020	. . . . . . . . . . . . 13
78	72, 77	syl 16	. . . . . . . . . . . 12 $/\$ Word $/\$
79	72, 78	s2cld 12797	. . . . . . . . . . 11 $/\$ Word $/\$ Word
80		ccatrid 12569	. . . . . . . . . . . . . 14 Word concat
81	80	ad2antrl 727	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat
82	81	eqcomd 2475	. . . . . . . . . . . 12 $/\$ Word $/\$ concat
83	82	oveq1d 6299	. . . . . . . . . . 11 $/\$ Word $/\$ concat reverse concat concat reverse
84		eqidd 2468	. . . . . . . . . . 11 $/\$ Word $/\$
85		hash0 12405	. . . . . . . . . . . . 13
86	85	oveq2i 6295	. . . . . . . . . . . 12
87	57	nn0cnd 10854	. . . . . . . . . . . . 13 $/\$ Word $/\$
88	87	addid1d 9779	. . . . . . . . . . . 12 $/\$ Word $/\$
89	86, 88	syl5req 2521	. . . . . . . . . . 11 $/\$ Word $/\$
90	45, 76, 51, 79, 83, 84, 89	splval2 12696	. . . . . . . . . 10 $/\$ Word $/\$ concat reverse splice concat concat reverse
91	72	s1cld 12578	. . . . . . . . . . . . . . . 16 $/\$ Word $/\$ Word
92		revccat 12703	. . . . . . . . . . . . . . . 16 Word $/\$ Word reverse concat reverse concat reverse
93	45, 91, 92	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ Word $/\$ reverse concat reverse concat reverse
94		revs1 12702	. . . . . . . . . . . . . . . 16 reverse
95	94	oveq1i 6294	. . . . . . . . . . . . . . 15 reverse concat reverse concat reverse
96	93, 95	syl6eq 2524	. . . . . . . . . . . . . 14 $/\$ Word $/\$ reverse concat concat reverse
97	96	coeq2d 5165	. . . . . . . . . . . . 13 $/\$ Word $/\$ reverse concat concat reverse
98	49	a1i 11	. . . . . . . . . . . . . 14 $/\$ Word $/\$
99		ccatco 12764	. . . . . . . . . . . . . 14 Word $/\$ reverse Word $/\$ concat reverse concat reverse
100	91, 47, 98, 99	syl3anc 1228	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat reverse concat reverse
101		s1co 12762	. . . . . . . . . . . . . . 15 $/\$
102	72, 49, 101	sylancl 662	. . . . . . . . . . . . . 14 $/\$ Word $/\$
103	102	oveq1d 6299	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat reverse concat reverse
104	97, 100, 103	3eqtrd 2512	. . . . . . . . . . . 12 $/\$ Word $/\$ reverse concat concat reverse
105	104	oveq2d 6300	. . . . . . . . . . 11 $/\$ Word $/\$ concat concat reverse concat concat concat concat reverse
106		ccatcl 12558	. . . . . . . . . . . . 13 Word $/\$ Word concat Word
107	45, 91, 106	syl2anc 661	. . . . . . . . . . . 12 $/\$ Word $/\$ concat Word
108	78	s1cld 12578	. . . . . . . . . . . 12 $/\$ Word $/\$ Word
109		ccatass 12570	. . . . . . . . . . . 12 concat Word $/\$ Word $/\$ reverse Word concat concat concat reverse concat concat concat reverse
110	107, 108, 51, 109	syl3anc 1228	. . . . . . . . . . 11 $/\$ Word $/\$ concat concat concat reverse concat concat concat reverse
111		ccatass 12570	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ Word concat concat concat concat
112	45, 91, 108, 111	syl3anc 1228	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat concat concat concat
113		df-s2 12776	. . . . . . . . . . . . . 14 concat
114	113	oveq2i 6295	. . . . . . . . . . . . 13 concat concat concat
115	112, 114	syl6eqr 2526	. . . . . . . . . . . 12 $/\$ Word $/\$ concat concat concat
116	115	oveq1d 6299	. . . . . . . . . . 11 $/\$ Word $/\$ concat concat concat reverse concat concat reverse
117	105, 110, 116	3eqtr2rd 2515	. . . . . . . . . 10 $/\$ Word $/\$ concat concat reverse concat concat reverse concat
118	75, 90, 117	3eqtrd 2512	. . . . . . . . 9 $/\$ Word $/\$ concat reverse concat concat reverse concat
119	1, 36, 48, 73	efgtf 16546	. . . . . . . . . . . 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 5731	. . . . . . . . . . 11 concat reverse concat reverse concat reverse concat reverse
122	55, 120, 121	3syl 20	. . . . . . . . . 10 $/\$ Word $/\$ concat reverse concat reverse
123		fnovrn 6434	. . . . . . . . . 10 concat reverse concat reverse $/\$ concat reverse $/\$ concat reverse concat reverse
124	122, 71, 72, 123	syl3anc 1228	. . . . . . . . 9 $/\$ Word $/\$ concat reverse concat reverse
125	118, 124	eqeltrrd 2556	. . . . . . . 8 $/\$ Word $/\$ concat concat reverse concat concat reverse
126	1, 36, 48, 73	efgi2 16549	. . . . . . . 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 7323	. . . . . 6 $/\$ Word $/\$ concat concat reverse concat concat reverse
129	44	ertr 7326	. . . . . 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 12665	. 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 1379

wcel 1767

cvv 3113 $\$ cdif 3473

c0 3785

cop 4033

cotp 4035 class class class wbr 4447

cmpt 4505

cid 4790

cxp 4997

crn 5000

ccom 5003

wfn 5583

wf 5584

cfv 5588 (class class class)co 6284

cmpt2 6286

c1o 7123

c2o 7124

wer 7308

cc0 9492

caddc 9495

cn0 10795

cz 10864

cuz 11082

cfz 11672

chash 12373 Word cword 12500 concat cconcat 12502

cs1 12503 splice csplice 12505 reversecreverse 12506

cs2 12769 ~_FG cefg 16530

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6576 ax-cnex 9548 ax-resscn 9549 ax-1cn 9550 ax-icn 9551 ax-addcl 9552 ax-addrcl 9553 ax-mulcl 9554 ax-mulrcl 9555 ax-mulcom 9556 ax-addass 9557 ax-mulass 9558 ax-distr 9559 ax-i2m1 9560 ax-1ne0 9561 ax-1rid 9562 ax-rnegex 9563 ax-rrecex 9564 ax-cnre 9565 ax-pre-lttri 9566 ax-pre-lttrn 9567 ax-pre-ltadd 9568 ax-pre-mulgt0 9569

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-ot 4036 df-uni 4246 df-int 4283 df-iun 4327 df-iin 4328 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-riota 6245 df-ov 6287 df-oprab 6288 df-mpt2 6289 df-om 6685 df-1st 6784 df-2nd 6785 df-recs 7042 df-rdg 7076 df-1o 7130 df-2o 7131 df-oadd 7134 df-er 7311 df-ec 7313 df-map 7422 df-pm 7423 df-en 7517 df-dom 7518 df-sdom 7519 df-fin 7520 df-card 8320 df-pnf 9630 df-mnf 9631 df-xr 9632 df-ltxr 9633 df-le 9634 df-sub 9807 df-neg 9808 df-nn 10537 df-n0 10796 df-z 10865 df-uz 11083 df-fz 11673 df-fzo 11793 df-hash 12374 df-word 12508 df-concat 12510 df-s1 12511 df-substr 12512 df-splice 12513 df-reverse 12514 df-s2 12776 df-efg 16533

This theorem is referenced by: efginvrel1 16552 frgpinv 16588

W3C validator