psgnunilem1 - Metamath Proof Explorer

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

Theorem psgnunilem1 16645

Description: Lemma for psgnuni 16651. 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 2457	. . . . . . . . 9 pmTrsp pmTrsp
3		psgnunilem1.t	. . . . . . . . 9 pmTrsp
4	2, 3	pmtrfinv 16613	. . . . . . . 8
5	1, 4	syl 16	. . . . . . 7
6		coeq1 5170	. . . . . . . 8
7	6	eqeq1d 2459	. . . . . . 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 16616	. . . . . . . . . 10
14	12, 13	syl 16	. . . . . . . . 9
15	14	eqcomd 2465	. . . . . . . 8
16	15	coeq2d 5175	. . . . . . 7
17	2, 3	pmtrff1o 16615	. . . . . . . . 9
18	12, 17	syl 16	. . . . . . . 8
19	2, 3	pmtrfconj 16618	. . . . . . . 8 $/\$
20	1, 18, 19	syl2anc 661	. . . . . . 7
21	16, 20	eqeltrd 2545	. . . . . 6
22	21	ad2antrr 725	. . . . 5 $/\$ $\$ $/\$
23	12	ad2antrr 725	. . . . 5 $/\$ $\$ $/\$
24		coass 5532	. . . . . . 7
25	2, 3	pmtrfinv 16613	. . . . . . . . . 10
26	12, 25	syl 16	. . . . . . . . 9
27	26	coeq2d 5175	. . . . . . . 8
28		f1of 5822	. . . . . . . . . . 11
29	18, 28	syl 16	. . . . . . . . . 10
30	2, 3	pmtrff1o 16615	. . . . . . . . . . . 12
31	1, 30	syl 16	. . . . . . . . . . 11
32		f1of 5822	. . . . . . . . . . 11
33	31, 32	syl 16	. . . . . . . . . 10
34		fco 5747	. . . . . . . . . 10 $/\$
35	29, 33, 34	syl2anc 661	. . . . . . . . 9
36		fcoi1 5765	. . . . . . . . 9
37	35, 36	syl 16	. . . . . . . 8
38	27, 37	eqtrd 2498	. . . . . . 7
39	24, 38	syl5req 2511	. . . . . 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 16617	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
46	45	simp3bi 1013	. . . . . . . . . . . 12 $\$
47	12, 46	syl 16	. . . . . . . . . . 11 $\$
48	47	adantr 465	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$ $\$
49		2onn 7307	. . . . . . . . . . . . . . 15
50		nnfi 7729	. . . . . . . . . . . . . . 15
51	49, 50	ax-mp 5	. . . . . . . . . . . . . 14
52	2, 3	pmtrfb 16617	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$
53	52	simp3bi 1013	. . . . . . . . . . . . . . . 16 $\$
54	1, 53	syl 16	. . . . . . . . . . . . . . 15 $\$
55		enfi 7755	. . . . . . . . . . . . . . 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 8403	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$ $\$
61	59, 48, 60	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
62		simprl 756	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $\$ $\$
63		f1ofn 5823	. . . . . . . . . . . . . . . . . 18
64	18, 63	syl 16	. . . . . . . . . . . . . . . . 17
65	64	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$
66		imassrn 5358	. . . . . . . . . . . . . . . . . . 19 $\$
67		frn 5743	. . . . . . . . . . . . . . . . . . 19
68	66, 67	syl5ss 3510	. . . . . . . . . . . . . . . . . 18 $\$
69	29, 68	syl 16	. . . . . . . . . . . . . . . . 17 $\$
70	69	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$ $\$
71		simprr 757	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$ $\$
72		fnfvima 6151	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$ $\$
73	65, 70, 71, 72	syl3anc 1228	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $\$ $\$
74		difss 3627	. . . . . . . . . . . . . . . . . . . . 21 $\$
75		dmss 5212	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
76	74, 75	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 $\$
77		f1odm 5826	. . . . . . . . . . . . . . . . . . . . 21
78	18, 77	syl 16	. . . . . . . . . . . . . . . . . . . 20
79	76, 78	syl5sseq 3547	. . . . . . . . . . . . . . . . . . 19 $\$
80	79, 41	sseldd 3500	. . . . . . . . . . . . . . . . . 18
81		eqid 2457	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
82	2, 3, 81	pmtrffv 16611	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$ $\$
83	12, 80, 82	syl2anc 661	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
84	41	iftrued 3952	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$ $\$ $\$
85	83, 84	eqtrd 2498	. . . . . . . . . . . . . . . 16 $\$ $\$
86	85	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $\$ $\$ $\$
87		imaco 5518	. . . . . . . . . . . . . . . . 17 $\$ $\$
88	26	imaeq1d 5346	. . . . . . . . . . . . . . . . . 18 $\$ $\$
89		difss 3627	. . . . . . . . . . . . . . . . . . . . . 22 $\$
90		dmss 5212	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
91	89, 90	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 $\$
92		f1odm 5826	. . . . . . . . . . . . . . . . . . . . 21
93	91, 92	syl5sseq 3547	. . . . . . . . . . . . . . . . . . . 20 $\$
94	31, 93	syl 16	. . . . . . . . . . . . . . . . . . 19 $\$
95		resiima 5361	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$
96	94, 95	syl 16	. . . . . . . . . . . . . . . . . 18 $\$ $\$
97	88, 96	eqtrd 2498	. . . . . . . . . . . . . . . . 17 $\$ $\$
98	87, 97	syl5eqr 2512	. . . . . . . . . . . . . . . 16 $\$ $\$
99	98	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $\$ $\$ $\$
100	73, 86, 99	3eltr3d 2559	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
101		prssi 4188	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
102	62, 100, 101	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
103	61, 102	eqsstrd 3533	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $\$ $\$
104	54	ensymd 7585	. . . . . . . . . . . . . 14 $\$
105		entr 7586	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$
106	47, 104, 105	syl2anc 661	. . . . . . . . . . . . 13 $\$ $\$
107	106	adantr 465	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $\$ $\$
108		fisseneq 7750	. . . . . . . . . . . 12 $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$
109	58, 103, 107, 108	syl3anc 1228	. . . . . . . . . . 11 $/\$ $\$ $/\$ $\$ $\$ $\$
110	109	eqcomd 2465	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$ $\$ $\$
111		f1otrspeq 16599	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $\$ $\$
112	43, 44, 48, 110, 111	syl22anc 1229	. . . . . . . . 9 $/\$ $\$ $/\$ $\$
113	112	expr 615	. . . . . . . 8 $/\$ $\$ $\$
114	113	necon3ad 2667	. . . . . . 7 $/\$ $\$ $\$
115	114	imp 429	. . . . . 6 $/\$ $\$ $/\$ $\$
116	16	difeq1d 3617	. . . . . . . . . 10 $\$ $\$
117	116	dmeqd 5215	. . . . . . . . 9 $\$ $\$
118		f1omvdconj 16598	. . . . . . . . . 10 $/\$ $\$ $\$
119	33, 18, 118	syl2anc 661	. . . . . . . . 9 $\$ $\$
120	117, 119	eqtrd 2498	. . . . . . . 8 $\$ $\$
121	120	eleq2d 2527	. . . . . . 7 $\$ $\$
122	121	ad2antrr 725	. . . . . 6 $/\$ $\$ $/\$ $\$ $\$
123	115, 122	mtbird 301	. . . . 5 $/\$ $\$ $/\$ $\$
124		coeq1 5170	. . . . . . . 8
125	124	eqeq2d 2471	. . . . . . 7
126		difeq1 3611	. . . . . . . . . 10 $\$ $\$
127	126	dmeqd 5215	. . . . . . . . 9 $\$ $\$
128	127	eleq2d 2527	. . . . . . . 8 $\$ $\$
129	128	notbid 294	. . . . . . 7 $\$ $\$
130	125, 129	3anbi13d 1301	. . . . . 6 $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
131		coeq2 5171	. . . . . . . 8
132	131	eqeq2d 2471	. . . . . . 7
133		difeq1 3611	. . . . . . . . 9 $\$ $\$
134	133	dmeqd 5215	. . . . . . . 8 $\$ $\$
135	134	eleq2d 2527	. . . . . . 7 $\$ $\$
136	132, 135	3anbi12d 1300	. . . . . 6 $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
137	130, 136	rspc2ev 3221	. . . . 5 $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
138	22, 23, 40, 42, 123, 137	syl113anc 1240	. . . 4 $/\$ $\$ $/\$ $/\$ $\$ $/\$ $\$
139	138	olcd 393	. . 3 $/\$ $\$ $/\$ $\/$ $/\$ $\$ $/\$ $\$
140	11, 139	pm2.61dane 2775	. 2 $/\$ $\$ $\/$ $/\$ $\$ $/\$ $\$
141	1	adantr 465	. . . 4 $/\$ $\$
142		coass 5532	. . . . . . 7
143	2, 3	pmtrfcnv 16616	. . . . . . . . . 10
144	1, 143	syl 16	. . . . . . . . 9
145	144	eqcomd 2465	. . . . . . . 8
146	145	coeq2d 5175	. . . . . . 7
147	142, 146	syl5eqr 2512	. . . . . 6
148	2, 3	pmtrfconj 16618	. . . . . . 7 $/\$
149	12, 31, 148	syl2anc 661	. . . . . 6
150	147, 149	eqeltrd 2545	. . . . 5
151	150	adantr 465	. . . 4 $/\$ $\$
152	5	coeq1d 5174	. . . . . . 7
153		fcoi2 5766	. . . . . . . 8
154	35, 153	syl 16	. . . . . . 7
155	152, 154	eqtr2d 2499	. . . . . 6
156		coass 5532	. . . . . 6
157	155, 156	syl6eq 2514	. . . . 5
158	157	adantr 465	. . . 4 $/\$ $\$
159		f1ofn 5823	. . . . . . . . . 10
160	31, 159	syl 16	. . . . . . . . 9
161		fnelnfp 6102	. . . . . . . . 9 $/\$ $\$
162	160, 80, 161	syl2anc 661	. . . . . . . 8 $\$
163	162	necon2bbid 2713	. . . . . . 7 $\$
164	163	biimpar 485	. . . . . 6 $/\$ $\$
165		fnfvima 6151	. . . . . . . 8 $/\$ $\$ $/\$ $\$ $\$
166	160, 79, 41, 165	syl3anc 1228	. . . . . . 7 $\$
167	166	adantr 465	. . . . . 6 $/\$ $\$ $\$
168	164, 167	eqeltrrd 2546	. . . . 5 $/\$ $\$ $\$
169	147	difeq1d 3617	. . . . . . . 8 $\$ $\$
170	169	dmeqd 5215	. . . . . . 7 $\$ $\$
171		f1omvdconj 16598	. . . . . . . 8 $/\$ $\$ $\$
172	29, 31, 171	syl2anc 661	. . . . . . 7 $\$ $\$
173	170, 172	eqtrd 2498	. . . . . 6 $\$ $\$
174	173	adantr 465	. . . . 5 $/\$ $\$ $\$ $\$
175	168, 174	eleqtrrd 2548	. . . 4 $/\$ $\$ $\$
176		simpr 461	. . . 4 $/\$ $\$ $\$
177		coeq1 5170	. . . . . . 7
178	177	eqeq2d 2471	. . . . . 6
179		difeq1 3611	. . . . . . . . 9 $\$ $\$
180	179	dmeqd 5215	. . . . . . . 8 $\$ $\$
181	180	eleq2d 2527	. . . . . . 7 $\$ $\$
182	181	notbid 294	. . . . . 6 $\$ $\$
183	178, 182	3anbi13d 1301	. . . . 5 $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
184		coeq2 5171	. . . . . . 7
185	184	eqeq2d 2471	. . . . . 6
186		difeq1 3611	. . . . . . . 8 $\$ $\$
187	186	dmeqd 5215	. . . . . . 7 $\$ $\$
188	187	eleq2d 2527	. . . . . 6 $\$ $\$
189	185, 188	3anbi12d 1300	. . . . 5 $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
190	183, 189	rspc2ev 3221	. . . 4 $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
191	141, 151, 158, 175, 176, 190	syl113anc 1240	. . 3 $/\$ $\$ $/\$ $\$ $/\$ $\$
192	191	olcd 393	. 2 $/\$ $\$ $\/$ $/\$ $\$ $/\$ $\$
193	140, 192	pm2.61dan 791	1 $\/$ $/\$ $\$ $/\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1395

wcel 1819

wne 2652

wrex 2808

cvv 3109 $\$ cdif 3468

wss 3471

cif 3944

csn 4032

cpr 4034

cuni 4251 class class class wbr 4456

cid 4799

ccnv 5007

cdm 5008

crn 5009

cres 5010

cima 5011

ccom 5012

wfn 5589

wf 5590

wf1o 5593

cfv 5594

com 6699

c2o 7142

cen 7532

cfn 7535 pmTrspcpmtr 16593

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-ral 2812 df-rex 2813 df-reu 2814 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-om 6700 df-1o 7148 df-2o 7149 df-er 7329 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-pmtr 16594

This theorem is referenced by: psgnunilem2 16647

W3C validator