Metamath Proof Explorer


Theorem mdetralt

Description: The determinant function is alternating regarding rows: if a matrix has two identical rows, its determinant is 0. Corollary 4.9 in Lang p. 515. (Contributed by SO, 10-Jul-2018) (Proof shortened by AV, 23-Jul-2018)

Ref Expression
Hypotheses mdetralt.d D=NmaDetR
mdetralt.a A=NMatR
mdetralt.b B=BaseA
mdetralt.z 0˙=0R
mdetralt.r φRCRing
mdetralt.x φXB
mdetralt.i φIN
mdetralt.j φJN
mdetralt.ij φIJ
mdetralt.eq φaNIXa=JXa
Assertion mdetralt φDX=0˙

Proof

Step Hyp Ref Expression
1 mdetralt.d D=NmaDetR
2 mdetralt.a A=NMatR
3 mdetralt.b B=BaseA
4 mdetralt.z 0˙=0R
5 mdetralt.r φRCRing
6 mdetralt.x φXB
7 mdetralt.i φIN
8 mdetralt.j φJN
9 mdetralt.ij φIJ
10 mdetralt.eq φaNIXa=JXa
11 eqid BaseSymGrpN=BaseSymGrpN
12 eqid ℤRHomR=ℤRHomR
13 eqid pmSgnN=pmSgnN
14 eqid R=R
15 eqid mulGrpR=mulGrpR
16 1 2 3 11 12 13 14 15 mdetleib XBDX=RpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcXc
17 6 16 syl φDX=RpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcXc
18 eqid BaseR=BaseR
19 eqid +R=+R
20 crngring RCRingRRing
21 5 20 syl φRRing
22 ringcmn RRingRCMnd
23 21 22 syl φRCMnd
24 2 3 matrcl XBNFinRV
25 6 24 syl φNFinRV
26 25 simpld φNFin
27 eqid SymGrpN=SymGrpN
28 27 11 symgbasfi NFinBaseSymGrpNFin
29 26 28 syl φBaseSymGrpNFin
30 21 adantr φpBaseSymGrpNRRing
31 zrhpsgnmhm RRingNFinℤRHomRpmSgnNSymGrpNMndHommulGrpR
32 21 26 31 syl2anc φℤRHomRpmSgnNSymGrpNMndHommulGrpR
33 15 18 mgpbas BaseR=BasemulGrpR
34 11 33 mhmf ℤRHomRpmSgnNSymGrpNMndHommulGrpRℤRHomRpmSgnN:BaseSymGrpNBaseR
35 32 34 syl φℤRHomRpmSgnN:BaseSymGrpNBaseR
36 35 ffvelrnda φpBaseSymGrpNℤRHomRpmSgnNpBaseR
37 15 crngmgp RCRingmulGrpRCMnd
38 5 37 syl φmulGrpRCMnd
39 38 adantr φpBaseSymGrpNmulGrpRCMnd
40 26 adantr φpBaseSymGrpNNFin
41 2 18 3 matbas2i XBXBaseRN×N
42 6 41 syl φXBaseRN×N
43 elmapi XBaseRN×NX:N×NBaseR
44 42 43 syl φX:N×NBaseR
45 44 ad2antrr φpBaseSymGrpNcNX:N×NBaseR
46 27 11 symgbasf1o pBaseSymGrpNp:N1-1 ontoN
47 46 adantl φpBaseSymGrpNp:N1-1 ontoN
48 f1of p:N1-1 ontoNp:NN
49 47 48 syl φpBaseSymGrpNp:NN
50 49 ffvelrnda φpBaseSymGrpNcNpcN
51 simpr φpBaseSymGrpNcNcN
52 45 50 51 fovrnd φpBaseSymGrpNcNpcXcBaseR
53 52 ralrimiva φpBaseSymGrpNcNpcXcBaseR
54 33 39 40 53 gsummptcl φpBaseSymGrpNmulGrpRcNpcXcBaseR
55 18 14 ringcl RRingℤRHomRpmSgnNpBaseRmulGrpRcNpcXcBaseRℤRHomRpmSgnNpRmulGrpRcNpcXcBaseR
56 30 36 54 55 syl3anc φpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcXcBaseR
57 disjdif pmEvenNBaseSymGrpNpmEvenN=
58 57 a1i φpmEvenNBaseSymGrpNpmEvenN=
59 27 11 evpmss pmEvenNBaseSymGrpN
60 undif pmEvenNBaseSymGrpNpmEvenNBaseSymGrpNpmEvenN=BaseSymGrpN
61 59 60 mpbi pmEvenNBaseSymGrpNpmEvenN=BaseSymGrpN
62 61 eqcomi BaseSymGrpN=pmEvenNBaseSymGrpNpmEvenN
63 62 a1i φBaseSymGrpN=pmEvenNBaseSymGrpNpmEvenN
64 eqid pBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcXc=pBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcXc
65 18 19 23 29 56 58 63 64 gsummptfidmsplitres φRpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcXc=RpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcXcpmEvenN+RRpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcXcBaseSymGrpNpmEvenN
66 resmpt pmEvenNBaseSymGrpNpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcXcpmEvenN=ppmEvenNℤRHomRpmSgnNpRmulGrpRcNpcXc
67 59 66 ax-mp pBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcXcpmEvenN=ppmEvenNℤRHomRpmSgnNpRmulGrpRcNpcXc
68 21 adantr φppmEvenNRRing
69 26 adantr φppmEvenNNFin
70 simpr φppmEvenNppmEvenN
71 eqid 1R=1R
72 12 13 71 zrhpsgnevpm RRingNFinppmEvenNℤRHomRpmSgnNp=1R
73 68 69 70 72 syl3anc φppmEvenNℤRHomRpmSgnNp=1R
74 73 oveq1d φppmEvenNℤRHomRpmSgnNpRmulGrpRcNpcXc=1RRmulGrpRcNpcXc
75 59 sseli ppmEvenNpBaseSymGrpN
76 75 54 sylan2 φppmEvenNmulGrpRcNpcXcBaseR
77 18 14 71 ringlidm RRingmulGrpRcNpcXcBaseR1RRmulGrpRcNpcXc=mulGrpRcNpcXc
78 68 76 77 syl2anc φppmEvenN1RRmulGrpRcNpcXc=mulGrpRcNpcXc
79 74 78 eqtrd φppmEvenNℤRHomRpmSgnNpRmulGrpRcNpcXc=mulGrpRcNpcXc
80 79 mpteq2dva φppmEvenNℤRHomRpmSgnNpRmulGrpRcNpcXc=ppmEvenNmulGrpRcNpcXc
81 67 80 eqtrid φpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcXcpmEvenN=ppmEvenNmulGrpRcNpcXc
82 81 oveq2d φRpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcXcpmEvenN=RppmEvenNmulGrpRcNpcXc
83 difss BaseSymGrpNpmEvenNBaseSymGrpN
84 resmpt BaseSymGrpNpmEvenNBaseSymGrpNpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcXcBaseSymGrpNpmEvenN=pBaseSymGrpNpmEvenNℤRHomRpmSgnNpRmulGrpRcNpcXc
85 83 84 ax-mp pBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcXcBaseSymGrpNpmEvenN=pBaseSymGrpNpmEvenNℤRHomRpmSgnNpRmulGrpRcNpcXc
86 21 adantr φpBaseSymGrpNpmEvenNRRing
87 26 adantr φpBaseSymGrpNpmEvenNNFin
88 simpr φpBaseSymGrpNpmEvenNpBaseSymGrpNpmEvenN
89 eqid invgR=invgR
90 12 13 71 11 89 zrhpsgnodpm RRingNFinpBaseSymGrpNpmEvenNℤRHomRpmSgnNp=invgR1R
91 86 87 88 90 syl3anc φpBaseSymGrpNpmEvenNℤRHomRpmSgnNp=invgR1R
92 91 oveq1d φpBaseSymGrpNpmEvenNℤRHomRpmSgnNpRmulGrpRcNpcXc=invgR1RRmulGrpRcNpcXc
93 eldifi pBaseSymGrpNpmEvenNpBaseSymGrpN
94 93 54 sylan2 φpBaseSymGrpNpmEvenNmulGrpRcNpcXcBaseR
95 18 14 71 89 86 94 ringnegl φpBaseSymGrpNpmEvenNinvgR1RRmulGrpRcNpcXc=invgRmulGrpRcNpcXc
96 92 95 eqtrd φpBaseSymGrpNpmEvenNℤRHomRpmSgnNpRmulGrpRcNpcXc=invgRmulGrpRcNpcXc
97 96 mpteq2dva φpBaseSymGrpNpmEvenNℤRHomRpmSgnNpRmulGrpRcNpcXc=pBaseSymGrpNpmEvenNinvgRmulGrpRcNpcXc
98 ringgrp RRingRGrp
99 21 98 syl φRGrp
100 18 89 grpinvf RGrpinvgR:BaseRBaseR
101 99 100 syl φinvgR:BaseRBaseR
102 101 94 cofmpt φinvgRpBaseSymGrpNpmEvenNmulGrpRcNpcXc=pBaseSymGrpNpmEvenNinvgRmulGrpRcNpcXc
103 97 102 eqtr4d φpBaseSymGrpNpmEvenNℤRHomRpmSgnNpRmulGrpRcNpcXc=invgRpBaseSymGrpNpmEvenNmulGrpRcNpcXc
104 85 103 eqtrid φpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcXcBaseSymGrpNpmEvenN=invgRpBaseSymGrpNpmEvenNmulGrpRcNpcXc
105 104 oveq2d φRpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcXcBaseSymGrpNpmEvenN=RinvgRpBaseSymGrpNpmEvenNmulGrpRcNpcXc
106 ringabl RRingRAbel
107 21 106 syl φRAbel
108 difssd φBaseSymGrpNpmEvenNBaseSymGrpN
109 29 108 ssfid φBaseSymGrpNpmEvenNFin
110 eqid pBaseSymGrpNpmEvenNmulGrpRcNpcXc=pBaseSymGrpNpmEvenNmulGrpRcNpcXc
111 18 4 89 107 109 94 110 gsummptfidminv φRinvgRpBaseSymGrpNpmEvenNmulGrpRcNpcXc=invgRRpBaseSymGrpNpmEvenNmulGrpRcNpcXc
112 94 ralrimiva φpBaseSymGrpNpmEvenNmulGrpRcNpcXcBaseR
113 7 8 prssd φIJN
114 pr2nelem INJNIJIJ2𝑜
115 7 8 9 114 syl3anc φIJ2𝑜
116 eqid pmTrspN=pmTrspN
117 eqid ranpmTrspN=ranpmTrspN
118 116 117 pmtrrn NFinIJNIJ2𝑜pmTrspNIJranpmTrspN
119 26 113 115 118 syl3anc φpmTrspNIJranpmTrspN
120 27 11 117 pmtrodpm NFinpmTrspNIJranpmTrspNpmTrspNIJBaseSymGrpNpmEvenN
121 26 119 120 syl2anc φpmTrspNIJBaseSymGrpNpmEvenN
122 27 11 evpmodpmf1o NFinpmTrspNIJBaseSymGrpNpmEvenNqpmEvenNpmTrspNIJ+SymGrpNq:pmEvenN1-1 ontoBaseSymGrpNpmEvenN
123 26 121 122 syl2anc φqpmEvenNpmTrspNIJ+SymGrpNq:pmEvenN1-1 ontoBaseSymGrpNpmEvenN
124 18 23 109 112 110 123 gsummptfif1o φRpBaseSymGrpNpmEvenNmulGrpRcNpcXc=RpBaseSymGrpNpmEvenNmulGrpRcNpcXcqpmEvenNpmTrspNIJ+SymGrpNq
125 eleq1w p=qppmEvenNqpmEvenN
126 125 anbi2d p=qφppmEvenNφqpmEvenN
127 oveq2 p=qpmTrspNIJ+SymGrpNp=pmTrspNIJ+SymGrpNq
128 127 eleq1d p=qpmTrspNIJ+SymGrpNpBaseSymGrpNpmEvenNpmTrspNIJ+SymGrpNqBaseSymGrpNpmEvenN
129 126 128 imbi12d p=qφppmEvenNpmTrspNIJ+SymGrpNpBaseSymGrpNpmEvenNφqpmEvenNpmTrspNIJ+SymGrpNqBaseSymGrpNpmEvenN
130 27 symggrp NFinSymGrpNGrp
131 26 130 syl φSymGrpNGrp
132 131 adantr φppmEvenNSymGrpNGrp
133 117 27 11 symgtrf ranpmTrspNBaseSymGrpN
134 119 adantr φppmEvenNpmTrspNIJranpmTrspN
135 133 134 sselid φppmEvenNpmTrspNIJBaseSymGrpN
136 75 adantl φppmEvenNpBaseSymGrpN
137 eqid +SymGrpN=+SymGrpN
138 11 137 grpcl SymGrpNGrppmTrspNIJBaseSymGrpNpBaseSymGrpNpmTrspNIJ+SymGrpNpBaseSymGrpN
139 132 135 136 138 syl3anc φppmEvenNpmTrspNIJ+SymGrpNpBaseSymGrpN
140 eqid mulGrpfld𝑠11=mulGrpfld𝑠11
141 27 13 140 psgnghm2 NFinpmSgnNSymGrpNGrpHommulGrpfld𝑠11
142 26 141 syl φpmSgnNSymGrpNGrpHommulGrpfld𝑠11
143 142 adantr φppmEvenNpmSgnNSymGrpNGrpHommulGrpfld𝑠11
144 prex 11V
145 eqid mulGrpfld=mulGrpfld
146 cnfldmul ×=fld
147 145 146 mgpplusg ×=+mulGrpfld
148 140 147 ressplusg 11V×=+mulGrpfld𝑠11
149 144 148 ax-mp ×=+mulGrpfld𝑠11
150 11 137 149 ghmlin pmSgnNSymGrpNGrpHommulGrpfld𝑠11pmTrspNIJBaseSymGrpNpBaseSymGrpNpmSgnNpmTrspNIJ+SymGrpNp=pmSgnNpmTrspNIJpmSgnNp
151 143 135 136 150 syl3anc φppmEvenNpmSgnNpmTrspNIJ+SymGrpNp=pmSgnNpmTrspNIJpmSgnNp
152 27 117 13 psgnpmtr pmTrspNIJranpmTrspNpmSgnNpmTrspNIJ=1
153 134 152 syl φppmEvenNpmSgnNpmTrspNIJ=1
154 27 11 13 psgnevpm NFinppmEvenNpmSgnNp=1
155 26 154 sylan φppmEvenNpmSgnNp=1
156 153 155 oveq12d φppmEvenNpmSgnNpmTrspNIJpmSgnNp=-11
157 neg1cn 1
158 157 mulid1i -11=1
159 156 158 eqtrdi φppmEvenNpmSgnNpmTrspNIJpmSgnNp=1
160 151 159 eqtrd φppmEvenNpmSgnNpmTrspNIJ+SymGrpNp=1
161 27 11 13 psgnodpmr NFinpmTrspNIJ+SymGrpNpBaseSymGrpNpmSgnNpmTrspNIJ+SymGrpNp=1pmTrspNIJ+SymGrpNpBaseSymGrpNpmEvenN
162 69 139 160 161 syl3anc φppmEvenNpmTrspNIJ+SymGrpNpBaseSymGrpNpmEvenN
163 129 162 chvarvv φqpmEvenNpmTrspNIJ+SymGrpNqBaseSymGrpNpmEvenN
164 eqidd φqpmEvenNpmTrspNIJ+SymGrpNq=qpmEvenNpmTrspNIJ+SymGrpNq
165 eqidd φpBaseSymGrpNpmEvenNmulGrpRcNpcXc=pBaseSymGrpNpmEvenNmulGrpRcNpcXc
166 fveq1 p=pmTrspNIJ+SymGrpNqpc=pmTrspNIJ+SymGrpNqc
167 166 oveq1d p=pmTrspNIJ+SymGrpNqpcXc=pmTrspNIJ+SymGrpNqcXc
168 167 mpteq2dv p=pmTrspNIJ+SymGrpNqcNpcXc=cNpmTrspNIJ+SymGrpNqcXc
169 168 oveq2d p=pmTrspNIJ+SymGrpNqmulGrpRcNpcXc=mulGrpRcNpmTrspNIJ+SymGrpNqcXc
170 163 164 165 169 fmptco φpBaseSymGrpNpmEvenNmulGrpRcNpcXcqpmEvenNpmTrspNIJ+SymGrpNq=qpmEvenNmulGrpRcNpmTrspNIJ+SymGrpNqcXc
171 oveq2 q=ppmTrspNIJ+SymGrpNq=pmTrspNIJ+SymGrpNp
172 171 fveq1d q=ppmTrspNIJ+SymGrpNqc=pmTrspNIJ+SymGrpNpc
173 172 oveq1d q=ppmTrspNIJ+SymGrpNqcXc=pmTrspNIJ+SymGrpNpcXc
174 173 mpteq2dv q=pcNpmTrspNIJ+SymGrpNqcXc=cNpmTrspNIJ+SymGrpNpcXc
175 174 oveq2d q=pmulGrpRcNpmTrspNIJ+SymGrpNqcXc=mulGrpRcNpmTrspNIJ+SymGrpNpcXc
176 175 cbvmptv qpmEvenNmulGrpRcNpmTrspNIJ+SymGrpNqcXc=ppmEvenNmulGrpRcNpmTrspNIJ+SymGrpNpcXc
177 176 a1i φqpmEvenNmulGrpRcNpmTrspNIJ+SymGrpNqcXc=ppmEvenNmulGrpRcNpmTrspNIJ+SymGrpNpcXc
178 135 adantr φppmEvenNcNpmTrspNIJBaseSymGrpN
179 136 adantr φppmEvenNcNpBaseSymGrpN
180 27 11 137 symgov pmTrspNIJBaseSymGrpNpBaseSymGrpNpmTrspNIJ+SymGrpNp=pmTrspNIJp
181 178 179 180 syl2anc φppmEvenNcNpmTrspNIJ+SymGrpNp=pmTrspNIJp
182 181 fveq1d φppmEvenNcNpmTrspNIJ+SymGrpNpc=pmTrspNIJpc
183 75 49 sylan2 φppmEvenNp:NN
184 fvco3 p:NNcNpmTrspNIJpc=pmTrspNIJpc
185 183 184 sylan φppmEvenNcNpmTrspNIJpc=pmTrspNIJpc
186 182 185 eqtrd φppmEvenNcNpmTrspNIJ+SymGrpNpc=pmTrspNIJpc
187 186 oveq1d φppmEvenNcNpmTrspNIJ+SymGrpNpcXc=pmTrspNIJpcXc
188 116 pmtrprfv NFinINJNIJpmTrspNIJI=J
189 26 7 8 9 188 syl13anc φpmTrspNIJI=J
190 189 ad2antrr φppmEvenNcNpmTrspNIJI=J
191 190 oveq1d φppmEvenNcNpmTrspNIJIXc=JXc
192 oveq2 a=cIXa=IXc
193 oveq2 a=cJXa=JXc
194 192 193 eqeq12d a=cIXa=JXaIXc=JXc
195 10 ad2antrr φppmEvenNcNaNIXa=JXa
196 simpr φppmEvenNcNcN
197 194 195 196 rspcdva φppmEvenNcNIXc=JXc
198 191 197 eqtr4d φppmEvenNcNpmTrspNIJIXc=IXc
199 fveq2 pc=IpmTrspNIJpc=pmTrspNIJI
200 199 oveq1d pc=IpmTrspNIJpcXc=pmTrspNIJIXc
201 oveq1 pc=IpcXc=IXc
202 200 201 eqeq12d pc=IpmTrspNIJpcXc=pcXcpmTrspNIJIXc=IXc
203 198 202 syl5ibrcom φppmEvenNcNpc=IpmTrspNIJpcXc=pcXc
204 prcom IJ=JI
205 204 fveq2i pmTrspNIJ=pmTrspNJI
206 205 fveq1i pmTrspNIJJ=pmTrspNJIJ
207 9 necomd φJI
208 116 pmtrprfv NFinJNINJIpmTrspNJIJ=I
209 26 8 7 207 208 syl13anc φpmTrspNJIJ=I
210 206 209 eqtrid φpmTrspNIJJ=I
211 210 oveq1d φpmTrspNIJJXc=IXc
212 211 ad2antrr φppmEvenNcNpmTrspNIJJXc=IXc
213 212 197 eqtrd φppmEvenNcNpmTrspNIJJXc=JXc
214 fveq2 pc=JpmTrspNIJpc=pmTrspNIJJ
215 214 oveq1d pc=JpmTrspNIJpcXc=pmTrspNIJJXc
216 oveq1 pc=JpcXc=JXc
217 215 216 eqeq12d pc=JpmTrspNIJpcXc=pcXcpmTrspNIJJXc=JXc
218 213 217 syl5ibrcom φppmEvenNcNpc=JpmTrspNIJpcXc=pcXc
219 218 a1dd φppmEvenNcNpc=JpcIpmTrspNIJpcXc=pcXc
220 neanior pcJpcI¬pc=Jpc=I
221 elpri pcIJpc=Ipc=J
222 221 orcomd pcIJpc=Jpc=I
223 222 con3i ¬pc=Jpc=I¬pcIJ
224 220 223 sylbi pcJpcI¬pcIJ
225 224 3adant1 φppmEvenNcNpcJpcI¬pcIJ
226 116 pmtrmvd NFinIJNIJ2𝑜dompmTrspNIJI=IJ
227 26 113 115 226 syl3anc φdompmTrspNIJI=IJ
228 227 ad2antrr φppmEvenNcNdompmTrspNIJI=IJ
229 228 3ad2ant1 φppmEvenNcNpcJpcIdompmTrspNIJI=IJ
230 225 229 neleqtrrd φppmEvenNcNpcJpcI¬pcdompmTrspNIJI
231 116 pmtrf NFinIJNIJ2𝑜pmTrspNIJ:NN
232 26 113 115 231 syl3anc φpmTrspNIJ:NN
233 232 ffnd φpmTrspNIJFnN
234 233 ad2antrr φppmEvenNcNpmTrspNIJFnN
235 183 ffvelrnda φppmEvenNcNpcN
236 fnelnfp pmTrspNIJFnNpcNpcdompmTrspNIJIpmTrspNIJpcpc
237 234 235 236 syl2anc φppmEvenNcNpcdompmTrspNIJIpmTrspNIJpcpc
238 237 3ad2ant1 φppmEvenNcNpcJpcIpcdompmTrspNIJIpmTrspNIJpcpc
239 238 necon2bbid φppmEvenNcNpcJpcIpmTrspNIJpc=pc¬pcdompmTrspNIJI
240 230 239 mpbird φppmEvenNcNpcJpcIpmTrspNIJpc=pc
241 240 oveq1d φppmEvenNcNpcJpcIpmTrspNIJpcXc=pcXc
242 241 3exp φppmEvenNcNpcJpcIpmTrspNIJpcXc=pcXc
243 219 242 pm2.61dne φppmEvenNcNpcIpmTrspNIJpcXc=pcXc
244 203 243 pm2.61dne φppmEvenNcNpmTrspNIJpcXc=pcXc
245 187 244 eqtrd φppmEvenNcNpmTrspNIJ+SymGrpNpcXc=pcXc
246 245 mpteq2dva φppmEvenNcNpmTrspNIJ+SymGrpNpcXc=cNpcXc
247 246 oveq2d φppmEvenNmulGrpRcNpmTrspNIJ+SymGrpNpcXc=mulGrpRcNpcXc
248 247 mpteq2dva φppmEvenNmulGrpRcNpmTrspNIJ+SymGrpNpcXc=ppmEvenNmulGrpRcNpcXc
249 170 177 248 3eqtrd φpBaseSymGrpNpmEvenNmulGrpRcNpcXcqpmEvenNpmTrspNIJ+SymGrpNq=ppmEvenNmulGrpRcNpcXc
250 249 oveq2d φRpBaseSymGrpNpmEvenNmulGrpRcNpcXcqpmEvenNpmTrspNIJ+SymGrpNq=RppmEvenNmulGrpRcNpcXc
251 124 250 eqtrd φRpBaseSymGrpNpmEvenNmulGrpRcNpcXc=RppmEvenNmulGrpRcNpcXc
252 251 fveq2d φinvgRRpBaseSymGrpNpmEvenNmulGrpRcNpcXc=invgRRppmEvenNmulGrpRcNpcXc
253 105 111 252 3eqtrd φRpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcXcBaseSymGrpNpmEvenN=invgRRppmEvenNmulGrpRcNpcXc
254 82 253 oveq12d φRpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcXcpmEvenN+RRpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcXcBaseSymGrpNpmEvenN=RppmEvenNmulGrpRcNpcXc+RinvgRRppmEvenNmulGrpRcNpcXc
255 59 a1i φpmEvenNBaseSymGrpN
256 29 255 ssfid φpmEvenNFin
257 76 ralrimiva φppmEvenNmulGrpRcNpcXcBaseR
258 18 23 256 257 gsummptcl φRppmEvenNmulGrpRcNpcXcBaseR
259 18 19 4 89 grprinv RGrpRppmEvenNmulGrpRcNpcXcBaseRRppmEvenNmulGrpRcNpcXc+RinvgRRppmEvenNmulGrpRcNpcXc=0˙
260 99 258 259 syl2anc φRppmEvenNmulGrpRcNpcXc+RinvgRRppmEvenNmulGrpRcNpcXc=0˙
261 254 260 eqtrd φRpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcXcpmEvenN+RRpBaseSymGrpNℤRHomRpmSgnNpRmulGrpRcNpcXcBaseSymGrpNpmEvenN=0˙
262 17 65 261 3eqtrd φDX=0˙