Description: First substitution for the definition of a matrix for a minor. (Contributed by AV, 31-Dec-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | minmar1fval.a | |
|
minmar1fval.b | |
||
minmar1fval.q | |
||
minmar1fval.o | |
||
minmar1fval.z | |
||
Assertion | minmar1fval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | minmar1fval.a | |
|
2 | minmar1fval.b | |
|
3 | minmar1fval.q | |
|
4 | minmar1fval.o | |
|
5 | minmar1fval.z | |
|
6 | oveq12 | |
|
7 | 6 1 | eqtr4di | |
8 | 7 | fveq2d | |
9 | 8 2 | eqtr4di | |
10 | simpl | |
|
11 | fveq2 | |
|
12 | 11 4 | eqtr4di | |
13 | fveq2 | |
|
14 | 13 5 | eqtr4di | |
15 | 12 14 | ifeq12d | |
16 | 15 | ifeq1d | |
17 | 16 | adantl | |
18 | 10 10 17 | mpoeq123dv | |
19 | 10 10 18 | mpoeq123dv | |
20 | 9 19 | mpteq12dv | |
21 | df-minmar1 | |
|
22 | 2 | fvexi | |
23 | 22 | mptex | |
24 | 20 21 23 | ovmpoa | |
25 | 21 | mpondm0 | |
26 | mpt0 | |
|
27 | 25 26 | eqtr4di | |
28 | 1 | fveq2i | |
29 | 2 28 | eqtri | |
30 | matbas0pc | |
|
31 | 29 30 | eqtrid | |
32 | 31 | mpteq1d | |
33 | 27 32 | eqtr4d | |
34 | 24 33 | pm2.61i | |
35 | 3 34 | eqtri | |