efginvrel2 - Metamath Proof Explorer

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

Theorem efginvrel2 17365

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 5936	. . . 4 Word Word
3	1, 2	eqsstri 3494	. . 3 Word
4	3	sseli 3460	. 2 Word
5		id 23	. . . . . 6
6		fveq2 5878	. . . . . . . . 9 reverse reverse
7		rev0 12860	. . . . . . . . 9 reverse
8	6, 7	syl6eq 2479	. . . . . . . 8 reverse
9	8	coeq2d 5013	. . . . . . 7 reverse
10		co02 5365	. . . . . . 7
11	9, 10	syl6eq 2479	. . . . . 6 reverse
12	5, 11	oveq12d 6320	. . . . 5 ++ reverse ++
13	12	breq1d 4430	. . . 4 ++ reverse ++
14	13	imbi2d 317	. . 3 ++ reverse ++
15		id 23	. . . . . 6
16		fveq2 5878	. . . . . . 7 reverse reverse
17	16	coeq2d 5013	. . . . . 6 reverse reverse
18	15, 17	oveq12d 6320	. . . . 5 ++ reverse ++ reverse
19	18	breq1d 4430	. . . 4 ++ reverse ++ reverse
20	19	imbi2d 317	. . 3 ++ reverse ++ reverse
21		id 23	. . . . . 6 ++ ++
22		fveq2 5878	. . . . . . 7 ++ reverse reverse ++
23	22	coeq2d 5013	. . . . . 6 ++ reverse reverse ++
24	21, 23	oveq12d 6320	. . . . 5 ++ ++ reverse ++ ++ reverse ++
25	24	breq1d 4430	. . . 4 ++ ++ reverse ++ ++ reverse ++
26	25	imbi2d 317	. . 3 ++ ++ reverse ++ ++ reverse ++
27		id 23	. . . . . 6
28		fveq2 5878	. . . . . . 7 reverse reverse
29	28	coeq2d 5013	. . . . . 6 reverse reverse
30	27, 29	oveq12d 6320	. . . . 5 ++ reverse ++ reverse
31	30	breq1d 4430	. . . 4 ++ reverse ++ reverse
32	31	imbi2d 317	. . 3 ++ reverse ++ reverse
33		wrd0 12684	. . . . 5 Word
34		ccatlid 12723	. . . . 5 Word ++
35	33, 34	ax-mp 5	. . . 4 ++
36		efgval.r	. . . . . . 7 ~_FG
37	1, 36	efger 17356	. . . . . 6
38	37	a1i 11	. . . . 5
39	1	efgrcl 17353	. . . . . . 7 $/\$ Word
40	39	simprd 464	. . . . . 6 Word
41	33, 40	syl5eleqr 2517	. . . . 5
42	38, 41	erref 7388	. . . 4
43	35, 42	syl5eqbr 4454	. . 3 ++
44	37	a1i 11	. . . . . . 7 $/\$ Word $/\$
45		simprl 762	. . . . . . . . . 10 $/\$ Word $/\$ Word
46		revcl 12857	. . . . . . . . . . . 12 Word reverse Word
47	46	ad2antrl 732	. . . . . . . . . . 11 $/\$ Word $/\$ reverse Word
48		efgval2.m	. . . . . . . . . . . 12 $\$
49	48	efgmf 17351	. . . . . . . . . . 11
50		wrdco 12919	. . . . . . . . . . 11 reverse Word $/\$ reverse Word
51	47, 49, 50	sylancl 666	. . . . . . . . . 10 $/\$ Word $/\$ reverse Word
52		ccatcl 12713	. . . . . . . . . 10 Word $/\$ reverse Word ++ reverse Word
53	45, 51, 52	syl2anc 665	. . . . . . . . 9 $/\$ Word $/\$ ++ reverse Word
54	40	adantr 466	. . . . . . . . 9 $/\$ Word $/\$ Word
55	53, 54	eleqtrrd 2513	. . . . . . . 8 $/\$ Word $/\$ ++ reverse
56		lencl 12680	. . . . . . . . . . . . . 14 Word
57	56	ad2antrl 732	. . . . . . . . . . . . 13 $/\$ Word $/\$
58		nn0uz 11194	. . . . . . . . . . . . 13
59	57, 58	syl6eleq 2520	. . . . . . . . . . . 12 $/\$ Word $/\$
60		ccatlen 12714	. . . . . . . . . . . . . 14 Word $/\$ reverse Word ++ reverse reverse
61	45, 51, 60	syl2anc 665	. . . . . . . . . . . . 13 $/\$ Word $/\$ ++ reverse reverse
62	57	nn0zd 11039	. . . . . . . . . . . . . . 15 $/\$ Word $/\$
63		uzid 11174	. . . . . . . . . . . . . . 15
64	62, 63	syl 17	. . . . . . . . . . . . . 14 $/\$ Word $/\$
65		lencl 12680	. . . . . . . . . . . . . . 15 reverse Word reverse
66	51, 65	syl 17	. . . . . . . . . . . . . 14 $/\$ Word $/\$ reverse
67		uzaddcl 11216	. . . . . . . . . . . . . 14 $/\$ reverse reverse
68	64, 66, 67	syl2anc 665	. . . . . . . . . . . . 13 $/\$ Word $/\$ reverse
69	61, 68	eqeltrd 2510	. . . . . . . . . . . 12 $/\$ Word $/\$ ++ reverse
70		elfzuzb 11795	. . . . . . . . . . . 12 ++ reverse $/\$ ++ reverse
71	59, 69, 70	sylanbrc 668	. . . . . . . . . . 11 $/\$ Word $/\$ ++ reverse
72		simprr 764	. . . . . . . . . . 11 $/\$ Word $/\$
73		efgval2.t	. . . . . . . . . . . 12 splice
74	1, 36, 48, 73	efgtval 17361	. . . . . . . . . . 11 ++ reverse $/\$ ++ reverse $/\$ ++ reverse ++ reverse splice
75	55, 71, 72, 74	syl3anc 1264	. . . . . . . . . 10 $/\$ Word $/\$ ++ reverse ++ reverse splice
76	33	a1i 11	. . . . . . . . . . 11 $/\$ Word $/\$ Word
77	49	ffvelrni 6033	. . . . . . . . . . . . 13
78	72, 77	syl 17	. . . . . . . . . . . 12 $/\$ Word $/\$
79	72, 78	s2cld 12956	. . . . . . . . . . 11 $/\$ Word $/\$ Word
80		ccatrid 12724	. . . . . . . . . . . . . 14 Word ++
81	80	ad2antrl 732	. . . . . . . . . . . . 13 $/\$ Word $/\$ ++
82	81	eqcomd 2430	. . . . . . . . . . . 12 $/\$ Word $/\$ ++
83	82	oveq1d 6317	. . . . . . . . . . 11 $/\$ Word $/\$ ++ reverse ++ ++ reverse
84		eqidd 2423	. . . . . . . . . . 11 $/\$ Word $/\$
85		hash0 12548	. . . . . . . . . . . . 13
86	85	oveq2i 6313	. . . . . . . . . . . 12
87	57	nn0cnd 10928	. . . . . . . . . . . . 13 $/\$ Word $/\$
88	87	addid1d 9834	. . . . . . . . . . . 12 $/\$ Word $/\$
89	86, 88	syl5req 2476	. . . . . . . . . . 11 $/\$ Word $/\$
90	45, 76, 51, 79, 83, 84, 89	splval2 12855	. . . . . . . . . 10 $/\$ Word $/\$ ++ reverse splice ++ ++ reverse
91	72	s1cld 12735	. . . . . . . . . . . . . . . 16 $/\$ Word $/\$ Word
92		revccat 12862	. . . . . . . . . . . . . . . 16 Word $/\$ Word reverse ++ reverse ++ reverse
93	45, 91, 92	syl2anc 665	. . . . . . . . . . . . . . 15 $/\$ Word $/\$ reverse ++ reverse ++ reverse
94		revs1 12861	. . . . . . . . . . . . . . . 16 reverse
95	94	oveq1i 6312	. . . . . . . . . . . . . . 15 reverse ++ reverse ++ reverse
96	93, 95	syl6eq 2479	. . . . . . . . . . . . . 14 $/\$ Word $/\$ reverse ++ ++ reverse
97	96	coeq2d 5013	. . . . . . . . . . . . 13 $/\$ Word $/\$ reverse ++ ++ reverse
98	49	a1i 11	. . . . . . . . . . . . . 14 $/\$ Word $/\$
99		ccatco 12923	. . . . . . . . . . . . . 14 Word $/\$ reverse Word $/\$ ++ reverse ++ reverse
100	91, 47, 98, 99	syl3anc 1264	. . . . . . . . . . . . 13 $/\$ Word $/\$ ++ reverse ++ reverse
101		s1co 12921	. . . . . . . . . . . . . . 15 $/\$
102	72, 49, 101	sylancl 666	. . . . . . . . . . . . . 14 $/\$ Word $/\$
103	102	oveq1d 6317	. . . . . . . . . . . . 13 $/\$ Word $/\$ ++ reverse ++ reverse
104	97, 100, 103	3eqtrd 2467	. . . . . . . . . . . 12 $/\$ Word $/\$ reverse ++ ++ reverse
105	104	oveq2d 6318	. . . . . . . . . . 11 $/\$ Word $/\$ ++ ++ reverse ++ ++ ++ ++ reverse
106		ccatcl 12713	. . . . . . . . . . . . 13 Word $/\$ Word ++ Word
107	45, 91, 106	syl2anc 665	. . . . . . . . . . . 12 $/\$ Word $/\$ ++ Word
108	78	s1cld 12735	. . . . . . . . . . . 12 $/\$ Word $/\$ Word
109		ccatass 12725	. . . . . . . . . . . 12 ++ Word $/\$ Word $/\$ reverse Word ++ ++ ++ reverse ++ ++ ++ reverse
110	107, 108, 51, 109	syl3anc 1264	. . . . . . . . . . 11 $/\$ Word $/\$ ++ ++ ++ reverse ++ ++ ++ reverse
111		ccatass 12725	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ Word ++ ++ ++ ++
112	45, 91, 108, 111	syl3anc 1264	. . . . . . . . . . . . 13 $/\$ Word $/\$ ++ ++ ++ ++
113		df-s2 12935	. . . . . . . . . . . . . 14 ++
114	113	oveq2i 6313	. . . . . . . . . . . . 13 ++ ++ ++
115	112, 114	syl6eqr 2481	. . . . . . . . . . . 12 $/\$ Word $/\$ ++ ++ ++
116	115	oveq1d 6317	. . . . . . . . . . 11 $/\$ Word $/\$ ++ ++ ++ reverse ++ ++ reverse
117	105, 110, 116	3eqtr2rd 2470	. . . . . . . . . 10 $/\$ Word $/\$ ++ ++ reverse ++ ++ reverse ++
118	75, 90, 117	3eqtrd 2467	. . . . . . . . 9 $/\$ Word $/\$ ++ reverse ++ ++ reverse ++
119	1, 36, 48, 73	efgtf 17360	. . . . . . . . . . . 12 ++ reverse ++ reverse ++ reverse ++ reverse splice $/\$ ++ reverse ++ reverse
120	119	simprd 464	. . . . . . . . . . 11 ++ reverse ++ reverse ++ reverse
121		ffn 5743	. . . . . . . . . . 11 ++ reverse ++ reverse ++ reverse ++ reverse
122	55, 120, 121	3syl 18	. . . . . . . . . 10 $/\$ Word $/\$ ++ reverse ++ reverse
123		fnovrn 6455	. . . . . . . . . 10 ++ reverse ++ reverse $/\$ ++ reverse $/\$ ++ reverse ++ reverse
124	122, 71, 72, 123	syl3anc 1264	. . . . . . . . 9 $/\$ Word $/\$ ++ reverse ++ reverse
125	118, 124	eqeltrrd 2511	. . . . . . . 8 $/\$ Word $/\$ ++ ++ reverse ++ ++ reverse
126	1, 36, 48, 73	efgi2 17363	. . . . . . . 8 ++ reverse $/\$ ++ ++ reverse ++ ++ reverse ++ reverse ++ ++ reverse ++
127	55, 125, 126	syl2anc 665	. . . . . . 7 $/\$ Word $/\$ ++ reverse ++ ++ reverse ++
128	44, 127	ersym 7380	. . . . . 6 $/\$ Word $/\$ ++ ++ reverse ++ ++ reverse
129	44	ertr 7383	. . . . . 6 $/\$ Word $/\$ ++ ++ reverse ++ ++ reverse $/\$ ++ reverse ++ ++ reverse ++
130	128, 129	mpand 679	. . . . 5 $/\$ Word $/\$ ++ reverse ++ ++ reverse ++
131	130	expcom 436	. . . 4 Word $/\$ ++ reverse ++ ++ reverse ++
132	131	a2d 29	. . 3 Word $/\$ ++ reverse ++ ++ reverse ++
133	14, 20, 26, 32, 43, 132	wrdind 12824	. 2 Word ++ reverse
134	4, 133	mpcom 37	1 ++ reverse

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 370

wceq 1437

wcel 1868

cvv 3081 $\$ cdif 3433

c0 3761

cop 4002

cotp 4004 class class class wbr 4420

cmpt 4479

cid 4760

cxp 4848

crn 4851

ccom 4854

wfn 5593

wf 5594

cfv 5598 (class class class)co 6302

cmpt2 6304

c1o 7180

c2o 7181

wer 7365

cc0 9540

caddc 9543

cn0 10870

cz 10938

cuz 11160

cfz 11785

chash 12515 Word cword 12649 ++ cconcat 12651

cs1 12652 splice csplice 12654 reversecreverse 12655

cs2 12928 ~_FG cefg 17344

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1839 ax-8 1870 ax-9 1872 ax-10 1887 ax-11 1892 ax-12 1905 ax-13 2053 ax-ext 2400 ax-rep 4533 ax-sep 4543 ax-nul 4552 ax-pow 4599 ax-pr 4657 ax-un 6594 ax-cnex 9596 ax-resscn 9597 ax-1cn 9598 ax-icn 9599 ax-addcl 9600 ax-addrcl 9601 ax-mulcl 9602 ax-mulrcl 9603 ax-mulcom 9604 ax-addass 9605 ax-mulass 9606 ax-distr 9607 ax-i2m1 9608 ax-1ne0 9609 ax-1rid 9610 ax-rnegex 9611 ax-rrecex 9612 ax-cnre 9613 ax-pre-lttri 9614 ax-pre-lttrn 9615 ax-pre-ltadd 9616 ax-pre-mulgt0 9617

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2269 df-mo 2270 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2572 df-ne 2620 df-nel 2621 df-ral 2780 df-rex 2781 df-reu 2782 df-rmo 2783 df-rab 2784 df-v 3083 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3910 df-pw 3981 df-sn 3997 df-pr 3999 df-tp 4001 df-op 4003 df-ot 4005 df-uni 4217 df-int 4253 df-iun 4298 df-iin 4299 df-br 4421 df-opab 4480 df-mpt 4481 df-tr 4516 df-eprel 4761 df-id 4765 df-po 4771 df-so 4772 df-fr 4809 df-we 4811 df-xp 4856 df-rel 4857 df-cnv 4858 df-co 4859 df-dm 4860 df-rn 4861 df-res 4862 df-ima 4863 df-pred 5396 df-ord 5442 df-on 5443 df-lim 5444 df-suc 5445 df-iota 5562 df-fun 5600 df-fn 5601 df-f 5602 df-f1 5603 df-fo 5604 df-f1o 5605 df-fv 5606 df-riota 6264 df-ov 6305 df-oprab 6306 df-mpt2 6307 df-om 6704 df-1st 6804 df-2nd 6805 df-wrecs 7033 df-recs 7095 df-rdg 7133 df-1o 7187 df-2o 7188 df-oadd 7191 df-er 7368 df-ec 7370 df-map 7479 df-pm 7480 df-en 7575 df-dom 7576 df-sdom 7577 df-fin 7578 df-card 8375 df-cda 8599 df-pnf 9678 df-mnf 9679 df-xr 9680 df-ltxr 9681 df-le 9682 df-sub 9863 df-neg 9864 df-nn 10611 df-2 10669 df-n0 10871 df-z 10939 df-uz 11161 df-fz 11786 df-fzo 11917 df-hash 12516 df-word 12657 df-lsw 12658 df-concat 12659 df-s1 12660 df-substr 12661 df-splice 12662 df-reverse 12663 df-s2 12935 df-efg 17347

This theorem is referenced by: efginvrel1 17366 frgpinv 17402

W3C validator