Metamath Proof Explorer

Theorem smadiadetr

Description: The determinant of a square matrix with one row replaced with 0's and an arbitrary element of the underlying ring at the diagonal position equals the ring element multiplied with the determinant of a submatrix of the square matrix obtained by removing the row and the column at the same index. Closed form of smadiadetg . Special case of the "Laplace expansion", see definition in Lang p. 515. (Contributed by AV, 15-Feb-2019)

Ref Expression
Assertion smadiadetr 
|- ( ( ( R e. CRing /\ M e. ( Base ` ( N Mat R ) ) ) /\ ( K e. N /\ S e. ( Base ` R ) ) ) -> ( ( N maDet R ) ` ( K ( M ( N matRRep R ) S ) K ) ) = ( S ( .r ` R ) ( ( ( N \ { K } ) maDet R ) ` ( K ( ( N subMat R ) ` M ) K ) ) ) )

Proof

Step Hyp Ref Expression
1 3anass 
 |-  ( ( M e. ( Base ` ( N Mat R ) ) /\ K e. N /\ S e. ( Base ` R ) ) <-> ( M e. ( Base ` ( N Mat R ) ) /\ ( K e. N /\ S e. ( Base ` R ) ) ) )
2 oveq2 
 |-  ( R = if ( R e. CRing , R , CCfld ) -> ( N Mat R ) = ( N Mat if ( R e. CRing , R , CCfld ) ) )
3 2 fveq2d 
 |-  ( R = if ( R e. CRing , R , CCfld ) -> ( Base ` ( N Mat R ) ) = ( Base ` ( N Mat if ( R e. CRing , R , CCfld ) ) ) )
4 3 eleq2d 
 |-  ( R = if ( R e. CRing , R , CCfld ) -> ( M e. ( Base ` ( N Mat R ) ) <-> M e. ( Base ` ( N Mat if ( R e. CRing , R , CCfld ) ) ) ) )
5 fveq2 
 |-  ( R = if ( R e. CRing , R , CCfld ) -> ( Base ` R ) = ( Base ` if ( R e. CRing , R , CCfld ) ) )
6 5 eleq2d 
 |-  ( R = if ( R e. CRing , R , CCfld ) -> ( S e. ( Base ` R ) <-> S e. ( Base ` if ( R e. CRing , R , CCfld ) ) ) )
7 4 6 3anbi13d 
 |-  ( R = if ( R e. CRing , R , CCfld ) -> ( ( M e. ( Base ` ( N Mat R ) ) /\ K e. N /\ S e. ( Base ` R ) ) <-> ( M e. ( Base ` ( N Mat if ( R e. CRing , R , CCfld ) ) ) /\ K e. N /\ S e. ( Base ` if ( R e. CRing , R , CCfld ) ) ) ) )
8 1 7 bitr3id 
 |-  ( R = if ( R e. CRing , R , CCfld ) -> ( ( M e. ( Base ` ( N Mat R ) ) /\ ( K e. N /\ S e. ( Base ` R ) ) ) <-> ( M e. ( Base ` ( N Mat if ( R e. CRing , R , CCfld ) ) ) /\ K e. N /\ S e. ( Base ` if ( R e. CRing , R , CCfld ) ) ) ) )
9 oveq2 
 |-  ( R = if ( R e. CRing , R , CCfld ) -> ( N maDet R ) = ( N maDet if ( R e. CRing , R , CCfld ) ) )
10 oveq2 
 |-  ( R = if ( R e. CRing , R , CCfld ) -> ( N matRRep R ) = ( N matRRep if ( R e. CRing , R , CCfld ) ) )
11 10 oveqd 
 |-  ( R = if ( R e. CRing , R , CCfld ) -> ( M ( N matRRep R ) S ) = ( M ( N matRRep if ( R e. CRing , R , CCfld ) ) S ) )
12 11 oveqd 
 |-  ( R = if ( R e. CRing , R , CCfld ) -> ( K ( M ( N matRRep R ) S ) K ) = ( K ( M ( N matRRep if ( R e. CRing , R , CCfld ) ) S ) K ) )
13 9 12 fveq12d 
 |-  ( R = if ( R e. CRing , R , CCfld ) -> ( ( N maDet R ) ` ( K ( M ( N matRRep R ) S ) K ) ) = ( ( N maDet if ( R e. CRing , R , CCfld ) ) ` ( K ( M ( N matRRep if ( R e. CRing , R , CCfld ) ) S ) K ) ) )
14 fveq2 
 |-  ( R = if ( R e. CRing , R , CCfld ) -> ( .r ` R ) = ( .r ` if ( R e. CRing , R , CCfld ) ) )
15 eqidd 
 |-  ( R = if ( R e. CRing , R , CCfld ) -> S = S )
16 oveq2 
 |-  ( R = if ( R e. CRing , R , CCfld ) -> ( ( N \ { K } ) maDet R ) = ( ( N \ { K } ) maDet if ( R e. CRing , R , CCfld ) ) )
17 oveq2 
 |-  ( R = if ( R e. CRing , R , CCfld ) -> ( N subMat R ) = ( N subMat if ( R e. CRing , R , CCfld ) ) )
18 17 fveq1d 
 |-  ( R = if ( R e. CRing , R , CCfld ) -> ( ( N subMat R ) ` M ) = ( ( N subMat if ( R e. CRing , R , CCfld ) ) ` M ) )
19 18 oveqd 
 |-  ( R = if ( R e. CRing , R , CCfld ) -> ( K ( ( N subMat R ) ` M ) K ) = ( K ( ( N subMat if ( R e. CRing , R , CCfld ) ) ` M ) K ) )
20 16 19 fveq12d 
 |-  ( R = if ( R e. CRing , R , CCfld ) -> ( ( ( N \ { K } ) maDet R ) ` ( K ( ( N subMat R ) ` M ) K ) ) = ( ( ( N \ { K } ) maDet if ( R e. CRing , R , CCfld ) ) ` ( K ( ( N subMat if ( R e. CRing , R , CCfld ) ) ` M ) K ) ) )
21 14 15 20 oveq123d 
 |-  ( R = if ( R e. CRing , R , CCfld ) -> ( S ( .r ` R ) ( ( ( N \ { K } ) maDet R ) ` ( K ( ( N subMat R ) ` M ) K ) ) ) = ( S ( .r ` if ( R e. CRing , R , CCfld ) ) ( ( ( N \ { K } ) maDet if ( R e. CRing , R , CCfld ) ) ` ( K ( ( N subMat if ( R e. CRing , R , CCfld ) ) ` M ) K ) ) ) )
22 13 21 eqeq12d 
 |-  ( R = if ( R e. CRing , R , CCfld ) -> ( ( ( N maDet R ) ` ( K ( M ( N matRRep R ) S ) K ) ) = ( S ( .r ` R ) ( ( ( N \ { K } ) maDet R ) ` ( K ( ( N subMat R ) ` M ) K ) ) ) <-> ( ( N maDet if ( R e. CRing , R , CCfld ) ) ` ( K ( M ( N matRRep if ( R e. CRing , R , CCfld ) ) S ) K ) ) = ( S ( .r ` if ( R e. CRing , R , CCfld ) ) ( ( ( N \ { K } ) maDet if ( R e. CRing , R , CCfld ) ) ` ( K ( ( N subMat if ( R e. CRing , R , CCfld ) ) ` M ) K ) ) ) ) )
23 8 22 imbi12d 
 |-  ( R = if ( R e. CRing , R , CCfld ) -> ( ( ( M e. ( Base ` ( N Mat R ) ) /\ ( K e. N /\ S e. ( Base ` R ) ) ) -> ( ( N maDet R ) ` ( K ( M ( N matRRep R ) S ) K ) ) = ( S ( .r ` R ) ( ( ( N \ { K } ) maDet R ) ` ( K ( ( N subMat R ) ` M ) K ) ) ) ) <-> ( ( M e. ( Base ` ( N Mat if ( R e. CRing , R , CCfld ) ) ) /\ K e. N /\ S e. ( Base ` if ( R e. CRing , R , CCfld ) ) ) -> ( ( N maDet if ( R e. CRing , R , CCfld ) ) ` ( K ( M ( N matRRep if ( R e. CRing , R , CCfld ) ) S ) K ) ) = ( S ( .r ` if ( R e. CRing , R , CCfld ) ) ( ( ( N \ { K } ) maDet if ( R e. CRing , R , CCfld ) ) ` ( K ( ( N subMat if ( R e. CRing , R , CCfld ) ) ` M ) K ) ) ) ) ) )
24 cncrng 
 |-  CCfld e. CRing
25 24 elimel 
 |-  if ( R e. CRing , R , CCfld ) e. CRing
26 25 smadiadetg0 
 |-  ( ( M e. ( Base ` ( N Mat if ( R e. CRing , R , CCfld ) ) ) /\ K e. N /\ S e. ( Base ` if ( R e. CRing , R , CCfld ) ) ) -> ( ( N maDet if ( R e. CRing , R , CCfld ) ) ` ( K ( M ( N matRRep if ( R e. CRing , R , CCfld ) ) S ) K ) ) = ( S ( .r ` if ( R e. CRing , R , CCfld ) ) ( ( ( N \ { K } ) maDet if ( R e. CRing , R , CCfld ) ) ` ( K ( ( N subMat if ( R e. CRing , R , CCfld ) ) ` M ) K ) ) ) )
27 23 26 dedth 
 |-  ( R e. CRing -> ( ( M e. ( Base ` ( N Mat R ) ) /\ ( K e. N /\ S e. ( Base ` R ) ) ) -> ( ( N maDet R ) ` ( K ( M ( N matRRep R ) S ) K ) ) = ( S ( .r ` R ) ( ( ( N \ { K } ) maDet R ) ` ( K ( ( N subMat R ) ` M ) K ) ) ) ) )
28 27 impl 
 |-  ( ( ( R e. CRing /\ M e. ( Base ` ( N Mat R ) ) ) /\ ( K e. N /\ S e. ( Base ` R ) ) ) -> ( ( N maDet R ) ` ( K ( M ( N matRRep R ) S ) K ) ) = ( S ( .r ` R ) ( ( ( N \ { K } ) maDet R ) ` ( K ( ( N subMat R ) ` M ) K ) ) ) )