psgnunilem1 - Metamath Proof Explorer

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

Theorem psgnunilem1 16844

Description: Lemma for psgnuni 16850. 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 2404	. . . . . . . . 9 pmTrsp pmTrsp
3		psgnunilem1.t	. . . . . . . . 9 pmTrsp
4	2, 3	pmtrfinv 16812	. . . . . . . 8
5	1, 4	syl 17	. . . . . . 7
6		coeq1 4983	. . . . . . . 8
7	6	eqeq1d 2406	. . . . . . 7
8	5, 7	syl5ibrcom 224	. . . . . 6
9	8	adantr 465	. . . . 5 $/\$ $\$
10	9	imp 429	. . . 4 $/\$ $\$ $/\$
11	10	orcd 392	. . 3 $/\$ $\$ $/\$ $\/$ $/\$ $\$ $/\$ $\$
12		psgnunilem1.p	. . . . . . . . . 10
13	2, 3	pmtrfcnv 16815	. . . . . . . . . 10
14	12, 13	syl 17	. . . . . . . . 9
15	14	eqcomd 2412	. . . . . . . 8
16	15	coeq2d 4988	. . . . . . 7
17	2, 3	pmtrff1o 16814	. . . . . . . . 9
18	12, 17	syl 17	. . . . . . . 8
19	2, 3	pmtrfconj 16817	. . . . . . . 8 $/\$
20	1, 18, 19	syl2anc 661	. . . . . . 7
21	16, 20	eqeltrd 2492	. . . . . 6
22	21	ad2antrr 726	. . . . 5 $/\$ $\$ $/\$
23	12	ad2antrr 726	. . . . 5 $/\$ $\$ $/\$
24		coass 5344	. . . . . . 7
25	2, 3	pmtrfinv 16812	. . . . . . . . . 10
26	12, 25	syl 17	. . . . . . . . 9
27	26	coeq2d 4988	. . . . . . . 8
28		f1of 5801	. . . . . . . . . . 11
29	18, 28	syl 17	. . . . . . . . . 10
30	2, 3	pmtrff1o 16814	. . . . . . . . . . . 12
31	1, 30	syl 17	. . . . . . . . . . 11
32		f1of 5801	. . . . . . . . . . 11
33	31, 32	syl 17	. . . . . . . . . 10
34		fco 5726	. . . . . . . . . 10 $/\$
35	29, 33, 34	syl2anc 661	. . . . . . . . 9
36		fcoi1 5744	. . . . . . . . 9
37	35, 36	syl 17	. . . . . . . 8
38	27, 37	eqtrd 2445	. . . . . . 7
39	24, 38	syl5req 2458	. . . . . 6
40	39	ad2antrr 726	. . . . 5 $/\$ $\$ $/\$
41		psgnunilem1.a	. . . . . 6 $\$
42	41	ad2antrr 726	. . . . 5 $/\$ $\$ $/\$ $\$
43	18	adantr 465	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$
44	31	adantr 465	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$
45	2, 3	pmtrfb 16816	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
46	45	simp3bi 1016	. . . . . . . . . . . 12 $\$
47	12, 46	syl 17	. . . . . . . . . . 11 $\$
48	47	adantr 465	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$ $\$
49		2onn 7328	. . . . . . . . . . . . . . 15
50		nnfi 7750	. . . . . . . . . . . . . . 15
51	49, 50	ax-mp 5	. . . . . . . . . . . . . 14
52	2, 3	pmtrfb 16816	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$
53	52	simp3bi 1016	. . . . . . . . . . . . . . . 16 $\$
54	1, 53	syl 17	. . . . . . . . . . . . . . 15 $\$
55		enfi 7773	. . . . . . . . . . . . . . 15 $\$ $\$
56	54, 55	syl 17	. . . . . . . . . . . . . 14 $\$
57	51, 56	mpbiri 235	. . . . . . . . . . . . 13 $\$
58	57	adantr 465	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $\$
59	41	adantr 465	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $\$ $\$
60		en2eleq 8420	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$ $\$
61	59, 48, 60	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
62		simprl 758	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $\$ $\$
63		f1ofn 5802	. . . . . . . . . . . . . . . . . 18
64	18, 63	syl 17	. . . . . . . . . . . . . . . . 17
65	64	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$
66		imassrn 5170	. . . . . . . . . . . . . . . . . . 19 $\$
67		frn 5722	. . . . . . . . . . . . . . . . . . 19
68	66, 67	syl5ss 3455	. . . . . . . . . . . . . . . . . 18 $\$
69	29, 68	syl 17	. . . . . . . . . . . . . . . . 17 $\$
70	69	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$ $\$
71		simprr 760	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$ $\$
72		fnfvima 6133	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$ $\$
73	65, 70, 71, 72	syl3anc 1232	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $\$ $\$
74		difss 3572	. . . . . . . . . . . . . . . . . . . . 21 $\$
75		dmss 5025	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
76	74, 75	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 $\$
77		f1odm 5805	. . . . . . . . . . . . . . . . . . . . 21
78	18, 77	syl 17	. . . . . . . . . . . . . . . . . . . 20
79	76, 78	syl5sseq 3492	. . . . . . . . . . . . . . . . . . 19 $\$
80	79, 41	sseldd 3445	. . . . . . . . . . . . . . . . . 18
81		eqid 2404	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
82	2, 3, 81	pmtrffv 16810	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$ $\$
83	12, 80, 82	syl2anc 661	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
84	41	iftrued 3895	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$ $\$ $\$
85	83, 84	eqtrd 2445	. . . . . . . . . . . . . . . 16 $\$ $\$
86	85	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $\$ $\$ $\$
87		imaco 5330	. . . . . . . . . . . . . . . . 17 $\$ $\$
88	26	imaeq1d 5158	. . . . . . . . . . . . . . . . . 18 $\$ $\$
89		difss 3572	. . . . . . . . . . . . . . . . . . . . . 22 $\$
90		dmss 5025	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
91	89, 90	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 $\$
92		f1odm 5805	. . . . . . . . . . . . . . . . . . . . 21
93	91, 92	syl5sseq 3492	. . . . . . . . . . . . . . . . . . . 20 $\$
94	31, 93	syl 17	. . . . . . . . . . . . . . . . . . 19 $\$
95		resiima 5173	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$
96	94, 95	syl 17	. . . . . . . . . . . . . . . . . 18 $\$ $\$
97	88, 96	eqtrd 2445	. . . . . . . . . . . . . . . . 17 $\$ $\$
98	87, 97	syl5eqr 2459	. . . . . . . . . . . . . . . 16 $\$ $\$
99	98	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $\$ $\$ $\$
100	73, 86, 99	3eltr3d 2506	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
101		prssi 4130	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
102	62, 100, 101	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
103	61, 102	eqsstrd 3478	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $\$ $\$
104	54	ensymd 7606	. . . . . . . . . . . . . 14 $\$
105		entr 7607	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$
106	47, 104, 105	syl2anc 661	. . . . . . . . . . . . 13 $\$ $\$
107	106	adantr 465	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $\$ $\$
108		fisseneq 7768	. . . . . . . . . . . 12 $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$
109	58, 103, 107, 108	syl3anc 1232	. . . . . . . . . . 11 $/\$ $\$ $/\$ $\$ $\$ $\$
110	109	eqcomd 2412	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$ $\$ $\$
111		f1otrspeq 16798	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $\$ $\$
112	43, 44, 48, 110, 111	syl22anc 1233	. . . . . . . . 9 $/\$ $\$ $/\$ $\$
113	112	expr 615	. . . . . . . 8 $/\$ $\$ $\$
114	113	necon3ad 2615	. . . . . . 7 $/\$ $\$ $\$
115	114	imp 429	. . . . . 6 $/\$ $\$ $/\$ $\$
116	16	difeq1d 3562	. . . . . . . . . 10 $\$ $\$
117	116	dmeqd 5028	. . . . . . . . 9 $\$ $\$
118		f1omvdconj 16797	. . . . . . . . . 10 $/\$ $\$ $\$
119	33, 18, 118	syl2anc 661	. . . . . . . . 9 $\$ $\$
120	117, 119	eqtrd 2445	. . . . . . . 8 $\$ $\$
121	120	eleq2d 2474	. . . . . . 7 $\$ $\$
122	121	ad2antrr 726	. . . . . 6 $/\$ $\$ $/\$ $\$ $\$
123	115, 122	mtbird 301	. . . . 5 $/\$ $\$ $/\$ $\$
124		coeq1 4983	. . . . . . . 8
125	124	eqeq2d 2418	. . . . . . 7
126		difeq1 3556	. . . . . . . . . 10 $\$ $\$
127	126	dmeqd 5028	. . . . . . . . 9 $\$ $\$
128	127	eleq2d 2474	. . . . . . . 8 $\$ $\$
129	128	notbid 294	. . . . . . 7 $\$ $\$
130	125, 129	3anbi13d 1305	. . . . . 6 $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
131		coeq2 4984	. . . . . . . 8
132	131	eqeq2d 2418	. . . . . . 7
133		difeq1 3556	. . . . . . . . 9 $\$ $\$
134	133	dmeqd 5028	. . . . . . . 8 $\$ $\$
135	134	eleq2d 2474	. . . . . . 7 $\$ $\$
136	132, 135	3anbi12d 1304	. . . . . 6 $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
137	130, 136	rspc2ev 3173	. . . . 5 $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
138	22, 23, 40, 42, 123, 137	syl113anc 1244	. . . 4 $/\$ $\$ $/\$ $/\$ $\$ $/\$ $\$
139	138	olcd 393	. . 3 $/\$ $\$ $/\$ $\/$ $/\$ $\$ $/\$ $\$
140	11, 139	pm2.61dane 2723	. 2 $/\$ $\$ $\/$ $/\$ $\$ $/\$ $\$
141	1	adantr 465	. . . 4 $/\$ $\$
142		coass 5344	. . . . . . 7
143	2, 3	pmtrfcnv 16815	. . . . . . . . . 10
144	1, 143	syl 17	. . . . . . . . 9
145	144	eqcomd 2412	. . . . . . . 8
146	145	coeq2d 4988	. . . . . . 7
147	142, 146	syl5eqr 2459	. . . . . 6
148	2, 3	pmtrfconj 16817	. . . . . . 7 $/\$
149	12, 31, 148	syl2anc 661	. . . . . 6
150	147, 149	eqeltrd 2492	. . . . 5
151	150	adantr 465	. . . 4 $/\$ $\$
152	5	coeq1d 4987	. . . . . . 7
153		fcoi2 5745	. . . . . . . 8
154	35, 153	syl 17	. . . . . . 7
155	152, 154	eqtr2d 2446	. . . . . 6
156		coass 5344	. . . . . 6
157	155, 156	syl6eq 2461	. . . . 5
158	157	adantr 465	. . . 4 $/\$ $\$
159		f1ofn 5802	. . . . . . . . . 10
160	31, 159	syl 17	. . . . . . . . 9
161		fnelnfp 6083	. . . . . . . . 9 $/\$ $\$
162	160, 80, 161	syl2anc 661	. . . . . . . 8 $\$
163	162	necon2bbid 2661	. . . . . . 7 $\$
164	163	biimpar 485	. . . . . 6 $/\$ $\$
165		fnfvima 6133	. . . . . . . 8 $/\$ $\$ $/\$ $\$ $\$
166	160, 79, 41, 165	syl3anc 1232	. . . . . . 7 $\$
167	166	adantr 465	. . . . . 6 $/\$ $\$ $\$
168	164, 167	eqeltrrd 2493	. . . . 5 $/\$ $\$ $\$
169	147	difeq1d 3562	. . . . . . . 8 $\$ $\$
170	169	dmeqd 5028	. . . . . . 7 $\$ $\$
171		f1omvdconj 16797	. . . . . . . 8 $/\$ $\$ $\$
172	29, 31, 171	syl2anc 661	. . . . . . 7 $\$ $\$
173	170, 172	eqtrd 2445	. . . . . 6 $\$ $\$
174	173	adantr 465	. . . . 5 $/\$ $\$ $\$ $\$
175	168, 174	eleqtrrd 2495	. . . 4 $/\$ $\$ $\$
176		simpr 461	. . . 4 $/\$ $\$ $\$
177		coeq1 4983	. . . . . . 7
178	177	eqeq2d 2418	. . . . . 6
179		difeq1 3556	. . . . . . . . 9 $\$ $\$
180	179	dmeqd 5028	. . . . . . . 8 $\$ $\$
181	180	eleq2d 2474	. . . . . . 7 $\$ $\$
182	181	notbid 294	. . . . . 6 $\$ $\$
183	178, 182	3anbi13d 1305	. . . . 5 $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
184		coeq2 4984	. . . . . . 7
185	184	eqeq2d 2418	. . . . . 6
186		difeq1 3556	. . . . . . . 8 $\$ $\$
187	186	dmeqd 5028	. . . . . . 7 $\$ $\$
188	187	eleq2d 2474	. . . . . 6 $\$ $\$
189	185, 188	3anbi12d 1304	. . . . 5 $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
190	183, 189	rspc2ev 3173	. . . 4 $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
191	141, 151, 158, 175, 176, 190	syl113anc 1244	. . 3 $/\$ $\$ $/\$ $\$ $/\$ $\$
192	191	olcd 393	. 2 $/\$ $\$ $\/$ $/\$ $\$ $/\$ $\$
193	140, 192	pm2.61dan 794	1 $\/$ $/\$ $\$ $/\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 186 $\/$ wo 368 $/\$ wa 369 $/\$ w3a 976

wceq 1407

wcel 1844

wne 2600

wrex 2757

cvv 3061 $\$ cdif 3413

wss 3416

cif 3887

csn 3974

cpr 3976

cuni 4193 class class class wbr 4397

cid 4735

ccnv 4824

cdm 4825

crn 4826

cres 4827

cima 4828

ccom 4829

wfn 5566

wf 5567

wf1o 5570

cfv 5571

com 6685

c2o 7163

cen 7553

cfn 7556 pmTrspcpmtr 16792

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1641 ax-4 1654 ax-5 1727 ax-6 1773 ax-7 1816 ax-8 1846 ax-9 1848 ax-10 1863 ax-11 1868 ax-12 1880 ax-13 2028 ax-ext 2382 ax-rep 4509 ax-sep 4519 ax-nul 4527 ax-pow 4574 ax-pr 4632 ax-un 6576

This theorem depends on definitions: df-bi 187 df-or 370 df-an 371 df-3or 977 df-3an 978 df-tru 1410 df-ex 1636 df-nf 1640 df-sb 1766 df-eu 2244 df-mo 2245 df-clab 2390 df-cleq 2396 df-clel 2399 df-nfc 2554 df-ne 2602 df-ral 2761 df-rex 2762 df-reu 2763 df-rab 2765 df-v 3063 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-pss 3432 df-nul 3741 df-if 3888 df-pw 3959 df-sn 3975 df-pr 3977 df-tp 3979 df-op 3981 df-uni 4194 df-iun 4275 df-br 4398 df-opab 4456 df-mpt 4457 df-tr 4492 df-eprel 4736 df-id 4740 df-po 4746 df-so 4747 df-fr 4784 df-we 4786 df-xp 4831 df-rel 4832 df-cnv 4833 df-co 4834 df-dm 4835 df-rn 4836 df-res 4837 df-ima 4838 df-ord 5415 df-on 5416 df-lim 5417 df-suc 5418 df-iota 5535 df-fun 5573 df-fn 5574 df-f 5575 df-f1 5576 df-fo 5577 df-f1o 5578 df-fv 5579 df-om 6686 df-1o 7169 df-2o 7170 df-er 7350 df-en 7557 df-dom 7558 df-sdom 7559 df-fin 7560 df-pmtr 16793

This theorem is referenced by: psgnunilem2 16846

W3C validator