Metamath Proof Explorer

Theorem submaval0

Description: Second substitution for a submatrix. (Contributed by AV, 28-Dec-2018)

Ref Expression
Hypotheses submafval.a ⊢A=NMatR
submafval.q ⊢Q=NsubMatR
submafval.b ⊢B=BaseA
Assertion submaval0 ⊢M∈B→Q⁡M=k∈N,l∈N⟼i∈N∖k,j∈N∖l⟼iMj

Proof

Step Hyp Ref Expression
1 submafval.a ⊢A=NMatR
2 submafval.q ⊢Q=NsubMatR
3 submafval.b ⊢B=BaseA
4 1 3 matrcl ⊢M∈B→N∈Fin∧R∈V
5 4 simpld ⊢M∈B→N∈Fin
6 mpoexga ⊢N∈Fin∧N∈Fin→k∈N,l∈N⟼i∈N∖k,j∈N∖l⟼iMj∈V
7 5 5 6 syl2anc ⊢M∈B→k∈N,l∈N⟼i∈N∖k,j∈N∖l⟼iMj∈V
8 oveq ⊢m=M→imj=iMj
9 8 mpoeq3dv ⊢m=M→i∈N∖k,j∈N∖l⟼imj=i∈N∖k,j∈N∖l⟼iMj
10 9 mpoeq3dv ⊢m=M→k∈N,l∈N⟼i∈N∖k,j∈N∖l⟼imj=k∈N,l∈N⟼i∈N∖k,j∈N∖l⟼iMj
11 1 2 3 submafval ⊢Q=m∈B⟼k∈N,l∈N⟼i∈N∖k,j∈N∖l⟼imj
12 10 11 fvmptg ⊢M∈B∧k∈N,l∈N⟼i∈N∖k,j∈N∖l⟼iMj∈V→Q⁡M=k∈N,l∈N⟼i∈N∖k,j∈N∖l⟼iMj
13 7 12 mpdan ⊢M∈B→Q⁡M=k∈N,l∈N⟼i∈N∖k,j∈N∖l⟼iMj