Metamath Proof Explorer

Theorem minmar1val0

Description: Second substitution for the definition of a matrix for a minor. (Contributed by AV, 31-Dec-2018)

Ref Expression
Hypotheses minmar1fval.a ⊢ A = N Mat R
minmar1fval.b ⊢ B = Base A
minmar1fval.q ⊢ Q = N minMatR1 R
minmar1fval.o ⊢ 1 ˙ = 1 R
minmar1fval.z ⊢ 0 ˙ = 0 R
Assertion minmar1val0 ⊢ M ∈ B → Q ⁡ M = k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l 1 ˙ 0 ˙ i M j

Proof

Step Hyp Ref Expression
1 minmar1fval.a ⊢ A = N Mat R
2 minmar1fval.b ⊢ B = Base A
3 minmar1fval.q ⊢ Q = N minMatR1 R
4 minmar1fval.o ⊢ 1 ˙ = 1 R
5 minmar1fval.z ⊢ 0 ˙ = 0 R
6 1 2 matrcl ⊢ M ∈ B → N ∈ Fin ∧ R ∈ V
7 6 simpld ⊢ M ∈ B → N ∈ Fin
8 mpoexga ⊢ N ∈ Fin ∧ N ∈ Fin → k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l 1 ˙ 0 ˙ i M j ∈ V
9 7 7 8 syl2anc ⊢ M ∈ B → k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l 1 ˙ 0 ˙ i M j ∈ V
10 oveq ⊢ m = M → i m j = i M j
11 10 ifeq2d ⊢ m = M → if i = k if j = l 1 ˙ 0 ˙ i m j = if i = k if j = l 1 ˙ 0 ˙ i M j
12 11 mpoeq3dv ⊢ m = M → i ∈ N , j ∈ N ⟼ if i = k if j = l 1 ˙ 0 ˙ i m j = i ∈ N , j ∈ N ⟼ if i = k if j = l 1 ˙ 0 ˙ i M j
13 12 mpoeq3dv ⊢ m = M → k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l 1 ˙ 0 ˙ i m j = k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l 1 ˙ 0 ˙ i M j
14 1 2 3 4 5 minmar1fval ⊢ Q = m ∈ B ⟼ k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l 1 ˙ 0 ˙ i m j
15 13 14 fvmptg ⊢ M ∈ B ∧ k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l 1 ˙ 0 ˙ i M j ∈ V → Q ⁡ M = k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l 1 ˙ 0 ˙ i M j
16 9 15 mpdan ⊢ M ∈ B → Q ⁡ M = k ∈ N , l ∈ N ⟼ i ∈ N , j ∈ N ⟼ if i = k if j = l 1 ˙ 0 ˙ i M j