mdetlap1

Description: A Laplace expansion of the determinant of a matrix, using the adjunct (cofactor) matrix. (Contributed by Thierry Arnoux, 16-Aug-2020)

	Ref	Expression
Hypotheses	mdetlap1.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mdetlap1.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	mdetlap1.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
	mdetlap1.k	⊢ 𝐾 = ( 𝑁 maAdju 𝑅 )
	mdetlap1.t	⊢ · = ( ._r ‘ 𝑅 )
Assertion	mdetlap1	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁 ) → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σ_g ( 𝑗 ∈ 𝑁 ↦ ( ( 𝐼 𝑀 𝑗 ) · ( 𝑗 ( 𝐾 ‘ 𝑀 ) 𝐼 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mdetlap1.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		mdetlap1.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		mdetlap1.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
4		mdetlap1.k	⊢ 𝐾 = ( 𝑁 maAdju 𝑅 )
5		mdetlap1.t	⊢ · = ( ._r ‘ 𝑅 )
6		simp2	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁 ) → 𝑀 ∈ 𝐵 )
7	1 2	matmpo	⊢ ( 𝑀 ∈ 𝐵 → 𝑀 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑖 𝑀 𝑗 ) ) )
8		eqid	⊢ 𝑁 = 𝑁
9		simpr	⊢ ( ( ⊤ ∧ 𝑖 = 𝐼 ) → 𝑖 = 𝐼 )
10	9	eqcomd	⊢ ( ( ⊤ ∧ 𝑖 = 𝐼 ) → 𝐼 = 𝑖 )
11	10	oveq1d	⊢ ( ( ⊤ ∧ 𝑖 = 𝐼 ) → ( 𝐼 𝑀 𝑗 ) = ( 𝑖 𝑀 𝑗 ) )
12		eqidd	⊢ ( ( ⊤ ∧ ¬ 𝑖 = 𝐼 ) → ( 𝑖 𝑀 𝑗 ) = ( 𝑖 𝑀 𝑗 ) )
13	11 12	ifeqda	⊢ ( ⊤ → if ( 𝑖 = 𝐼 , ( 𝐼 𝑀 𝑗 ) , ( 𝑖 𝑀 𝑗 ) ) = ( 𝑖 𝑀 𝑗 ) )
14	13	mptru	⊢ if ( 𝑖 = 𝐼 , ( 𝐼 𝑀 𝑗 ) , ( 𝑖 𝑀 𝑗 ) ) = ( 𝑖 𝑀 𝑗 )
15	8 8 14	mpoeq123i	⊢ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝐼 𝑀 𝑗 ) , ( 𝑖 𝑀 𝑗 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑖 𝑀 𝑗 ) )
16	7 15	eqtr4di	⊢ ( 𝑀 ∈ 𝐵 → 𝑀 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝐼 𝑀 𝑗 ) , ( 𝑖 𝑀 𝑗 ) ) ) )
17	16	fveq2d	⊢ ( 𝑀 ∈ 𝐵 → ( 𝐷 ‘ 𝑀 ) = ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝐼 𝑀 𝑗 ) , ( 𝑖 𝑀 𝑗 ) ) ) ) )
18	6 17	syl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁 ) → ( 𝐷 ‘ 𝑀 ) = ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝐼 𝑀 𝑗 ) , ( 𝑖 𝑀 𝑗 ) ) ) ) )
19		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
20		simp1	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁 ) → 𝑅 ∈ CRing )
21		simpl3	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝐼 ∈ 𝑁 )
22		simpr	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
23	6 2	eleqtrdi	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁 ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
24	23	adantr	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
25	1 19	matecl	⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 𝐼 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
26	21 22 24 25	syl3anc	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝐼 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
27		simp3	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁 ) → 𝐼 ∈ 𝑁 )
28	1 4 2 3 5 19 6 20 26 27	madugsum	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁 ) → ( 𝑅 Σ_g ( 𝑗 ∈ 𝑁 ↦ ( ( 𝐼 𝑀 𝑗 ) · ( 𝑗 ( 𝐾 ‘ 𝑀 ) 𝐼 ) ) ) ) = ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝐼 𝑀 𝑗 ) , ( 𝑖 𝑀 𝑗 ) ) ) ) )
29	18 28	eqtr4d	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁 ) → ( 𝐷 ‘ 𝑀 ) = ( 𝑅 Σ_g ( 𝑗 ∈ 𝑁 ↦ ( ( 𝐼 𝑀 𝑗 ) · ( 𝑗 ( 𝐾 ‘ 𝑀 ) 𝐼 ) ) ) ) )

Metamath Proof Explorer

Theorem mdetlap1

Proof