Metamath Proof Explorer


Theorem mdetmul

Description: Multiplicativity of the determinant function: the determinant of a matrix product of square matrices equals the product of their determinants. Proposition 4.15 in Lang p. 517. (Contributed by Stefan O'Rear, 16-Jul-2018)

Ref Expression
Hypotheses mdetmul.a A=NMatR
mdetmul.b B=BaseA
mdetmul.d D=NmaDetR
mdetmul.t1 ·˙=R
mdetmul.t2 ˙=A
Assertion mdetmul RCRingFBGBDF˙G=DF·˙DG

Proof

Step Hyp Ref Expression
1 mdetmul.a A=NMatR
2 mdetmul.b B=BaseA
3 mdetmul.d D=NmaDetR
4 mdetmul.t1 ·˙=R
5 mdetmul.t2 ˙=A
6 eqid BaseR=BaseR
7 eqid 0R=0R
8 eqid 1R=1R
9 eqid +R=+R
10 1 2 matrcl FBNFinRV
11 10 simpld FBNFin
12 11 3ad2ant2 RCRingFBGBNFin
13 crngring RCRingRRing
14 13 3ad2ant1 RCRingFBGBRRing
15 3 1 2 6 mdetf RCRingD:BBaseR
16 15 3ad2ant1 RCRingFBGBD:BBaseR
17 16 adantr RCRingFBGBaBD:BBaseR
18 1 matring NFinRRingARing
19 12 14 18 syl2anc RCRingFBGBARing
20 19 adantr RCRingFBGBaBARing
21 simpr RCRingFBGBaBaB
22 simpl3 RCRingFBGBaBGB
23 2 5 ringcl ARingaBGBa˙GB
24 20 21 22 23 syl3anc RCRingFBGBaBa˙GB
25 17 24 ffvelrnd RCRingFBGBaBDa˙GBaseR
26 25 fmpttd RCRingFBGBaBDa˙G:BBaseR
27 simp21 RCRingFBGBbBcNdNcdeNcbe=dbebB
28 fvoveq1 a=bDa˙G=Db˙G
29 eqid aBDa˙G=aBDa˙G
30 fvex Db˙GV
31 28 29 30 fvmpt bBaBDa˙Gb=Db˙G
32 27 31 syl RCRingFBGBbBcNdNcdeNcbe=dbeaBDa˙Gb=Db˙G
33 simp11 RCRingFBGBbBcNdNcdeNcbe=dbeRCRing
34 19 adantr RCRingFBGBbBcNdNARing
35 simpr1 RCRingFBGBbBcNdNbB
36 simpl3 RCRingFBGBbBcNdNGB
37 2 5 ringcl ARingbBGBb˙GB
38 34 35 36 37 syl3anc RCRingFBGBbBcNdNb˙GB
39 38 3adant3 RCRingFBGBbBcNdNcdeNcbe=dbeb˙GB
40 simp22 RCRingFBGBbBcNdNcdeNcbe=dbecN
41 simp23 RCRingFBGBbBcNdNcdeNcbe=dbedN
42 simp3l RCRingFBGBbBcNdNcdeNcbe=dbecd
43 simpl3r RCRingFBGBbBcNdNcdeNcbe=dbeaNeNcbe=dbe
44 eqid N=N
45 oveq1 cbe=dbecbe·˙eGa=dbe·˙eGa
46 45 ralimi eNcbe=dbeeNcbe·˙eGa=dbe·˙eGa
47 mpteq12 N=NeNcbe·˙eGa=dbe·˙eGaeNcbe·˙eGa=eNdbe·˙eGa
48 44 46 47 sylancr eNcbe=dbeeNcbe·˙eGa=eNdbe·˙eGa
49 48 oveq2d eNcbe=dbeReNcbe·˙eGa=ReNdbe·˙eGa
50 43 49 syl RCRingFBGBbBcNdNcdeNcbe=dbeaNReNcbe·˙eGa=ReNdbe·˙eGa
51 simp1 RCRingFBGBRCRing
52 eqid RmaMulNNN=RmaMulNNN
53 1 52 matmulr NFinRCRingRmaMulNNN=A
54 53 5 eqtr4di NFinRCRingRmaMulNNN=˙
55 12 51 54 syl2anc RCRingFBGBRmaMulNNN=˙
56 55 ad2antrr RCRingFBGBbBcNdNaNRmaMulNNN=˙
57 56 oveqd RCRingFBGBbBcNdNaNbRmaMulNNNG=b˙G
58 57 oveqd RCRingFBGBbBcNdNaNcbRmaMulNNNGa=cb˙Ga
59 simpll1 RCRingFBGBbBcNdNaNRCRing
60 12 ad2antrr RCRingFBGBbBcNdNaNNFin
61 simplr1 RCRingFBGBbBcNdNaNbB
62 1 6 2 matbas2i bBbBaseRN×N
63 61 62 syl RCRingFBGBbBcNdNaNbBaseRN×N
64 1 6 2 matbas2i GBGBaseRN×N
65 64 3ad2ant3 RCRingFBGBGBaseRN×N
66 65 ad2antrr RCRingFBGBbBcNdNaNGBaseRN×N
67 simplr2 RCRingFBGBbBcNdNaNcN
68 simpr RCRingFBGBbBcNdNaNaN
69 52 6 4 59 60 60 60 63 66 67 68 mamufv RCRingFBGBbBcNdNaNcbRmaMulNNNGa=ReNcbe·˙eGa
70 58 69 eqtr3d RCRingFBGBbBcNdNaNcb˙Ga=ReNcbe·˙eGa
71 70 3adantl3 RCRingFBGBbBcNdNcdeNcbe=dbeaNcb˙Ga=ReNcbe·˙eGa
72 57 oveqd RCRingFBGBbBcNdNaNdbRmaMulNNNGa=db˙Ga
73 simplr3 RCRingFBGBbBcNdNaNdN
74 52 6 4 59 60 60 60 63 66 73 68 mamufv RCRingFBGBbBcNdNaNdbRmaMulNNNGa=ReNdbe·˙eGa
75 72 74 eqtr3d RCRingFBGBbBcNdNaNdb˙Ga=ReNdbe·˙eGa
76 75 3adantl3 RCRingFBGBbBcNdNcdeNcbe=dbeaNdb˙Ga=ReNdbe·˙eGa
77 50 71 76 3eqtr4d RCRingFBGBbBcNdNcdeNcbe=dbeaNcb˙Ga=db˙Ga
78 77 ralrimiva RCRingFBGBbBcNdNcdeNcbe=dbeaNcb˙Ga=db˙Ga
79 3 1 2 7 33 39 40 41 42 78 mdetralt RCRingFBGBbBcNdNcdeNcbe=dbeDb˙G=0R
80 32 79 eqtrd RCRingFBGBbBcNdNcdeNcbe=dbeaBDa˙Gb=0R
81 80 3expia RCRingFBGBbBcNdNcdeNcbe=dbeaBDa˙Gb=0R
82 81 ralrimivvva RCRingFBGBbBcNdNcdeNcbe=dbeaBDa˙Gb=0R
83 simp11 RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×NRCRing
84 19 adantr RCRingFBGBbBcBdBeNARing
85 simprll RCRingFBGBbBcBdBeNbB
86 simpl3 RCRingFBGBbBcBdBeNGB
87 84 85 86 37 syl3anc RCRingFBGBbBcBdBeNb˙GB
88 87 3adant3 RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×Nb˙GB
89 simprlr RCRingFBGBbBcBdBeNcB
90 2 5 ringcl ARingcBGBc˙GB
91 84 89 86 90 syl3anc RCRingFBGBbBcBdBeNc˙GB
92 91 3adant3 RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×Nc˙GB
93 simprrl RCRingFBGBbBcBdBeNdB
94 2 5 ringcl ARingdBGBd˙GB
95 84 93 86 94 syl3anc RCRingFBGBbBcBdBeNd˙GB
96 95 3adant3 RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×Nd˙GB
97 simp2rr RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×NeN
98 simp31 RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×Nbe×N=ce×N+Rfde×N
99 98 oveq1d RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×Nbe×NRmaMuleNNG=ce×N+Rfde×NRmaMuleNNG
100 14 adantr RCRingFBGBbBcBdBeNRRing
101 eqid RmaMuleNN=RmaMuleNN
102 snfi eFin
103 102 a1i RCRingFBGBbBcBdBeNeFin
104 12 adantr RCRingFBGBbBcBdBeNNFin
105 1 6 2 matbas2i cBcBaseRN×N
106 89 105 syl RCRingFBGBbBcBdBeNcBaseRN×N
107 simprrr RCRingFBGBbBcBdBeNeN
108 107 snssd RCRingFBGBbBcBdBeNeN
109 xpss1 eNe×NN×N
110 108 109 syl RCRingFBGBbBcBdBeNe×NN×N
111 elmapssres cBaseRN×Ne×NN×Nce×NBaseRe×N
112 106 110 111 syl2anc RCRingFBGBbBcBdBeNce×NBaseRe×N
113 1 6 2 matbas2i dBdBaseRN×N
114 93 113 syl RCRingFBGBbBcBdBeNdBaseRN×N
115 elmapssres dBaseRN×Ne×NN×Nde×NBaseRe×N
116 114 110 115 syl2anc RCRingFBGBbBcBdBeNde×NBaseRe×N
117 65 adantr RCRingFBGBbBcBdBeNGBaseRN×N
118 6 100 101 103 104 104 9 112 116 117 mamudi RCRingFBGBbBcBdBeNce×N+Rfde×NRmaMuleNNG=ce×NRmaMuleNNG+Rfde×NRmaMuleNNG
119 118 3adant3 RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×Nce×N+Rfde×NRmaMuleNNG=ce×NRmaMuleNNG+Rfde×NRmaMuleNNG
120 99 119 eqtrd RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×Nbe×NRmaMuleNNG=ce×NRmaMuleNNG+Rfde×NRmaMuleNNG
121 55 adantr RCRingFBGBbBcBdBeNRmaMulNNN=˙
122 121 oveqd RCRingFBGBbBcBdBeNbRmaMulNNNG=b˙G
123 122 reseq1d RCRingFBGBbBcBdBeNbRmaMulNNNGe×N=b˙Ge×N
124 simpl1 RCRingFBGBbBcBdBeNRCRing
125 85 62 syl RCRingFBGBbBcBdBeNbBaseRN×N
126 52 101 6 124 104 104 104 108 125 117 mamures RCRingFBGBbBcBdBeNbRmaMulNNNGe×N=be×NRmaMuleNNG
127 123 126 eqtr3d RCRingFBGBbBcBdBeNb˙Ge×N=be×NRmaMuleNNG
128 127 3adant3 RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×Nb˙Ge×N=be×NRmaMuleNNG
129 121 oveqd RCRingFBGBbBcBdBeNcRmaMulNNNG=c˙G
130 129 reseq1d RCRingFBGBbBcBdBeNcRmaMulNNNGe×N=c˙Ge×N
131 52 101 6 124 104 104 104 108 106 117 mamures RCRingFBGBbBcBdBeNcRmaMulNNNGe×N=ce×NRmaMuleNNG
132 130 131 eqtr3d RCRingFBGBbBcBdBeNc˙Ge×N=ce×NRmaMuleNNG
133 121 oveqd RCRingFBGBbBcBdBeNdRmaMulNNNG=d˙G
134 133 reseq1d RCRingFBGBbBcBdBeNdRmaMulNNNGe×N=d˙Ge×N
135 52 101 6 124 104 104 104 108 114 117 mamures RCRingFBGBbBcBdBeNdRmaMulNNNGe×N=de×NRmaMuleNNG
136 134 135 eqtr3d RCRingFBGBbBcBdBeNd˙Ge×N=de×NRmaMuleNNG
137 132 136 oveq12d RCRingFBGBbBcBdBeNc˙Ge×N+Rfd˙Ge×N=ce×NRmaMuleNNG+Rfde×NRmaMuleNNG
138 137 3adant3 RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×Nc˙Ge×N+Rfd˙Ge×N=ce×NRmaMuleNNG+Rfde×NRmaMuleNNG
139 120 128 138 3eqtr4d RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×Nb˙Ge×N=c˙Ge×N+Rfd˙Ge×N
140 simp32 RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×NbNe×N=cNe×N
141 140 oveq1d RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×NbNe×NRmaMulNeNNG=cNe×NRmaMulNeNNG
142 122 reseq1d RCRingFBGBbBcBdBeNbRmaMulNNNGNe×N=b˙GNe×N
143 eqid RmaMulNeNN=RmaMulNeNN
144 difssd RCRingFBGBbBcBdBeNNeN
145 52 143 6 124 104 104 104 144 125 117 mamures RCRingFBGBbBcBdBeNbRmaMulNNNGNe×N=bNe×NRmaMulNeNNG
146 142 145 eqtr3d RCRingFBGBbBcBdBeNb˙GNe×N=bNe×NRmaMulNeNNG
147 146 3adant3 RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×Nb˙GNe×N=bNe×NRmaMulNeNNG
148 129 reseq1d RCRingFBGBbBcBdBeNcRmaMulNNNGNe×N=c˙GNe×N
149 52 143 6 124 104 104 104 144 106 117 mamures RCRingFBGBbBcBdBeNcRmaMulNNNGNe×N=cNe×NRmaMulNeNNG
150 148 149 eqtr3d RCRingFBGBbBcBdBeNc˙GNe×N=cNe×NRmaMulNeNNG
151 150 3adant3 RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×Nc˙GNe×N=cNe×NRmaMulNeNNG
152 141 147 151 3eqtr4d RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×Nb˙GNe×N=c˙GNe×N
153 simp33 RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×NbNe×N=dNe×N
154 153 oveq1d RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×NbNe×NRmaMulNeNNG=dNe×NRmaMulNeNNG
155 133 reseq1d RCRingFBGBbBcBdBeNdRmaMulNNNGNe×N=d˙GNe×N
156 52 143 6 124 104 104 104 144 114 117 mamures RCRingFBGBbBcBdBeNdRmaMulNNNGNe×N=dNe×NRmaMulNeNNG
157 155 156 eqtr3d RCRingFBGBbBcBdBeNd˙GNe×N=dNe×NRmaMulNeNNG
158 157 3adant3 RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×Nd˙GNe×N=dNe×NRmaMulNeNNG
159 154 147 158 3eqtr4d RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×Nb˙GNe×N=d˙GNe×N
160 3 1 2 9 83 88 92 96 97 139 152 159 mdetrlin RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×NDb˙G=Dc˙G+RDd˙G
161 85 31 syl RCRingFBGBbBcBdBeNaBDa˙Gb=Db˙G
162 161 3adant3 RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×NaBDa˙Gb=Db˙G
163 fvoveq1 a=cDa˙G=Dc˙G
164 fvex Dc˙GV
165 163 29 164 fvmpt cBaBDa˙Gc=Dc˙G
166 89 165 syl RCRingFBGBbBcBdBeNaBDa˙Gc=Dc˙G
167 fvoveq1 a=dDa˙G=Dd˙G
168 fvex Dd˙GV
169 167 29 168 fvmpt dBaBDa˙Gd=Dd˙G
170 93 169 syl RCRingFBGBbBcBdBeNaBDa˙Gd=Dd˙G
171 166 170 oveq12d RCRingFBGBbBcBdBeNaBDa˙Gc+RaBDa˙Gd=Dc˙G+RDd˙G
172 171 3adant3 RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×NaBDa˙Gc+RaBDa˙Gd=Dc˙G+RDd˙G
173 160 162 172 3eqtr4d RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×NaBDa˙Gb=aBDa˙Gc+RaBDa˙Gd
174 173 3expia RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×NaBDa˙Gb=aBDa˙Gc+RaBDa˙Gd
175 174 anassrs RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×NaBDa˙Gb=aBDa˙Gc+RaBDa˙Gd
176 175 ralrimivva RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×NaBDa˙Gb=aBDa˙Gc+RaBDa˙Gd
177 176 ralrimivva RCRingFBGBbBcBdBeNbe×N=ce×N+Rfde×NbNe×N=cNe×NbNe×N=dNe×NaBDa˙Gb=aBDa˙Gc+RaBDa˙Gd
178 simp11 RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×NRCRing
179 19 adantr RCRingFBGBbBcBaseRdBeNARing
180 simprll RCRingFBGBbBcBaseRdBeNbB
181 simpl3 RCRingFBGBbBcBaseRdBeNGB
182 179 180 181 37 syl3anc RCRingFBGBbBcBaseRdBeNb˙GB
183 182 3adant3 RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×Nb˙GB
184 simp2lr RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×NcBaseR
185 simprrl RCRingFBGBbBcBaseRdBeNdB
186 179 185 181 94 syl3anc RCRingFBGBbBcBaseRdBeNd˙GB
187 186 3adant3 RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×Nd˙GB
188 simp2rr RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×NeN
189 simp3l RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×Nbe×N=e×N×c·˙fde×N
190 189 oveq1d RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×Nbe×NRmaMuleNNG=e×N×c·˙fde×NRmaMuleNNG
191 55 adantr RCRingFBGBbBcBaseRdBeNRmaMulNNN=˙
192 191 oveqd RCRingFBGBbBcBaseRdBeNbRmaMulNNNG=b˙G
193 192 reseq1d RCRingFBGBbBcBaseRdBeNbRmaMulNNNGe×N=b˙Ge×N
194 simpl1 RCRingFBGBbBcBaseRdBeNRCRing
195 12 adantr RCRingFBGBbBcBaseRdBeNNFin
196 simprrr RCRingFBGBbBcBaseRdBeNeN
197 196 snssd RCRingFBGBbBcBaseRdBeNeN
198 180 62 syl RCRingFBGBbBcBaseRdBeNbBaseRN×N
199 65 adantr RCRingFBGBbBcBaseRdBeNGBaseRN×N
200 52 101 6 194 195 195 195 197 198 199 mamures RCRingFBGBbBcBaseRdBeNbRmaMulNNNGe×N=be×NRmaMuleNNG
201 193 200 eqtr3d RCRingFBGBbBcBaseRdBeNb˙Ge×N=be×NRmaMuleNNG
202 201 3adant3 RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×Nb˙Ge×N=be×NRmaMuleNNG
203 191 oveqd RCRingFBGBbBcBaseRdBeNdRmaMulNNNG=d˙G
204 203 reseq1d RCRingFBGBbBcBaseRdBeNdRmaMulNNNGe×N=d˙Ge×N
205 185 113 syl RCRingFBGBbBcBaseRdBeNdBaseRN×N
206 52 101 6 194 195 195 195 197 205 199 mamures RCRingFBGBbBcBaseRdBeNdRmaMulNNNGe×N=de×NRmaMuleNNG
207 204 206 eqtr3d RCRingFBGBbBcBaseRdBeNd˙Ge×N=de×NRmaMuleNNG
208 207 oveq2d RCRingFBGBbBcBaseRdBeNe×N×c·˙fd˙Ge×N=e×N×c·˙fde×NRmaMuleNNG
209 14 adantr RCRingFBGBbBcBaseRdBeNRRing
210 102 a1i RCRingFBGBbBcBaseRdBeNeFin
211 simprlr RCRingFBGBbBcBaseRdBeNcBaseR
212 197 109 syl RCRingFBGBbBcBaseRdBeNe×NN×N
213 205 212 115 syl2anc RCRingFBGBbBcBaseRdBeNde×NBaseRe×N
214 6 209 101 210 195 195 4 211 213 199 mamuvs1 RCRingFBGBbBcBaseRdBeNe×N×c·˙fde×NRmaMuleNNG=e×N×c·˙fde×NRmaMuleNNG
215 208 214 eqtr4d RCRingFBGBbBcBaseRdBeNe×N×c·˙fd˙Ge×N=e×N×c·˙fde×NRmaMuleNNG
216 215 3adant3 RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×Ne×N×c·˙fd˙Ge×N=e×N×c·˙fde×NRmaMuleNNG
217 190 202 216 3eqtr4d RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×Nb˙Ge×N=e×N×c·˙fd˙Ge×N
218 simp3r RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×NbNe×N=dNe×N
219 218 oveq1d RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×NbNe×NRmaMulNeNNG=dNe×NRmaMulNeNNG
220 192 reseq1d RCRingFBGBbBcBaseRdBeNbRmaMulNNNGNe×N=b˙GNe×N
221 difssd RCRingFBGBbBcBaseRdBeNNeN
222 52 143 6 194 195 195 195 221 198 199 mamures RCRingFBGBbBcBaseRdBeNbRmaMulNNNGNe×N=bNe×NRmaMulNeNNG
223 220 222 eqtr3d RCRingFBGBbBcBaseRdBeNb˙GNe×N=bNe×NRmaMulNeNNG
224 223 3adant3 RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×Nb˙GNe×N=bNe×NRmaMulNeNNG
225 203 reseq1d RCRingFBGBbBcBaseRdBeNdRmaMulNNNGNe×N=d˙GNe×N
226 52 143 6 194 195 195 195 221 205 199 mamures RCRingFBGBbBcBaseRdBeNdRmaMulNNNGNe×N=dNe×NRmaMulNeNNG
227 225 226 eqtr3d RCRingFBGBbBcBaseRdBeNd˙GNe×N=dNe×NRmaMulNeNNG
228 227 3adant3 RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×Nd˙GNe×N=dNe×NRmaMulNeNNG
229 219 224 228 3eqtr4d RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×Nb˙GNe×N=d˙GNe×N
230 3 1 2 6 4 178 183 184 187 188 217 229 mdetrsca RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×NDb˙G=c·˙Dd˙G
231 simp2ll RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×NbB
232 231 31 syl RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×NaBDa˙Gb=Db˙G
233 simp2rl RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×NdB
234 169 oveq2d dBc·˙aBDa˙Gd=c·˙Dd˙G
235 233 234 syl RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×Nc·˙aBDa˙Gd=c·˙Dd˙G
236 230 232 235 3eqtr4d RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×NaBDa˙Gb=c·˙aBDa˙Gd
237 236 3expia RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×NaBDa˙Gb=c·˙aBDa˙Gd
238 237 anassrs RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×NaBDa˙Gb=c·˙aBDa˙Gd
239 238 ralrimivva RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×NaBDa˙Gb=c·˙aBDa˙Gd
240 239 ralrimivva RCRingFBGBbBcBaseRdBeNbe×N=e×N×c·˙fde×NbNe×N=dNe×NaBDa˙Gb=c·˙aBDa˙Gd
241 simp2 RCRingFBGBFB
242 1 2 6 7 8 9 4 12 14 26 82 177 240 3 51 241 mdetuni0 RCRingFBGBaBDa˙GF=aBDa˙G1A·˙DF
243 fvoveq1 a=FDa˙G=DF˙G
244 fvex DF˙GV
245 243 29 244 fvmpt FBaBDa˙GF=DF˙G
246 245 3ad2ant2 RCRingFBGBaBDa˙GF=DF˙G
247 eqid 1A=1A
248 2 247 ringidcl ARing1AB
249 fvoveq1 a=1ADa˙G=D1A˙G
250 fvex D1A˙GV
251 249 29 250 fvmpt 1ABaBDa˙G1A=D1A˙G
252 19 248 251 3syl RCRingFBGBaBDa˙G1A=D1A˙G
253 simp3 RCRingFBGBGB
254 2 5 247 ringlidm ARingGB1A˙G=G
255 19 253 254 syl2anc RCRingFBGB1A˙G=G
256 255 fveq2d RCRingFBGBD1A˙G=DG
257 252 256 eqtrd RCRingFBGBaBDa˙G1A=DG
258 257 oveq1d RCRingFBGBaBDa˙G1A·˙DF=DG·˙DF
259 16 253 ffvelrnd RCRingFBGBDGBaseR
260 16 241 ffvelrnd RCRingFBGBDFBaseR
261 6 4 crngcom RCRingDGBaseRDFBaseRDG·˙DF=DF·˙DG
262 51 259 260 261 syl3anc RCRingFBGBDG·˙DF=DF·˙DG
263 258 262 eqtrd RCRingFBGBaBDa˙G1A·˙DF=DF·˙DG
264 242 246 263 3eqtr3d RCRingFBGBDF˙G=DF·˙DG