Metamath Proof Explorer

Theorem submaeval

Description: An entry of a submatrix of a square matrix. (Contributed by AV, 28-Dec-2018)

Ref Expression
Hypotheses submafval.a ⊢A=NMatR
submafval.q ⊢Q=NsubMatR
submafval.b ⊢B=BaseA
Assertion submaeval ⊢M∈B∧K∈N∧L∈N∧I∈N∖K∧J∈N∖L→IKQ⁡MLJ=IMJ

Proof

Step Hyp Ref Expression
1 submafval.a ⊢A=NMatR
2 submafval.q ⊢Q=NsubMatR
3 submafval.b ⊢B=BaseA
4 1 2 3 submaval ⊢M∈B∧K∈N∧L∈N→KQ⁡ML=i∈N∖K,j∈N∖L⟼iMj
5 4 3expb ⊢M∈B∧K∈N∧L∈N→KQ⁡ML=i∈N∖K,j∈N∖L⟼iMj
6 5 3adant3 ⊢M∈B∧K∈N∧L∈N∧I∈N∖K∧J∈N∖L→KQ⁡ML=i∈N∖K,j∈N∖L⟼iMj
7 simp3l ⊢M∈B∧K∈N∧L∈N∧I∈N∖K∧J∈N∖L→I∈N∖K
8 simpl3r ⊢M∈B∧K∈N∧L∈N∧I∈N∖K∧J∈N∖L∧i=I→J∈N∖L
9 ovexd ⊢M∈B∧K∈N∧L∈N∧I∈N∖K∧J∈N∖L∧i=I∧j=J→iMj∈V
10 oveq12 ⊢i=I∧j=J→iMj=IMJ
11 10 adantl ⊢M∈B∧K∈N∧L∈N∧I∈N∖K∧J∈N∖L∧i=I∧j=J→iMj=IMJ
12 7 8 9 11 ovmpodv2 ⊢M∈B∧K∈N∧L∈N∧I∈N∖K∧J∈N∖L→KQ⁡ML=i∈N∖K,j∈N∖L⟼iMj→IKQ⁡MLJ=IMJ
13 6 12 mpd ⊢M∈B∧K∈N∧L∈N∧I∈N∖K∧J∈N∖L→IKQ⁡MLJ=IMJ