Metamath Proof Explorer

Theorem marrepeval

Description: An entry of a matrix with a replaced row. (Contributed by AV, 12-Feb-2019)

Ref Expression
Hypotheses marrepfval.a ⊢A=NMatR
marrepfval.b ⊢B=BaseA
marrepfval.q ⊢Q=NmatRRepR
marrepfval.z ⊢0˙=0R
Assertion marrepeval ⊢M∈B∧S∈BaseR∧K∈N∧L∈N∧I∈N∧J∈N→IKMQSLJ=ifI=KifJ=LS0˙IMJ

Proof

Step Hyp Ref Expression
1 marrepfval.a ⊢A=NMatR
2 marrepfval.b ⊢B=BaseA
3 marrepfval.q ⊢Q=NmatRRepR
4 marrepfval.z ⊢0˙=0R
5 1 2 3 4 marrepval ⊢M∈B∧S∈BaseR∧K∈N∧L∈N→KMQSL=i∈N,j∈N⟼ifi=Kifj=LS0˙iMj
6 5 3adant3 ⊢M∈B∧S∈BaseR∧K∈N∧L∈N∧I∈N∧J∈N→KMQSL=i∈N,j∈N⟼ifi=Kifj=LS0˙iMj
7 simp3l ⊢M∈B∧S∈BaseR∧K∈N∧L∈N∧I∈N∧J∈N→I∈N
8 simpl3r ⊢M∈B∧S∈BaseR∧K∈N∧L∈N∧I∈N∧J∈N∧i=I→J∈N
9 4 fvexi ⊢0˙∈V
10 ifexg ⊢S∈BaseR∧0˙∈V→ifj=LS0˙∈V
11 9 10 mpan2 ⊢S∈BaseR→ifj=LS0˙∈V
12 ovexd ⊢S∈BaseR→iMj∈V
13 11 12 ifcld ⊢S∈BaseR→ifi=Kifj=LS0˙iMj∈V
14 13 adantl ⊢M∈B∧S∈BaseR→ifi=Kifj=LS0˙iMj∈V
15 14 3ad2ant1 ⊢M∈B∧S∈BaseR∧K∈N∧L∈N∧I∈N∧J∈N→ifi=Kifj=LS0˙iMj∈V
16 15 adantr ⊢M∈B∧S∈BaseR∧K∈N∧L∈N∧I∈N∧J∈N∧i=I∧j=J→ifi=Kifj=LS0˙iMj∈V
17 eqeq1 ⊢i=I→i=K↔I=K
18 17 adantr ⊢i=I∧j=J→i=K↔I=K
19 eqeq1 ⊢j=J→j=L↔J=L
20 19 ifbid ⊢j=J→ifj=LS0˙=ifJ=LS0˙
21 20 adantl ⊢i=I∧j=J→ifj=LS0˙=ifJ=LS0˙
22 oveq12 ⊢i=I∧j=J→iMj=IMJ
23 18 21 22 ifbieq12d ⊢i=I∧j=J→ifi=Kifj=LS0˙iMj=ifI=KifJ=LS0˙IMJ
24 23 adantl ⊢M∈B∧S∈BaseR∧K∈N∧L∈N∧I∈N∧J∈N∧i=I∧j=J→ifi=Kifj=LS0˙iMj=ifI=KifJ=LS0˙IMJ
25 7 8 16 24 ovmpodv2 ⊢M∈B∧S∈BaseR∧K∈N∧L∈N∧I∈N∧J∈N→KMQSL=i∈N,j∈N⟼ifi=Kifj=LS0˙iMj→IKMQSLJ=ifI=KifJ=LS0˙IMJ
26 6 25 mpd ⊢M∈B∧S∈BaseR∧K∈N∧L∈N∧I∈N∧J∈N→IKMQSLJ=ifI=KifJ=LS0˙IMJ