Theorem smadiadetg

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. (Contributed by AV, 14-Feb-2019)

	Ref	Expression
Hypotheses	smadiadet.a	|- A = ( N Mat R )
	smadiadet.b	|- B = ( Base ` A )
	smadiadet.r	|- R e. CRing
	smadiadet.d	|- D = ( N maDet R )
	smadiadet.h	|- E = ( ( N \ { K } ) maDet R )
	smadiadetg.x	|- .x. = ( .r ` R )
Assertion	smadiadetg	|- ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( D ` ( K ( M ( N matRRep R ) S ) K ) ) = ( S .x. ( E ` ( K ( ( N subMat R ) ` M ) K ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		smadiadet.a	|- A = ( N Mat R )
2		smadiadet.b	|- B = ( Base ` A )
3		smadiadet.r	|- R e. CRing
4		smadiadet.d	|- D = ( N maDet R )
5		smadiadet.h	|- E = ( ( N \ { K } ) maDet R )
6		smadiadetg.x	|- .x. = ( .r ` R )
7		eqid	|- ( Base ` R ) = ( Base ` R )
8	3	a1i	|- ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> R e. CRing )
9		crngring	|- ( R e. CRing -> R e. Ring )
10	3 9	mp1i	|- ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> R e. Ring )
11		simp1	|- ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> M e. B )
12		simp3	|- ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> S e. ( Base ` R ) )
13		simp2	|- ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> K e. N )
14	1 2	marrepcl	|- ( ( ( R e. Ring /\ M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ K e. N ) ) -> ( K ( M ( N matRRep R ) S ) K ) e. B )
15	10 11 12 13 13 14	syl32anc	|- ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( K ( M ( N matRRep R ) S ) K ) e. B )
16	1 2	minmar1cl	|- ( ( ( R e. Ring /\ M e. B ) /\ ( K e. N /\ K e. N ) ) -> ( K ( ( N minMatR1 R ) ` M ) K ) e. B )
17	10 11 13 13 16	syl22anc	|- ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( K ( ( N minMatR1 R ) ` M ) K ) e. B )
18	1 2 3 4 5 6	smadiadetglem2	|- ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( K ( M ( N matRRep R ) S ) K ) |` ( { K } X. N ) ) = ( ( ( { K } X. N ) X. { S } ) oF .x. ( ( K ( ( N minMatR1 R ) ` M ) K ) |` ( { K } X. N ) ) ) )
19	1 2 3 4 5	smadiadetglem1	|- ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( K ( M ( N matRRep R ) S ) K ) |` ( ( N \ { K } ) X. N ) ) = ( ( K ( ( N minMatR1 R ) ` M ) K ) |` ( ( N \ { K } ) X. N ) ) )
20	4 1 2 7 6 8 15 12 17 13 18 19	mdetrsca	|- ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( D ` ( K ( M ( N matRRep R ) S ) K ) ) = ( S .x. ( D ` ( K ( ( N minMatR1 R ) ` M ) K ) ) ) )
21	1 2 3 4 5	smadiadet	|- ( ( M e. B /\ K e. N ) -> ( E ` ( K ( ( N subMat R ) ` M ) K ) ) = ( D ` ( K ( ( N minMatR1 R ) ` M ) K ) ) )
22	21	3adant3	|- ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( E ` ( K ( ( N subMat R ) ` M ) K ) ) = ( D ` ( K ( ( N minMatR1 R ) ` M ) K ) ) )
23	22	eqcomd	|- ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( D ` ( K ( ( N minMatR1 R ) ` M ) K ) ) = ( E ` ( K ( ( N subMat R ) ` M ) K ) ) )
24	23	oveq2d	|- ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( S .x. ( D ` ( K ( ( N minMatR1 R ) ` M ) K ) ) ) = ( S .x. ( E ` ( K ( ( N subMat R ) ` M ) K ) ) ) )
25	20 24	eqtrd	|- ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( D ` ( K ( M ( N matRRep R ) S ) K ) ) = ( S .x. ( E ` ( K ( ( N subMat R ) ` M ) K ) ) ) )