Metamath Proof Explorer

Theorem marrepval

Description: Third substitution for the definition of the matrix row replacement function. (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 marrepval ⊢M∈B∧S∈BaseR∧K∈N∧L∈N→KMQSL=i∈N,j∈N⟼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 marrepval0 ⊢M∈B∧S∈BaseR→MQS=k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=lS0˙iMj
6 5 adantr ⊢M∈B∧S∈BaseR∧K∈N∧L∈N→MQS=k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=lS0˙iMj
7 simprl ⊢M∈B∧S∈BaseR∧K∈N∧L∈N→K∈N
8 simplrr ⊢M∈B∧S∈BaseR∧K∈N∧L∈N∧k=K→L∈N
9 1 2 matrcl ⊢M∈B→N∈Fin∧R∈V
10 9 simpld ⊢M∈B→N∈Fin
11 10 10 jca ⊢M∈B→N∈Fin∧N∈Fin
12 11 ad3antrrr ⊢M∈B∧S∈BaseR∧K∈N∧L∈N∧k=K∧l=L→N∈Fin∧N∈Fin
13 mpoexga ⊢N∈Fin∧N∈Fin→i∈N,j∈N⟼ifi=kifj=lS0˙iMj∈V
14 12 13 syl ⊢M∈B∧S∈BaseR∧K∈N∧L∈N∧k=K∧l=L→i∈N,j∈N⟼ifi=kifj=lS0˙iMj∈V
15 eqeq2 ⊢k=K→i=k↔i=K
16 15 adantr ⊢k=K∧l=L→i=k↔i=K
17 eqeq2 ⊢l=L→j=l↔j=L
18 17 ifbid ⊢l=L→ifj=lS0˙=ifj=LS0˙
19 18 adantl ⊢k=K∧l=L→ifj=lS0˙=ifj=LS0˙
20 16 19 ifbieq1d ⊢k=K∧l=L→ifi=kifj=lS0˙iMj=ifi=Kifj=LS0˙iMj
21 20 mpoeq3dv ⊢k=K∧l=L→i∈N,j∈N⟼ifi=kifj=lS0˙iMj=i∈N,j∈N⟼ifi=Kifj=LS0˙iMj
22 21 adantl ⊢M∈B∧S∈BaseR∧K∈N∧L∈N∧k=K∧l=L→i∈N,j∈N⟼ifi=kifj=lS0˙iMj=i∈N,j∈N⟼ifi=Kifj=LS0˙iMj
23 7 8 14 22 ovmpodv2 ⊢M∈B∧S∈BaseR∧K∈N∧L∈N→MQS=k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=lS0˙iMj→KMQSL=i∈N,j∈N⟼ifi=Kifj=LS0˙iMj
24 6 23 mpd ⊢M∈B∧S∈BaseR∧K∈N∧L∈N→KMQSL=i∈N,j∈N⟼ifi=Kifj=LS0˙iMj