Metamath Proof Explorer

Theorem marepveval

Description: An entry of a matrix with a replaced column. (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 marepveval ⊢M∈B∧C∈V∧K∈N∧I∈N∧J∈N→IMQC⁡KJ=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 marepvval ⊢M∈B∧C∈V∧K∈N→MQC⁡K=i∈N,j∈N⟼ifj=KC⁡iiMj
6 5 adantr ⊢M∈B∧C∈V∧K∈N∧I∈N∧J∈N→MQC⁡K=i∈N,j∈N⟼ifj=KC⁡iiMj
7 simprl ⊢M∈B∧C∈V∧K∈N∧I∈N∧J∈N→I∈N
8 simplrr ⊢M∈B∧C∈V∧K∈N∧I∈N∧J∈N∧i=I→J∈N
9 fvexd ⊢M∈B∧C∈V∧K∈N∧I∈N∧J∈N→C⁡i∈V
10 ovexd ⊢M∈B∧C∈V∧K∈N∧I∈N∧J∈N→iMj∈V
11 9 10 ifcld ⊢M∈B∧C∈V∧K∈N∧I∈N∧J∈N→ifj=KC⁡iiMj∈V
12 11 adantr ⊢M∈B∧C∈V∧K∈N∧I∈N∧J∈N∧i=I∧j=J→ifj=KC⁡iiMj∈V
13 eqeq1 ⊢j=J→j=K↔J=K
14 13 adantl ⊢i=I∧j=J→j=K↔J=K
15 fveq2 ⊢i=I→C⁡i=C⁡I
16 15 adantr ⊢i=I∧j=J→C⁡i=C⁡I
17 oveq12 ⊢i=I∧j=J→iMj=IMJ
18 14 16 17 ifbieq12d ⊢i=I∧j=J→ifj=KC⁡iiMj=ifJ=KC⁡IIMJ
19 18 adantl ⊢M∈B∧C∈V∧K∈N∧I∈N∧J∈N∧i=I∧j=J→ifj=KC⁡iiMj=ifJ=KC⁡IIMJ
20 7 8 12 19 ovmpodv2 ⊢M∈B∧C∈V∧K∈N∧I∈N∧J∈N→MQC⁡K=i∈N,j∈N⟼ifj=KC⁡iiMj→IMQC⁡KJ=ifJ=KC⁡IIMJ
21 6 20 mpd ⊢M∈B∧C∈V∧K∈N∧I∈N∧J∈N→IMQC⁡KJ=ifJ=KC⁡IIMJ