Metamath Proof Explorer

Theorem 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 ( 𝑗 ∈ 𝑁 ↦ ( ( 𝐼 𝑀 𝑗 ) · ( 𝑗 ( 𝐾 ‘ 𝑀 ) 𝐼 ) ) ) ) )