Metamath Proof Explorer

Theorem marepvval0

Description: Second 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 marepvval0 ⊢M∈B∧C∈V→MQC=k∈N⟼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 matrcl ⊢M∈B→N∈Fin∧R∈V
6 5 simpld ⊢M∈B→N∈Fin
7 6 adantr ⊢M∈B∧C∈V→N∈Fin
8 7 mptexd ⊢M∈B∧C∈V→k∈N⟼i∈N,j∈N⟼ifj=kC⁡iiMj∈V
9 fveq1 ⊢c=C→c⁡i=C⁡i
10 9 adantl ⊢m=M∧c=C→c⁡i=C⁡i
11 oveq ⊢m=M→imj=iMj
12 11 adantr ⊢m=M∧c=C→imj=iMj
13 10 12 ifeq12d ⊢m=M∧c=C→ifj=kc⁡iimj=ifj=kC⁡iiMj
14 13 mpoeq3dv ⊢m=M∧c=C→i∈N,j∈N⟼ifj=kc⁡iimj=i∈N,j∈N⟼ifj=kC⁡iiMj
15 14 mpteq2dv ⊢m=M∧c=C→k∈N⟼i∈N,j∈N⟼ifj=kc⁡iimj=k∈N⟼i∈N,j∈N⟼ifj=kC⁡iiMj
16 1 2 3 4 marepvfval ⊢Q=m∈B,c∈V⟼k∈N⟼i∈N,j∈N⟼ifj=kc⁡iimj
17 15 16 ovmpoga ⊢M∈B∧C∈V∧k∈N⟼i∈N,j∈N⟼ifj=kC⁡iiMj∈V→MQC=k∈N⟼i∈N,j∈N⟼ifj=kC⁡iiMj
18 8 17 mpd3an3 ⊢M∈B∧C∈V→MQC=k∈N⟼i∈N,j∈N⟼ifj=kC⁡iiMj