Metamath Proof Explorer

Theorem maduval

Description: Second substitution for the adjunct (cofactor) matrix. (Contributed by SO, 11-Jul-2018)

Ref Expression
Hypotheses madufval.a ⊢A=NMatR
madufval.d ⊢D=NmaDetR
madufval.j ⊢J=NmaAdjuR
madufval.b ⊢B=BaseA
madufval.o ⊢1˙=1R
madufval.z ⊢0˙=0R
Assertion maduval ⊢M∈B→J⁡M=i∈N,j∈N⟼D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kMl

Proof

Step Hyp Ref Expression
1 madufval.a ⊢A=NMatR
2 madufval.d ⊢D=NmaDetR
3 madufval.j ⊢J=NmaAdjuR
4 madufval.b ⊢B=BaseA
5 madufval.o ⊢1˙=1R
6 madufval.z ⊢0˙=0R
7 1 4 matrcl ⊢M∈B→N∈Fin∧R∈V
8 7 simpld ⊢M∈B→N∈Fin
9 mpoexga ⊢N∈Fin∧N∈Fin→i∈N,j∈N⟼D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kMl∈V
10 8 8 9 syl2anc ⊢M∈B→i∈N,j∈N⟼D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kMl∈V
11 oveq ⊢m=M→kml=kMl
12 11 ifeq2d ⊢m=M→ifk=jifl=i1˙0˙kml=ifk=jifl=i1˙0˙kMl
13 12 mpoeq3dv ⊢m=M→k∈N,l∈N⟼ifk=jifl=i1˙0˙kml=k∈N,l∈N⟼ifk=jifl=i1˙0˙kMl
14 13 3ad2ant1 ⊢m=M∧i∈N∧j∈N→k∈N,l∈N⟼ifk=jifl=i1˙0˙kml=k∈N,l∈N⟼ifk=jifl=i1˙0˙kMl
15 14 fveq2d ⊢m=M∧i∈N∧j∈N→D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kml=D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kMl
16 15 mpoeq3dva ⊢m=M→i∈N,j∈N⟼D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kml=i∈N,j∈N⟼D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kMl
17 1 2 3 4 5 6 madufval ⊢J=m∈B⟼i∈N,j∈N⟼D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kml
18 16 17 fvmptg ⊢M∈B∧i∈N,j∈N⟼D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kMl∈V→J⁡M=i∈N,j∈N⟼D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kMl
19 10 18 mpdan ⊢M∈B→J⁡M=i∈N,j∈N⟼D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kMl