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

Theorem mdetmul 18998
 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.)
Hypotheses
Ref Expression
mdetmul.a Mat
mdetmul.b
mdetmul.t1
mdetmul.t2
Assertion
Ref Expression
mdetmul

Proof of Theorem mdetmul
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mdetmul.a . . 3 Mat
2 mdetmul.b . . 3
3 eqid 2443 . . 3
4 eqid 2443 . . 3
5 eqid 2443 . . 3
6 eqid 2443 . . 3
7 mdetmul.t1 . . 3
81, 2matrcl 18787 . . . . 5
98simpld 459 . . . 4
11 crngring 17083 . . . 4
13 mdetmul.d . . . . . . . 8 maDet
1413, 1, 2, 3mdetf 18970 . . . . . . 7
15143ad2ant1 1018 . . . . . 6
1615adantr 465 . . . . 5
171matring 18818 . . . . . . . 8
1810, 12, 17syl2anc 661 . . . . . . 7
1918adantr 465 . . . . . 6
20 simpr 461 . . . . . 6
21 simpl3 1002 . . . . . 6
22 mdetmul.t2 . . . . . . 7
232, 22ringcl 17086 . . . . . 6
2419, 20, 21, 23syl3anc 1229 . . . . 5
2516, 24ffvelrnd 6017 . . . 4
26 eqid 2443 . . . 4
2725, 26fmptd 6040 . . 3
28 simp21 1030 . . . . . . 7
29 oveq1 6288 . . . . . . . . 9
3029fveq2d 5860 . . . . . . . 8
31 fvex 5866 . . . . . . . 8
3230, 26, 31fvmpt 5941 . . . . . . 7
3328, 32syl 16 . . . . . 6
34 simp11 1027 . . . . . . 7
3518adantr 465 . . . . . . . . 9
36 simpr1 1003 . . . . . . . . 9
37 simpl3 1002 . . . . . . . . 9
382, 22ringcl 17086 . . . . . . . . 9
3935, 36, 37, 38syl3anc 1229 . . . . . . . 8
40393adant3 1017 . . . . . . 7
41 simp22 1031 . . . . . . 7
42 simp23 1032 . . . . . . 7
43 simp3l 1025 . . . . . . 7
44 simpl3r 1053 . . . . . . . . . 10
45 eqid 2443 . . . . . . . . . . . 12
46 oveq1 6288 . . . . . . . . . . . . 13
4746ralimi 2836 . . . . . . . . . . . 12
48 mpteq12 4516 . . . . . . . . . . . 12
4945, 47, 48sylancr 663 . . . . . . . . . . 11
5049oveq2d 6297 . . . . . . . . . 10 g g
5144, 50syl 16 . . . . . . . . 9 g g
52 simp1 997 . . . . . . . . . . . . . . 15
53 eqid 2443 . . . . . . . . . . . . . . . . 17 maMul maMul
541, 53matmulr 18813 . . . . . . . . . . . . . . . 16 maMul
5554, 22syl6eqr 2502 . . . . . . . . . . . . . . 15 maMul
5610, 52, 55syl2anc 661 . . . . . . . . . . . . . 14 maMul
5756ad2antrr 725 . . . . . . . . . . . . 13 maMul
5857oveqd 6298 . . . . . . . . . . . 12 maMul
5958oveqd 6298 . . . . . . . . . . 11 maMul
60 simpll1 1036 . . . . . . . . . . . 12
6110ad2antrr 725 . . . . . . . . . . . 12
62 simplr1 1039 . . . . . . . . . . . . 13
631, 3, 2matbas2i 18797 . . . . . . . . . . . . 13
6462, 63syl 16 . . . . . . . . . . . 12
651, 3, 2matbas2i 18797 . . . . . . . . . . . . . 14
66653ad2ant3 1020 . . . . . . . . . . . . 13
6766ad2antrr 725 . . . . . . . . . . . 12
68 simplr2 1040 . . . . . . . . . . . 12
69 simpr 461 . . . . . . . . . . . 12
7053, 3, 7, 60, 61, 61, 61, 64, 67, 68, 69mamufv 18762 . . . . . . . . . . 11 maMul g
7159, 70eqtr3d 2486 . . . . . . . . . 10 g
72713adantl3 1155 . . . . . . . . 9 g
7358oveqd 6298 . . . . . . . . . . 11 maMul
74 simplr3 1041 . . . . . . . . . . . 12
7553, 3, 7, 60, 61, 61, 61, 64, 67, 74, 69mamufv 18762 . . . . . . . . . . 11 maMul g
7673, 75eqtr3d 2486 . . . . . . . . . 10 g
77763adantl3 1155 . . . . . . . . 9 g
7851, 72, 773eqtr4d 2494 . . . . . . . 8
7978ralrimiva 2857 . . . . . . 7
8013, 1, 2, 4, 34, 40, 41, 42, 43, 79mdetralt 18983 . . . . . 6
8133, 80eqtrd 2484 . . . . 5
82813expia 1199 . . . 4
8382ralrimivvva 2865 . . 3
84 simp11 1027 . . . . . . . . 9
8518adantr 465 . . . . . . . . . . 11
86 simprll 763 . . . . . . . . . . 11
87 simpl3 1002 . . . . . . . . . . 11
8885, 86, 87, 38syl3anc 1229 . . . . . . . . . 10
89883adant3 1017 . . . . . . . . 9
90 simprlr 764 . . . . . . . . . . 11
912, 22ringcl 17086 . . . . . . . . . . 11
9285, 90, 87, 91syl3anc 1229 . . . . . . . . . 10
93923adant3 1017 . . . . . . . . 9
94 simprrl 765 . . . . . . . . . . 11
952, 22ringcl 17086 . . . . . . . . . . 11
9685, 94, 87, 95syl3anc 1229 . . . . . . . . . 10
97963adant3 1017 . . . . . . . . 9
98 simp2rr 1067 . . . . . . . . 9
99 simp31 1033 . . . . . . . . . . . 12
10099oveq1d 6296 . . . . . . . . . . 11 maMul maMul
10112adantr 465 . . . . . . . . . . . . 13
102 eqid 2443 . . . . . . . . . . . . 13 maMul maMul
103 snfi 7598 . . . . . . . . . . . . . 14
104103a1i 11 . . . . . . . . . . . . 13
10510adantr 465 . . . . . . . . . . . . 13
1061, 3, 2matbas2i 18797 . . . . . . . . . . . . . . 15
10790, 106syl 16 . . . . . . . . . . . . . 14
108 simprrr 766 . . . . . . . . . . . . . . . 16
109108snssd 4160 . . . . . . . . . . . . . . 15
110 xpss1 5101 . . . . . . . . . . . . . . 15
111109, 110syl 16 . . . . . . . . . . . . . 14
112 elmapssres 7445 . . . . . . . . . . . . . 14
113107, 111, 112syl2anc 661 . . . . . . . . . . . . 13
1141, 3, 2matbas2i 18797 . . . . . . . . . . . . . . 15
11594, 114syl 16 . . . . . . . . . . . . . 14
116 elmapssres 7445 . . . . . . . . . . . . . 14
117115, 111, 116syl2anc 661 . . . . . . . . . . . . 13
11866adantr 465 . . . . . . . . . . . . 13
1193, 101, 102, 104, 105, 105, 6, 113, 117, 118mamudi 18778 . . . . . . . . . . . 12 maMul maMul maMul
1201193adant3 1017 . . . . . . . . . . 11 maMul maMul maMul
121100, 120eqtrd 2484 . . . . . . . . . 10 maMul maMul maMul
12256adantr 465 . . . . . . . . . . . . . 14 maMul
123122oveqd 6298 . . . . . . . . . . . . 13 maMul
124123reseq1d 5262 . . . . . . . . . . . 12 maMul
125 simpl1 1000 . . . . . . . . . . . . 13
12686, 63syl 16 . . . . . . . . . . . . 13
12753, 102, 3, 125, 105, 105, 105, 109, 126, 118mamures 18765 . . . . . . . . . . . 12 maMul maMul
128124, 127eqtr3d 2486 . . . . . . . . . . 11 maMul
1291283adant3 1017 . . . . . . . . . 10 maMul
130122oveqd 6298 . . . . . . . . . . . . . 14 maMul
131130reseq1d 5262 . . . . . . . . . . . . 13 maMul
13253, 102, 3, 125, 105, 105, 105, 109, 107, 118mamures 18765 . . . . . . . . . . . . 13 maMul maMul
133131, 132eqtr3d 2486 . . . . . . . . . . . 12 maMul
134122oveqd 6298 . . . . . . . . . . . . . 14 maMul
135134reseq1d 5262 . . . . . . . . . . . . 13 maMul
13653, 102, 3, 125, 105, 105, 105, 109, 115, 118mamures 18765 . . . . . . . . . . . . 13 maMul maMul
137135, 136eqtr3d 2486 . . . . . . . . . . . 12 maMul
138133, 137oveq12d 6299 . . . . . . . . . . 11 maMul maMul
1391383adant3 1017 . . . . . . . . . 10 maMul maMul
140121, 129, 1393eqtr4d 2494 . . . . . . . . 9
141 simp32 1034 . . . . . . . . . . 11
142141oveq1d 6296 . . . . . . . . . 10 maMul maMul
143123reseq1d 5262 . . . . . . . . . . . 12 maMul
144 eqid 2443 . . . . . . . . . . . . 13 maMul maMul
145 difssd 3617 . . . . . . . . . . . . 13
14653, 144, 3, 125, 105, 105, 105, 145, 126, 118mamures 18765 . . . . . . . . . . . 12 maMul maMul
147143, 146eqtr3d 2486 . . . . . . . . . . 11 maMul
1481473adant3 1017 . . . . . . . . . 10 maMul
149130reseq1d 5262 . . . . . . . . . . . 12 maMul
15053, 144, 3, 125, 105, 105, 105, 145, 107, 118mamures 18765 . . . . . . . . . . . 12 maMul maMul
151149, 150eqtr3d 2486 . . . . . . . . . . 11 maMul
1521513adant3 1017 . . . . . . . . . 10 maMul
153142, 148, 1523eqtr4d 2494 . . . . . . . . 9
154 simp33 1035 . . . . . . . . . . 11
155154oveq1d 6296 . . . . . . . . . 10 maMul maMul
156134reseq1d 5262 . . . . . . . . . . . 12 maMul
15753, 144, 3, 125, 105, 105, 105, 145, 115, 118mamures 18765 . . . . . . . . . . . 12 maMul maMul
158156, 157eqtr3d 2486 . . . . . . . . . . 11 maMul
1591583adant3 1017 . . . . . . . . . 10 maMul
160155, 148, 1593eqtr4d 2494 . . . . . . . . 9
16113, 1, 2, 6, 84, 89, 93, 97, 98, 140, 153, 160mdetrlin 18977 . . . . . . . 8
16286, 32syl 16 . . . . . . . . 9
1631623adant3 1017 . . . . . . . 8
164 oveq1 6288 . . . . . . . . . . . . 13
165164fveq2d 5860 . . . . . . . . . . . 12
166 fvex 5866 . . . . . . . . . . . 12
167165, 26, 166fvmpt 5941 . . . . . . . . . . 11
16890, 167syl 16 . . . . . . . . . 10
169 oveq1 6288 . . . . . . . . . . . . 13
170169fveq2d 5860 . . . . . . . . . . . 12
171 fvex 5866 . . . . . . . . . . . 12
172170, 26, 171fvmpt 5941 . . . . . . . . . . 11
17394, 172syl 16 . . . . . . . . . 10
174168, 173oveq12d 6299 . . . . . . . . 9
1751743adant3 1017 . . . . . . . 8
176161, 163, 1753eqtr4d 2494 . . . . . . 7
1771763expia 1199 . . . . . 6
178177anassrs 648 . . . . 5
179178ralrimivva 2864 . . . 4
180179ralrimivva 2864 . . 3
181 simp11 1027 . . . . . . . . 9
18218adantr 465 . . . . . . . . . . 11
183 simprll 763 . . . . . . . . . . 11
184 simpl3 1002 . . . . . . . . . . 11
185182, 183, 184, 38syl3anc 1229 . . . . . . . . . 10
1861853adant3 1017 . . . . . . . . 9
187 simp2lr 1065 . . . . . . . . 9
188 simprrl 765 . . . . . . . . . . 11
189182, 188, 184, 95syl3anc 1229 . . . . . . . . . 10
1901893adant3 1017 . . . . . . . . 9
191 simp2rr 1067 . . . . . . . . 9
192 simp3l 1025 . . . . . . . . . . 11
193192oveq1d 6296 . . . . . . . . . 10 maMul maMul
19456adantr 465 . . . . . . . . . . . . . 14 maMul
195194oveqd 6298 . . . . . . . . . . . . 13 maMul
196195reseq1d 5262 . . . . . . . . . . . 12 maMul
197 simpl1 1000 . . . . . . . . . . . . 13
19810adantr 465 . . . . . . . . . . . . 13
199 simprrr 766 . . . . . . . . . . . . . 14
200199snssd 4160 . . . . . . . . . . . . 13
201183, 63syl 16 . . . . . . . . . . . . 13
20266adantr 465 . . . . . . . . . . . . 13
20353, 102, 3, 197, 198, 198, 198, 200, 201, 202mamures 18765 . . . . . . . . . . . 12 maMul maMul
204196, 203eqtr3d 2486 . . . . . . . . . . 11 maMul
2052043adant3 1017 . . . . . . . . . 10 maMul
206194oveqd 6298 . . . . . . . . . . . . . . 15 maMul
207206reseq1d 5262 . . . . . . . . . . . . . 14 maMul
208188, 114syl 16 . . . . . . . . . . . . . . 15
20953, 102, 3, 197, 198, 198, 198, 200, 208, 202mamures 18765 . . . . . . . . . . . . . 14 maMul maMul
210207, 209eqtr3d 2486 . . . . . . . . . . . . 13 maMul
211210oveq2d 6297 . . . . . . . . . . . 12 maMul
21212adantr 465 . . . . . . . . . . . . 13
213103a1i 11 . . . . . . . . . . . . 13
214 simprlr 764 . . . . . . . . . . . . 13
215200, 110syl 16 . . . . . . . . . . . . . 14
216208, 215, 116syl2anc 661 . . . . . . . . . . . . 13
2173, 212, 102, 213, 198, 198, 7, 214, 216, 202mamuvs1 18780 . . . . . . . . . . . 12 maMul maMul
218211, 217eqtr4d 2487 . . . . . . . . . . 11 maMul
2192183adant3 1017 . . . . . . . . . 10