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=NMatR
minmar1fval.b ⊢B=BaseA
minmar1fval.q ⊢Q=NminMatR1R
minmar1fval.o ⊢1˙=1R
minmar1fval.z ⊢0˙=0R
Assertion minmar1val0 ⊢M∈B→Q⁡M=k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=l1˙0˙iMj

Proof

Step Hyp Ref Expression
1 minmar1fval.a ⊢A=NMatR
2 minmar1fval.b ⊢B=BaseA
3 minmar1fval.q ⊢Q=NminMatR1R
4 minmar1fval.o ⊢1˙=1R
5 minmar1fval.z ⊢0˙=0R
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⟼ifi=kifj=l1˙0˙iMj∈V
9 7 7 8 syl2anc ⊢M∈B→k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=l1˙0˙iMj∈V
10 oveq ⊢m=M→imj=iMj
11 10 ifeq2d ⊢m=M→ifi=kifj=l1˙0˙imj=ifi=kifj=l1˙0˙iMj
12 11 mpoeq3dv ⊢m=M→i∈N,j∈N⟼ifi=kifj=l1˙0˙imj=i∈N,j∈N⟼ifi=kifj=l1˙0˙iMj
13 12 mpoeq3dv ⊢m=M→k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=l1˙0˙imj=k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=l1˙0˙iMj
14 1 2 3 4 5 minmar1fval ⊢Q=m∈B⟼k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=l1˙0˙imj
15 13 14 fvmptg ⊢M∈B∧k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=l1˙0˙iMj∈V→Q⁡M=k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=l1˙0˙iMj
16 9 15 mpdan ⊢M∈B→Q⁡M=k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=l1˙0˙iMj