Step | Hyp | Ref
| Expression |
1 | | madufval.j |
. 2
maAdju |
2 | | oveq1 6657 |
. . . . . . 7
Mat Mat |
3 | 2 | fveq2d 6195 |
. . . . . 6
Mat Mat |
4 | | id 22 |
. . . . . . 7
|
5 | | oveq1 6657 |
. . . . . . . 8
maDet maDet |
6 | | eqidd 2623 |
. . . . . . . . 9
|
7 | 4, 4, 6 | mpt2eq123dv 6717 |
. . . . . . . 8
|
8 | 5, 7 | fveq12d 6197 |
. . . . . . 7
maDet
maDet
|
9 | 4, 4, 8 | mpt2eq123dv 6717 |
. . . . . 6
maDet
maDet |
10 | 3, 9 | mpteq12dv 4733 |
. . . . 5
Mat maDet Mat maDet |
11 | | oveq2 6658 |
. . . . . . 7
Mat Mat |
12 | 11 | fveq2d 6195 |
. . . . . 6
Mat Mat |
13 | | oveq2 6658 |
. . . . . . . 8
maDet maDet |
14 | | fveq2 6191 |
. . . . . . . . . . 11
|
15 | | fveq2 6191 |
. . . . . . . . . . 11
|
16 | 14, 15 | ifeq12d 4106 |
. . . . . . . . . 10
|
17 | 16 | ifeq1d 4104 |
. . . . . . . . 9
|
18 | 17 | mpt2eq3dv 6721 |
. . . . . . . 8
|
19 | 13, 18 | fveq12d 6197 |
. . . . . . 7
maDet
maDet
|
20 | 19 | mpt2eq3dv 6721 |
. . . . . 6
maDet
maDet |
21 | 12, 20 | mpteq12dv 4733 |
. . . . 5
Mat maDet Mat maDet |
22 | | df-madu 20440 |
. . . . 5
maAdju Mat maDet |
23 | | fvex 6201 |
. . . . . 6
Mat |
24 | 23 | mptex 6486 |
. . . . 5
Mat maDet |
25 | 10, 21, 22, 24 | ovmpt2 6796 |
. . . 4
maAdju Mat maDet |
26 | | madufval.b |
. . . . . 6
|
27 | | madufval.a |
. . . . . . 7
Mat |
28 | 27 | fveq2i 6194 |
. . . . . 6
Mat |
29 | 26, 28 | eqtri 2644 |
. . . . 5
Mat |
30 | | madufval.d |
. . . . . . . 8
maDet |
31 | | madufval.o |
. . . . . . . . . . . 12
|
32 | 31 | a1i 11 |
. . . . . . . . . . 11
|
33 | | madufval.z |
. . . . . . . . . . . 12
|
34 | 33 | a1i 11 |
. . . . . . . . . . 11
|
35 | 32, 34 | ifeq12d 4106 |
. . . . . . . . . 10
|
36 | 35 | ifeq1d 4104 |
. . . . . . . . 9
|
37 | 36 | mpt2eq3ia 6720 |
. . . . . . . 8
|
38 | 30, 37 | fveq12i 6196 |
. . . . . . 7
maDet |
39 | 38 | a1i 11 |
. . . . . 6
maDet |
40 | 39 | mpt2eq3ia 6720 |
. . . . 5
maDet |
41 | 29, 40 | mpteq12i 4742 |
. . . 4
Mat maDet |
42 | 25, 41 | syl6eqr 2674 |
. . 3
maAdju
|
43 | 22 | reldmmpt2 6771 |
. . . . 5
maAdju |
44 | 43 | ovprc 6683 |
. . . 4
maAdju |
45 | | df-mat 20214 |
. . . . . . . . . . 11
Mat freeLMod sSet
maMul |
46 | 45 | reldmmpt2 6771 |
. . . . . . . . . 10
Mat |
47 | 46 | ovprc 6683 |
. . . . . . . . 9
Mat |
48 | 27, 47 | syl5eq 2668 |
. . . . . . . 8
|
49 | 48 | fveq2d 6195 |
. . . . . . 7
|
50 | | base0 15912 |
. . . . . . 7
|
51 | 49, 26, 50 | 3eqtr4g 2681 |
. . . . . 6
|
52 | 51 | mpteq1d 4738 |
. . . . 5
|
53 | | mpt0 6021 |
. . . . 5
|
54 | 52, 53 | syl6eq 2672 |
. . . 4
|
55 | 44, 54 | eqtr4d 2659 |
. . 3
maAdju
|
56 | 42, 55 | pm2.61i 176 |
. 2
maAdju |
57 | 1, 56 | eqtri 2644 |
1
|