Metamath Proof Explorer

Theorem submaval

Description: Third 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 submaval ⊢M∈B∧K∈N∧L∈N→KQ⁡ML=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 2 3 submaval0 ⊢M∈B→Q⁡M=k∈N,l∈N⟼i∈N∖k,j∈N∖l⟼iMj
5 4 3ad2ant1 ⊢M∈B∧K∈N∧L∈N→Q⁡M=k∈N,l∈N⟼i∈N∖k,j∈N∖l⟼iMj
6 simp2 ⊢M∈B∧K∈N∧L∈N→K∈N
7 simpl3 ⊢M∈B∧K∈N∧L∈N∧k=K→L∈N
8 1 3 matrcl ⊢M∈B→N∈Fin∧R∈V
9 8 simpld ⊢M∈B→N∈Fin
10 diffi ⊢N∈Fin→N∖k∈Fin
11 9 10 syl ⊢M∈B→N∖k∈Fin
12 diffi ⊢N∈Fin→N∖l∈Fin
13 9 12 syl ⊢M∈B→N∖l∈Fin
14 11 13 jca ⊢M∈B→N∖k∈Fin∧N∖l∈Fin
15 14 3ad2ant1 ⊢M∈B∧K∈N∧L∈N→N∖k∈Fin∧N∖l∈Fin
16 15 adantr ⊢M∈B∧K∈N∧L∈N∧k=K∧l=L→N∖k∈Fin∧N∖l∈Fin
17 mpoexga ⊢N∖k∈Fin∧N∖l∈Fin→i∈N∖k,j∈N∖l⟼iMj∈V
18 16 17 syl ⊢M∈B∧K∈N∧L∈N∧k=K∧l=L→i∈N∖k,j∈N∖l⟼iMj∈V
19 sneq ⊢k=K→k=K
20 19 difeq2d ⊢k=K→N∖k=N∖K
21 20 adantr ⊢k=K∧l=L→N∖k=N∖K
22 sneq ⊢l=L→l=L
23 22 difeq2d ⊢l=L→N∖l=N∖L
24 23 adantl ⊢k=K∧l=L→N∖l=N∖L
25 eqidd ⊢k=K∧l=L→iMj=iMj
26 21 24 25 mpoeq123dv ⊢k=K∧l=L→i∈N∖k,j∈N∖l⟼iMj=i∈N∖K,j∈N∖L⟼iMj
27 26 adantl ⊢M∈B∧K∈N∧L∈N∧k=K∧l=L→i∈N∖k,j∈N∖l⟼iMj=i∈N∖K,j∈N∖L⟼iMj
28 6 7 18 27 ovmpodv2 ⊢M∈B∧K∈N∧L∈N→Q⁡M=k∈N,l∈N⟼i∈N∖k,j∈N∖l⟼iMj→KQ⁡ML=i∈N∖K,j∈N∖L⟼iMj
29 5 28 mpd ⊢M∈B∧K∈N∧L∈N→KQ⁡ML=i∈N∖K,j∈N∖L⟼iMj