Metamath Proof Explorer

Theorem maduval

Description: Second 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 maduval ⊢ M ∈ B → J ⁡ M = 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 1 4 matrcl ⊢ M ∈ B → N ∈ Fin ∧ R ∈ V
8 7 simpld ⊢ M ∈ B → N ∈ Fin
9 mpoexga ⊢ N ∈ Fin ∧ N ∈ Fin → i ∈ N , j ∈ N ⟼ D ⁡ k ∈ N , l ∈ N ⟼ if k = j if l = i 1 ˙ 0 ˙ k M l ∈ V
10 8 8 9 syl2anc ⊢ M ∈ B → i ∈ N , j ∈ N ⟼ D ⁡ k ∈ N , l ∈ N ⟼ if k = j if l = i 1 ˙ 0 ˙ k M l ∈ V
11 oveq ⊢ m = M → k m l = k M l
12 11 ifeq2d ⊢ m = M → if k = j if l = i 1 ˙ 0 ˙ k m l = if k = j if l = i 1 ˙ 0 ˙ k M l
13 12 mpoeq3dv ⊢ m = M → 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 ˙ 0 ˙ k M l
14 13 3ad2ant1 ⊢ m = M ∧ i ∈ N ∧ j ∈ N → 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 ˙ 0 ˙ k M l
15 14 fveq2d ⊢ m = M ∧ i ∈ N ∧ j ∈ N → D ⁡ k ∈ N , l ∈ N ⟼ if k = j if l = i 1 ˙ 0 ˙ k m l = D ⁡ k ∈ N , l ∈ N ⟼ if k = j if l = i 1 ˙ 0 ˙ k M l
16 15 mpoeq3dva ⊢ m = M → i ∈ N , j ∈ N ⟼ D ⁡ k ∈ N , l ∈ N ⟼ if k = j if l = i 1 ˙ 0 ˙ k m l = i ∈ N , j ∈ N ⟼ D ⁡ k ∈ N , l ∈ N ⟼ if k = j if l = i 1 ˙ 0 ˙ k M l
17 1 2 3 4 5 6 madufval ⊢ J = m ∈ B ⟼ i ∈ N , j ∈ N ⟼ D ⁡ k ∈ N , l ∈ N ⟼ if k = j if l = i 1 ˙ 0 ˙ k m l
18 16 17 fvmptg ⊢ M ∈ B ∧ i ∈ N , j ∈ N ⟼ D ⁡ k ∈ N , l ∈ N ⟼ if k = j if l = i 1 ˙ 0 ˙ k M l ∈ V → J ⁡ M = i ∈ N , j ∈ N ⟼ D ⁡ k ∈ N , l ∈ N ⟼ if k = j if l = i 1 ˙ 0 ˙ k M l
19 10 18 mpdan ⊢ M ∈ B → J ⁡ M = i ∈ N , j ∈ N ⟼ D ⁡ k ∈ N , l ∈ N ⟼ if k = j if l = i 1 ˙ 0 ˙ k M l