Metamath Proof Explorer

Theorem madufval

Description: First 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 madufval ⊢J=m∈B⟼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 fvoveq1 ⊢n=N→BasenMatr=BaseNMatr
8 id ⊢n=N→n=N
9 oveq1 ⊢n=N→nmaDetr=NmaDetr
10 eqidd ⊢n=N→ifk=jifl=i1r0rkml=ifk=jifl=i1r0rkml
11 8 8 10 mpoeq123dv ⊢n=N→k∈n,l∈n⟼ifk=jifl=i1r0rkml=k∈N,l∈N⟼ifk=jifl=i1r0rkml
12 9 11 fveq12d ⊢n=N→nmaDetr⁡k∈n,l∈n⟼ifk=jifl=i1r0rkml=NmaDetr⁡k∈N,l∈N⟼ifk=jifl=i1r0rkml
13 8 8 12 mpoeq123dv ⊢n=N→i∈n,j∈n⟼nmaDetr⁡k∈n,l∈n⟼ifk=jifl=i1r0rkml=i∈N,j∈N⟼NmaDetr⁡k∈N,l∈N⟼ifk=jifl=i1r0rkml
14 7 13 mpteq12dv ⊢n=N→m∈BasenMatr⟼i∈n,j∈n⟼nmaDetr⁡k∈n,l∈n⟼ifk=jifl=i1r0rkml=m∈BaseNMatr⟼i∈N,j∈N⟼NmaDetr⁡k∈N,l∈N⟼ifk=jifl=i1r0rkml
15 oveq2 ⊢r=R→NMatr=NMatR
16 15 fveq2d ⊢r=R→BaseNMatr=BaseNMatR
17 oveq2 ⊢r=R→NmaDetr=NmaDetR
18 fveq2 ⊢r=R→1r=1R
19 fveq2 ⊢r=R→0r=0R
20 18 19 ifeq12d ⊢r=R→ifl=i1r0r=ifl=i1R0R
21 20 ifeq1d ⊢r=R→ifk=jifl=i1r0rkml=ifk=jifl=i1R0Rkml
22 21 mpoeq3dv ⊢r=R→k∈N,l∈N⟼ifk=jifl=i1r0rkml=k∈N,l∈N⟼ifk=jifl=i1R0Rkml
23 17 22 fveq12d ⊢r=R→NmaDetr⁡k∈N,l∈N⟼ifk=jifl=i1r0rkml=NmaDetR⁡k∈N,l∈N⟼ifk=jifl=i1R0Rkml
24 23 mpoeq3dv ⊢r=R→i∈N,j∈N⟼NmaDetr⁡k∈N,l∈N⟼ifk=jifl=i1r0rkml=i∈N,j∈N⟼NmaDetR⁡k∈N,l∈N⟼ifk=jifl=i1R0Rkml
25 16 24 mpteq12dv ⊢r=R→m∈BaseNMatr⟼i∈N,j∈N⟼NmaDetr⁡k∈N,l∈N⟼ifk=jifl=i1r0rkml=m∈BaseNMatR⟼i∈N,j∈N⟼NmaDetR⁡k∈N,l∈N⟼ifk=jifl=i1R0Rkml
26 df-madu ⊢maAdju=n∈V,r∈V⟼m∈BasenMatr⟼i∈n,j∈n⟼nmaDetr⁡k∈n,l∈n⟼ifk=jifl=i1r0rkml
27 fvex ⊢BaseNMatR∈V
28 27 mptex ⊢m∈BaseNMatR⟼i∈N,j∈N⟼NmaDetR⁡k∈N,l∈N⟼ifk=jifl=i1R0Rkml∈V
29 14 25 26 28 ovmpo ⊢N∈V∧R∈V→NmaAdjuR=m∈BaseNMatR⟼i∈N,j∈N⟼NmaDetR⁡k∈N,l∈N⟼ifk=jifl=i1R0Rkml
30 1 fveq2i ⊢BaseA=BaseNMatR
31 4 30 eqtri ⊢B=BaseNMatR
32 5 a1i ⊢k∈N∧l∈N→1˙=1R
33 6 a1i ⊢k∈N∧l∈N→0˙=0R
34 32 33 ifeq12d ⊢k∈N∧l∈N→ifl=i1˙0˙=ifl=i1R0R
35 34 ifeq1d ⊢k∈N∧l∈N→ifk=jifl=i1˙0˙kml=ifk=jifl=i1R0Rkml
36 35 mpoeq3ia ⊢k∈N,l∈N⟼ifk=jifl=i1˙0˙kml=k∈N,l∈N⟼ifk=jifl=i1R0Rkml
37 2 36 fveq12i ⊢D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kml=NmaDetR⁡k∈N,l∈N⟼ifk=jifl=i1R0Rkml
38 37 a1i ⊢i∈N∧j∈N→D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kml=NmaDetR⁡k∈N,l∈N⟼ifk=jifl=i1R0Rkml
39 38 mpoeq3ia ⊢i∈N,j∈N⟼D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kml=i∈N,j∈N⟼NmaDetR⁡k∈N,l∈N⟼ifk=jifl=i1R0Rkml
40 31 39 mpteq12i ⊢m∈B⟼i∈N,j∈N⟼D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kml=m∈BaseNMatR⟼i∈N,j∈N⟼NmaDetR⁡k∈N,l∈N⟼ifk=jifl=i1R0Rkml
41 29 40 eqtr4di ⊢N∈V∧R∈V→NmaAdjuR=m∈B⟼i∈N,j∈N⟼D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kml
42 26 reldmmpo ⊢Rel⁡dom⁡maAdju
43 42 ovprc ⊢¬N∈V∧R∈V→NmaAdjuR=∅
44 df-mat ⊢Mat=n∈Fin,r∈V⟼rfreeLModn×nsSet⋅ndxrmaMulnnn
45 44 reldmmpo ⊢Rel⁡dom⁡Mat
46 45 ovprc ⊢¬N∈V∧R∈V→NMatR=∅
47 1 46 eqtrid ⊢¬N∈V∧R∈V→A=∅
48 47 fveq2d ⊢¬N∈V∧R∈V→BaseA=Base∅
49 base0 ⊢∅=Base∅
50 48 4 49 3eqtr4g ⊢¬N∈V∧R∈V→B=∅
51 50 mpteq1d ⊢¬N∈V∧R∈V→m∈B⟼i∈N,j∈N⟼D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kml=m∈∅⟼i∈N,j∈N⟼D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kml
52 mpt0 ⊢m∈∅⟼i∈N,j∈N⟼D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kml=∅
53 51 52 eqtrdi ⊢¬N∈V∧R∈V→m∈B⟼i∈N,j∈N⟼D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kml=∅
54 43 53 eqtr4d ⊢¬N∈V∧R∈V→NmaAdjuR=m∈B⟼i∈N,j∈N⟼D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kml
55 41 54 pm2.61i ⊢NmaAdjuR=m∈B⟼i∈N,j∈N⟼D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kml
56 3 55 eqtri ⊢J=m∈B⟼i∈N,j∈N⟼D⁡k∈N,l∈N⟼ifk=jifl=i1˙0˙kml