Metamath Proof Explorer

Theorem maducoeval

Description: An entry of 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 maducoeval ⊢M∈B∧I∈N∧H∈N→IJ⁡MH=D⁡k∈N,l∈N⟼ifk=Hifl=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 2 3 4 5 6 maduval ⊢M∈B→J⁡M=i∈N,j∈N⟼D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kMl
8 7 3ad2ant1 ⊢M∈B∧I∈N∧H∈N→J⁡M=i∈N,j∈N⟼D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kMl
9 simp1r ⊢i=I∧j=H∧k∈N∧l∈N→j=H
10 9 eqeq2d ⊢i=I∧j=H∧k∈N∧l∈N→k=j↔k=H
11 simp1l ⊢i=I∧j=H∧k∈N∧l∈N→i=I
12 11 eqeq2d ⊢i=I∧j=H∧k∈N∧l∈N→l=i↔l=I
13 12 ifbid ⊢i=I∧j=H∧k∈N∧l∈N→ifl=i1˙0˙=ifl=I1˙0˙
14 10 13 ifbieq1d ⊢i=I∧j=H∧k∈N∧l∈N→ifk=jifl=i1˙0˙kMl=ifk=Hifl=I1˙0˙kMl
15 14 mpoeq3dva ⊢i=I∧j=H→k∈N,l∈N⟼ifk=jifl=i1˙0˙kMl=k∈N,l∈N⟼ifk=Hifl=I1˙0˙kMl
16 15 fveq2d ⊢i=I∧j=H→D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kMl=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙kMl
17 16 adantl ⊢M∈B∧I∈N∧H∈N∧i=I∧j=H→D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kMl=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙kMl
18 simp2 ⊢M∈B∧I∈N∧H∈N→I∈N
19 simp3 ⊢M∈B∧I∈N∧H∈N→H∈N
20 fvexd ⊢M∈B∧I∈N∧H∈N→D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙kMl∈V
21 8 17 18 19 20 ovmpod ⊢M∈B∧I∈N∧H∈N→IJ⁡MH=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙kMl