Metamath Proof Explorer

Theorem marepvfval

Description: First substitution for the definition of the function replacing a column of a matrix by a vector. (Contributed by AV, 14-Feb-2019) (Revised by AV, 26-Feb-2019) (Proof shortened by AV, 2-Mar-2024)

Ref Expression
Hypotheses marepvfval.a ⊢A=NMatR
marepvfval.b ⊢B=BaseA
marepvfval.q ⊢Q=NmatRepVR
marepvfval.v ⊢V=BaseRN
Assertion marepvfval ⊢Q=m∈B,v∈V⟼k∈N⟼i∈N,j∈N⟼ifj=kv⁡iimj

Proof

Step Hyp Ref Expression
1 marepvfval.a ⊢A=NMatR
2 marepvfval.b ⊢B=BaseA
3 marepvfval.q ⊢Q=NmatRepVR
4 marepvfval.v ⊢V=BaseRN
5 2 fvexi ⊢B∈V
6 4 ovexi ⊢V∈V
7 6 a1i ⊢N∈V∧R∈V→V∈V
8 mpoexga ⊢B∈V∧V∈V→m∈B,v∈V⟼k∈N⟼i∈N,j∈N⟼ifj=kv⁡iimj∈V
9 5 7 8 sylancr ⊢N∈V∧R∈V→m∈B,v∈V⟼k∈N⟼i∈N,j∈N⟼ifj=kv⁡iimj∈V
10 oveq12 ⊢n=N∧r=R→nMatr=NMatR
11 10 1 eqtr4di ⊢n=N∧r=R→nMatr=A
12 11 fveq2d ⊢n=N∧r=R→BasenMatr=BaseA
13 12 2 eqtr4di ⊢n=N∧r=R→BasenMatr=B
14 fveq2 ⊢r=R→Baser=BaseR
15 14 adantl ⊢n=N∧r=R→Baser=BaseR
16 simpl ⊢n=N∧r=R→n=N
17 15 16 oveq12d ⊢n=N∧r=R→Basern=BaseRN
18 17 4 eqtr4di ⊢n=N∧r=R→Basern=V
19 eqidd ⊢n=N∧r=R→ifj=kv⁡iimj=ifj=kv⁡iimj
20 16 16 19 mpoeq123dv ⊢n=N∧r=R→i∈n,j∈n⟼ifj=kv⁡iimj=i∈N,j∈N⟼ifj=kv⁡iimj
21 16 20 mpteq12dv ⊢n=N∧r=R→k∈n⟼i∈n,j∈n⟼ifj=kv⁡iimj=k∈N⟼i∈N,j∈N⟼ifj=kv⁡iimj
22 13 18 21 mpoeq123dv ⊢n=N∧r=R→m∈BasenMatr,v∈Basern⟼k∈n⟼i∈n,j∈n⟼ifj=kv⁡iimj=m∈B,v∈V⟼k∈N⟼i∈N,j∈N⟼ifj=kv⁡iimj
23 df-marepv ⊢matRepV=n∈V,r∈V⟼m∈BasenMatr,v∈Basern⟼k∈n⟼i∈n,j∈n⟼ifj=kv⁡iimj
24 22 23 ovmpoga ⊢N∈V∧R∈V∧m∈B,v∈V⟼k∈N⟼i∈N,j∈N⟼ifj=kv⁡iimj∈V→NmatRepVR=m∈B,v∈V⟼k∈N⟼i∈N,j∈N⟼ifj=kv⁡iimj
25 9 24 mpd3an3 ⊢N∈V∧R∈V→NmatRepVR=m∈B,v∈V⟼k∈N⟼i∈N,j∈N⟼ifj=kv⁡iimj
26 23 mpondm0 ⊢¬N∈V∧R∈V→NmatRepVR=∅
27 1 fveq2i ⊢BaseA=BaseNMatR
28 2 27 eqtri ⊢B=BaseNMatR
29 matbas0pc ⊢¬N∈V∧R∈V→BaseNMatR=∅
30 28 29 eqtrid ⊢¬N∈V∧R∈V→B=∅
31 30 orcd ⊢¬N∈V∧R∈V→B=∅∨V=∅
32 0mpo0 ⊢B=∅∨V=∅→m∈B,v∈V⟼k∈N⟼i∈N,j∈N⟼ifj=kv⁡iimj=∅
33 31 32 syl ⊢¬N∈V∧R∈V→m∈B,v∈V⟼k∈N⟼i∈N,j∈N⟼ifj=kv⁡iimj=∅
34 26 33 eqtr4d ⊢¬N∈V∧R∈V→NmatRepVR=m∈B,v∈V⟼k∈N⟼i∈N,j∈N⟼ifj=kv⁡iimj
35 25 34 pm2.61i ⊢NmatRepVR=m∈B,v∈V⟼k∈N⟼i∈N,j∈N⟼ifj=kv⁡iimj
36 3 35 eqtri ⊢Q=m∈B,v∈V⟼k∈N⟼i∈N,j∈N⟼ifj=kv⁡iimj