Metamath Proof Explorer


Theorem mdetunilem7

Description: Lemma for mdetuni . (Contributed by SO, 15-Jul-2018)

Ref Expression
Hypotheses mdetuni.a A=NMatR
mdetuni.b B=BaseA
mdetuni.k K=BaseR
mdetuni.0g 0˙=0R
mdetuni.1r 1˙=1R
mdetuni.pg +˙=+R
mdetuni.tg ·˙=R
mdetuni.n φNFin
mdetuni.r φRRing
mdetuni.ff φD:BK
mdetuni.al φxByNzNyzwNyxw=zxwDx=0˙
mdetuni.li φxByBzBwNxw×N=yw×N+˙fzw×NxNw×N=yNw×NxNw×N=zNw×NDx=Dy+˙Dz
mdetuni.sc φxByKzBwNxw×N=w×N×y·˙fzw×NxNw×N=zNw×NDx=y·˙Dz
Assertion mdetunilem7 φE:N1-1 ontoNFBDaN,bNEaFb=ℤRHomRpmSgnNE·˙DF

Proof

Step Hyp Ref Expression
1 mdetuni.a A=NMatR
2 mdetuni.b B=BaseA
3 mdetuni.k K=BaseR
4 mdetuni.0g 0˙=0R
5 mdetuni.1r 1˙=1R
6 mdetuni.pg +˙=+R
7 mdetuni.tg ·˙=R
8 mdetuni.n φNFin
9 mdetuni.r φRRing
10 mdetuni.ff φD:BK
11 mdetuni.al φxByNzNyzwNyxw=zxwDx=0˙
12 mdetuni.li φxByBzBwNxw×N=yw×N+˙fzw×NxNw×N=yNw×NxNw×N=zNw×NDx=Dy+˙Dz
13 mdetuni.sc φxByKzBwNxw×N=w×N×y·˙fzw×NxNw×N=zNw×NDx=y·˙Dz
14 fveq1 c=dca=da
15 14 oveq1d c=dcaFb=daFb
16 15 mpoeq3dv c=daN,bNcaFb=aN,bNdaFb
17 16 fveq2d c=dDaN,bNcaFb=DaN,bNdaFb
18 fveq2 c=dℤRHomRpmSgnNc=ℤRHomRpmSgnNd
19 18 oveq1d c=dℤRHomRpmSgnNc·˙DF=ℤRHomRpmSgnNd·˙DF
20 17 19 eqeq12d c=dDaN,bNcaFb=ℤRHomRpmSgnNc·˙DFDaN,bNdaFb=ℤRHomRpmSgnNd·˙DF
21 fveq1 c=d+SymGrpNeca=d+SymGrpNea
22 21 oveq1d c=d+SymGrpNecaFb=d+SymGrpNeaFb
23 22 mpoeq3dv c=d+SymGrpNeaN,bNcaFb=aN,bNd+SymGrpNeaFb
24 23 fveq2d c=d+SymGrpNeDaN,bNcaFb=DaN,bNd+SymGrpNeaFb
25 fveq2 c=d+SymGrpNeℤRHomRpmSgnNc=ℤRHomRpmSgnNd+SymGrpNe
26 25 oveq1d c=d+SymGrpNeℤRHomRpmSgnNc·˙DF=ℤRHomRpmSgnNd+SymGrpNe·˙DF
27 24 26 eqeq12d c=d+SymGrpNeDaN,bNcaFb=ℤRHomRpmSgnNc·˙DFDaN,bNd+SymGrpNeaFb=ℤRHomRpmSgnNd+SymGrpNe·˙DF
28 fveq1 c=0SymGrpNca=0SymGrpNa
29 28 oveq1d c=0SymGrpNcaFb=0SymGrpNaFb
30 29 mpoeq3dv c=0SymGrpNaN,bNcaFb=aN,bN0SymGrpNaFb
31 30 fveq2d c=0SymGrpNDaN,bNcaFb=DaN,bN0SymGrpNaFb
32 fveq2 c=0SymGrpNℤRHomRpmSgnNc=ℤRHomRpmSgnN0SymGrpN
33 32 oveq1d c=0SymGrpNℤRHomRpmSgnNc·˙DF=ℤRHomRpmSgnN0SymGrpN·˙DF
34 31 33 eqeq12d c=0SymGrpNDaN,bNcaFb=ℤRHomRpmSgnNc·˙DFDaN,bN0SymGrpNaFb=ℤRHomRpmSgnN0SymGrpN·˙DF
35 fveq1 c=Eca=Ea
36 35 oveq1d c=EcaFb=EaFb
37 36 mpoeq3dv c=EaN,bNcaFb=aN,bNEaFb
38 37 fveq2d c=EDaN,bNcaFb=DaN,bNEaFb
39 fveq2 c=EℤRHomRpmSgnNc=ℤRHomRpmSgnNE
40 39 oveq1d c=EℤRHomRpmSgnNc·˙DF=ℤRHomRpmSgnNE·˙DF
41 38 40 eqeq12d c=EDaN,bNcaFb=ℤRHomRpmSgnNc·˙DFDaN,bNEaFb=ℤRHomRpmSgnNE·˙DF
42 eqid 0SymGrpN=0SymGrpN
43 eqid +SymGrpN=+SymGrpN
44 eqid BaseSymGrpN=BaseSymGrpN
45 8 3ad2ant1 φE:N1-1 ontoNFBNFin
46 eqid SymGrpN=SymGrpN
47 46 symggrp NFinSymGrpNGrp
48 grpmnd SymGrpNGrpSymGrpNMnd
49 45 47 48 3syl φE:N1-1 ontoNFBSymGrpNMnd
50 eqid ranpmTrspN=ranpmTrspN
51 50 46 44 symgtrf ranpmTrspNBaseSymGrpN
52 51 a1i φE:N1-1 ontoNFBranpmTrspNBaseSymGrpN
53 eqid mrClsSubMndSymGrpN=mrClsSubMndSymGrpN
54 50 46 44 53 symggen2 NFinmrClsSubMndSymGrpNranpmTrspN=BaseSymGrpN
55 8 54 syl φmrClsSubMndSymGrpNranpmTrspN=BaseSymGrpN
56 55 eqcomd φBaseSymGrpN=mrClsSubMndSymGrpNranpmTrspN
57 56 3ad2ant1 φE:N1-1 ontoNFBBaseSymGrpN=mrClsSubMndSymGrpNranpmTrspN
58 9 3ad2ant1 φE:N1-1 ontoNFBRRing
59 10 3ad2ant1 φE:N1-1 ontoNFBD:BK
60 simp3 φE:N1-1 ontoNFBFB
61 59 60 ffvelrnd φE:N1-1 ontoNFBDFK
62 3 7 5 ringlidm RRingDFK1˙·˙DF=DF
63 58 61 62 syl2anc φE:N1-1 ontoNFB1˙·˙DF=DF
64 zrhpsgnmhm RRingNFinℤRHomRpmSgnNSymGrpNMndHommulGrpR
65 9 8 64 syl2anc φℤRHomRpmSgnNSymGrpNMndHommulGrpR
66 eqid mulGrpR=mulGrpR
67 66 5 ringidval 1˙=0mulGrpR
68 42 67 mhm0 ℤRHomRpmSgnNSymGrpNMndHommulGrpRℤRHomRpmSgnN0SymGrpN=1˙
69 65 68 syl φℤRHomRpmSgnN0SymGrpN=1˙
70 69 3ad2ant1 φE:N1-1 ontoNFBℤRHomRpmSgnN0SymGrpN=1˙
71 70 oveq1d φE:N1-1 ontoNFBℤRHomRpmSgnN0SymGrpN·˙DF=1˙·˙DF
72 46 symgid NFinIN=0SymGrpN
73 8 72 syl φIN=0SymGrpN
74 73 3ad2ant1 φE:N1-1 ontoNFBIN=0SymGrpN
75 74 3ad2ant1 φE:N1-1 ontoNFBaNbNIN=0SymGrpN
76 75 fveq1d φE:N1-1 ontoNFBaNbNINa=0SymGrpNa
77 simp2 φE:N1-1 ontoNFBaNbNaN
78 fvresi aNINa=a
79 77 78 syl φE:N1-1 ontoNFBaNbNINa=a
80 76 79 eqtr3d φE:N1-1 ontoNFBaNbN0SymGrpNa=a
81 80 oveq1d φE:N1-1 ontoNFBaNbN0SymGrpNaFb=aFb
82 81 mpoeq3dva φE:N1-1 ontoNFBaN,bN0SymGrpNaFb=aN,bNaFb
83 1 3 2 matbas2i FBFKN×N
84 83 3ad2ant3 φE:N1-1 ontoNFBFKN×N
85 elmapi FKN×NF:N×NK
86 ffn F:N×NKFFnN×N
87 84 85 86 3syl φE:N1-1 ontoNFBFFnN×N
88 fnov FFnN×NF=aN,bNaFb
89 87 88 sylib φE:N1-1 ontoNFBF=aN,bNaFb
90 82 89 eqtr4d φE:N1-1 ontoNFBaN,bN0SymGrpNaFb=F
91 90 fveq2d φE:N1-1 ontoNFBDaN,bN0SymGrpNaFb=DF
92 63 71 91 3eqtr4rd φE:N1-1 ontoNFBDaN,bN0SymGrpNaFb=ℤRHomRpmSgnN0SymGrpN·˙DF
93 simp2 φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNdBaseSymGrpN
94 51 sseli eranpmTrspNeBaseSymGrpN
95 94 3ad2ant3 φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNeBaseSymGrpN
96 46 44 43 symgov dBaseSymGrpNeBaseSymGrpNd+SymGrpNe=de
97 93 95 96 syl2anc φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNd+SymGrpNe=de
98 97 fveq1d φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNd+SymGrpNea=dea
99 98 3ad2ant1 φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNaNbNd+SymGrpNea=dea
100 46 44 symgbasf1o eBaseSymGrpNe:N1-1 ontoN
101 f1of e:N1-1 ontoNe:NN
102 95 100 101 3syl φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNe:NN
103 102 3ad2ant1 φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNaNbNe:NN
104 simp2 φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNaNbNaN
105 fvco3 e:NNaNdea=dea
106 103 104 105 syl2anc φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNaNbNdea=dea
107 99 106 eqtrd φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNaNbNd+SymGrpNea=dea
108 107 oveq1d φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNaNbNd+SymGrpNeaFb=deaFb
109 108 mpoeq3dva φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNaN,bNd+SymGrpNeaFb=aN,bNdeaFb
110 109 fveq2d φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNDaN,bNd+SymGrpNeaFb=DaN,bNdeaFb
111 46 44 symgbasf dBaseSymGrpNd:NN
112 eqid pmTrspN=pmTrspN
113 112 50 pmtrrn2 eranpmTrspNcNfNcfe=pmTrspNcf
114 simpll1 φE:N1-1 ontoNFBd:NNcNfNcfφ
115 df-3an cNfNcfcNfNcf
116 115 biimpri cNfNcfcNfNcf
117 116 adantl φE:N1-1 ontoNFBd:NNcNfNcfcNfNcf
118 84 85 syl φE:N1-1 ontoNFBF:N×NK
119 118 adantr φE:N1-1 ontoNFBd:NNF:N×NK
120 119 ad2antrr φE:N1-1 ontoNFBd:NNcNfNcfbNF:N×NK
121 simpllr φE:N1-1 ontoNFBd:NNcNfNcfbNd:NN
122 simprlr φE:N1-1 ontoNFBd:NNcNfNcffN
123 122 adantr φE:N1-1 ontoNFBd:NNcNfNcfbNfN
124 121 123 ffvelrnd φE:N1-1 ontoNFBd:NNcNfNcfbNdfN
125 simpr φE:N1-1 ontoNFBd:NNcNfNcfbNbN
126 120 124 125 fovrnd φE:N1-1 ontoNFBd:NNcNfNcfbNdfFbK
127 simprll φE:N1-1 ontoNFBd:NNcNfNcfcN
128 127 adantr φE:N1-1 ontoNFBd:NNcNfNcfbNcN
129 121 128 ffvelrnd φE:N1-1 ontoNFBd:NNcNfNcfbNdcN
130 120 129 125 fovrnd φE:N1-1 ontoNFBd:NNcNfNcfbNdcFbK
131 126 130 jca φE:N1-1 ontoNFBd:NNcNfNcfbNdfFbKdcFbK
132 118 ad2antrr φE:N1-1 ontoNFBd:NNcNfNcfF:N×NK
133 132 3ad2ant1 φE:N1-1 ontoNFBd:NNcNfNcfaNbNF:N×NK
134 simp1lr φE:N1-1 ontoNFBd:NNcNfNcfaNbNd:NN
135 simp2 φE:N1-1 ontoNFBd:NNcNfNcfaNbNaN
136 134 135 ffvelrnd φE:N1-1 ontoNFBd:NNcNfNcfaNbNdaN
137 simp3 φE:N1-1 ontoNFBd:NNcNfNcfaNbNbN
138 133 136 137 fovrnd φE:N1-1 ontoNFBd:NNcNfNcfaNbNdaFbK
139 1 2 3 4 5 6 7 8 9 10 11 12 13 114 117 131 138 mdetunilem6 φE:N1-1 ontoNFBd:NNcNfNcfDaN,bNifa=cdfFbifa=fdcFbdaFb=invgRDaN,bNifa=cdcFbifa=fdfFbdaFb
140 simpl1 φE:N1-1 ontoNFBd:NNφ
141 fveq2 a=cpmTrspNcfa=pmTrspNcfc
142 8 adantr φcNfNcfNFin
143 simprll φcNfNcfcN
144 simprlr φcNfNcffN
145 simprr φcNfNcfcf
146 112 pmtrprfv NFincNfNcfpmTrspNcfc=f
147 142 143 144 145 146 syl13anc φcNfNcfpmTrspNcfc=f
148 147 adantr φcNfNcfaNpmTrspNcfc=f
149 141 148 sylan9eqr φcNfNcfaNa=cpmTrspNcfa=f
150 149 fveq2d φcNfNcfaNa=cdpmTrspNcfa=df
151 150 oveq1d φcNfNcfaNa=cdpmTrspNcfaFb=dfFb
152 iftrue a=cifa=cdfFbifa=fdcFbdaFb=dfFb
153 152 adantl φcNfNcfaNa=cifa=cdfFbifa=fdcFbdaFb=dfFb
154 151 153 eqtr4d φcNfNcfaNa=cdpmTrspNcfaFb=ifa=cdfFbifa=fdcFbdaFb
155 fveq2 a=fpmTrspNcfa=pmTrspNcff
156 prcom cf=fc
157 156 fveq2i pmTrspNcf=pmTrspNfc
158 157 fveq1i pmTrspNcff=pmTrspNfcf
159 8 ad2antrr φcNfNcfaNNFin
160 simplrl φcNfNcfaNcNfN
161 160 simprd φcNfNcfaNfN
162 160 simpld φcNfNcfaNcN
163 simplrr φcNfNcfaNcf
164 163 necomd φcNfNcfaNfc
165 112 pmtrprfv NFinfNcNfcpmTrspNfcf=c
166 159 161 162 164 165 syl13anc φcNfNcfaNpmTrspNfcf=c
167 158 166 eqtrid φcNfNcfaNpmTrspNcff=c
168 155 167 sylan9eqr φcNfNcfaNa=fpmTrspNcfa=c
169 168 fveq2d φcNfNcfaNa=fdpmTrspNcfa=dc
170 169 oveq1d φcNfNcfaNa=fdpmTrspNcfaFb=dcFb
171 iftrue a=fifa=fdcFbdaFb=dcFb
172 171 adantl φcNfNcfaNa=fifa=fdcFbdaFb=dcFb
173 170 172 eqtr4d φcNfNcfaNa=fdpmTrspNcfaFb=ifa=fdcFbdaFb
174 173 adantlr φcNfNcfaN¬a=ca=fdpmTrspNcfaFb=ifa=fdcFbdaFb
175 vex aV
176 175 elpr acfa=ca=f
177 176 notbii ¬acf¬a=ca=f
178 ioran ¬a=ca=f¬a=c¬a=f
179 177 178 sylbbr ¬a=c¬a=f¬acf
180 179 adantll φcNfNcfaN¬a=c¬a=f¬acf
181 prssi cNfNcfN
182 160 181 syl φcNfNcfaNcfN
183 pr2ne cNfNcf2𝑜cf
184 160 183 syl φcNfNcfaNcf2𝑜cf
185 163 184 mpbird φcNfNcfaNcf2𝑜
186 112 pmtrmvd NFincfNcf2𝑜dompmTrspNcfI=cf
187 159 182 185 186 syl3anc φcNfNcfaNdompmTrspNcfI=cf
188 187 eleq2d φcNfNcfaNadompmTrspNcfIacf
189 188 notbid φcNfNcfaN¬adompmTrspNcfI¬acf
190 189 ad2antrr φcNfNcfaN¬a=c¬a=f¬adompmTrspNcfI¬acf
191 180 190 mpbird φcNfNcfaN¬a=c¬a=f¬adompmTrspNcfI
192 112 pmtrf NFincfNcf2𝑜pmTrspNcf:NN
193 159 182 185 192 syl3anc φcNfNcfaNpmTrspNcf:NN
194 193 ffnd φcNfNcfaNpmTrspNcfFnN
195 simpr φcNfNcfaNaN
196 fnelnfp pmTrspNcfFnNaNadompmTrspNcfIpmTrspNcfaa
197 196 necon2bbid pmTrspNcfFnNaNpmTrspNcfa=a¬adompmTrspNcfI
198 194 195 197 syl2anc φcNfNcfaNpmTrspNcfa=a¬adompmTrspNcfI
199 198 ad2antrr φcNfNcfaN¬a=c¬a=fpmTrspNcfa=a¬adompmTrspNcfI
200 191 199 mpbird φcNfNcfaN¬a=c¬a=fpmTrspNcfa=a
201 200 fveq2d φcNfNcfaN¬a=c¬a=fdpmTrspNcfa=da
202 201 oveq1d φcNfNcfaN¬a=c¬a=fdpmTrspNcfaFb=daFb
203 iffalse ¬a=fifa=fdcFbdaFb=daFb
204 203 adantl φcNfNcfaN¬a=c¬a=fifa=fdcFbdaFb=daFb
205 202 204 eqtr4d φcNfNcfaN¬a=c¬a=fdpmTrspNcfaFb=ifa=fdcFbdaFb
206 174 205 pm2.61dan φcNfNcfaN¬a=cdpmTrspNcfaFb=ifa=fdcFbdaFb
207 iffalse ¬a=cifa=cdfFbifa=fdcFbdaFb=ifa=fdcFbdaFb
208 207 adantl φcNfNcfaN¬a=cifa=cdfFbifa=fdcFbdaFb=ifa=fdcFbdaFb
209 206 208 eqtr4d φcNfNcfaN¬a=cdpmTrspNcfaFb=ifa=cdfFbifa=fdcFbdaFb
210 154 209 pm2.61dan φcNfNcfaNdpmTrspNcfaFb=ifa=cdfFbifa=fdcFbdaFb
211 210 3adant3 φcNfNcfaNbNdpmTrspNcfaFb=ifa=cdfFbifa=fdcFbdaFb
212 211 mpoeq3dva φcNfNcfaN,bNdpmTrspNcfaFb=aN,bNifa=cdfFbifa=fdcFbdaFb
213 140 212 sylan φE:N1-1 ontoNFBd:NNcNfNcfaN,bNdpmTrspNcfaFb=aN,bNifa=cdfFbifa=fdcFbdaFb
214 213 fveq2d φE:N1-1 ontoNFBd:NNcNfNcfDaN,bNdpmTrspNcfaFb=DaN,bNifa=cdfFbifa=fdcFbdaFb
215 fveq2 a=cda=dc
216 215 oveq1d a=cdaFb=dcFb
217 iftrue a=cifa=cdcFbifa=fdfFbdaFb=dcFb
218 216 217 eqtr4d a=cdaFb=ifa=cdcFbifa=fdfFbdaFb
219 fveq2 a=fda=df
220 219 oveq1d a=fdaFb=dfFb
221 iftrue a=fifa=fdfFbdaFb=dfFb
222 220 221 eqtr4d a=fdaFb=ifa=fdfFbdaFb
223 222 adantl ¬a=ca=fdaFb=ifa=fdfFbdaFb
224 iffalse ¬a=fifa=fdfFbdaFb=daFb
225 224 eqcomd ¬a=fdaFb=ifa=fdfFbdaFb
226 225 adantl ¬a=c¬a=fdaFb=ifa=fdfFbdaFb
227 223 226 pm2.61dan ¬a=cdaFb=ifa=fdfFbdaFb
228 iffalse ¬a=cifa=cdcFbifa=fdfFbdaFb=ifa=fdfFbdaFb
229 227 228 eqtr4d ¬a=cdaFb=ifa=cdcFbifa=fdfFbdaFb
230 218 229 pm2.61i daFb=ifa=cdcFbifa=fdfFbdaFb
231 230 a1i aNbNdaFb=ifa=cdcFbifa=fdfFbdaFb
232 231 mpoeq3ia aN,bNdaFb=aN,bNifa=cdcFbifa=fdfFbdaFb
233 232 fveq2i DaN,bNdaFb=DaN,bNifa=cdcFbifa=fdfFbdaFb
234 233 fveq2i invgRDaN,bNdaFb=invgRDaN,bNifa=cdcFbifa=fdfFbdaFb
235 234 a1i φE:N1-1 ontoNFBd:NNcNfNcfinvgRDaN,bNdaFb=invgRDaN,bNifa=cdcFbifa=fdfFbdaFb
236 139 214 235 3eqtr4d φE:N1-1 ontoNFBd:NNcNfNcfDaN,bNdpmTrspNcfaFb=invgRDaN,bNdaFb
237 fveq1 e=pmTrspNcfea=pmTrspNcfa
238 237 fveq2d e=pmTrspNcfdea=dpmTrspNcfa
239 238 oveq1d e=pmTrspNcfdeaFb=dpmTrspNcfaFb
240 239 mpoeq3dv e=pmTrspNcfaN,bNdeaFb=aN,bNdpmTrspNcfaFb
241 240 fveqeq2d e=pmTrspNcfDaN,bNdeaFb=invgRDaN,bNdaFbDaN,bNdpmTrspNcfaFb=invgRDaN,bNdaFb
242 236 241 syl5ibrcom φE:N1-1 ontoNFBd:NNcNfNcfe=pmTrspNcfDaN,bNdeaFb=invgRDaN,bNdaFb
243 242 expr φE:N1-1 ontoNFBd:NNcNfNcfe=pmTrspNcfDaN,bNdeaFb=invgRDaN,bNdaFb
244 243 impd φE:N1-1 ontoNFBd:NNcNfNcfe=pmTrspNcfDaN,bNdeaFb=invgRDaN,bNdaFb
245 244 rexlimdvva φE:N1-1 ontoNFBd:NNcNfNcfe=pmTrspNcfDaN,bNdeaFb=invgRDaN,bNdaFb
246 113 245 syl5 φE:N1-1 ontoNFBd:NNeranpmTrspNDaN,bNdeaFb=invgRDaN,bNdaFb
247 246 3impia φE:N1-1 ontoNFBd:NNeranpmTrspNDaN,bNdeaFb=invgRDaN,bNdaFb
248 111 247 syl3an2 φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNDaN,bNdeaFb=invgRDaN,bNdaFb
249 110 248 eqtrd φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNDaN,bNd+SymGrpNeaFb=invgRDaN,bNdaFb
250 249 adantr φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNDaN,bNdaFb=ℤRHomRpmSgnNd·˙DFDaN,bNd+SymGrpNeaFb=invgRDaN,bNdaFb
251 fveq2 DaN,bNdaFb=ℤRHomRpmSgnNd·˙DFinvgRDaN,bNdaFb=invgRℤRHomRpmSgnNd·˙DF
252 251 adantl φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNDaN,bNdaFb=ℤRHomRpmSgnNd·˙DFinvgRDaN,bNdaFb=invgRℤRHomRpmSgnNd·˙DF
253 eqid invgR=invgR
254 58 3ad2ant1 φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNRRing
255 65 3ad2ant1 φE:N1-1 ontoNFBℤRHomRpmSgnNSymGrpNMndHommulGrpR
256 255 3ad2ant1 φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNℤRHomRpmSgnNSymGrpNMndHommulGrpR
257 66 3 mgpbas K=BasemulGrpR
258 44 257 mhmf ℤRHomRpmSgnNSymGrpNMndHommulGrpRℤRHomRpmSgnN:BaseSymGrpNK
259 256 258 syl φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNℤRHomRpmSgnN:BaseSymGrpNK
260 259 93 ffvelrnd φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNℤRHomRpmSgnNdK
261 59 3ad2ant1 φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspND:BK
262 simp13 φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNFB
263 261 262 ffvelrnd φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNDFK
264 3 7 253 254 260 263 ringmneg1 φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNinvgRℤRHomRpmSgnNd·˙DF=invgRℤRHomRpmSgnNd·˙DF
265 66 7 mgpplusg ·˙=+mulGrpR
266 44 43 265 mhmlin ℤRHomRpmSgnNSymGrpNMndHommulGrpRdBaseSymGrpNeBaseSymGrpNℤRHomRpmSgnNd+SymGrpNe=ℤRHomRpmSgnNd·˙ℤRHomRpmSgnNe
267 256 93 95 266 syl3anc φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNℤRHomRpmSgnNd+SymGrpNe=ℤRHomRpmSgnNd·˙ℤRHomRpmSgnNe
268 45 3ad2ant1 φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNNFin
269 simp3 φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNeranpmTrspN
270 46 44 50 pmtrodpm NFineranpmTrspNeBaseSymGrpNpmEvenN
271 268 269 270 syl2anc φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNeBaseSymGrpNpmEvenN
272 eqid ℤRHomR=ℤRHomR
273 eqid pmSgnN=pmSgnN
274 272 273 5 44 253 zrhpsgnodpm RRingNFineBaseSymGrpNpmEvenNℤRHomRpmSgnNe=invgR1˙
275 254 268 271 274 syl3anc φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNℤRHomRpmSgnNe=invgR1˙
276 275 oveq2d φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNℤRHomRpmSgnNd·˙ℤRHomRpmSgnNe=ℤRHomRpmSgnNd·˙invgR1˙
277 3 7 5 253 254 260 rngnegr φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNℤRHomRpmSgnNd·˙invgR1˙=invgRℤRHomRpmSgnNd
278 267 276 277 3eqtrrd φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNinvgRℤRHomRpmSgnNd=ℤRHomRpmSgnNd+SymGrpNe
279 278 oveq1d φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNinvgRℤRHomRpmSgnNd·˙DF=ℤRHomRpmSgnNd+SymGrpNe·˙DF
280 264 279 eqtr3d φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNinvgRℤRHomRpmSgnNd·˙DF=ℤRHomRpmSgnNd+SymGrpNe·˙DF
281 280 adantr φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNDaN,bNdaFb=ℤRHomRpmSgnNd·˙DFinvgRℤRHomRpmSgnNd·˙DF=ℤRHomRpmSgnNd+SymGrpNe·˙DF
282 250 252 281 3eqtrd φE:N1-1 ontoNFBdBaseSymGrpNeranpmTrspNDaN,bNdaFb=ℤRHomRpmSgnNd·˙DFDaN,bNd+SymGrpNeaFb=ℤRHomRpmSgnNd+SymGrpNe·˙DF
283 simp2 φE:N1-1 ontoNFBE:N1-1 ontoN
284 46 44 elsymgbas NFinEBaseSymGrpNE:N1-1 ontoN
285 45 284 syl φE:N1-1 ontoNFBEBaseSymGrpNE:N1-1 ontoN
286 283 285 mpbird φE:N1-1 ontoNFBEBaseSymGrpN
287 20 27 34 41 42 43 44 49 52 57 92 282 286 mndind φE:N1-1 ontoNFBDaN,bNEaFb=ℤRHomRpmSgnNE·˙DF