Metamath Proof Explorer


Theorem minmar1eval

Description: An entry 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 minmar1eval MBKNLNINJNIKQMLJ=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 minmar1val MBKNLNKQML=iN,jNifi=Kifj=L1˙0˙iMj
7 6 3expb MBKNLNKQML=iN,jNifi=Kifj=L1˙0˙iMj
8 7 3adant3 MBKNLNINJNKQML=iN,jNifi=Kifj=L1˙0˙iMj
9 simp3l MBKNLNINJNIN
10 simpl3r MBKNLNINJNi=IJN
11 4 fvexi 1˙V
12 5 fvexi 0˙V
13 11 12 ifex ifj=L1˙0˙V
14 ovex iMjV
15 13 14 ifex ifi=Kifj=L1˙0˙iMjV
16 15 a1i MBKNLNINJNi=Ij=Jifi=Kifj=L1˙0˙iMjV
17 eqeq1 i=Ii=KI=K
18 17 adantr i=Ij=Ji=KI=K
19 eqeq1 j=Jj=LJ=L
20 19 adantl i=Ij=Jj=LJ=L
21 20 ifbid i=Ij=Jifj=L1˙0˙=ifJ=L1˙0˙
22 oveq12 i=Ij=JiMj=IMJ
23 18 21 22 ifbieq12d i=Ij=Jifi=Kifj=L1˙0˙iMj=ifI=KifJ=L1˙0˙IMJ
24 23 adantl MBKNLNINJNi=Ij=Jifi=Kifj=L1˙0˙iMj=ifI=KifJ=L1˙0˙IMJ
25 9 10 16 24 ovmpodv2 MBKNLNINJNKQML=iN,jNifi=Kifj=L1˙0˙iMjIKQMLJ=ifI=KifJ=L1˙0˙IMJ
26 8 25 mpd MBKNLNINJNIKQMLJ=ifI=KifJ=L1˙0˙IMJ