Metamath Proof Explorer


Theorem minmar1fval

Description: First 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 minmar1fval Q=mBkN,lNiN,jNifi=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 oveq12 n=Nr=RnMatr=NMatR
7 6 1 eqtr4di n=Nr=RnMatr=A
8 7 fveq2d n=Nr=RBasenMatr=BaseA
9 8 2 eqtr4di n=Nr=RBasenMatr=B
10 simpl n=Nr=Rn=N
11 fveq2 r=R1r=1R
12 11 4 eqtr4di r=R1r=1˙
13 fveq2 r=R0r=0R
14 13 5 eqtr4di r=R0r=0˙
15 12 14 ifeq12d r=Rifj=l1r0r=ifj=l1˙0˙
16 15 ifeq1d r=Rifi=kifj=l1r0rimj=ifi=kifj=l1˙0˙imj
17 16 adantl n=Nr=Rifi=kifj=l1r0rimj=ifi=kifj=l1˙0˙imj
18 10 10 17 mpoeq123dv n=Nr=Rin,jnifi=kifj=l1r0rimj=iN,jNifi=kifj=l1˙0˙imj
19 10 10 18 mpoeq123dv n=Nr=Rkn,lnin,jnifi=kifj=l1r0rimj=kN,lNiN,jNifi=kifj=l1˙0˙imj
20 9 19 mpteq12dv n=Nr=RmBasenMatrkn,lnin,jnifi=kifj=l1r0rimj=mBkN,lNiN,jNifi=kifj=l1˙0˙imj
21 df-minmar1 minMatR1=nV,rVmBasenMatrkn,lnin,jnifi=kifj=l1r0rimj
22 2 fvexi BV
23 22 mptex mBkN,lNiN,jNifi=kifj=l1˙0˙imjV
24 20 21 23 ovmpoa NVRVNminMatR1R=mBkN,lNiN,jNifi=kifj=l1˙0˙imj
25 21 mpondm0 ¬NVRVNminMatR1R=
26 mpt0 mkN,lNiN,jNifi=kifj=l1˙0˙imj=
27 25 26 eqtr4di ¬NVRVNminMatR1R=mkN,lNiN,jNifi=kifj=l1˙0˙imj
28 1 fveq2i BaseA=BaseNMatR
29 2 28 eqtri B=BaseNMatR
30 matbas0pc ¬NVRVBaseNMatR=
31 29 30 eqtrid ¬NVRVB=
32 31 mpteq1d ¬NVRVmBkN,lNiN,jNifi=kifj=l1˙0˙imj=mkN,lNiN,jNifi=kifj=l1˙0˙imj
33 27 32 eqtr4d ¬NVRVNminMatR1R=mBkN,lNiN,jNifi=kifj=l1˙0˙imj
34 24 33 pm2.61i NminMatR1R=mBkN,lNiN,jNifi=kifj=l1˙0˙imj
35 3 34 eqtri Q=mBkN,lNiN,jNifi=kifj=l1˙0˙imj