Metamath Proof Explorer

Theorem marepvval

Description: Third 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)

Ref Expression
Hypotheses marepvfval.a ⊢A=NMatR
marepvfval.b ⊢B=BaseA
marepvfval.q ⊢Q=NmatRepVR
marepvfval.v ⊢V=BaseRN
Assertion marepvval ⊢M∈B∧C∈V∧K∈N→MQC⁡K=i∈N,j∈N⟼ifj=KC⁡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 1 2 3 4 marepvval0 ⊢M∈B∧C∈V→MQC=k∈N⟼i∈N,j∈N⟼ifj=kC⁡iiMj
6 5 3adant3 ⊢M∈B∧C∈V∧K∈N→MQC=k∈N⟼i∈N,j∈N⟼ifj=kC⁡iiMj
7 6 fveq1d ⊢M∈B∧C∈V∧K∈N→MQC⁡K=k∈N⟼i∈N,j∈N⟼ifj=kC⁡iiMj⁡K
8 eqid ⊢k∈N⟼i∈N,j∈N⟼ifj=kC⁡iiMj=k∈N⟼i∈N,j∈N⟼ifj=kC⁡iiMj
9 eqeq2 ⊢k=K→j=k↔j=K
10 9 ifbid ⊢k=K→ifj=kC⁡iiMj=ifj=KC⁡iiMj
11 10 mpoeq3dv ⊢k=K→i∈N,j∈N⟼ifj=kC⁡iiMj=i∈N,j∈N⟼ifj=KC⁡iiMj
12 simp3 ⊢M∈B∧C∈V∧K∈N→K∈N
13 1 2 matrcl ⊢M∈B→N∈Fin∧R∈V
14 13 simpld ⊢M∈B→N∈Fin
15 14 14 jca ⊢M∈B→N∈Fin∧N∈Fin
16 15 3ad2ant1 ⊢M∈B∧C∈V∧K∈N→N∈Fin∧N∈Fin
17 mpoexga ⊢N∈Fin∧N∈Fin→i∈N,j∈N⟼ifj=KC⁡iiMj∈V
18 16 17 syl ⊢M∈B∧C∈V∧K∈N→i∈N,j∈N⟼ifj=KC⁡iiMj∈V
19 8 11 12 18 fvmptd3 ⊢M∈B∧C∈V∧K∈N→k∈N⟼i∈N,j∈N⟼ifj=kC⁡iiMj⁡K=i∈N,j∈N⟼ifj=KC⁡iiMj
20 7 19 eqtrd ⊢M∈B∧C∈V∧K∈N→MQC⁡K=i∈N,j∈N⟼ifj=KC⁡iiMj