Metamath Proof Explorer

Theorem maducoeval

Description: An entry of 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 maducoeval ⊢ M ∈ B ∧ I ∈ N ∧ H ∈ N → I J ⁡ M H = D ⁡ k ∈ N , l ∈ N ⟼ if k = H 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 2 3 4 5 6 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
8 7 3ad2ant1 ⊢ M ∈ B ∧ I ∈ N ∧ H ∈ N → J ⁡ M = i ∈ N , j ∈ N ⟼ D ⁡ k ∈ N , l ∈ N ⟼ if k = j if l = i 1 ˙ 0 ˙ k M l
9 simp1r ⊢ i = I ∧ j = H ∧ k ∈ N ∧ l ∈ N → j = H
10 9 eqeq2d ⊢ i = I ∧ j = H ∧ k ∈ N ∧ l ∈ N → k = j ↔ k = H
11 simp1l ⊢ i = I ∧ j = H ∧ k ∈ N ∧ l ∈ N → i = I
12 11 eqeq2d ⊢ i = I ∧ j = H ∧ k ∈ N ∧ l ∈ N → l = i ↔ l = I
13 12 ifbid ⊢ i = I ∧ j = H ∧ k ∈ N ∧ l ∈ N → if l = i 1 ˙ 0 ˙ = if l = I 1 ˙ 0 ˙
14 10 13 ifbieq1d ⊢ i = I ∧ j = H ∧ k ∈ N ∧ l ∈ N → if k = j if l = i 1 ˙ 0 ˙ k M l = if k = H if l = I 1 ˙ 0 ˙ k M l
15 14 mpoeq3dva ⊢ i = I ∧ j = H → k ∈ N , l ∈ N ⟼ if k = j if l = i 1 ˙ 0 ˙ k M l = k ∈ N , l ∈ N ⟼ if k = H if l = I 1 ˙ 0 ˙ k M l
16 15 fveq2d ⊢ i = I ∧ j = H → D ⁡ k ∈ N , l ∈ N ⟼ if k = j if l = i 1 ˙ 0 ˙ k M l = D ⁡ k ∈ N , l ∈ N ⟼ if k = H if l = I 1 ˙ 0 ˙ k M l
17 16 adantl ⊢ M ∈ B ∧ I ∈ N ∧ H ∈ N ∧ i = I ∧ j = H → D ⁡ k ∈ N , l ∈ N ⟼ if k = j if l = i 1 ˙ 0 ˙ k M l = D ⁡ k ∈ N , l ∈ N ⟼ if k = H if l = I 1 ˙ 0 ˙ k M l
18 simp2 ⊢ M ∈ B ∧ I ∈ N ∧ H ∈ N → I ∈ N
19 simp3 ⊢ M ∈ B ∧ I ∈ N ∧ H ∈ N → H ∈ N
20 fvexd ⊢ M ∈ B ∧ I ∈ N ∧ H ∈ N → D ⁡ k ∈ N , l ∈ N ⟼ if k = H if l = I 1 ˙ 0 ˙ k M l ∈ V
21 8 17 18 19 20 ovmpod ⊢ M ∈ B ∧ I ∈ N ∧ H ∈ N → I J ⁡ M H = D ⁡ k ∈ N , l ∈ N ⟼ if k = H if l = I 1 ˙ 0 ˙ k M l