psgnunilem1 - Metamath Proof Explorer

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

Theorem psgnunilem1 17133

Description: Lemma for psgnuni 17139. Given two consequtive transpositions in a representation of a permutation, either they are equal and therefore equivalent to the identity, or they are not and it is possible to commute them such that a chosen point in the left transposition is preserved in the right. By repeating this process, a point can be removed from a representation of the identity. (Contributed by Stefan O'Rear, 22-Aug-2015.)

**Hypotheses**
Ref	Expression
psgnunilem1.t	pmTrsp
psgnunilem1.d
psgnunilem1.p
psgnunilem1.q
psgnunilem1.a	$\$

**Assertion**
Ref	Expression
psgnunilem1	$\/$ $/\$ $\$ $/\$ $\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

**Proof of Theorem psgnunilem1**
Step	Hyp	Ref	Expression
1		psgnunilem1.q	. . . . . . . 8
2		eqid 2422	. . . . . . . . 9 pmTrsp pmTrsp
3		psgnunilem1.t	. . . . . . . . 9 pmTrsp
4	2, 3	pmtrfinv 17101	. . . . . . . 8
5	1, 4	syl 17	. . . . . . 7
6		coeq1 5011	. . . . . . . 8
7	6	eqeq1d 2424	. . . . . . 7
8	5, 7	syl5ibrcom 225	. . . . . 6
9	8	adantr 466	. . . . 5 $/\$ $\$
10	9	imp 430	. . . 4 $/\$ $\$ $/\$
11	10	orcd 393	. . 3 $/\$ $\$ $/\$ $\/$ $/\$ $\$ $/\$ $\$
12		psgnunilem1.p	. . . . . . . . . 10
13	2, 3	pmtrfcnv 17104	. . . . . . . . . 10
14	12, 13	syl 17	. . . . . . . . 9
15	14	eqcomd 2430	. . . . . . . 8
16	15	coeq2d 5016	. . . . . . 7
17	2, 3	pmtrff1o 17103	. . . . . . . . 9
18	12, 17	syl 17	. . . . . . . 8
19	2, 3	pmtrfconj 17106	. . . . . . . 8 $/\$
20	1, 18, 19	syl2anc 665	. . . . . . 7
21	16, 20	eqeltrd 2507	. . . . . 6
22	21	ad2antrr 730	. . . . 5 $/\$ $\$ $/\$
23	12	ad2antrr 730	. . . . 5 $/\$ $\$ $/\$
24		coass 5373	. . . . . . 7
25	2, 3	pmtrfinv 17101	. . . . . . . . . 10
26	12, 25	syl 17	. . . . . . . . 9
27	26	coeq2d 5016	. . . . . . . 8
28		f1of 5831	. . . . . . . . . . 11
29	18, 28	syl 17	. . . . . . . . . 10
30	2, 3	pmtrff1o 17103	. . . . . . . . . . . 12
31	1, 30	syl 17	. . . . . . . . . . 11
32		f1of 5831	. . . . . . . . . . 11
33	31, 32	syl 17	. . . . . . . . . 10
34		fco 5756	. . . . . . . . . 10 $/\$
35	29, 33, 34	syl2anc 665	. . . . . . . . 9
36		fcoi1 5774	. . . . . . . . 9
37	35, 36	syl 17	. . . . . . . 8
38	27, 37	eqtrd 2463	. . . . . . 7
39	24, 38	syl5req 2476	. . . . . 6
40	39	ad2antrr 730	. . . . 5 $/\$ $\$ $/\$
41		psgnunilem1.a	. . . . . 6 $\$
42	41	ad2antrr 730	. . . . 5 $/\$ $\$ $/\$ $\$
43	18	adantr 466	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$
44	31	adantr 466	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$
45	2, 3	pmtrfb 17105	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
46	45	simp3bi 1022	. . . . . . . . . . . 12 $\$
47	12, 46	syl 17	. . . . . . . . . . 11 $\$
48	47	adantr 466	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$ $\$
49		2onn 7352	. . . . . . . . . . . . . . 15
50		nnfi 7774	. . . . . . . . . . . . . . 15
51	49, 50	ax-mp 5	. . . . . . . . . . . . . 14
52	2, 3	pmtrfb 17105	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$
53	52	simp3bi 1022	. . . . . . . . . . . . . . . 16 $\$
54	1, 53	syl 17	. . . . . . . . . . . . . . 15 $\$
55		enfi 7797	. . . . . . . . . . . . . . 15 $\$ $\$
56	54, 55	syl 17	. . . . . . . . . . . . . 14 $\$
57	51, 56	mpbiri 236	. . . . . . . . . . . . 13 $\$
58	57	adantr 466	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $\$
59	41	adantr 466	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $\$ $\$
60		en2eleq 8447	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$ $\$
61	59, 48, 60	syl2anc 665	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
62		simprl 762	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $\$ $\$
63		f1ofn 5832	. . . . . . . . . . . . . . . . . 18
64	18, 63	syl 17	. . . . . . . . . . . . . . . . 17
65	64	adantr 466	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$
66		imassrn 5198	. . . . . . . . . . . . . . . . . . 19 $\$
67		frn 5752	. . . . . . . . . . . . . . . . . . 19
68	66, 67	syl5ss 3475	. . . . . . . . . . . . . . . . . 18 $\$
69	29, 68	syl 17	. . . . . . . . . . . . . . . . 17 $\$
70	69	adantr 466	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$ $\$
71		simprr 764	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$ $\$
72		fnfvima 6158	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$ $\$
73	65, 70, 71, 72	syl3anc 1264	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $\$ $\$
74		difss 3592	. . . . . . . . . . . . . . . . . . . . 21 $\$
75		dmss 5053	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
76	74, 75	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 $\$
77		f1odm 5835	. . . . . . . . . . . . . . . . . . . . 21
78	18, 77	syl 17	. . . . . . . . . . . . . . . . . . . 20
79	76, 78	syl5sseq 3512	. . . . . . . . . . . . . . . . . . 19 $\$
80	79, 41	sseldd 3465	. . . . . . . . . . . . . . . . . 18
81		eqid 2422	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
82	2, 3, 81	pmtrffv 17099	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$ $\$
83	12, 80, 82	syl2anc 665	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
84	41	iftrued 3919	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$ $\$ $\$
85	83, 84	eqtrd 2463	. . . . . . . . . . . . . . . 16 $\$ $\$
86	85	adantr 466	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $\$ $\$ $\$
87		imaco 5359	. . . . . . . . . . . . . . . . 17 $\$ $\$
88	26	imaeq1d 5186	. . . . . . . . . . . . . . . . . 18 $\$ $\$
89		difss 3592	. . . . . . . . . . . . . . . . . . . . . 22 $\$
90		dmss 5053	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
91	89, 90	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 $\$
92		f1odm 5835	. . . . . . . . . . . . . . . . . . . . 21
93	91, 92	syl5sseq 3512	. . . . . . . . . . . . . . . . . . . 20 $\$
94	31, 93	syl 17	. . . . . . . . . . . . . . . . . . 19 $\$
95		resiima 5201	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$
96	94, 95	syl 17	. . . . . . . . . . . . . . . . . 18 $\$ $\$
97	88, 96	eqtrd 2463	. . . . . . . . . . . . . . . . 17 $\$ $\$
98	87, 97	syl5eqr 2477	. . . . . . . . . . . . . . . 16 $\$ $\$
99	98	adantr 466	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $\$ $\$ $\$
100	73, 86, 99	3eltr3d 2521	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
101		prssi 4156	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
102	62, 100, 101	syl2anc 665	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
103	61, 102	eqsstrd 3498	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $\$ $\$
104	54	ensymd 7630	. . . . . . . . . . . . . 14 $\$
105		entr 7631	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$
106	47, 104, 105	syl2anc 665	. . . . . . . . . . . . 13 $\$ $\$
107	106	adantr 466	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $\$ $\$
108		fisseneq 7792	. . . . . . . . . . . 12 $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$
109	58, 103, 107, 108	syl3anc 1264	. . . . . . . . . . 11 $/\$ $\$ $/\$ $\$ $\$ $\$
110	109	eqcomd 2430	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$ $\$ $\$
111		f1otrspeq 17087	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $\$ $\$
112	43, 44, 48, 110, 111	syl22anc 1265	. . . . . . . . 9 $/\$ $\$ $/\$ $\$
113	112	expr 618	. . . . . . . 8 $/\$ $\$ $\$
114	113	necon3ad 2630	. . . . . . 7 $/\$ $\$ $\$
115	114	imp 430	. . . . . 6 $/\$ $\$ $/\$ $\$
116	16	difeq1d 3582	. . . . . . . . . 10 $\$ $\$
117	116	dmeqd 5056	. . . . . . . . 9 $\$ $\$
118		f1omvdconj 17086	. . . . . . . . . 10 $/\$ $\$ $\$
119	33, 18, 118	syl2anc 665	. . . . . . . . 9 $\$ $\$
120	117, 119	eqtrd 2463	. . . . . . . 8 $\$ $\$
121	120	eleq2d 2492	. . . . . . 7 $\$ $\$
122	121	ad2antrr 730	. . . . . 6 $/\$ $\$ $/\$ $\$ $\$
123	115, 122	mtbird 302	. . . . 5 $/\$ $\$ $/\$ $\$
124		coeq1 5011	. . . . . . . 8
125	124	eqeq2d 2436	. . . . . . 7
126		difeq1 3576	. . . . . . . . . 10 $\$ $\$
127	126	dmeqd 5056	. . . . . . . . 9 $\$ $\$
128	127	eleq2d 2492	. . . . . . . 8 $\$ $\$
129	128	notbid 295	. . . . . . 7 $\$ $\$
130	125, 129	3anbi13d 1337	. . . . . 6 $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
131		coeq2 5012	. . . . . . . 8
132	131	eqeq2d 2436	. . . . . . 7
133		difeq1 3576	. . . . . . . . 9 $\$ $\$
134	133	dmeqd 5056	. . . . . . . 8 $\$ $\$
135	134	eleq2d 2492	. . . . . . 7 $\$ $\$
136	132, 135	3anbi12d 1336	. . . . . 6 $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
137	130, 136	rspc2ev 3193	. . . . 5 $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
138	22, 23, 40, 42, 123, 137	syl113anc 1276	. . . 4 $/\$ $\$ $/\$ $/\$ $\$ $/\$ $\$
139	138	olcd 394	. . 3 $/\$ $\$ $/\$ $\/$ $/\$ $\$ $/\$ $\$
140	11, 139	pm2.61dane 2738	. 2 $/\$ $\$ $\/$ $/\$ $\$ $/\$ $\$
141	1	adantr 466	. . . 4 $/\$ $\$
142		coass 5373	. . . . . . 7
143	2, 3	pmtrfcnv 17104	. . . . . . . . . 10
144	1, 143	syl 17	. . . . . . . . 9
145	144	eqcomd 2430	. . . . . . . 8
146	145	coeq2d 5016	. . . . . . 7
147	142, 146	syl5eqr 2477	. . . . . 6
148	2, 3	pmtrfconj 17106	. . . . . . 7 $/\$
149	12, 31, 148	syl2anc 665	. . . . . 6
150	147, 149	eqeltrd 2507	. . . . 5
151	150	adantr 466	. . . 4 $/\$ $\$
152	5	coeq1d 5015	. . . . . . 7
153		fcoi2 5775	. . . . . . . 8
154	35, 153	syl 17	. . . . . . 7
155	152, 154	eqtr2d 2464	. . . . . 6
156		coass 5373	. . . . . 6
157	155, 156	syl6eq 2479	. . . . 5
158	157	adantr 466	. . . 4 $/\$ $\$
159		f1ofn 5832	. . . . . . . . . 10
160	31, 159	syl 17	. . . . . . . . 9
161		fnelnfp 6109	. . . . . . . . 9 $/\$ $\$
162	160, 80, 161	syl2anc 665	. . . . . . . 8 $\$
163	162	necon2bbid 2676	. . . . . . 7 $\$
164	163	biimpar 487	. . . . . 6 $/\$ $\$
165		fnfvima 6158	. . . . . . . 8 $/\$ $\$ $/\$ $\$ $\$
166	160, 79, 41, 165	syl3anc 1264	. . . . . . 7 $\$
167	166	adantr 466	. . . . . 6 $/\$ $\$ $\$
168	164, 167	eqeltrrd 2508	. . . . 5 $/\$ $\$ $\$
169	147	difeq1d 3582	. . . . . . . 8 $\$ $\$
170	169	dmeqd 5056	. . . . . . 7 $\$ $\$
171		f1omvdconj 17086	. . . . . . . 8 $/\$ $\$ $\$
172	29, 31, 171	syl2anc 665	. . . . . . 7 $\$ $\$
173	170, 172	eqtrd 2463	. . . . . 6 $\$ $\$
174	173	adantr 466	. . . . 5 $/\$ $\$ $\$ $\$
175	168, 174	eleqtrrd 2510	. . . 4 $/\$ $\$ $\$
176		simpr 462	. . . 4 $/\$ $\$ $\$
177		coeq1 5011	. . . . . . 7
178	177	eqeq2d 2436	. . . . . 6
179		difeq1 3576	. . . . . . . . 9 $\$ $\$
180	179	dmeqd 5056	. . . . . . . 8 $\$ $\$
181	180	eleq2d 2492	. . . . . . 7 $\$ $\$
182	181	notbid 295	. . . . . 6 $\$ $\$
183	178, 182	3anbi13d 1337	. . . . 5 $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
184		coeq2 5012	. . . . . . 7
185	184	eqeq2d 2436	. . . . . 6
186		difeq1 3576	. . . . . . . 8 $\$ $\$
187	186	dmeqd 5056	. . . . . . 7 $\$ $\$
188	187	eleq2d 2492	. . . . . 6 $\$ $\$
189	185, 188	3anbi12d 1336	. . . . 5 $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
190	183, 189	rspc2ev 3193	. . . 4 $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
191	141, 151, 158, 175, 176, 190	syl113anc 1276	. . 3 $/\$ $\$ $/\$ $\$ $/\$ $\$
192	191	olcd 394	. 2 $/\$ $\$ $\/$ $/\$ $\$ $/\$ $\$
193	140, 192	pm2.61dan 798	1 $\/$ $/\$ $\$ $/\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $\/$ wo 369 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1872

wne 2614

wrex 2772

cvv 3080 $\$ cdif 3433

wss 3436

cif 3911

csn 3998

cpr 4000

cuni 4219 class class class wbr 4423

cid 4763

ccnv 4852

cdm 4853

crn 4854

cres 4855

cima 4856

ccom 4857

wfn 5596

wf 5597

wf1o 5600

cfv 5601

com 6706

c2o 7187

cen 7577

cfn 7580 pmTrspcpmtr 17081

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2057 ax-ext 2401 ax-rep 4536 ax-sep 4546 ax-nul 4555 ax-pow 4602 ax-pr 4660 ax-un 6597

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 1658 df-nf 1662 df-sb 1791 df-eu 2273 df-mo 2274 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2568 df-ne 2616 df-ral 2776 df-rex 2777 df-reu 2778 df-rab 2780 df-v 3082 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 3912 df-pw 3983 df-sn 3999 df-pr 4001 df-tp 4003 df-op 4005 df-uni 4220 df-iun 4301 df-br 4424 df-opab 4483 df-mpt 4484 df-tr 4519 df-eprel 4764 df-id 4768 df-po 4774 df-so 4775 df-fr 4812 df-we 4814 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-om 6707 df-1o 7193 df-2o 7194 df-er 7374 df-en 7581 df-dom 7582 df-sdom 7583 df-fin 7584 df-pmtr 17082

This theorem is referenced by: psgnunilem2 17135

W3C validator