psgnunilem1 - Metamath Proof Explorer

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

Theorem psgnunilem1 16324

Description: Lemma for psgnuni 16330. 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 2467	. . . . . . . . 9 pmTrsp pmTrsp
3		psgnunilem1.t	. . . . . . . . 9 pmTrsp
4	2, 3	pmtrfinv 16292	. . . . . . . 8
5	1, 4	syl 16	. . . . . . 7
6		coeq1 5160	. . . . . . . 8
7	6	eqeq1d 2469	. . . . . . 7
8	5, 7	syl5ibrcom 222	. . . . . 6
9	8	adantr 465	. . . . 5 $/\$ $\$
10	9	imp 429	. . . 4 $/\$ $\$ $/\$
11	10	orcd 392	. . 3 $/\$ $\$ $/\$ $\/$ $/\$ $\$ $/\$ $\$
12		psgnunilem1.p	. . . . . . . . . 10
13	2, 3	pmtrfcnv 16295	. . . . . . . . . 10
14	12, 13	syl 16	. . . . . . . . 9
15	14	eqcomd 2475	. . . . . . . 8
16	15	coeq2d 5165	. . . . . . 7
17	2, 3	pmtrff1o 16294	. . . . . . . . 9
18	12, 17	syl 16	. . . . . . . 8
19	2, 3	pmtrfconj 16297	. . . . . . . 8 $/\$
20	1, 18, 19	syl2anc 661	. . . . . . 7
21	16, 20	eqeltrd 2555	. . . . . 6
22	21	ad2antrr 725	. . . . 5 $/\$ $\$ $/\$
23	12	ad2antrr 725	. . . . 5 $/\$ $\$ $/\$
24		coass 5526	. . . . . . 7
25	2, 3	pmtrfinv 16292	. . . . . . . . . 10
26	12, 25	syl 16	. . . . . . . . 9
27	26	coeq2d 5165	. . . . . . . 8
28		f1of 5816	. . . . . . . . . . 11
29	18, 28	syl 16	. . . . . . . . . 10
30	2, 3	pmtrff1o 16294	. . . . . . . . . . . 12
31	1, 30	syl 16	. . . . . . . . . . 11
32		f1of 5816	. . . . . . . . . . 11
33	31, 32	syl 16	. . . . . . . . . 10
34		fco 5741	. . . . . . . . . 10 $/\$
35	29, 33, 34	syl2anc 661	. . . . . . . . 9
36		fcoi1 5759	. . . . . . . . 9
37	35, 36	syl 16	. . . . . . . 8
38	27, 37	eqtrd 2508	. . . . . . 7
39	24, 38	syl5req 2521	. . . . . 6
40	39	ad2antrr 725	. . . . 5 $/\$ $\$ $/\$
41		psgnunilem1.a	. . . . . 6 $\$
42	41	ad2antrr 725	. . . . 5 $/\$ $\$ $/\$ $\$
43	18	adantr 465	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$
44	31	adantr 465	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$
45	2, 3	pmtrfb 16296	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
46	45	simp3bi 1013	. . . . . . . . . . . 12 $\$
47	12, 46	syl 16	. . . . . . . . . . 11 $\$
48	47	adantr 465	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$ $\$
49		2onn 7289	. . . . . . . . . . . . . . 15
50		nnfi 7710	. . . . . . . . . . . . . . 15
51	49, 50	ax-mp 5	. . . . . . . . . . . . . 14
52	2, 3	pmtrfb 16296	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$
53	52	simp3bi 1013	. . . . . . . . . . . . . . . 16 $\$
54	1, 53	syl 16	. . . . . . . . . . . . . . 15 $\$
55		enfi 7736	. . . . . . . . . . . . . . 15 $\$ $\$
56	54, 55	syl 16	. . . . . . . . . . . . . 14 $\$
57	51, 56	mpbiri 233	. . . . . . . . . . . . 13 $\$
58	57	adantr 465	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $\$
59	41	adantr 465	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $\$ $\$
60		en2eleq 8386	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$ $\$
61	59, 48, 60	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
62		simprl 755	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $\$ $\$
63		f1ofn 5817	. . . . . . . . . . . . . . . . . 18
64	18, 63	syl 16	. . . . . . . . . . . . . . . . 17
65	64	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$
66		imassrn 5348	. . . . . . . . . . . . . . . . . . 19 $\$
67		frn 5737	. . . . . . . . . . . . . . . . . . 19
68	66, 67	syl5ss 3515	. . . . . . . . . . . . . . . . . 18 $\$
69	29, 68	syl 16	. . . . . . . . . . . . . . . . 17 $\$
70	69	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$ $\$
71		simprr 756	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$ $\$
72		fnfvima 6138	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$ $\$
73	65, 70, 71, 72	syl3anc 1228	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $\$ $\$
74		difss 3631	. . . . . . . . . . . . . . . . . . . . 21 $\$
75		dmss 5202	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
76	74, 75	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 $\$
77		f1odm 5820	. . . . . . . . . . . . . . . . . . . . 21
78	18, 77	syl 16	. . . . . . . . . . . . . . . . . . . 20
79	76, 78	syl5sseq 3552	. . . . . . . . . . . . . . . . . . 19 $\$
80	79, 41	sseldd 3505	. . . . . . . . . . . . . . . . . 18
81		eqid 2467	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
82	2, 3, 81	pmtrffv 16290	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$ $\$
83	12, 80, 82	syl2anc 661	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
84		iftrue 3945	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$ $\$ $\$ $\$
85	41, 84	syl 16	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$ $\$ $\$
86	83, 85	eqtrd 2508	. . . . . . . . . . . . . . . 16 $\$ $\$
87	86	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $\$ $\$ $\$
88		imaco 5512	. . . . . . . . . . . . . . . . 17 $\$ $\$
89	26	imaeq1d 5336	. . . . . . . . . . . . . . . . . 18 $\$ $\$
90		difss 3631	. . . . . . . . . . . . . . . . . . . . . 22 $\$
91		dmss 5202	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
92	90, 91	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 $\$
93		f1odm 5820	. . . . . . . . . . . . . . . . . . . . 21
94	92, 93	syl5sseq 3552	. . . . . . . . . . . . . . . . . . . 20 $\$
95	31, 94	syl 16	. . . . . . . . . . . . . . . . . . 19 $\$
96		resiima 5351	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$
97	95, 96	syl 16	. . . . . . . . . . . . . . . . . 18 $\$ $\$
98	89, 97	eqtrd 2508	. . . . . . . . . . . . . . . . 17 $\$ $\$
99	88, 98	syl5eqr 2522	. . . . . . . . . . . . . . . 16 $\$ $\$
100	99	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $\$ $\$ $\$
101	73, 87, 100	3eltr3d 2569	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
102		prssi 4183	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
103	62, 101, 102	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
104	61, 103	eqsstrd 3538	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $\$ $\$
105	54	ensymd 7566	. . . . . . . . . . . . . 14 $\$
106		entr 7567	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$
107	47, 105, 106	syl2anc 661	. . . . . . . . . . . . 13 $\$ $\$
108	107	adantr 465	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $\$ $\$
109		fisseneq 7731	. . . . . . . . . . . 12 $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$
110	58, 104, 108, 109	syl3anc 1228	. . . . . . . . . . 11 $/\$ $\$ $/\$ $\$ $\$ $\$
111	110	eqcomd 2475	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$ $\$ $\$
112		f1otrspeq 16278	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $\$ $\$
113	43, 44, 48, 111, 112	syl22anc 1229	. . . . . . . . 9 $/\$ $\$ $/\$ $\$
114	113	expr 615	. . . . . . . 8 $/\$ $\$ $\$
115	114	necon3ad 2677	. . . . . . 7 $/\$ $\$ $\$
116	115	imp 429	. . . . . 6 $/\$ $\$ $/\$ $\$
117	16	difeq1d 3621	. . . . . . . . . 10 $\$ $\$
118	117	dmeqd 5205	. . . . . . . . 9 $\$ $\$
119		f1omvdconj 16277	. . . . . . . . . 10 $/\$ $\$ $\$
120	33, 18, 119	syl2anc 661	. . . . . . . . 9 $\$ $\$
121	118, 120	eqtrd 2508	. . . . . . . 8 $\$ $\$
122	121	eleq2d 2537	. . . . . . 7 $\$ $\$
123	122	ad2antrr 725	. . . . . 6 $/\$ $\$ $/\$ $\$ $\$
124	116, 123	mtbird 301	. . . . 5 $/\$ $\$ $/\$ $\$
125		coeq1 5160	. . . . . . . 8
126	125	eqeq2d 2481	. . . . . . 7
127		difeq1 3615	. . . . . . . . . 10 $\$ $\$
128	127	dmeqd 5205	. . . . . . . . 9 $\$ $\$
129	128	eleq2d 2537	. . . . . . . 8 $\$ $\$
130	129	notbid 294	. . . . . . 7 $\$ $\$
131	126, 130	3anbi13d 1301	. . . . . 6 $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
132		coeq2 5161	. . . . . . . 8
133	132	eqeq2d 2481	. . . . . . 7
134		difeq1 3615	. . . . . . . . 9 $\$ $\$
135	134	dmeqd 5205	. . . . . . . 8 $\$ $\$
136	135	eleq2d 2537	. . . . . . 7 $\$ $\$
137	133, 136	3anbi12d 1300	. . . . . 6 $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
138	131, 137	rspc2ev 3225	. . . . 5 $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
139	22, 23, 40, 42, 124, 138	syl113anc 1240	. . . 4 $/\$ $\$ $/\$ $/\$ $\$ $/\$ $\$
140	139	olcd 393	. . 3 $/\$ $\$ $/\$ $\/$ $/\$ $\$ $/\$ $\$
141	11, 140	pm2.61dane 2785	. 2 $/\$ $\$ $\/$ $/\$ $\$ $/\$ $\$
142	1	adantr 465	. . . 4 $/\$ $\$
143		coass 5526	. . . . . . 7
144	2, 3	pmtrfcnv 16295	. . . . . . . . . 10
145	1, 144	syl 16	. . . . . . . . 9
146	145	eqcomd 2475	. . . . . . . 8
147	146	coeq2d 5165	. . . . . . 7
148	143, 147	syl5eqr 2522	. . . . . 6
149	2, 3	pmtrfconj 16297	. . . . . . 7 $/\$
150	12, 31, 149	syl2anc 661	. . . . . 6
151	148, 150	eqeltrd 2555	. . . . 5
152	151	adantr 465	. . . 4 $/\$ $\$
153	5	coeq1d 5164	. . . . . . 7
154		fcoi2 5760	. . . . . . . 8
155	35, 154	syl 16	. . . . . . 7
156	153, 155	eqtr2d 2509	. . . . . 6
157		coass 5526	. . . . . 6
158	156, 157	syl6eq 2524	. . . . 5
159	158	adantr 465	. . . 4 $/\$ $\$
160		f1ofn 5817	. . . . . . . . . 10
161	31, 160	syl 16	. . . . . . . . 9
162		fnelnfp 6091	. . . . . . . . 9 $/\$ $\$
163	161, 80, 162	syl2anc 661	. . . . . . . 8 $\$
164	163	necon2bbid 2723	. . . . . . 7 $\$
165	164	biimpar 485	. . . . . 6 $/\$ $\$
166		fnfvima 6138	. . . . . . . 8 $/\$ $\$ $/\$ $\$ $\$
167	161, 79, 41, 166	syl3anc 1228	. . . . . . 7 $\$
168	167	adantr 465	. . . . . 6 $/\$ $\$ $\$
169	165, 168	eqeltrrd 2556	. . . . 5 $/\$ $\$ $\$
170	148	difeq1d 3621	. . . . . . . 8 $\$ $\$
171	170	dmeqd 5205	. . . . . . 7 $\$ $\$
172		f1omvdconj 16277	. . . . . . . 8 $/\$ $\$ $\$
173	29, 31, 172	syl2anc 661	. . . . . . 7 $\$ $\$
174	171, 173	eqtrd 2508	. . . . . 6 $\$ $\$
175	174	adantr 465	. . . . 5 $/\$ $\$ $\$ $\$
176	169, 175	eleqtrrd 2558	. . . 4 $/\$ $\$ $\$
177		simpr 461	. . . 4 $/\$ $\$ $\$
178		coeq1 5160	. . . . . . 7
179	178	eqeq2d 2481	. . . . . 6
180		difeq1 3615	. . . . . . . . 9 $\$ $\$
181	180	dmeqd 5205	. . . . . . . 8 $\$ $\$
182	181	eleq2d 2537	. . . . . . 7 $\$ $\$
183	182	notbid 294	. . . . . 6 $\$ $\$
184	179, 183	3anbi13d 1301	. . . . 5 $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
185		coeq2 5161	. . . . . . 7
186	185	eqeq2d 2481	. . . . . 6
187		difeq1 3615	. . . . . . . 8 $\$ $\$
188	187	dmeqd 5205	. . . . . . 7 $\$ $\$
189	188	eleq2d 2537	. . . . . 6 $\$ $\$
190	186, 189	3anbi12d 1300	. . . . 5 $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
191	184, 190	rspc2ev 3225	. . . 4 $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
192	142, 152, 159, 176, 177, 191	syl113anc 1240	. . 3 $/\$ $\$ $/\$ $\$ $/\$ $\$
193	192	olcd 393	. 2 $/\$ $\$ $\/$ $/\$ $\$ $/\$ $\$
194	141, 193	pm2.61dan 789	1 $\/$ $/\$ $\$ $/\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369 $/\$ w3a 973

wceq 1379

wcel 1767

wne 2662

wrex 2815

cvv 3113 $\$ cdif 3473

wss 3476

cif 3939

csn 4027

cpr 4029

cuni 4245 class class class wbr 4447

cid 4790

ccnv 4998

cdm 4999

crn 5000

cres 5001

cima 5002

ccom 5003

wfn 5583

wf 5584

wf1o 5587

cfv 5588

com 6684

c2o 7124

cen 7513

cfn 7516 pmTrspcpmtr 16272

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6576

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-ral 2819 df-rex 2820 df-reu 2821 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-om 6685 df-1o 7130 df-2o 7131 df-er 7311 df-en 7517 df-dom 7518 df-sdom 7519 df-fin 7520 df-pmtr 16273

This theorem is referenced by: psgnunilem2 16326

W3C validator