Metamath Proof Explorer


Theorem psgnunilem1

Description: Lemma for psgnuni . 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)

Ref Expression
Hypotheses psgnunilem1.t T = ran pmTrsp D
psgnunilem1.d φ D V
psgnunilem1.p φ P T
psgnunilem1.q φ Q T
psgnunilem1.a φ A dom P I
Assertion psgnunilem1 φ P Q = I D r T s T P Q = r s A dom s I ¬ A dom r I

Proof

Step Hyp Ref Expression
1 psgnunilem1.t T = ran pmTrsp D
2 psgnunilem1.d φ D V
3 psgnunilem1.p φ P T
4 psgnunilem1.q φ Q T
5 psgnunilem1.a φ A dom P I
6 eqid pmTrsp D = pmTrsp D
7 6 1 pmtrfinv Q T Q Q = I D
8 4 7 syl φ Q Q = I D
9 coeq1 P = Q P Q = Q Q
10 9 eqeq1d P = Q P Q = I D Q Q = I D
11 8 10 syl5ibrcom φ P = Q P Q = I D
12 11 adantr φ A dom Q I P = Q P Q = I D
13 12 imp φ A dom Q I P = Q P Q = I D
14 13 orcd φ A dom Q I P = Q P Q = I D r T s T P Q = r s A dom s I ¬ A dom r I
15 6 1 pmtrfcnv P T P -1 = P
16 3 15 syl φ P -1 = P
17 16 eqcomd φ P = P -1
18 17 coeq2d φ P Q P = P Q P -1
19 6 1 pmtrff1o P T P : D 1-1 onto D
20 3 19 syl φ P : D 1-1 onto D
21 6 1 pmtrfconj Q T P : D 1-1 onto D P Q P -1 T
22 4 20 21 syl2anc φ P Q P -1 T
23 18 22 eqeltrd φ P Q P T
24 23 ad2antrr φ A dom Q I P Q P Q P T
25 3 ad2antrr φ A dom Q I P Q P T
26 coass P Q P P = P Q P P
27 6 1 pmtrfinv P T P P = I D
28 3 27 syl φ P P = I D
29 28 coeq2d φ P Q P P = P Q I D
30 f1of P : D 1-1 onto D P : D D
31 20 30 syl φ P : D D
32 6 1 pmtrff1o Q T Q : D 1-1 onto D
33 4 32 syl φ Q : D 1-1 onto D
34 f1of Q : D 1-1 onto D Q : D D
35 33 34 syl φ Q : D D
36 fco P : D D Q : D D P Q : D D
37 31 35 36 syl2anc φ P Q : D D
38 fcoi1 P Q : D D P Q I D = P Q
39 37 38 syl φ P Q I D = P Q
40 29 39 eqtrd φ P Q P P = P Q
41 26 40 eqtr2id φ P Q = P Q P P
42 41 ad2antrr φ A dom Q I P Q P Q = P Q P P
43 5 ad2antrr φ A dom Q I P Q A dom P I
44 20 adantr φ A dom Q I A P dom Q I P : D 1-1 onto D
45 33 adantr φ A dom Q I A P dom Q I Q : D 1-1 onto D
46 6 1 pmtrfb P T D V P : D 1-1 onto D dom P I 2 𝑜
47 46 simp3bi P T dom P I 2 𝑜
48 3 47 syl φ dom P I 2 𝑜
49 48 adantr φ A dom Q I A P dom Q I dom P I 2 𝑜
50 2onn 2 𝑜 ω
51 nnfi 2 𝑜 ω 2 𝑜 Fin
52 50 51 ax-mp 2 𝑜 Fin
53 6 1 pmtrfb Q T D V Q : D 1-1 onto D dom Q I 2 𝑜
54 53 simp3bi Q T dom Q I 2 𝑜
55 4 54 syl φ dom Q I 2 𝑜
56 enfi dom Q I 2 𝑜 dom Q I Fin 2 𝑜 Fin
57 55 56 syl φ dom Q I Fin 2 𝑜 Fin
58 52 57 mpbiri φ dom Q I Fin
59 58 adantr φ A dom Q I A P dom Q I dom Q I Fin
60 5 adantr φ A dom Q I A P dom Q I A dom P I
61 en2eleq A dom P I dom P I 2 𝑜 dom P I = A dom P I A
62 60 49 61 syl2anc φ A dom Q I A P dom Q I dom P I = A dom P I A
63 simprl φ A dom Q I A P dom Q I A dom Q I
64 f1ofn P : D 1-1 onto D P Fn D
65 20 64 syl φ P Fn D
66 65 adantr φ A dom Q I A P dom Q I P Fn D
67 fimass P : D D P dom Q I D
68 31 67 syl φ P dom Q I D
69 68 adantr φ A dom Q I A P dom Q I P dom Q I D
70 simprr φ A dom Q I A P dom Q I A P dom Q I
71 fnfvima P Fn D P dom Q I D A P dom Q I P A P P dom Q I
72 66 69 70 71 syl3anc φ A dom Q I A P dom Q I P A P P dom Q I
73 difss P I P
74 dmss P I P dom P I dom P
75 73 74 ax-mp dom P I dom P
76 f1odm P : D 1-1 onto D dom P = D
77 20 76 syl φ dom P = D
78 75 77 sseqtrid φ dom P I D
79 78 5 sseldd φ A D
80 eqid dom P I = dom P I
81 6 1 80 pmtrffv P T A D P A = if A dom P I dom P I A A
82 3 79 81 syl2anc φ P A = if A dom P I dom P I A A
83 5 iftrued φ if A dom P I dom P I A A = dom P I A
84 82 83 eqtrd φ P A = dom P I A
85 84 adantr φ A dom Q I A P dom Q I P A = dom P I A
86 imaco P P dom Q I = P P dom Q I
87 28 imaeq1d φ P P dom Q I = I D dom Q I
88 difss Q I Q
89 dmss Q I Q dom Q I dom Q
90 88 89 ax-mp dom Q I dom Q
91 f1odm Q : D 1-1 onto D dom Q = D
92 90 91 sseqtrid Q : D 1-1 onto D dom Q I D
93 33 92 syl φ dom Q I D
94 resiima dom Q I D I D dom Q I = dom Q I
95 93 94 syl φ I D dom Q I = dom Q I
96 87 95 eqtrd φ P P dom Q I = dom Q I
97 86 96 eqtr3id φ P P dom Q I = dom Q I
98 97 adantr φ A dom Q I A P dom Q I P P dom Q I = dom Q I
99 72 85 98 3eltr3d φ A dom Q I A P dom Q I dom P I A dom Q I
100 63 99 prssd φ A dom Q I A P dom Q I A dom P I A dom Q I
101 62 100 eqsstrd φ A dom Q I A P dom Q I dom P I dom Q I
102 55 ensymd φ 2 𝑜 dom Q I
103 entr dom P I 2 𝑜 2 𝑜 dom Q I dom P I dom Q I
104 48 102 103 syl2anc φ dom P I dom Q I
105 104 adantr φ A dom Q I A P dom Q I dom P I dom Q I
106 fisseneq dom Q I Fin dom P I dom Q I dom P I dom Q I dom P I = dom Q I
107 59 101 105 106 syl3anc φ A dom Q I A P dom Q I dom P I = dom Q I
108 107 eqcomd φ A dom Q I A P dom Q I dom Q I = dom P I
109 f1otrspeq P : D 1-1 onto D Q : D 1-1 onto D dom P I 2 𝑜 dom Q I = dom P I P = Q
110 44 45 49 108 109 syl22anc φ A dom Q I A P dom Q I P = Q
111 110 expr φ A dom Q I A P dom Q I P = Q
112 111 necon3ad φ A dom Q I P Q ¬ A P dom Q I
113 112 imp φ A dom Q I P Q ¬ A P dom Q I
114 18 difeq1d φ P Q P I = P Q P -1 I
115 114 dmeqd φ dom P Q P I = dom P Q P -1 I
116 f1omvdconj Q : D D P : D 1-1 onto D dom P Q P -1 I = P dom Q I
117 35 20 116 syl2anc φ dom P Q P -1 I = P dom Q I
118 115 117 eqtrd φ dom P Q P I = P dom Q I
119 118 eleq2d φ A dom P Q P I A P dom Q I
120 119 ad2antrr φ A dom Q I P Q A dom P Q P I A P dom Q I
121 113 120 mtbird φ A dom Q I P Q ¬ A dom P Q P I
122 coeq1 r = P Q P r s = P Q P s
123 122 eqeq2d r = P Q P P Q = r s P Q = P Q P s
124 difeq1 r = P Q P r I = P Q P I
125 124 dmeqd r = P Q P dom r I = dom P Q P I
126 125 eleq2d r = P Q P A dom r I A dom P Q P I
127 126 notbid r = P Q P ¬ A dom r I ¬ A dom P Q P I
128 123 127 3anbi13d r = P Q P P Q = r s A dom s I ¬ A dom r I P Q = P Q P s A dom s I ¬ A dom P Q P I
129 coeq2 s = P P Q P s = P Q P P
130 129 eqeq2d s = P P Q = P Q P s P Q = P Q P P
131 difeq1 s = P s I = P I
132 131 dmeqd s = P dom s I = dom P I
133 132 eleq2d s = P A dom s I A dom P I
134 130 133 3anbi12d s = P P Q = P Q P s A dom s I ¬ A dom P Q P I P Q = P Q P P A dom P I ¬ A dom P Q P I
135 128 134 rspc2ev P Q P T P T P Q = P Q P P A dom P I ¬ A dom P Q P I r T s T P Q = r s A dom s I ¬ A dom r I
136 24 25 42 43 121 135 syl113anc φ A dom Q I P Q r T s T P Q = r s A dom s I ¬ A dom r I
137 136 olcd φ A dom Q I P Q P Q = I D r T s T P Q = r s A dom s I ¬ A dom r I
138 14 137 pm2.61dane φ A dom Q I P Q = I D r T s T P Q = r s A dom s I ¬ A dom r I
139 4 adantr φ ¬ A dom Q I Q T
140 coass Q P Q = Q P Q
141 6 1 pmtrfcnv Q T Q -1 = Q
142 4 141 syl φ Q -1 = Q
143 142 eqcomd φ Q = Q -1
144 143 coeq2d φ Q P Q = Q P Q -1
145 140 144 eqtr3id φ Q P Q = Q P Q -1
146 6 1 pmtrfconj P T Q : D 1-1 onto D Q P Q -1 T
147 3 33 146 syl2anc φ Q P Q -1 T
148 145 147 eqeltrd φ Q P Q T
149 148 adantr φ ¬ A dom Q I Q P Q T
150 8 coeq1d φ Q Q P Q = I D P Q
151 fcoi2 P Q : D D I D P Q = P Q
152 37 151 syl φ I D P Q = P Q
153 150 152 eqtr2d φ P Q = Q Q P Q
154 coass Q Q P Q = Q Q P Q
155 153 154 eqtrdi φ P Q = Q Q P Q
156 155 adantr φ ¬ A dom Q I P Q = Q Q P Q
157 f1ofn Q : D 1-1 onto D Q Fn D
158 33 157 syl φ Q Fn D
159 fnelnfp Q Fn D A D A dom Q I Q A A
160 158 79 159 syl2anc φ A dom Q I Q A A
161 160 necon2bbid φ Q A = A ¬ A dom Q I
162 161 biimpar φ ¬ A dom Q I Q A = A
163 fnfvima Q Fn D dom P I D A dom P I Q A Q dom P I
164 158 78 5 163 syl3anc φ Q A Q dom P I
165 164 adantr φ ¬ A dom Q I Q A Q dom P I
166 162 165 eqeltrrd φ ¬ A dom Q I A Q dom P I
167 145 difeq1d φ Q P Q I = Q P Q -1 I
168 167 dmeqd φ dom Q P Q I = dom Q P Q -1 I
169 f1omvdconj P : D D Q : D 1-1 onto D dom Q P Q -1 I = Q dom P I
170 31 33 169 syl2anc φ dom Q P Q -1 I = Q dom P I
171 168 170 eqtrd φ dom Q P Q I = Q dom P I
172 171 adantr φ ¬ A dom Q I dom Q P Q I = Q dom P I
173 166 172 eleqtrrd φ ¬ A dom Q I A dom Q P Q I
174 simpr φ ¬ A dom Q I ¬ A dom Q I
175 coeq1 r = Q r s = Q s
176 175 eqeq2d r = Q P Q = r s P Q = Q s
177 difeq1 r = Q r I = Q I
178 177 dmeqd r = Q dom r I = dom Q I
179 178 eleq2d r = Q A dom r I A dom Q I
180 179 notbid r = Q ¬ A dom r I ¬ A dom Q I
181 176 180 3anbi13d r = Q P Q = r s A dom s I ¬ A dom r I P Q = Q s A dom s I ¬ A dom Q I
182 coeq2 s = Q P Q Q s = Q Q P Q
183 182 eqeq2d s = Q P Q P Q = Q s P Q = Q Q P Q
184 difeq1 s = Q P Q s I = Q P Q I
185 184 dmeqd s = Q P Q dom s I = dom Q P Q I
186 185 eleq2d s = Q P Q A dom s I A dom Q P Q I
187 183 186 3anbi12d s = Q P Q P Q = Q s A dom s I ¬ A dom Q I P Q = Q Q P Q A dom Q P Q I ¬ A dom Q I
188 181 187 rspc2ev Q T Q P Q T P Q = Q Q P Q A dom Q P Q I ¬ A dom Q I r T s T P Q = r s A dom s I ¬ A dom r I
189 139 149 156 173 174 188 syl113anc φ ¬ A dom Q I r T s T P Q = r s A dom s I ¬ A dom r I
190 189 olcd φ ¬ A dom Q I P Q = I D r T s T P Q = r s A dom s I ¬ A dom r I
191 138 190 pm2.61dan φ P Q = I D r T s T P Q = r s A dom s I ¬ A dom r I