Metamath Proof Explorer

Theorem maducoevalmin1

Description: The coefficients of an adjunct (matrix of cofactors) expressed as determinants of the minor matrices (alternative definition) of the original matrix. (Contributed by AV, 31-Dec-2018)

Ref Expression
Hypotheses maducoevalmin1.a ⊢ A = N Mat R
maducoevalmin1.b ⊢ B = Base A
maducoevalmin1.d ⊢ D = N maDet R
maducoevalmin1.j ⊢ J = N maAdju R
Assertion maducoevalmin1 ⊢ M ∈ B ∧ I ∈ N ∧ H ∈ N → I J ⁡ M H = D ⁡ H N minMatR1 R ⁡ M I

Proof

Step Hyp Ref Expression
1 maducoevalmin1.a ⊢ A = N Mat R
2 maducoevalmin1.b ⊢ B = Base A
3 maducoevalmin1.d ⊢ D = N maDet R
4 maducoevalmin1.j ⊢ J = N maAdju R
5 eqid ⊢ 1 R = 1 R
6 eqid ⊢ 0 R = 0 R
7 1 3 4 2 5 6 maducoeval ⊢ M ∈ B ∧ I ∈ N ∧ H ∈ N → I J ⁡ M H = D ⁡ i ∈ N , j ∈ N ⟼ if i = H if j = I 1 R 0 R i M j
8 eqid ⊢ N minMatR1 R = N minMatR1 R
9 1 2 8 5 6 minmar1val ⊢ M ∈ B ∧ H ∈ N ∧ I ∈ N → H N minMatR1 R ⁡ M I = i ∈ N , j ∈ N ⟼ if i = H if j = I 1 R 0 R i M j
10 9 3com23 ⊢ M ∈ B ∧ I ∈ N ∧ H ∈ N → H N minMatR1 R ⁡ M I = i ∈ N , j ∈ N ⟼ if i = H if j = I 1 R 0 R i M j
11 10 eqcomd ⊢ M ∈ B ∧ I ∈ N ∧ H ∈ N → i ∈ N , j ∈ N ⟼ if i = H if j = I 1 R 0 R i M j = H N minMatR1 R ⁡ M I
12 11 fveq2d ⊢ M ∈ B ∧ I ∈ N ∧ H ∈ N → D ⁡ i ∈ N , j ∈ N ⟼ if i = H if j = I 1 R 0 R i M j = D ⁡ H N minMatR1 R ⁡ M I
13 7 12 eqtrd ⊢ M ∈ B ∧ I ∈ N ∧ H ∈ N → I J ⁡ M H = D ⁡ H N minMatR1 R ⁡ M I