efginvrel2 - Metamath Proof Explorer

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

Theorem efginvrel2 16944

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	++ 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 5906	. . . 4 Word Word
3	1, 2	eqsstri 3519	. . 3 Word
4	3	sseli 3485	. 2 Word
5		id 22	. . . . . 6
6		fveq2 5848	. . . . . . . . 9 reverse reverse
7		rev0 12729	. . . . . . . . 9 reverse
8	6, 7	syl6eq 2511	. . . . . . . 8 reverse
9	8	coeq2d 5154	. . . . . . 7 reverse
10		co02 5504	. . . . . . 7
11	9, 10	syl6eq 2511	. . . . . 6 reverse
12	5, 11	oveq12d 6288	. . . . 5 ++ reverse ++
13	12	breq1d 4449	. . . 4 ++ reverse ++
14	13	imbi2d 314	. . 3 ++ reverse ++
15		id 22	. . . . . 6
16		fveq2 5848	. . . . . . 7 reverse reverse
17	16	coeq2d 5154	. . . . . 6 reverse reverse
18	15, 17	oveq12d 6288	. . . . 5 ++ reverse ++ reverse
19	18	breq1d 4449	. . . 4 ++ reverse ++ reverse
20	19	imbi2d 314	. . 3 ++ reverse ++ reverse
21		id 22	. . . . . 6 ++ ++
22		fveq2 5848	. . . . . . 7 ++ reverse reverse ++
23	22	coeq2d 5154	. . . . . 6 ++ reverse reverse ++
24	21, 23	oveq12d 6288	. . . . 5 ++ ++ reverse ++ ++ reverse ++
25	24	breq1d 4449	. . . 4 ++ ++ reverse ++ ++ reverse ++
26	25	imbi2d 314	. . 3 ++ ++ reverse ++ ++ reverse ++
27		id 22	. . . . . 6
28		fveq2 5848	. . . . . . 7 reverse reverse
29	28	coeq2d 5154	. . . . . 6 reverse reverse
30	27, 29	oveq12d 6288	. . . . 5 ++ reverse ++ reverse
31	30	breq1d 4449	. . . 4 ++ reverse ++ reverse
32	31	imbi2d 314	. . 3 ++ reverse ++ reverse
33		wrd0 12553	. . . . 5 Word
34		ccatlid 12592	. . . . 5 Word ++
35	33, 34	ax-mp 5	. . . 4 ++
36		efgval.r	. . . . . . 7 ~_FG
37	1, 36	efger 16935	. . . . . 6
38	37	a1i 11	. . . . 5
39	1	efgrcl 16932	. . . . . . 7 $/\$ Word
40	39	simprd 461	. . . . . 6 Word
41	33, 40	syl5eleqr 2549	. . . . 5
42	38, 41	erref 7323	. . . 4
43	35, 42	syl5eqbr 4472	. . 3 ++
44	37	a1i 11	. . . . . . 7 $/\$ Word $/\$
45		simprl 754	. . . . . . . . . 10 $/\$ Word $/\$ Word
46		revcl 12726	. . . . . . . . . . . 12 Word reverse Word
47	46	ad2antrl 725	. . . . . . . . . . 11 $/\$ Word $/\$ reverse Word
48		efgval2.m	. . . . . . . . . . . 12 $\$
49	48	efgmf 16930	. . . . . . . . . . 11
50		wrdco 12788	. . . . . . . . . . 11 reverse Word $/\$ reverse Word
51	47, 49, 50	sylancl 660	. . . . . . . . . 10 $/\$ Word $/\$ reverse Word
52		ccatcl 12582	. . . . . . . . . 10 Word $/\$ reverse Word ++ reverse Word
53	45, 51, 52	syl2anc 659	. . . . . . . . 9 $/\$ Word $/\$ ++ reverse Word
54	40	adantr 463	. . . . . . . . 9 $/\$ Word $/\$ Word
55	53, 54	eleqtrrd 2545	. . . . . . . 8 $/\$ Word $/\$ ++ reverse
56		lencl 12549	. . . . . . . . . . . . . 14 Word
57	56	ad2antrl 725	. . . . . . . . . . . . 13 $/\$ Word $/\$
58		nn0uz 11116	. . . . . . . . . . . . 13
59	57, 58	syl6eleq 2552	. . . . . . . . . . . 12 $/\$ Word $/\$
60		ccatlen 12583	. . . . . . . . . . . . . 14 Word $/\$ reverse Word ++ reverse reverse
61	45, 51, 60	syl2anc 659	. . . . . . . . . . . . 13 $/\$ Word $/\$ ++ reverse reverse
62	57	nn0zd 10963	. . . . . . . . . . . . . . 15 $/\$ Word $/\$
63		uzid 11096	. . . . . . . . . . . . . . 15
64	62, 63	syl 16	. . . . . . . . . . . . . 14 $/\$ Word $/\$
65		lencl 12549	. . . . . . . . . . . . . . 15 reverse Word reverse
66	51, 65	syl 16	. . . . . . . . . . . . . 14 $/\$ Word $/\$ reverse
67		uzaddcl 11138	. . . . . . . . . . . . . 14 $/\$ reverse reverse
68	64, 66, 67	syl2anc 659	. . . . . . . . . . . . 13 $/\$ Word $/\$ reverse
69	61, 68	eqeltrd 2542	. . . . . . . . . . . 12 $/\$ Word $/\$ ++ reverse
70		elfzuzb 11685	. . . . . . . . . . . 12 ++ reverse $/\$ ++ reverse
71	59, 69, 70	sylanbrc 662	. . . . . . . . . . 11 $/\$ Word $/\$ ++ reverse
72		simprr 755	. . . . . . . . . . 11 $/\$ Word $/\$
73		efgval2.t	. . . . . . . . . . . 12 splice
74	1, 36, 48, 73	efgtval 16940	. . . . . . . . . . 11 ++ reverse $/\$ ++ reverse $/\$ ++ reverse ++ reverse splice
75	55, 71, 72, 74	syl3anc 1226	. . . . . . . . . 10 $/\$ Word $/\$ ++ reverse ++ reverse splice
76	33	a1i 11	. . . . . . . . . . 11 $/\$ Word $/\$ Word
77	49	ffvelrni 6006	. . . . . . . . . . . . 13
78	72, 77	syl 16	. . . . . . . . . . . 12 $/\$ Word $/\$
79	72, 78	s2cld 12825	. . . . . . . . . . 11 $/\$ Word $/\$ Word
80		ccatrid 12593	. . . . . . . . . . . . . 14 Word ++
81	80	ad2antrl 725	. . . . . . . . . . . . 13 $/\$ Word $/\$ ++
82	81	eqcomd 2462	. . . . . . . . . . . 12 $/\$ Word $/\$ ++
83	82	oveq1d 6285	. . . . . . . . . . 11 $/\$ Word $/\$ ++ reverse ++ ++ reverse
84		eqidd 2455	. . . . . . . . . . 11 $/\$ Word $/\$
85		hash0 12420	. . . . . . . . . . . . 13
86	85	oveq2i 6281	. . . . . . . . . . . 12
87	57	nn0cnd 10850	. . . . . . . . . . . . 13 $/\$ Word $/\$
88	87	addid1d 9769	. . . . . . . . . . . 12 $/\$ Word $/\$
89	86, 88	syl5req 2508	. . . . . . . . . . 11 $/\$ Word $/\$
90	45, 76, 51, 79, 83, 84, 89	splval2 12724	. . . . . . . . . 10 $/\$ Word $/\$ ++ reverse splice ++ ++ reverse
91	72	s1cld 12604	. . . . . . . . . . . . . . . 16 $/\$ Word $/\$ Word
92		revccat 12731	. . . . . . . . . . . . . . . 16 Word $/\$ Word reverse ++ reverse ++ reverse
93	45, 91, 92	syl2anc 659	. . . . . . . . . . . . . . 15 $/\$ Word $/\$ reverse ++ reverse ++ reverse
94		revs1 12730	. . . . . . . . . . . . . . . 16 reverse
95	94	oveq1i 6280	. . . . . . . . . . . . . . 15 reverse ++ reverse ++ reverse
96	93, 95	syl6eq 2511	. . . . . . . . . . . . . 14 $/\$ Word $/\$ reverse ++ ++ reverse
97	96	coeq2d 5154	. . . . . . . . . . . . 13 $/\$ Word $/\$ reverse ++ ++ reverse
98	49	a1i 11	. . . . . . . . . . . . . 14 $/\$ Word $/\$
99		ccatco 12792	. . . . . . . . . . . . . 14 Word $/\$ reverse Word $/\$ ++ reverse ++ reverse
100	91, 47, 98, 99	syl3anc 1226	. . . . . . . . . . . . 13 $/\$ Word $/\$ ++ reverse ++ reverse
101		s1co 12790	. . . . . . . . . . . . . . 15 $/\$
102	72, 49, 101	sylancl 660	. . . . . . . . . . . . . 14 $/\$ Word $/\$
103	102	oveq1d 6285	. . . . . . . . . . . . 13 $/\$ Word $/\$ ++ reverse ++ reverse
104	97, 100, 103	3eqtrd 2499	. . . . . . . . . . . 12 $/\$ Word $/\$ reverse ++ ++ reverse
105	104	oveq2d 6286	. . . . . . . . . . 11 $/\$ Word $/\$ ++ ++ reverse ++ ++ ++ ++ reverse
106		ccatcl 12582	. . . . . . . . . . . . 13 Word $/\$ Word ++ Word
107	45, 91, 106	syl2anc 659	. . . . . . . . . . . 12 $/\$ Word $/\$ ++ Word
108	78	s1cld 12604	. . . . . . . . . . . 12 $/\$ Word $/\$ Word
109		ccatass 12594	. . . . . . . . . . . 12 ++ Word $/\$ Word $/\$ reverse Word ++ ++ ++ reverse ++ ++ ++ reverse
110	107, 108, 51, 109	syl3anc 1226	. . . . . . . . . . 11 $/\$ Word $/\$ ++ ++ ++ reverse ++ ++ ++ reverse
111		ccatass 12594	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ Word ++ ++ ++ ++
112	45, 91, 108, 111	syl3anc 1226	. . . . . . . . . . . . 13 $/\$ Word $/\$ ++ ++ ++ ++
113		df-s2 12804	. . . . . . . . . . . . . 14 ++
114	113	oveq2i 6281	. . . . . . . . . . . . 13 ++ ++ ++
115	112, 114	syl6eqr 2513	. . . . . . . . . . . 12 $/\$ Word $/\$ ++ ++ ++
116	115	oveq1d 6285	. . . . . . . . . . 11 $/\$ Word $/\$ ++ ++ ++ reverse ++ ++ reverse
117	105, 110, 116	3eqtr2rd 2502	. . . . . . . . . 10 $/\$ Word $/\$ ++ ++ reverse ++ ++ reverse ++
118	75, 90, 117	3eqtrd 2499	. . . . . . . . 9 $/\$ Word $/\$ ++ reverse ++ ++ reverse ++
119	1, 36, 48, 73	efgtf 16939	. . . . . . . . . . . 12 ++ reverse ++ reverse ++ reverse ++ reverse splice $/\$ ++ reverse ++ reverse
120	119	simprd 461	. . . . . . . . . . 11 ++ reverse ++ reverse ++ reverse
121		ffn 5713	. . . . . . . . . . 11 ++ reverse ++ reverse ++ reverse ++ reverse
122	55, 120, 121	3syl 20	. . . . . . . . . 10 $/\$ Word $/\$ ++ reverse ++ reverse
123		fnovrn 6423	. . . . . . . . . 10 ++ reverse ++ reverse $/\$ ++ reverse $/\$ ++ reverse ++ reverse
124	122, 71, 72, 123	syl3anc 1226	. . . . . . . . 9 $/\$ Word $/\$ ++ reverse ++ reverse
125	118, 124	eqeltrrd 2543	. . . . . . . 8 $/\$ Word $/\$ ++ ++ reverse ++ ++ reverse
126	1, 36, 48, 73	efgi2 16942	. . . . . . . 8 ++ reverse $/\$ ++ ++ reverse ++ ++ reverse ++ reverse ++ ++ reverse ++
127	55, 125, 126	syl2anc 659	. . . . . . 7 $/\$ Word $/\$ ++ reverse ++ ++ reverse ++
128	44, 127	ersym 7315	. . . . . 6 $/\$ Word $/\$ ++ ++ reverse ++ ++ reverse
129	44	ertr 7318	. . . . . 6 $/\$ Word $/\$ ++ ++ reverse ++ ++ reverse $/\$ ++ reverse ++ ++ reverse ++
130	128, 129	mpand 673	. . . . 5 $/\$ Word $/\$ ++ reverse ++ ++ reverse ++
131	130	expcom 433	. . . 4 Word $/\$ ++ reverse ++ ++ reverse ++
132	131	a2d 26	. . 3 Word $/\$ ++ reverse ++ ++ reverse ++
133	14, 20, 26, 32, 43, 132	wrdind 12693	. 2 Word ++ reverse
134	4, 133	mpcom 36	1 ++ reverse

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 367

wceq 1398

wcel 1823

cvv 3106 $\$ cdif 3458

c0 3783

cop 4022

cotp 4024 class class class wbr 4439

cmpt 4497

cid 4779

cxp 4986

crn 4989

ccom 4992

wfn 5565

wf 5566

cfv 5570 (class class class)co 6270

cmpt2 6272

c1o 7115

c2o 7116

wer 7300

cc0 9481

caddc 9484

cn0 10791

cz 10860

cuz 11082

cfz 11675

chash 12387 Word cword 12518 ++ cconcat 12520

cs1 12521 splice csplice 12523 reversecreverse 12524

cs2 12797 ~_FG cefg 16923

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1623 ax-4 1636 ax-5 1709 ax-6 1752 ax-7 1795 ax-8 1825 ax-9 1827 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432 ax-rep 4550 ax-sep 4560 ax-nul 4568 ax-pow 4615 ax-pr 4676 ax-un 6565 ax-cnex 9537 ax-resscn 9538 ax-1cn 9539 ax-icn 9540 ax-addcl 9541 ax-addrcl 9542 ax-mulcl 9543 ax-mulrcl 9544 ax-mulcom 9545 ax-addass 9546 ax-mulass 9547 ax-distr 9548 ax-i2m1 9549 ax-1ne0 9550 ax-1rid 9551 ax-rnegex 9552 ax-rrecex 9553 ax-cnre 9554 ax-pre-lttri 9555 ax-pre-lttrn 9556 ax-pre-ltadd 9557 ax-pre-mulgt0 9558

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1401 df-ex 1618 df-nf 1622 df-sb 1745 df-eu 2288 df-mo 2289 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2651 df-nel 2652 df-ral 2809 df-rex 2810 df-reu 2811 df-rmo 2812 df-rab 2813 df-v 3108 df-sbc 3325 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3784 df-if 3930 df-pw 4001 df-sn 4017 df-pr 4019 df-tp 4021 df-op 4023 df-ot 4025 df-uni 4236 df-int 4272 df-iun 4317 df-iin 4318 df-br 4440 df-opab 4498 df-mpt 4499 df-tr 4533 df-eprel 4780 df-id 4784 df-po 4789 df-so 4790 df-fr 4827 df-we 4829 df-ord 4870 df-on 4871 df-lim 4872 df-suc 4873 df-xp 4994 df-rel 4995 df-cnv 4996 df-co 4997 df-dm 4998 df-rn 4999 df-res 5000 df-ima 5001 df-iota 5534 df-fun 5572 df-fn 5573 df-f 5574 df-f1 5575 df-fo 5576 df-f1o 5577 df-fv 5578 df-riota 6232 df-ov 6273 df-oprab 6274 df-mpt2 6275 df-om 6674 df-1st 6773 df-2nd 6774 df-recs 7034 df-rdg 7068 df-1o 7122 df-2o 7123 df-oadd 7126 df-er 7303 df-ec 7305 df-map 7414 df-pm 7415 df-en 7510 df-dom 7511 df-sdom 7512 df-fin 7513 df-card 8311 df-cda 8539 df-pnf 9619 df-mnf 9620 df-xr 9621 df-ltxr 9622 df-le 9623 df-sub 9798 df-neg 9799 df-nn 10532 df-2 10590 df-n0 10792 df-z 10861 df-uz 11083 df-fz 11676 df-fzo 11800 df-hash 12388 df-word 12526 df-lsw 12527 df-concat 12528 df-s1 12529 df-substr 12530 df-splice 12531 df-reverse 12532 df-s2 12804 df-efg 16926

This theorem is referenced by: efginvrel1 16945 frgpinv 16981

W3C validator