efginvrel2 - Metamath Proof Explorer

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

Theorem efginvrel2 17455

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 5938	. . . 4 Word Word
3	1, 2	eqsstri 3448	. . 3 Word
4	3	sseli 3414	. 2 Word
5		id 22	. . . . . 6
6		fveq2 5879	. . . . . . . . 9 reverse reverse
7		rev0 12923	. . . . . . . . 9 reverse
8	6, 7	syl6eq 2521	. . . . . . . 8 reverse
9	8	coeq2d 5002	. . . . . . 7 reverse
10		co02 5356	. . . . . . 7
11	9, 10	syl6eq 2521	. . . . . 6 reverse
12	5, 11	oveq12d 6326	. . . . 5 ++ reverse ++
13	12	breq1d 4405	. . . 4 ++ reverse ++
14	13	imbi2d 323	. . 3 ++ reverse ++
15		id 22	. . . . . 6
16		fveq2 5879	. . . . . . 7 reverse reverse
17	16	coeq2d 5002	. . . . . 6 reverse reverse
18	15, 17	oveq12d 6326	. . . . 5 ++ reverse ++ reverse
19	18	breq1d 4405	. . . 4 ++ reverse ++ reverse
20	19	imbi2d 323	. . 3 ++ reverse ++ reverse
21		id 22	. . . . . 6 ++ ++
22		fveq2 5879	. . . . . . 7 ++ reverse reverse ++
23	22	coeq2d 5002	. . . . . 6 ++ reverse reverse ++
24	21, 23	oveq12d 6326	. . . . 5 ++ ++ reverse ++ ++ reverse ++
25	24	breq1d 4405	. . . 4 ++ ++ reverse ++ ++ reverse ++
26	25	imbi2d 323	. . 3 ++ ++ reverse ++ ++ reverse ++
27		id 22	. . . . . 6
28		fveq2 5879	. . . . . . 7 reverse reverse
29	28	coeq2d 5002	. . . . . 6 reverse reverse
30	27, 29	oveq12d 6326	. . . . 5 ++ reverse ++ reverse
31	30	breq1d 4405	. . . 4 ++ reverse ++ reverse
32	31	imbi2d 323	. . 3 ++ reverse ++ reverse
33		wrd0 12742	. . . . 5 Word
34		ccatlid 12781	. . . . 5 Word ++
35	33, 34	ax-mp 5	. . . 4 ++
36		efgval.r	. . . . . . 7 ~_FG
37	1, 36	efger 17446	. . . . . 6
38	37	a1i 11	. . . . 5
39	1	efgrcl 17443	. . . . . . 7 $/\$ Word
40	39	simprd 470	. . . . . 6 Word
41	33, 40	syl5eleqr 2556	. . . . 5
42	38, 41	erref 7401	. . . 4
43	35, 42	syl5eqbr 4429	. . 3 ++
44	37	a1i 11	. . . . . . 7 $/\$ Word $/\$
45		simprl 772	. . . . . . . . . 10 $/\$ Word $/\$ Word
46		revcl 12920	. . . . . . . . . . . 12 Word reverse Word
47	46	ad2antrl 742	. . . . . . . . . . 11 $/\$ Word $/\$ reverse Word
48		efgval2.m	. . . . . . . . . . . 12 $\$
49	48	efgmf 17441	. . . . . . . . . . 11
50		wrdco 12987	. . . . . . . . . . 11 reverse Word $/\$ reverse Word
51	47, 49, 50	sylancl 675	. . . . . . . . . 10 $/\$ Word $/\$ reverse Word
52		ccatcl 12771	. . . . . . . . . 10 Word $/\$ reverse Word ++ reverse Word
53	45, 51, 52	syl2anc 673	. . . . . . . . 9 $/\$ Word $/\$ ++ reverse Word
54	40	adantr 472	. . . . . . . . 9 $/\$ Word $/\$ Word
55	53, 54	eleqtrrd 2552	. . . . . . . 8 $/\$ Word $/\$ ++ reverse
56		lencl 12737	. . . . . . . . . . . . . 14 Word
57	56	ad2antrl 742	. . . . . . . . . . . . 13 $/\$ Word $/\$
58		nn0uz 11217	. . . . . . . . . . . . 13
59	57, 58	syl6eleq 2559	. . . . . . . . . . . 12 $/\$ Word $/\$
60		ccatlen 12772	. . . . . . . . . . . . . 14 Word $/\$ reverse Word ++ reverse reverse
61	45, 51, 60	syl2anc 673	. . . . . . . . . . . . 13 $/\$ Word $/\$ ++ reverse reverse
62	57	nn0zd 11061	. . . . . . . . . . . . . . 15 $/\$ Word $/\$
63		uzid 11197	. . . . . . . . . . . . . . 15
64	62, 63	syl 17	. . . . . . . . . . . . . 14 $/\$ Word $/\$
65		lencl 12737	. . . . . . . . . . . . . . 15 reverse Word reverse
66	51, 65	syl 17	. . . . . . . . . . . . . 14 $/\$ Word $/\$ reverse
67		uzaddcl 11238	. . . . . . . . . . . . . 14 $/\$ reverse reverse
68	64, 66, 67	syl2anc 673	. . . . . . . . . . . . 13 $/\$ Word $/\$ reverse
69	61, 68	eqeltrd 2549	. . . . . . . . . . . 12 $/\$ Word $/\$ ++ reverse
70		elfzuzb 11820	. . . . . . . . . . . 12 ++ reverse $/\$ ++ reverse
71	59, 69, 70	sylanbrc 677	. . . . . . . . . . 11 $/\$ Word $/\$ ++ reverse
72		simprr 774	. . . . . . . . . . 11 $/\$ Word $/\$
73		efgval2.t	. . . . . . . . . . . 12 splice
74	1, 36, 48, 73	efgtval 17451	. . . . . . . . . . 11 ++ reverse $/\$ ++ reverse $/\$ ++ reverse ++ reverse splice
75	55, 71, 72, 74	syl3anc 1292	. . . . . . . . . 10 $/\$ Word $/\$ ++ reverse ++ reverse splice
76	33	a1i 11	. . . . . . . . . . 11 $/\$ Word $/\$ Word
77	49	ffvelrni 6036	. . . . . . . . . . . . 13
78	72, 77	syl 17	. . . . . . . . . . . 12 $/\$ Word $/\$
79	72, 78	s2cld 13025	. . . . . . . . . . 11 $/\$ Word $/\$ Word
80		ccatrid 12782	. . . . . . . . . . . . . 14 Word ++
81	80	ad2antrl 742	. . . . . . . . . . . . 13 $/\$ Word $/\$ ++
82	81	eqcomd 2477	. . . . . . . . . . . 12 $/\$ Word $/\$ ++
83	82	oveq1d 6323	. . . . . . . . . . 11 $/\$ Word $/\$ ++ reverse ++ ++ reverse
84		eqidd 2472	. . . . . . . . . . 11 $/\$ Word $/\$
85		hash0 12586	. . . . . . . . . . . . 13
86	85	oveq2i 6319	. . . . . . . . . . . 12
87	57	nn0cnd 10951	. . . . . . . . . . . . 13 $/\$ Word $/\$
88	87	addid1d 9851	. . . . . . . . . . . 12 $/\$ Word $/\$
89	86, 88	syl5req 2518	. . . . . . . . . . 11 $/\$ Word $/\$
90	45, 76, 51, 79, 83, 84, 89	splval2 12918	. . . . . . . . . 10 $/\$ Word $/\$ ++ reverse splice ++ ++ reverse
91	72	s1cld 12795	. . . . . . . . . . . . . . . 16 $/\$ Word $/\$ Word
92		revccat 12925	. . . . . . . . . . . . . . . 16 Word $/\$ Word reverse ++ reverse ++ reverse
93	45, 91, 92	syl2anc 673	. . . . . . . . . . . . . . 15 $/\$ Word $/\$ reverse ++ reverse ++ reverse
94		revs1 12924	. . . . . . . . . . . . . . . 16 reverse
95	94	oveq1i 6318	. . . . . . . . . . . . . . 15 reverse ++ reverse ++ reverse
96	93, 95	syl6eq 2521	. . . . . . . . . . . . . 14 $/\$ Word $/\$ reverse ++ ++ reverse
97	96	coeq2d 5002	. . . . . . . . . . . . 13 $/\$ Word $/\$ reverse ++ ++ reverse
98	49	a1i 11	. . . . . . . . . . . . . 14 $/\$ Word $/\$
99		ccatco 12991	. . . . . . . . . . . . . 14 Word $/\$ reverse Word $/\$ ++ reverse ++ reverse
100	91, 47, 98, 99	syl3anc 1292	. . . . . . . . . . . . 13 $/\$ Word $/\$ ++ reverse ++ reverse
101		s1co 12989	. . . . . . . . . . . . . . 15 $/\$
102	72, 49, 101	sylancl 675	. . . . . . . . . . . . . 14 $/\$ Word $/\$
103	102	oveq1d 6323	. . . . . . . . . . . . 13 $/\$ Word $/\$ ++ reverse ++ reverse
104	97, 100, 103	3eqtrd 2509	. . . . . . . . . . . 12 $/\$ Word $/\$ reverse ++ ++ reverse
105	104	oveq2d 6324	. . . . . . . . . . 11 $/\$ Word $/\$ ++ ++ reverse ++ ++ ++ ++ reverse
106		ccatcl 12771	. . . . . . . . . . . . 13 Word $/\$ Word ++ Word
107	45, 91, 106	syl2anc 673	. . . . . . . . . . . 12 $/\$ Word $/\$ ++ Word
108	78	s1cld 12795	. . . . . . . . . . . 12 $/\$ Word $/\$ Word
109		ccatass 12783	. . . . . . . . . . . 12 ++ Word $/\$ Word $/\$ reverse Word ++ ++ ++ reverse ++ ++ ++ reverse
110	107, 108, 51, 109	syl3anc 1292	. . . . . . . . . . 11 $/\$ Word $/\$ ++ ++ ++ reverse ++ ++ ++ reverse
111		ccatass 12783	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ Word ++ ++ ++ ++
112	45, 91, 108, 111	syl3anc 1292	. . . . . . . . . . . . 13 $/\$ Word $/\$ ++ ++ ++ ++
113		df-s2 13003	. . . . . . . . . . . . . 14 ++
114	113	oveq2i 6319	. . . . . . . . . . . . 13 ++ ++ ++
115	112, 114	syl6eqr 2523	. . . . . . . . . . . 12 $/\$ Word $/\$ ++ ++ ++
116	115	oveq1d 6323	. . . . . . . . . . 11 $/\$ Word $/\$ ++ ++ ++ reverse ++ ++ reverse
117	105, 110, 116	3eqtr2rd 2512	. . . . . . . . . 10 $/\$ Word $/\$ ++ ++ reverse ++ ++ reverse ++
118	75, 90, 117	3eqtrd 2509	. . . . . . . . 9 $/\$ Word $/\$ ++ reverse ++ ++ reverse ++
119	1, 36, 48, 73	efgtf 17450	. . . . . . . . . . . 12 ++ reverse ++ reverse ++ reverse ++ reverse splice $/\$ ++ reverse ++ reverse
120	119	simprd 470	. . . . . . . . . . 11 ++ reverse ++ reverse ++ reverse
121		ffn 5739	. . . . . . . . . . 11 ++ reverse ++ reverse ++ reverse ++ reverse
122	55, 120, 121	3syl 18	. . . . . . . . . 10 $/\$ Word $/\$ ++ reverse ++ reverse
123		fnovrn 6463	. . . . . . . . . 10 ++ reverse ++ reverse $/\$ ++ reverse $/\$ ++ reverse ++ reverse
124	122, 71, 72, 123	syl3anc 1292	. . . . . . . . 9 $/\$ Word $/\$ ++ reverse ++ reverse
125	118, 124	eqeltrrd 2550	. . . . . . . 8 $/\$ Word $/\$ ++ ++ reverse ++ ++ reverse
126	1, 36, 48, 73	efgi2 17453	. . . . . . . 8 ++ reverse $/\$ ++ ++ reverse ++ ++ reverse ++ reverse ++ ++ reverse ++
127	55, 125, 126	syl2anc 673	. . . . . . 7 $/\$ Word $/\$ ++ reverse ++ ++ reverse ++
128	44, 127	ersym 7393	. . . . . 6 $/\$ Word $/\$ ++ ++ reverse ++ ++ reverse
129	44	ertr 7396	. . . . . 6 $/\$ Word $/\$ ++ ++ reverse ++ ++ reverse $/\$ ++ reverse ++ ++ reverse ++
130	128, 129	mpand 689	. . . . 5 $/\$ Word $/\$ ++ reverse ++ ++ reverse ++
131	130	expcom 442	. . . 4 Word $/\$ ++ reverse ++ ++ reverse ++
132	131	a2d 28	. . 3 Word $/\$ ++ reverse ++ ++ reverse ++
133	14, 20, 26, 32, 43, 132	wrdind 12887	. 2 Word ++ reverse
134	4, 133	mpcom 36	1 ++ reverse

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 376

wceq 1452

wcel 1904

cvv 3031 $\$ cdif 3387

c0 3722

cop 3965

cotp 3967 class class class wbr 4395

cmpt 4454

cid 4749

cxp 4837

crn 4840

ccom 4843

wfn 5584

wf 5585

cfv 5589 (class class class)co 6308

cmpt2 6310

c1o 7193

c2o 7194

wer 7378

cc0 9557

caddc 9560

cn0 10893

cz 10961

cuz 11182

cfz 11810

chash 12553 Word cword 12703 ++ cconcat 12705

cs1 12706 splice csplice 12708 reversecreverse 12709

cs2 12996 ~_FG cefg 17434

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-ot 3968 df-uni 4191 df-int 4227 df-iun 4271 df-iin 4272 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-er 7381 df-ec 7383 df-map 7492 df-pm 7493 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-card 8391 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-nn 10632 df-2 10690 df-n0 10894 df-z 10962 df-uz 11183 df-fz 11811 df-fzo 11943 df-hash 12554 df-word 12711 df-lsw 12712 df-concat 12713 df-s1 12714 df-substr 12715 df-splice 12716 df-reverse 12717 df-s2 13003 df-efg 17437

This theorem is referenced by: efginvrel1 17456 frgpinv 17492

W3C validator