Description: Functionality of the determinant, see also definition in Lang p. 513. (Contributed by Stefan O'Rear, 9-Jul-2018) (Proof shortened by AV, 23-Jul-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mdetf.d | |
|
mdetf.a | |
||
mdetf.b | |
||
mdetf.k | |
||
Assertion | mdetf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mdetf.d | |
|
2 | mdetf.a | |
|
3 | mdetf.b | |
|
4 | mdetf.k | |
|
5 | crngring | |
|
6 | 5 | adantr | |
7 | ringcmn | |
|
8 | 6 7 | syl | |
9 | 2 3 | matrcl | |
10 | 9 | adantl | |
11 | 10 | simpld | |
12 | eqid | |
|
13 | eqid | |
|
14 | 12 13 | symgbasfi | |
15 | 11 14 | syl | |
16 | 5 | ad2antrr | |
17 | zrhpsgnmhm | |
|
18 | 6 11 17 | syl2anc | |
19 | eqid | |
|
20 | 19 4 | mgpbas | |
21 | 13 20 | mhmf | |
22 | 18 21 | syl | |
23 | 22 | ffvelrnda | |
24 | 19 | crngmgp | |
25 | 24 | ad2antrr | |
26 | 11 | adantr | |
27 | 2 4 3 | matbas2i | |
28 | 27 | ad3antlr | |
29 | elmapi | |
|
30 | 28 29 | syl | |
31 | 12 13 | symgbasf | |
32 | 31 | adantl | |
33 | 32 | ffvelrnda | |
34 | simpr | |
|
35 | 30 33 34 | fovrnd | |
36 | 35 | ralrimiva | |
37 | 20 25 26 36 | gsummptcl | |
38 | eqid | |
|
39 | 4 38 | ringcl | |
40 | 16 23 37 39 | syl3anc | |
41 | 40 | ralrimiva | |
42 | 4 8 15 41 | gsummptcl | |
43 | eqid | |
|
44 | eqid | |
|
45 | 1 2 3 13 43 44 38 19 | mdetfval | |
46 | 42 45 | fmptd | |