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 ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) ) = ( 𝑆 ( .r ‘ 𝑅 ) ( ( ( 𝑁 ∖ { 𝐾 } ) maDet 𝑅 ) ‘ ( 𝐾 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) ) )

Proof

Step Hyp Ref Expression
1 3anass ⊢ ( ( 𝑀 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ↔ ( 𝑀 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ) )
2 oveq2 ⊢ ( 𝑅 = if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) → ( 𝑁 Mat 𝑅 ) = ( 𝑁 Mat if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) )
3 2 fveq2d ⊢ ( 𝑅 = if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) → ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ( Base ‘ ( 𝑁 Mat if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ) )
4 3 eleq2d ⊢ ( 𝑅 = if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) → ( 𝑀 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ↔ 𝑀 ∈ ( Base ‘ ( 𝑁 Mat if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ) ) )
5 fveq2 ⊢ ( 𝑅 = if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) → ( Base ‘ 𝑅 ) = ( Base ‘ if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) )
6 5 eleq2d ⊢ ( 𝑅 = if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) → ( 𝑆 ∈ ( Base ‘ 𝑅 ) ↔ 𝑆 ∈ ( Base ‘ if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ) )
7 4 6 3anbi13d ⊢ ( 𝑅 = if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) → ( ( 𝑀 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ↔ ( 𝑀 ∈ ( Base ‘ ( 𝑁 Mat if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ) ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ) ) )
8 1 7 bitr3id ⊢ ( 𝑅 = if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) → ( ( 𝑀 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ) ↔ ( 𝑀 ∈ ( Base ‘ ( 𝑁 Mat if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ) ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ) ) )
9 oveq2 ⊢ ( 𝑅 = if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) → ( 𝑁 maDet 𝑅 ) = ( 𝑁 maDet if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) )
10 oveq2 ⊢ ( 𝑅 = if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) → ( 𝑁 matRRep 𝑅 ) = ( 𝑁 matRRep if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) )
11 10 oveqd ⊢ ( 𝑅 = if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) → ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) = ( 𝑀 ( 𝑁 matRRep if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) 𝑆 ) )
12 11 oveqd ⊢ ( 𝑅 = if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) → ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) = ( 𝐾 ( 𝑀 ( 𝑁 matRRep if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) 𝑆 ) 𝐾 ) )
13 9 12 fveq12d ⊢ ( 𝑅 = if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) → ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) ) = ( ( 𝑁 maDet if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ‘ ( 𝐾 ( 𝑀 ( 𝑁 matRRep if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) 𝑆 ) 𝐾 ) ) )
14 fveq2 ⊢ ( 𝑅 = if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) → ( .r ‘ 𝑅 ) = ( .r ‘ if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) )
15 eqidd ⊢ ( 𝑅 = if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) → 𝑆 = 𝑆 )
16 oveq2 ⊢ ( 𝑅 = if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) → ( ( 𝑁 ∖ { 𝐾 } ) maDet 𝑅 ) = ( ( 𝑁 ∖ { 𝐾 } ) maDet if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) )
17 oveq2 ⊢ ( 𝑅 = if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) → ( 𝑁 subMat 𝑅 ) = ( 𝑁 subMat if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) )
18 17 fveq1d ⊢ ( 𝑅 = if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) → ( ( 𝑁 subMat 𝑅 ) ‘ 𝑀 ) = ( ( 𝑁 subMat if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ‘ 𝑀 ) )
19 18 oveqd ⊢ ( 𝑅 = if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) → ( 𝐾 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑀 ) 𝐾 ) = ( 𝐾 ( ( 𝑁 subMat if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ‘ 𝑀 ) 𝐾 ) )
20 16 19 fveq12d ⊢ ( 𝑅 = if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) → ( ( ( 𝑁 ∖ { 𝐾 } ) maDet 𝑅 ) ‘ ( 𝐾 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) = ( ( ( 𝑁 ∖ { 𝐾 } ) maDet if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ‘ ( 𝐾 ( ( 𝑁 subMat if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ‘ 𝑀 ) 𝐾 ) ) )
21 14 15 20 oveq123d ⊢ ( 𝑅 = if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) → ( 𝑆 ( .r ‘ 𝑅 ) ( ( ( 𝑁 ∖ { 𝐾 } ) maDet 𝑅 ) ‘ ( 𝐾 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) ) = ( 𝑆 ( .r ‘ if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ( ( ( 𝑁 ∖ { 𝐾 } ) maDet if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ‘ ( 𝐾 ( ( 𝑁 subMat if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ‘ 𝑀 ) 𝐾 ) ) ) )
22 13 21 eqeq12d ⊢ ( 𝑅 = if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) → ( ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) ) = ( 𝑆 ( .r ‘ 𝑅 ) ( ( ( 𝑁 ∖ { 𝐾 } ) maDet 𝑅 ) ‘ ( 𝐾 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) ) ↔ ( ( 𝑁 maDet if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ‘ ( 𝐾 ( 𝑀 ( 𝑁 matRRep if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) 𝑆 ) 𝐾 ) ) = ( 𝑆 ( .r ‘ if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ( ( ( 𝑁 ∖ { 𝐾 } ) maDet if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ‘ ( 𝐾 ( ( 𝑁 subMat if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ‘ 𝑀 ) 𝐾 ) ) ) ) )
23 8 22 imbi12d ⊢ ( 𝑅 = if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) → ( ( ( 𝑀 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) ) = ( 𝑆 ( .r ‘ 𝑅 ) ( ( ( 𝑁 ∖ { 𝐾 } ) maDet 𝑅 ) ‘ ( 𝐾 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) ) ) ↔ ( ( 𝑀 ∈ ( Base ‘ ( 𝑁 Mat if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ) ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ) → ( ( 𝑁 maDet if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ‘ ( 𝐾 ( 𝑀 ( 𝑁 matRRep if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) 𝑆 ) 𝐾 ) ) = ( 𝑆 ( .r ‘ if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ( ( ( 𝑁 ∖ { 𝐾 } ) maDet if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ‘ ( 𝐾 ( ( 𝑁 subMat if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ‘ 𝑀 ) 𝐾 ) ) ) ) ) )
24 cncrng ⊢ ℂfld ∈ CRing
25 24 elimel ⊢ if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ∈ CRing
26 25 smadiadetg0 ⊢ ( ( 𝑀 ∈ ( Base ‘ ( 𝑁 Mat if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ) ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ) → ( ( 𝑁 maDet if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ‘ ( 𝐾 ( 𝑀 ( 𝑁 matRRep if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) 𝑆 ) 𝐾 ) ) = ( 𝑆 ( .r ‘ if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ( ( ( 𝑁 ∖ { 𝐾 } ) maDet if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ‘ ( 𝐾 ( ( 𝑁 subMat if ( 𝑅 ∈ CRing , 𝑅 , ℂfld ) ) ‘ 𝑀 ) 𝐾 ) ) ) )
27 23 26 dedth ⊢ ( 𝑅 ∈ CRing → ( ( 𝑀 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) ) = ( 𝑆 ( .r ‘ 𝑅 ) ( ( ( 𝑁 ∖ { 𝐾 } ) maDet 𝑅 ) ‘ ( 𝐾 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) ) ) )
28 27 impl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) ) = ( 𝑆 ( .r ‘ 𝑅 ) ( ( ( 𝑁 ∖ { 𝐾 } ) maDet 𝑅 ) ‘ ( 𝐾 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) ) )