Metamath Proof Explorer

Theorem minmar1val

Description: Third substitution for the definition of a matrix for a minor. (Contributed by AV, 31-Dec-2018)

Ref Expression
Hypotheses minmar1fval.a ⊢A=NMatR
minmar1fval.b ⊢B=BaseA
minmar1fval.q ⊢Q=NminMatR1R
minmar1fval.o ⊢1˙=1R
minmar1fval.z ⊢0˙=0R
Assertion minmar1val ⊢M∈B∧K∈N∧L∈N→KQ⁡ML=i∈N,j∈N⟼ifi=Kifj=L1˙0˙iMj

Proof

Step Hyp Ref Expression
1 minmar1fval.a ⊢A=NMatR
2 minmar1fval.b ⊢B=BaseA
3 minmar1fval.q ⊢Q=NminMatR1R
4 minmar1fval.o ⊢1˙=1R
5 minmar1fval.z ⊢0˙=0R
6 1 2 3 4 5 minmar1val0 ⊢M∈B→Q⁡M=k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=l1˙0˙iMj
7 6 3ad2ant1 ⊢M∈B∧K∈N∧L∈N→Q⁡M=k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=l1˙0˙iMj
8 simp2 ⊢M∈B∧K∈N∧L∈N→K∈N
9 simpl3 ⊢M∈B∧K∈N∧L∈N∧k=K→L∈N
10 1 2 matrcl ⊢M∈B→N∈Fin∧R∈V
11 10 simpld ⊢M∈B→N∈Fin
12 11 11 jca ⊢M∈B→N∈Fin∧N∈Fin
13 12 3ad2ant1 ⊢M∈B∧K∈N∧L∈N→N∈Fin∧N∈Fin
14 13 adantr ⊢M∈B∧K∈N∧L∈N∧k=K∧l=L→N∈Fin∧N∈Fin
15 mpoexga ⊢N∈Fin∧N∈Fin→i∈N,j∈N⟼ifi=kifj=l1˙0˙iMj∈V
16 14 15 syl ⊢M∈B∧K∈N∧L∈N∧k=K∧l=L→i∈N,j∈N⟼ifi=kifj=l1˙0˙iMj∈V
17 eqeq2 ⊢k=K→i=k↔i=K
18 17 adantr ⊢k=K∧l=L→i=k↔i=K
19 eqeq2 ⊢l=L→j=l↔j=L
20 19 ifbid ⊢l=L→ifj=l1˙0˙=ifj=L1˙0˙
21 20 adantl ⊢k=K∧l=L→ifj=l1˙0˙=ifj=L1˙0˙
22 18 21 ifbieq1d ⊢k=K∧l=L→ifi=kifj=l1˙0˙iMj=ifi=Kifj=L1˙0˙iMj
23 22 mpoeq3dv ⊢k=K∧l=L→i∈N,j∈N⟼ifi=kifj=l1˙0˙iMj=i∈N,j∈N⟼ifi=Kifj=L1˙0˙iMj
24 23 adantl ⊢M∈B∧K∈N∧L∈N∧k=K∧l=L→i∈N,j∈N⟼ifi=kifj=l1˙0˙iMj=i∈N,j∈N⟼ifi=Kifj=L1˙0˙iMj
25 8 9 16 24 ovmpodv2 ⊢M∈B∧K∈N∧L∈N→Q⁡M=k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=l1˙0˙iMj→KQ⁡ML=i∈N,j∈N⟼ifi=Kifj=L1˙0˙iMj
26 7 25 mpd ⊢M∈B∧K∈N∧L∈N→KQ⁡ML=i∈N,j∈N⟼ifi=Kifj=L1˙0˙iMj