Metamath Proof Explorer


Theorem madufval

Description: First substitution for the adjunct (cofactor) matrix. (Contributed by SO, 11-Jul-2018)

Ref Expression
Hypotheses madufval.a A = N Mat R
madufval.d D = N maDet R
madufval.j J = N maAdju R
madufval.b B = Base A
madufval.o 1 ˙ = 1 R
madufval.z 0 ˙ = 0 R
Assertion madufval J = m B i N , j N D k N , l N if k = j if l = i 1 ˙ 0 ˙ k m l

Proof

Step Hyp Ref Expression
1 madufval.a A = N Mat R
2 madufval.d D = N maDet R
3 madufval.j J = N maAdju R
4 madufval.b B = Base A
5 madufval.o 1 ˙ = 1 R
6 madufval.z 0 ˙ = 0 R
7 fvoveq1 n = N Base n Mat r = Base N Mat r
8 id n = N n = N
9 oveq1 n = N n maDet r = N maDet r
10 eqidd n = N if k = j if l = i 1 r 0 r k m l = if k = j if l = i 1 r 0 r k m l
11 8 8 10 mpoeq123dv n = N k n , l n if k = j if l = i 1 r 0 r k m l = k N , l N if k = j if l = i 1 r 0 r k m l
12 9 11 fveq12d n = N n maDet r k n , l n if k = j if l = i 1 r 0 r k m l = N maDet r k N , l N if k = j if l = i 1 r 0 r k m l
13 8 8 12 mpoeq123dv n = N i n , j n n maDet r k n , l n if k = j if l = i 1 r 0 r k m l = i N , j N N maDet r k N , l N if k = j if l = i 1 r 0 r k m l
14 7 13 mpteq12dv n = N m Base n Mat r i n , j n n maDet r k n , l n if k = j if l = i 1 r 0 r k m l = m Base N Mat r i N , j N N maDet r k N , l N if k = j if l = i 1 r 0 r k m l
15 oveq2 r = R N Mat r = N Mat R
16 15 fveq2d r = R Base N Mat r = Base N Mat R
17 oveq2 r = R N maDet r = N maDet R
18 fveq2 r = R 1 r = 1 R
19 fveq2 r = R 0 r = 0 R
20 18 19 ifeq12d r = R if l = i 1 r 0 r = if l = i 1 R 0 R
21 20 ifeq1d r = R if k = j if l = i 1 r 0 r k m l = if k = j if l = i 1 R 0 R k m l
22 21 mpoeq3dv r = R k N , l N if k = j if l = i 1 r 0 r k m l = k N , l N if k = j if l = i 1 R 0 R k m l
23 17 22 fveq12d r = R N maDet r k N , l N if k = j if l = i 1 r 0 r k m l = N maDet R k N , l N if k = j if l = i 1 R 0 R k m l
24 23 mpoeq3dv r = R i N , j N N maDet r k N , l N if k = j if l = i 1 r 0 r k m l = i N , j N N maDet R k N , l N if k = j if l = i 1 R 0 R k m l
25 16 24 mpteq12dv r = R m Base N Mat r i N , j N N maDet r k N , l N if k = j if l = i 1 r 0 r k m l = m Base N Mat R i N , j N N maDet R k N , l N if k = j if l = i 1 R 0 R k m l
26 df-madu maAdju = n V , r V m Base n Mat r i n , j n n maDet r k n , l n if k = j if l = i 1 r 0 r k m l
27 fvex Base N Mat R V
28 27 mptex m Base N Mat R i N , j N N maDet R k N , l N if k = j if l = i 1 R 0 R k m l V
29 14 25 26 28 ovmpo N V R V N maAdju R = m Base N Mat R i N , j N N maDet R k N , l N if k = j if l = i 1 R 0 R k m l
30 1 fveq2i Base A = Base N Mat R
31 4 30 eqtri B = Base N Mat R
32 5 a1i k N l N 1 ˙ = 1 R
33 6 a1i k N l N 0 ˙ = 0 R
34 32 33 ifeq12d k N l N if l = i 1 ˙ 0 ˙ = if l = i 1 R 0 R
35 34 ifeq1d k N l N if k = j if l = i 1 ˙ 0 ˙ k m l = if k = j if l = i 1 R 0 R k m l
36 35 mpoeq3ia k N , l N if k = j if l = i 1 ˙ 0 ˙ k m l = k N , l N if k = j if l = i 1 R 0 R k m l
37 2 36 fveq12i D k N , l N if k = j if l = i 1 ˙ 0 ˙ k m l = N maDet R k N , l N if k = j if l = i 1 R 0 R k m l
38 37 a1i i N j N D k N , l N if k = j if l = i 1 ˙ 0 ˙ k m l = N maDet R k N , l N if k = j if l = i 1 R 0 R k m l
39 38 mpoeq3ia i N , j N D k N , l N if k = j if l = i 1 ˙ 0 ˙ k m l = i N , j N N maDet R k N , l N if k = j if l = i 1 R 0 R k m l
40 31 39 mpteq12i m B i N , j N D k N , l N if k = j if l = i 1 ˙ 0 ˙ k m l = m Base N Mat R i N , j N N maDet R k N , l N if k = j if l = i 1 R 0 R k m l
41 29 40 eqtr4di N V R V N maAdju R = m B i N , j N D k N , l N if k = j if l = i 1 ˙ 0 ˙ k m l
42 26 reldmmpo Rel dom maAdju
43 42 ovprc ¬ N V R V N maAdju R =
44 df-mat Mat = n Fin , r V r freeLMod n × n sSet ndx r maMul n n n
45 44 reldmmpo Rel dom Mat
46 45 ovprc ¬ N V R V N Mat R =
47 1 46 syl5eq ¬ N V R V A =
48 47 fveq2d ¬ N V R V Base A = Base
49 base0 = Base
50 48 4 49 3eqtr4g ¬ N V R V B =
51 50 mpteq1d ¬ N V R V m B i N , j N D k N , l N if k = j if l = i 1 ˙ 0 ˙ k m l = m i N , j N D k N , l N if k = j if l = i 1 ˙ 0 ˙ k m l
52 mpt0 m i N , j N D k N , l N if k = j if l = i 1 ˙ 0 ˙ k m l =
53 51 52 eqtrdi ¬ N V R V m B i N , j N D k N , l N if k = j if l = i 1 ˙ 0 ˙ k m l =
54 43 53 eqtr4d ¬ N V R V N maAdju R = m B i N , j N D k N , l N if k = j if l = i 1 ˙ 0 ˙ k m l
55 41 54 pm2.61i N maAdju R = m B i N , j N D k N , l N if k = j if l = i 1 ˙ 0 ˙ k m l
56 3 55 eqtri J = m B i N , j N D k N , l N if k = j if l = i 1 ˙ 0 ˙ k m l