Metamath Proof Explorer

Theorem submafval

Description: First 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 submafval ⊢Q=m∈B⟼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 oveq12 ⊢n=N∧r=R→nMatr=NMatR
5 4 1 eqtr4di ⊢n=N∧r=R→nMatr=A
6 5 fveq2d ⊢n=N∧r=R→BasenMatr=BaseA
7 6 3 eqtr4di ⊢n=N∧r=R→BasenMatr=B
8 simpl ⊢n=N∧r=R→n=N
9 difeq1 ⊢n=N→n∖k=N∖k
10 9 adantr ⊢n=N∧r=R→n∖k=N∖k
11 difeq1 ⊢n=N→n∖l=N∖l
12 11 adantr ⊢n=N∧r=R→n∖l=N∖l
13 eqidd ⊢n=N∧r=R→imj=imj
14 10 12 13 mpoeq123dv ⊢n=N∧r=R→i∈n∖k,j∈n∖l⟼imj=i∈N∖k,j∈N∖l⟼imj
15 8 8 14 mpoeq123dv ⊢n=N∧r=R→k∈n,l∈n⟼i∈n∖k,j∈n∖l⟼imj=k∈N,l∈N⟼i∈N∖k,j∈N∖l⟼imj
16 7 15 mpteq12dv ⊢n=N∧r=R→m∈BasenMatr⟼k∈n,l∈n⟼i∈n∖k,j∈n∖l⟼imj=m∈B⟼k∈N,l∈N⟼i∈N∖k,j∈N∖l⟼imj
17 df-subma ⊢subMat=n∈V,r∈V⟼m∈BasenMatr⟼k∈n,l∈n⟼i∈n∖k,j∈n∖l⟼imj
18 3 fvexi ⊢B∈V
19 18 mptex ⊢m∈B⟼k∈N,l∈N⟼i∈N∖k,j∈N∖l⟼imj∈V
20 16 17 19 ovmpoa ⊢N∈V∧R∈V→NsubMatR=m∈B⟼k∈N,l∈N⟼i∈N∖k,j∈N∖l⟼imj
21 17 mpondm0 ⊢¬N∈V∧R∈V→NsubMatR=∅
22 mpt0 ⊢m∈∅⟼k∈N,l∈N⟼i∈N∖k,j∈N∖l⟼imj=∅
23 21 22 eqtr4di ⊢¬N∈V∧R∈V→NsubMatR=m∈∅⟼k∈N,l∈N⟼i∈N∖k,j∈N∖l⟼imj
24 1 fveq2i ⊢BaseA=BaseNMatR
25 3 24 eqtri ⊢B=BaseNMatR
26 matbas0pc ⊢¬N∈V∧R∈V→BaseNMatR=∅
27 25 26 eqtrid ⊢¬N∈V∧R∈V→B=∅
28 27 mpteq1d ⊢¬N∈V∧R∈V→m∈B⟼k∈N,l∈N⟼i∈N∖k,j∈N∖l⟼imj=m∈∅⟼k∈N,l∈N⟼i∈N∖k,j∈N∖l⟼imj
29 23 28 eqtr4d ⊢¬N∈V∧R∈V→NsubMatR=m∈B⟼k∈N,l∈N⟼i∈N∖k,j∈N∖l⟼imj
30 20 29 pm2.61i ⊢NsubMatR=m∈B⟼k∈N,l∈N⟼i∈N∖k,j∈N∖l⟼imj
31 2 30 eqtri ⊢Q=m∈B⟼k∈N,l∈N⟼i∈N∖k,j∈N∖l⟼imj