efginvrel2 - Metamath Proof Explorer

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

Theorem efginvrel2 16204

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 5737	. . . 4 Word Word
3	1, 2	eqsstri 3374	. . 3 Word
4	3	sseli 3340	. 2 Word
5		id 22	. . . . . 6
6		fveq2 5679	. . . . . . . . 9 reverse reverse
7		rev0 12388	. . . . . . . . 9 reverse
8	6, 7	syl6eq 2481	. . . . . . . 8 reverse
9	8	coeq2d 4989	. . . . . . 7 reverse
10		co02 5339	. . . . . . 7
11	9, 10	syl6eq 2481	. . . . . 6 reverse
12	5, 11	oveq12d 6098	. . . . 5 concat reverse concat
13	12	breq1d 4290	. . . 4 concat reverse concat
14	13	imbi2d 316	. . 3 concat reverse concat
15		id 22	. . . . . 6
16		fveq2 5679	. . . . . . 7 reverse reverse
17	16	coeq2d 4989	. . . . . 6 reverse reverse
18	15, 17	oveq12d 6098	. . . . 5 concat reverse concat reverse
19	18	breq1d 4290	. . . 4 concat reverse concat reverse
20	19	imbi2d 316	. . 3 concat reverse concat reverse
21		id 22	. . . . . 6 concat concat
22		fveq2 5679	. . . . . . 7 concat reverse reverse concat
23	22	coeq2d 4989	. . . . . 6 concat reverse reverse concat
24	21, 23	oveq12d 6098	. . . . 5 concat concat reverse concat concat reverse concat
25	24	breq1d 4290	. . . 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 5679	. . . . . . 7 reverse reverse
29	28	coeq2d 4989	. . . . . 6 reverse reverse
30	27, 29	oveq12d 6098	. . . . 5 concat reverse concat reverse
31	30	breq1d 4290	. . . 4 concat reverse concat reverse
32	31	imbi2d 316	. . 3 concat reverse concat reverse
33		wrd0 12236	. . . . 5 Word
34		ccatlid 12268	. . . . 5 Word concat
35	33, 34	ax-mp 5	. . . 4 concat
36		efgval.r	. . . . . . 7 ~_FG
37	1, 36	efger 16195	. . . . . 6
38	37	a1i 11	. . . . 5
39	1	efgrcl 16192	. . . . . . 7 $/\$ Word
40	39	simprd 460	. . . . . 6 Word
41	33, 40	syl5eleqr 2520	. . . . 5
42	38, 41	erref 7109	. . . 4
43	35, 42	syl5eqbr 4313	. . 3 concat
44	37	a1i 11	. . . . . . 7 $/\$ Word $/\$
45		simprl 748	. . . . . . . . . 10 $/\$ Word $/\$ Word
46		revcl 12385	. . . . . . . . . . . 12 Word reverse Word
47	46	ad2antrl 720	. . . . . . . . . . 11 $/\$ Word $/\$ reverse Word
48		efgval2.m	. . . . . . . . . . . 12 $\$
49	48	efgmf 16190	. . . . . . . . . . 11
50		wrdco 12443	. . . . . . . . . . 11 reverse Word $/\$ reverse Word
51	47, 49, 50	sylancl 655	. . . . . . . . . 10 $/\$ Word $/\$ reverse Word
52		ccatcl 12258	. . . . . . . . . 10 Word $/\$ reverse Word concat reverse Word
53	45, 51, 52	syl2anc 654	. . . . . . . . 9 $/\$ Word $/\$ concat reverse Word
54	40	adantr 462	. . . . . . . . 9 $/\$ Word $/\$ Word
55	53, 54	eleqtrrd 2510	. . . . . . . 8 $/\$ Word $/\$ concat reverse
56		lencl 12233	. . . . . . . . . . . . . 14 Word
57	56	ad2antrl 720	. . . . . . . . . . . . 13 $/\$ Word $/\$
58		nn0uz 10883	. . . . . . . . . . . . 13
59	57, 58	syl6eleq 2523	. . . . . . . . . . . 12 $/\$ Word $/\$
60		ccatlen 12259	. . . . . . . . . . . . . 14 Word $/\$ reverse Word concat reverse reverse
61	45, 51, 60	syl2anc 654	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat reverse reverse
62	57	nn0zd 10733	. . . . . . . . . . . . . . 15 $/\$ Word $/\$
63		uzid 10863	. . . . . . . . . . . . . . 15
64	62, 63	syl 16	. . . . . . . . . . . . . 14 $/\$ Word $/\$
65		lencl 12233	. . . . . . . . . . . . . . 15 reverse Word reverse
66	51, 65	syl 16	. . . . . . . . . . . . . 14 $/\$ Word $/\$ reverse
67		uzaddcl 10899	. . . . . . . . . . . . . 14 $/\$ reverse reverse
68	64, 66, 67	syl2anc 654	. . . . . . . . . . . . 13 $/\$ Word $/\$ reverse
69	61, 68	eqeltrd 2507	. . . . . . . . . . . 12 $/\$ Word $/\$ concat reverse
70		elfzuzb 11434	. . . . . . . . . . . 12 concat reverse $/\$ concat reverse
71	59, 69, 70	sylanbrc 657	. . . . . . . . . . 11 $/\$ Word $/\$ concat reverse
72		simprr 749	. . . . . . . . . . 11 $/\$ Word $/\$
73		efgval2.t	. . . . . . . . . . . 12 splice
74	1, 36, 48, 73	efgtval 16200	. . . . . . . . . . 11 concat reverse $/\$ concat reverse $/\$ concat reverse concat reverse splice
75	55, 71, 72, 74	syl3anc 1211	. . . . . . . . . 10 $/\$ Word $/\$ concat reverse concat reverse splice
76	33	a1i 11	. . . . . . . . . . 11 $/\$ Word $/\$ Word
77	49	ffvelrni 5830	. . . . . . . . . . . . 13
78	72, 77	syl 16	. . . . . . . . . . . 12 $/\$ Word $/\$
79	72, 78	s2cld 12480	. . . . . . . . . . 11 $/\$ Word $/\$ Word
80		ccatrid 12269	. . . . . . . . . . . . . 14 Word concat
81	80	ad2antrl 720	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat
82	81	eqcomd 2438	. . . . . . . . . . . 12 $/\$ Word $/\$ concat
83	82	oveq1d 6095	. . . . . . . . . . 11 $/\$ Word $/\$ concat reverse concat concat reverse
84		eqidd 2434	. . . . . . . . . . 11 $/\$ Word $/\$
85		hash0 12119	. . . . . . . . . . . . 13
86	85	oveq2i 6091	. . . . . . . . . . . 12
87	57	nn0cnd 10626	. . . . . . . . . . . . 13 $/\$ Word $/\$
88	87	addid1d 9557	. . . . . . . . . . . 12 $/\$ Word $/\$
89	86, 88	syl5req 2478	. . . . . . . . . . 11 $/\$ Word $/\$
90	45, 76, 51, 79, 83, 84, 89	splval2 12383	. . . . . . . . . 10 $/\$ Word $/\$ concat reverse splice concat concat reverse
91	72	s1cld 12278	. . . . . . . . . . . . . . . 16 $/\$ Word $/\$ Word
92		revccat 12390	. . . . . . . . . . . . . . . 16 Word $/\$ Word reverse concat reverse concat reverse
93	45, 91, 92	syl2anc 654	. . . . . . . . . . . . . . 15 $/\$ Word $/\$ reverse concat reverse concat reverse
94		revs1 12389	. . . . . . . . . . . . . . . 16 reverse
95	94	oveq1i 6090	. . . . . . . . . . . . . . 15 reverse concat reverse concat reverse
96	93, 95	syl6eq 2481	. . . . . . . . . . . . . 14 $/\$ Word $/\$ reverse concat concat reverse
97	96	coeq2d 4989	. . . . . . . . . . . . 13 $/\$ Word $/\$ reverse concat concat reverse
98	49	a1i 11	. . . . . . . . . . . . . 14 $/\$ Word $/\$
99		ccatco 12447	. . . . . . . . . . . . . 14 Word $/\$ reverse Word $/\$ concat reverse concat reverse
100	91, 47, 98, 99	syl3anc 1211	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat reverse concat reverse
101		s1co 12445	. . . . . . . . . . . . . . 15 $/\$
102	72, 49, 101	sylancl 655	. . . . . . . . . . . . . 14 $/\$ Word $/\$
103	102	oveq1d 6095	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat reverse concat reverse
104	97, 100, 103	3eqtrd 2469	. . . . . . . . . . . 12 $/\$ Word $/\$ reverse concat concat reverse
105	104	oveq2d 6096	. . . . . . . . . . 11 $/\$ Word $/\$ concat concat reverse concat concat concat concat reverse
106		ccatcl 12258	. . . . . . . . . . . . 13 Word $/\$ Word concat Word
107	45, 91, 106	syl2anc 654	. . . . . . . . . . . 12 $/\$ Word $/\$ concat Word
108	78	s1cld 12278	. . . . . . . . . . . 12 $/\$ Word $/\$ Word
109		ccatass 12270	. . . . . . . . . . . 12 concat Word $/\$ Word $/\$ reverse Word concat concat concat reverse concat concat concat reverse
110	107, 108, 51, 109	syl3anc 1211	. . . . . . . . . . 11 $/\$ Word $/\$ concat concat concat reverse concat concat concat reverse
111		ccatass 12270	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ Word concat concat concat concat
112	45, 91, 108, 111	syl3anc 1211	. . . . . . . . . . . . 13 $/\$ Word $/\$ concat concat concat concat
113		df-s2 12459	. . . . . . . . . . . . . 14 concat
114	113	oveq2i 6091	. . . . . . . . . . . . 13 concat concat concat
115	112, 114	syl6eqr 2483	. . . . . . . . . . . 12 $/\$ Word $/\$ concat concat concat
116	115	oveq1d 6095	. . . . . . . . . . 11 $/\$ Word $/\$ concat concat concat reverse concat concat reverse
117	105, 110, 116	3eqtr2rd 2472	. . . . . . . . . 10 $/\$ Word $/\$ concat concat reverse concat concat reverse concat
118	75, 90, 117	3eqtrd 2469	. . . . . . . . 9 $/\$ Word $/\$ concat reverse concat concat reverse concat
119	1, 36, 48, 73	efgtf 16199	. . . . . . . . . . . 12 concat reverse concat reverse concat reverse concat reverse splice $/\$ concat reverse concat reverse
120	119	simprd 460	. . . . . . . . . . 11 concat reverse concat reverse concat reverse
121		ffn 5547	. . . . . . . . . . 11 concat reverse concat reverse concat reverse concat reverse
122	55, 120, 121	3syl 20	. . . . . . . . . 10 $/\$ Word $/\$ concat reverse concat reverse
123		fnovrn 6227	. . . . . . . . . 10 concat reverse concat reverse $/\$ concat reverse $/\$ concat reverse concat reverse
124	122, 71, 72, 123	syl3anc 1211	. . . . . . . . 9 $/\$ Word $/\$ concat reverse concat reverse
125	118, 124	eqeltrrd 2508	. . . . . . . 8 $/\$ Word $/\$ concat concat reverse concat concat reverse
126	1, 36, 48, 73	efgi2 16202	. . . . . . . 8 concat reverse $/\$ concat concat reverse concat concat reverse concat reverse concat concat reverse concat
127	55, 125, 126	syl2anc 654	. . . . . . 7 $/\$ Word $/\$ concat reverse concat concat reverse concat
128	44, 127	ersym 7101	. . . . . 6 $/\$ Word $/\$ concat concat reverse concat concat reverse
129	44	ertr 7104	. . . . . 6 $/\$ Word $/\$ concat concat reverse concat concat reverse $/\$ concat reverse concat concat reverse concat
130	128, 129	mpand 668	. . . . 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 12355	. 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 1362

wcel 1755

cvv 2962 $\$ cdif 3313

c0 3625

cop 3871

cotp 3873 class class class wbr 4280

cmpt 4338

cid 4618

cxp 4825

crn 4828

ccom 4831

wfn 5401

wf 5402

cfv 5406 (class class class)co 6080

cmpt2 6082

c1o 6901

c2o 6902

wer 7086

cc0 9270

caddc 9273

cn0 10567

cz 10634

cuz 10849

cfz 11424

chash 12087 Word cword 12205 concat cconcat 12207

cs1 12208 splice csplice 12210 reversecreverse 12211

cs2 12452 ~_FG cefg 16183

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1594 ax-4 1605 ax-5 1669 ax-6 1707 ax-7 1727 ax-8 1757 ax-9 1759 ax-10 1774 ax-11 1779 ax-12 1791 ax-13 1942 ax-ext 2414 ax-rep 4391 ax-sep 4401 ax-nul 4409 ax-pow 4458 ax-pr 4519 ax-un 6361 ax-cnex 9326 ax-resscn 9327 ax-1cn 9328 ax-icn 9329 ax-addcl 9330 ax-addrcl 9331 ax-mulcl 9332 ax-mulrcl 9333 ax-mulcom 9334 ax-addass 9335 ax-mulass 9336 ax-distr 9337 ax-i2m1 9338 ax-1ne0 9339 ax-1rid 9340 ax-rnegex 9341 ax-rrecex 9342 ax-cnre 9343 ax-pre-lttri 9344 ax-pre-lttrn 9345 ax-pre-ltadd 9346 ax-pre-mulgt0 9347

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 959 df-3an 960 df-tru 1365 df-ex 1590 df-nf 1593 df-sb 1700 df-eu 2258 df-mo 2259 df-clab 2420 df-cleq 2426 df-clel 2429 df-nfc 2558 df-ne 2598 df-nel 2599 df-ral 2710 df-rex 2711 df-reu 2712 df-rab 2714 df-v 2964 df-sbc 3176 df-csb 3277 df-dif 3319 df-un 3321 df-in 3323 df-ss 3330 df-pss 3332 df-nul 3626 df-if 3780 df-pw 3850 df-sn 3866 df-pr 3868 df-tp 3870 df-op 3872 df-ot 3874 df-uni 4080 df-int 4117 df-iun 4161 df-iin 4162 df-br 4281 df-opab 4339 df-mpt 4340 df-tr 4374 df-eprel 4619 df-id 4623 df-po 4628 df-so 4629 df-fr 4666 df-we 4668 df-ord 4709 df-on 4710 df-lim 4711 df-suc 4712 df-xp 4833 df-rel 4834 df-cnv 4835 df-co 4836 df-dm 4837 df-rn 4838 df-res 4839 df-ima 4840 df-iota 5369 df-fun 5408 df-fn 5409 df-f 5410 df-f1 5411 df-fo 5412 df-f1o 5413 df-fv 5414 df-riota 6039 df-ov 6083 df-oprab 6084 df-mpt2 6085 df-om 6466 df-1st 6566 df-2nd 6567 df-recs 6818 df-rdg 6852 df-1o 6908 df-2o 6909 df-oadd 6912 df-er 7089 df-ec 7091 df-map 7204 df-pm 7205 df-en 7299 df-dom 7300 df-sdom 7301 df-fin 7302 df-card 8097 df-pnf 9408 df-mnf 9409 df-xr 9410 df-ltxr 9411 df-le 9412 df-sub 9585 df-neg 9586 df-nn 10311 df-n0 10568 df-z 10635 df-uz 10850 df-fz 11425 df-fzo 11533 df-hash 12088 df-word 12213 df-concat 12215 df-s1 12216 df-substr 12217 df-splice 12218 df-reverse 12219 df-s2 12459 df-efg 16186

This theorem is referenced by: efginvrel1 16205 frgpinv 16241

W3C validator