psgnunilem1 - Metamath Proof Explorer

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

Theorem psgnunilem1 17145

Description: Lemma for psgnuni 17151. 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 2452	. . . . . . . . 9 pmTrsp pmTrsp
3		psgnunilem1.t	. . . . . . . . 9 pmTrsp
4	2, 3	pmtrfinv 17113	. . . . . . . 8
5	1, 4	syl 17	. . . . . . 7
6		coeq1 4970	. . . . . . . 8
7	6	eqeq1d 2454	. . . . . . 7
8	5, 7	syl5ibrcom 230	. . . . . 6
9	8	adantr 471	. . . . 5 $/\$ $\$
10	9	imp 435	. . . 4 $/\$ $\$ $/\$
11	10	orcd 398	. . 3 $/\$ $\$ $/\$ $\/$ $/\$ $\$ $/\$ $\$
12		psgnunilem1.p	. . . . . . . . . 10
13	2, 3	pmtrfcnv 17116	. . . . . . . . . 10
14	12, 13	syl 17	. . . . . . . . 9
15	14	eqcomd 2458	. . . . . . . 8
16	15	coeq2d 4975	. . . . . . 7
17	2, 3	pmtrff1o 17115	. . . . . . . . 9
18	12, 17	syl 17	. . . . . . . 8
19	2, 3	pmtrfconj 17118	. . . . . . . 8 $/\$
20	1, 18, 19	syl2anc 671	. . . . . . 7
21	16, 20	eqeltrd 2530	. . . . . 6
22	21	ad2antrr 737	. . . . 5 $/\$ $\$ $/\$
23	12	ad2antrr 737	. . . . 5 $/\$ $\$ $/\$
24		coass 5333	. . . . . . 7
25	2, 3	pmtrfinv 17113	. . . . . . . . . 10
26	12, 25	syl 17	. . . . . . . . 9
27	26	coeq2d 4975	. . . . . . . 8
28		f1of 5797	. . . . . . . . . . 11
29	18, 28	syl 17	. . . . . . . . . 10
30	2, 3	pmtrff1o 17115	. . . . . . . . . . . 12
31	1, 30	syl 17	. . . . . . . . . . 11
32		f1of 5797	. . . . . . . . . . 11
33	31, 32	syl 17	. . . . . . . . . 10
34		fco 5722	. . . . . . . . . 10 $/\$
35	29, 33, 34	syl2anc 671	. . . . . . . . 9
36		fcoi1 5740	. . . . . . . . 9
37	35, 36	syl 17	. . . . . . . 8
38	27, 37	eqtrd 2486	. . . . . . 7
39	24, 38	syl5req 2499	. . . . . 6
40	39	ad2antrr 737	. . . . 5 $/\$ $\$ $/\$
41		psgnunilem1.a	. . . . . 6 $\$
42	41	ad2antrr 737	. . . . 5 $/\$ $\$ $/\$ $\$
43	18	adantr 471	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$
44	31	adantr 471	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$
45	2, 3	pmtrfb 17117	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
46	45	simp3bi 1026	. . . . . . . . . . . 12 $\$
47	12, 46	syl 17	. . . . . . . . . . 11 $\$
48	47	adantr 471	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$ $\$
49		2onn 7328	. . . . . . . . . . . . . . 15
50		nnfi 7752	. . . . . . . . . . . . . . 15
51	49, 50	ax-mp 5	. . . . . . . . . . . . . 14
52	2, 3	pmtrfb 17117	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$
53	52	simp3bi 1026	. . . . . . . . . . . . . . . 16 $\$
54	1, 53	syl 17	. . . . . . . . . . . . . . 15 $\$
55		enfi 7775	. . . . . . . . . . . . . . 15 $\$ $\$
56	54, 55	syl 17	. . . . . . . . . . . . . 14 $\$
57	51, 56	mpbiri 241	. . . . . . . . . . . . 13 $\$
58	57	adantr 471	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $\$
59	41	adantr 471	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $\$ $\$
60		en2eleq 8426	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$ $\$
61	59, 48, 60	syl2anc 671	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
62		simprl 769	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $\$ $\$
63		f1ofn 5798	. . . . . . . . . . . . . . . . . 18
64	18, 63	syl 17	. . . . . . . . . . . . . . . . 17
65	64	adantr 471	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$
66		imassrn 5157	. . . . . . . . . . . . . . . . . . 19 $\$
67		frn 5718	. . . . . . . . . . . . . . . . . . 19
68	66, 67	syl5ss 3411	. . . . . . . . . . . . . . . . . 18 $\$
69	29, 68	syl 17	. . . . . . . . . . . . . . . . 17 $\$
70	69	adantr 471	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$ $\$
71		simprr 771	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$ $\$
72		fnfvima 6129	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$ $\$
73	65, 70, 71, 72	syl3anc 1271	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $\$ $\$
74		difss 3528	. . . . . . . . . . . . . . . . . . . . 21 $\$
75		dmss 5012	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
76	74, 75	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 $\$
77		f1odm 5801	. . . . . . . . . . . . . . . . . . . . 21
78	18, 77	syl 17	. . . . . . . . . . . . . . . . . . . 20
79	76, 78	syl5sseq 3448	. . . . . . . . . . . . . . . . . . 19 $\$
80	79, 41	sseldd 3401	. . . . . . . . . . . . . . . . . 18
81		eqid 2452	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
82	2, 3, 81	pmtrffv 17111	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$ $\$
83	12, 80, 82	syl2anc 671	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
84	41	iftrued 3857	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$ $\$ $\$
85	83, 84	eqtrd 2486	. . . . . . . . . . . . . . . 16 $\$ $\$
86	85	adantr 471	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $\$ $\$ $\$
87		imaco 5319	. . . . . . . . . . . . . . . . 17 $\$ $\$
88	26	imaeq1d 5145	. . . . . . . . . . . . . . . . . 18 $\$ $\$
89		difss 3528	. . . . . . . . . . . . . . . . . . . . . 22 $\$
90		dmss 5012	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
91	89, 90	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 $\$
92		f1odm 5801	. . . . . . . . . . . . . . . . . . . . 21
93	91, 92	syl5sseq 3448	. . . . . . . . . . . . . . . . . . . 20 $\$
94	31, 93	syl 17	. . . . . . . . . . . . . . . . . . 19 $\$
95		resiima 5160	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$
96	94, 95	syl 17	. . . . . . . . . . . . . . . . . 18 $\$ $\$
97	88, 96	eqtrd 2486	. . . . . . . . . . . . . . . . 17 $\$ $\$
98	87, 97	syl5eqr 2500	. . . . . . . . . . . . . . . 16 $\$ $\$
99	98	adantr 471	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $\$ $\$ $\$
100	73, 86, 99	3eltr3d 2544	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
101		prssi 4097	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
102	62, 100, 101	syl2anc 671	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
103	61, 102	eqsstrd 3434	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $\$ $\$
104	54	ensymd 7607	. . . . . . . . . . . . . 14 $\$
105		entr 7608	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$
106	47, 104, 105	syl2anc 671	. . . . . . . . . . . . 13 $\$ $\$
107	106	adantr 471	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $\$ $\$
108		fisseneq 7770	. . . . . . . . . . . 12 $\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$
109	58, 103, 107, 108	syl3anc 1271	. . . . . . . . . . 11 $/\$ $\$ $/\$ $\$ $\$ $\$
110	109	eqcomd 2458	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$ $\$ $\$
111		f1otrspeq 17099	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$ $\$ $\$
112	43, 44, 48, 110, 111	syl22anc 1272	. . . . . . . . 9 $/\$ $\$ $/\$ $\$
113	112	expr 624	. . . . . . . 8 $/\$ $\$ $\$
114	113	necon3ad 2637	. . . . . . 7 $/\$ $\$ $\$
115	114	imp 435	. . . . . 6 $/\$ $\$ $/\$ $\$
116	16	difeq1d 3518	. . . . . . . . . 10 $\$ $\$
117	116	dmeqd 5015	. . . . . . . . 9 $\$ $\$
118		f1omvdconj 17098	. . . . . . . . . 10 $/\$ $\$ $\$
119	33, 18, 118	syl2anc 671	. . . . . . . . 9 $\$ $\$
120	117, 119	eqtrd 2486	. . . . . . . 8 $\$ $\$
121	120	eleq2d 2515	. . . . . . 7 $\$ $\$
122	121	ad2antrr 737	. . . . . 6 $/\$ $\$ $/\$ $\$ $\$
123	115, 122	mtbird 307	. . . . 5 $/\$ $\$ $/\$ $\$
124		coeq1 4970	. . . . . . . 8
125	124	eqeq2d 2462	. . . . . . 7
126		difeq1 3512	. . . . . . . . . 10 $\$ $\$
127	126	dmeqd 5015	. . . . . . . . 9 $\$ $\$
128	127	eleq2d 2515	. . . . . . . 8 $\$ $\$
129	128	notbid 300	. . . . . . 7 $\$ $\$
130	125, 129	3anbi13d 1345	. . . . . 6 $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
131		coeq2 4971	. . . . . . . 8
132	131	eqeq2d 2462	. . . . . . 7
133		difeq1 3512	. . . . . . . . 9 $\$ $\$
134	133	dmeqd 5015	. . . . . . . 8 $\$ $\$
135	134	eleq2d 2515	. . . . . . 7 $\$ $\$
136	132, 135	3anbi12d 1344	. . . . . 6 $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
137	130, 136	rspc2ev 3129	. . . . 5 $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
138	22, 23, 40, 42, 123, 137	syl113anc 1283	. . . 4 $/\$ $\$ $/\$ $/\$ $\$ $/\$ $\$
139	138	olcd 399	. . 3 $/\$ $\$ $/\$ $\/$ $/\$ $\$ $/\$ $\$
140	11, 139	pm2.61dane 2711	. 2 $/\$ $\$ $\/$ $/\$ $\$ $/\$ $\$
141	1	adantr 471	. . . 4 $/\$ $\$
142		coass 5333	. . . . . . 7
143	2, 3	pmtrfcnv 17116	. . . . . . . . . 10
144	1, 143	syl 17	. . . . . . . . 9
145	144	eqcomd 2458	. . . . . . . 8
146	145	coeq2d 4975	. . . . . . 7
147	142, 146	syl5eqr 2500	. . . . . 6
148	2, 3	pmtrfconj 17118	. . . . . . 7 $/\$
149	12, 31, 148	syl2anc 671	. . . . . 6
150	147, 149	eqeltrd 2530	. . . . 5
151	150	adantr 471	. . . 4 $/\$ $\$
152	5	coeq1d 4974	. . . . . . 7
153		fcoi2 5741	. . . . . . . 8
154	35, 153	syl 17	. . . . . . 7
155	152, 154	eqtr2d 2487	. . . . . 6
156		coass 5333	. . . . . 6
157	155, 156	syl6eq 2502	. . . . 5
158	157	adantr 471	. . . 4 $/\$ $\$
159		f1ofn 5798	. . . . . . . . . 10
160	31, 159	syl 17	. . . . . . . . 9
161		fnelnfp 6079	. . . . . . . . 9 $/\$ $\$
162	160, 80, 161	syl2anc 671	. . . . . . . 8 $\$
163	162	necon2bbid 2667	. . . . . . 7 $\$
164	163	biimpar 492	. . . . . 6 $/\$ $\$
165		fnfvima 6129	. . . . . . . 8 $/\$ $\$ $/\$ $\$ $\$
166	160, 79, 41, 165	syl3anc 1271	. . . . . . 7 $\$
167	166	adantr 471	. . . . . 6 $/\$ $\$ $\$
168	164, 167	eqeltrrd 2531	. . . . 5 $/\$ $\$ $\$
169	147	difeq1d 3518	. . . . . . . 8 $\$ $\$
170	169	dmeqd 5015	. . . . . . 7 $\$ $\$
171		f1omvdconj 17098	. . . . . . . 8 $/\$ $\$ $\$
172	29, 31, 171	syl2anc 671	. . . . . . 7 $\$ $\$
173	170, 172	eqtrd 2486	. . . . . 6 $\$ $\$
174	173	adantr 471	. . . . 5 $/\$ $\$ $\$ $\$
175	168, 174	eleqtrrd 2533	. . . 4 $/\$ $\$ $\$
176		simpr 467	. . . 4 $/\$ $\$ $\$
177		coeq1 4970	. . . . . . 7
178	177	eqeq2d 2462	. . . . . 6
179		difeq1 3512	. . . . . . . . 9 $\$ $\$
180	179	dmeqd 5015	. . . . . . . 8 $\$ $\$
181	180	eleq2d 2515	. . . . . . 7 $\$ $\$
182	181	notbid 300	. . . . . 6 $\$ $\$
183	178, 182	3anbi13d 1345	. . . . 5 $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
184		coeq2 4971	. . . . . . 7
185	184	eqeq2d 2462	. . . . . 6
186		difeq1 3512	. . . . . . . 8 $\$ $\$
187	186	dmeqd 5015	. . . . . . 7 $\$ $\$
188	187	eleq2d 2515	. . . . . 6 $\$ $\$
189	185, 188	3anbi12d 1344	. . . . 5 $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
190	183, 189	rspc2ev 3129	. . . 4 $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
191	141, 151, 158, 175, 176, 190	syl113anc 1283	. . 3 $/\$ $\$ $/\$ $\$ $/\$ $\$
192	191	olcd 399	. 2 $/\$ $\$ $\/$ $/\$ $\$ $/\$ $\$
193	140, 192	pm2.61dan 805	1 $\/$ $/\$ $\$ $/\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $\/$ wo 374 $/\$ wa 375 $/\$ w3a 986

wceq 1448

wcel 1891

wne 2622

wrex 2738

cvv 3013 $\$ cdif 3369

wss 3372

cif 3849

csn 3936

cpr 3938

cuni 4168 class class class wbr 4374

cid 4722

ccnv 4811

cdm 4812

crn 4813

cres 4814

cima 4815

ccom 4816

wfn 5556

wf 5557

wf1o 5560

cfv 5561

com 6680

c2o 7163

cen 7553

cfn 7556 pmTrspcpmtr 17093

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1673 ax-4 1686 ax-5 1762 ax-6 1809 ax-7 1855 ax-8 1893 ax-9 1900 ax-10 1919 ax-11 1924 ax-12 1937 ax-13 2092 ax-ext 2432 ax-rep 4487 ax-sep 4497 ax-nul 4506 ax-pow 4554 ax-pr 4612 ax-un 6571

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 987 df-3an 988 df-tru 1451 df-ex 1668 df-nf 1672 df-sb 1802 df-eu 2304 df-mo 2305 df-clab 2439 df-cleq 2445 df-clel 2448 df-nfc 2582 df-ne 2624 df-ral 2742 df-rex 2743 df-reu 2744 df-rab 2746 df-v 3015 df-sbc 3236 df-csb 3332 df-dif 3375 df-un 3377 df-in 3379 df-ss 3386 df-pss 3388 df-nul 3700 df-if 3850 df-pw 3921 df-sn 3937 df-pr 3939 df-tp 3941 df-op 3943 df-uni 4169 df-iun 4250 df-br 4375 df-opab 4434 df-mpt 4435 df-tr 4470 df-eprel 4723 df-id 4727 df-po 4733 df-so 4734 df-fr 4771 df-we 4773 df-xp 4818 df-rel 4819 df-cnv 4820 df-co 4821 df-dm 4822 df-rn 4823 df-res 4824 df-ima 4825 df-ord 5405 df-on 5406 df-lim 5407 df-suc 5408 df-iota 5525 df-fun 5563 df-fn 5564 df-f 5565 df-f1 5566 df-fo 5567 df-f1o 5568 df-fv 5569 df-om 6681 df-1o 7169 df-2o 7170 df-er 7350 df-en 7557 df-dom 7558 df-sdom 7559 df-fin 7560 df-pmtr 17094

This theorem is referenced by: psgnunilem2 17147

W3C validator