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 syl6eqr ⊢ 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 syl6eq ⊢ ¬ 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