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	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	smadiadet.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	smadiadet.r	⊢ 𝑅 ∈ CRing
	smadiadet.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
	smadiadet.h	⊢ 𝐸 = ( ( 𝑁 ∖ { 𝐾 } ) maDet 𝑅 )
	smadiadetg.x	⊢ · = ( .r ‘ 𝑅 )
Assertion	smadiadetg	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐷 ‘ ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) ) = ( 𝑆 · ( 𝐸 ‘ ( 𝐾 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		smadiadet.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		smadiadet.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		smadiadet.r	⊢ 𝑅 ∈ CRing
4		smadiadet.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
5		smadiadet.h	⊢ 𝐸 = ( ( 𝑁 ∖ { 𝐾 } ) maDet 𝑅 )
6		smadiadetg.x	⊢ · = ( .r ‘ 𝑅 )
7		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8	3	a1i	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → 𝑅 ∈ CRing )
9		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
10	3 9	mp1i	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
11		simp1	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → 𝑀 ∈ 𝐵 )
12		simp3	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → 𝑆 ∈ ( Base ‘ 𝑅 ) )
13		simp2	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → 𝐾 ∈ 𝑁 )
14	1 2	marrepcl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ) ) → ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) ∈ 𝐵 )
15	10 11 12 13 13 14	syl32anc	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) ∈ 𝐵 )
16	1 2	minmar1cl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ) ) → ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) ∈ 𝐵 )
17	10 11 13 13 16	syl22anc	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) ∈ 𝐵 )
18	1 2 3 4 5 6	smadiadetglem2	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) ↾ ( { 𝐾 } × 𝑁 ) ) = ( ( ( { 𝐾 } × 𝑁 ) × { 𝑆 } ) ∘f · ( ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) ↾ ( { 𝐾 } × 𝑁 ) ) ) )
19	1 2 3 4 5	smadiadetglem1	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) ↾ ( ( 𝑁 ∖ { 𝐾 } ) × 𝑁 ) ) = ( ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) ↾ ( ( 𝑁 ∖ { 𝐾 } ) × 𝑁 ) ) )
20	4 1 2 7 6 8 15 12 17 13 18 19	mdetrsca	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐷 ‘ ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) ) = ( 𝑆 · ( 𝐷 ‘ ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) ) )
21	1 2 3 4 5	smadiadet	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝐸 ‘ ( 𝐾 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) = ( 𝐷 ‘ ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) )
22	21	3adant3	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐸 ‘ ( 𝐾 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) = ( 𝐷 ‘ ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) )
23	22	eqcomd	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐷 ‘ ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) = ( 𝐸 ‘ ( 𝐾 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) )
24	23	oveq2d	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑆 · ( 𝐷 ‘ ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) ) = ( 𝑆 · ( 𝐸 ‘ ( 𝐾 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) ) )
25	20 24	eqtrd	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐷 ‘ ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) ) = ( 𝑆 · ( 𝐸 ‘ ( 𝐾 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) ) )