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 ⊢ R ∈ CRing ∧ M ∈ Base N Mat R ∧ K ∈ N ∧ S ∈ Base R → N maDet R ⁡ K M N matRRep R S K = S ⋅ R N ∖ K maDet R ⁡ K N subMat R ⁡ M K

Proof

Step Hyp Ref Expression
1 3anass ⊢ M ∈ Base N Mat R ∧ K ∈ N ∧ S ∈ Base R ↔ M ∈ Base N Mat R ∧ K ∈ N ∧ S ∈ Base R
2 oveq2 ⊢ R = if R ∈ CRing R ℂ fld → N Mat R = N Mat if R ∈ CRing R ℂ fld
3 2 fveq2d ⊢ R = if R ∈ CRing R ℂ fld → Base N Mat R = Base N Mat if R ∈ CRing R ℂ fld
4 3 eleq2d ⊢ R = if R ∈ CRing R ℂ fld → M ∈ Base N Mat R ↔ M ∈ Base N Mat if R ∈ CRing R ℂ fld
5 fveq2 ⊢ R = if R ∈ CRing R ℂ fld → Base R = Base if R ∈ CRing R ℂ fld
6 5 eleq2d ⊢ R = if R ∈ CRing R ℂ fld → S ∈ Base R ↔ S ∈ Base if R ∈ CRing R ℂ fld
7 4 6 3anbi13d ⊢ R = if R ∈ CRing R ℂ fld → M ∈ Base N Mat R ∧ K ∈ N ∧ S ∈ Base R ↔ M ∈ Base N Mat if R ∈ CRing R ℂ fld ∧ K ∈ N ∧ S ∈ Base if R ∈ CRing R ℂ fld
8 1 7 bitr3id ⊢ R = if R ∈ CRing R ℂ fld → M ∈ Base N Mat R ∧ K ∈ N ∧ S ∈ Base R ↔ M ∈ Base N Mat if R ∈ CRing R ℂ fld ∧ K ∈ N ∧ S ∈ Base if R ∈ CRing R ℂ fld
9 oveq2 ⊢ R = if R ∈ CRing R ℂ fld → N maDet R = N maDet if R ∈ CRing R ℂ fld
10 oveq2 ⊢ R = if R ∈ CRing R ℂ fld → N matRRep R = N matRRep if R ∈ CRing R ℂ fld
11 10 oveqd ⊢ R = if R ∈ CRing R ℂ fld → M N matRRep R S = M N matRRep if R ∈ CRing R ℂ fld S
12 11 oveqd ⊢ R = if R ∈ CRing R ℂ fld → K M N matRRep R S K = K M N matRRep if R ∈ CRing R ℂ fld S K
13 9 12 fveq12d ⊢ R = if R ∈ CRing R ℂ fld → N maDet R ⁡ K M N matRRep R S K = N maDet if R ∈ CRing R ℂ fld ⁡ K M N matRRep if R ∈ CRing R ℂ fld S K
14 fveq2 ⊢ R = if R ∈ CRing R ℂ fld → ⋅ R = ⋅ if R ∈ CRing R ℂ fld
15 eqidd ⊢ R = if R ∈ CRing R ℂ fld → S = S
16 oveq2 ⊢ R = if R ∈ CRing R ℂ fld → N ∖ K maDet R = N ∖ K maDet if R ∈ CRing R ℂ fld
17 oveq2 ⊢ R = if R ∈ CRing R ℂ fld → N subMat R = N subMat if R ∈ CRing R ℂ fld
18 17 fveq1d ⊢ R = if R ∈ CRing R ℂ fld → N subMat R ⁡ M = N subMat if R ∈ CRing R ℂ fld ⁡ M
19 18 oveqd ⊢ R = if R ∈ CRing R ℂ fld → K N subMat R ⁡ M K = K N subMat if R ∈ CRing R ℂ fld ⁡ M K
20 16 19 fveq12d ⊢ R = if R ∈ CRing R ℂ fld → N ∖ K maDet R ⁡ K N subMat R ⁡ M K = N ∖ K maDet if R ∈ CRing R ℂ fld ⁡ K N subMat if R ∈ CRing R ℂ fld ⁡ M K
21 14 15 20 oveq123d ⊢ R = if R ∈ CRing R ℂ fld → S ⋅ R N ∖ K maDet R ⁡ K N subMat R ⁡ M K = S ⋅ if R ∈ CRing R ℂ fld N ∖ K maDet if R ∈ CRing R ℂ fld ⁡ K N subMat if R ∈ CRing R ℂ fld ⁡ M K
22 13 21 eqeq12d ⊢ R = if R ∈ CRing R ℂ fld → N maDet R ⁡ K M N matRRep R S K = S ⋅ R N ∖ K maDet R ⁡ K N subMat R ⁡ M K ↔ N maDet if R ∈ CRing R ℂ fld ⁡ K M N matRRep if R ∈ CRing R ℂ fld S K = S ⋅ if R ∈ CRing R ℂ fld N ∖ K maDet if R ∈ CRing R ℂ fld ⁡ K N subMat if R ∈ CRing R ℂ fld ⁡ M K
23 8 22 imbi12d ⊢ R = if R ∈ CRing R ℂ fld → M ∈ Base N Mat R ∧ K ∈ N ∧ S ∈ Base R → N maDet R ⁡ K M N matRRep R S K = S ⋅ R N ∖ K maDet R ⁡ K N subMat R ⁡ M K ↔ M ∈ Base N Mat if R ∈ CRing R ℂ fld ∧ K ∈ N ∧ S ∈ Base if R ∈ CRing R ℂ fld → N maDet if R ∈ CRing R ℂ fld ⁡ K M N matRRep if R ∈ CRing R ℂ fld S K = S ⋅ if R ∈ CRing R ℂ fld N ∖ K maDet if R ∈ CRing R ℂ fld ⁡ K N subMat if R ∈ CRing R ℂ fld ⁡ M K
24 cncrng ⊢ ℂ fld ∈ CRing
25 24 elimel ⊢ if R ∈ CRing R ℂ fld ∈ CRing
26 25 smadiadetg0 ⊢ M ∈ Base N Mat if R ∈ CRing R ℂ fld ∧ K ∈ N ∧ S ∈ Base if R ∈ CRing R ℂ fld → N maDet if R ∈ CRing R ℂ fld ⁡ K M N matRRep if R ∈ CRing R ℂ fld S K = S ⋅ if R ∈ CRing R ℂ fld N ∖ K maDet if R ∈ CRing R ℂ fld ⁡ K N subMat if R ∈ CRing R ℂ fld ⁡ M K
27 23 26 dedth ⊢ R ∈ CRing → M ∈ Base N Mat R ∧ K ∈ N ∧ S ∈ Base R → N maDet R ⁡ K M N matRRep R S K = S ⋅ R N ∖ K maDet R ⁡ K N subMat R ⁡ M K
28 27 impl ⊢ R ∈ CRing ∧ M ∈ Base N Mat R ∧ K ∈ N ∧ S ∈ Base R → N maDet R ⁡ K M N matRRep R S K = S ⋅ R N ∖ K maDet R ⁡ K N subMat R ⁡ M K