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∈BaseNMatR∧K∈N∧S∈BaseR→NmaDetR⁡KMNmatRRepRSK=S⋅RN∖KmaDetR⁡KNsubMatR⁡MK

Proof

Step Hyp Ref Expression
1 3anass ⊢M∈BaseNMatR∧K∈N∧S∈BaseR↔M∈BaseNMatR∧K∈N∧S∈BaseR
2 oveq2 ⊢R=ifR∈CRingRℂfld→NMatR=NMatifR∈CRingRℂfld
3 2 fveq2d ⊢R=ifR∈CRingRℂfld→BaseNMatR=BaseNMatifR∈CRingRℂfld
4 3 eleq2d ⊢R=ifR∈CRingRℂfld→M∈BaseNMatR↔M∈BaseNMatifR∈CRingRℂfld
5 fveq2 ⊢R=ifR∈CRingRℂfld→BaseR=BaseifR∈CRingRℂfld
6 5 eleq2d ⊢R=ifR∈CRingRℂfld→S∈BaseR↔S∈BaseifR∈CRingRℂfld
7 4 6 3anbi13d ⊢R=ifR∈CRingRℂfld→M∈BaseNMatR∧K∈N∧S∈BaseR↔M∈BaseNMatifR∈CRingRℂfld∧K∈N∧S∈BaseifR∈CRingRℂfld
8 1 7 bitr3id ⊢R=ifR∈CRingRℂfld→M∈BaseNMatR∧K∈N∧S∈BaseR↔M∈BaseNMatifR∈CRingRℂfld∧K∈N∧S∈BaseifR∈CRingRℂfld
9 oveq2 ⊢R=ifR∈CRingRℂfld→NmaDetR=NmaDetifR∈CRingRℂfld
10 oveq2 ⊢R=ifR∈CRingRℂfld→NmatRRepR=NmatRRepifR∈CRingRℂfld
11 10 oveqd ⊢R=ifR∈CRingRℂfld→MNmatRRepRS=MNmatRRepifR∈CRingRℂfldS
12 11 oveqd ⊢R=ifR∈CRingRℂfld→KMNmatRRepRSK=KMNmatRRepifR∈CRingRℂfldSK
13 9 12 fveq12d ⊢R=ifR∈CRingRℂfld→NmaDetR⁡KMNmatRRepRSK=NmaDetifR∈CRingRℂfld⁡KMNmatRRepifR∈CRingRℂfldSK
14 fveq2 ⊢R=ifR∈CRingRℂfld→⋅R=⋅ifR∈CRingRℂfld
15 eqidd ⊢R=ifR∈CRingRℂfld→S=S
16 oveq2 ⊢R=ifR∈CRingRℂfld→N∖KmaDetR=N∖KmaDetifR∈CRingRℂfld
17 oveq2 ⊢R=ifR∈CRingRℂfld→NsubMatR=NsubMatifR∈CRingRℂfld
18 17 fveq1d ⊢R=ifR∈CRingRℂfld→NsubMatR⁡M=NsubMatifR∈CRingRℂfld⁡M
19 18 oveqd ⊢R=ifR∈CRingRℂfld→KNsubMatR⁡MK=KNsubMatifR∈CRingRℂfld⁡MK
20 16 19 fveq12d ⊢R=ifR∈CRingRℂfld→N∖KmaDetR⁡KNsubMatR⁡MK=N∖KmaDetifR∈CRingRℂfld⁡KNsubMatifR∈CRingRℂfld⁡MK
21 14 15 20 oveq123d ⊢R=ifR∈CRingRℂfld→S⋅RN∖KmaDetR⁡KNsubMatR⁡MK=S⋅ifR∈CRingRℂfldN∖KmaDetifR∈CRingRℂfld⁡KNsubMatifR∈CRingRℂfld⁡MK
22 13 21 eqeq12d ⊢R=ifR∈CRingRℂfld→NmaDetR⁡KMNmatRRepRSK=S⋅RN∖KmaDetR⁡KNsubMatR⁡MK↔NmaDetifR∈CRingRℂfld⁡KMNmatRRepifR∈CRingRℂfldSK=S⋅ifR∈CRingRℂfldN∖KmaDetifR∈CRingRℂfld⁡KNsubMatifR∈CRingRℂfld⁡MK
23 8 22 imbi12d ⊢R=ifR∈CRingRℂfld→M∈BaseNMatR∧K∈N∧S∈BaseR→NmaDetR⁡KMNmatRRepRSK=S⋅RN∖KmaDetR⁡KNsubMatR⁡MK↔M∈BaseNMatifR∈CRingRℂfld∧K∈N∧S∈BaseifR∈CRingRℂfld→NmaDetifR∈CRingRℂfld⁡KMNmatRRepifR∈CRingRℂfldSK=S⋅ifR∈CRingRℂfldN∖KmaDetifR∈CRingRℂfld⁡KNsubMatifR∈CRingRℂfld⁡MK
24 cncrng ⊢ℂfld∈CRing
25 24 elimel ⊢ifR∈CRingRℂfld∈CRing
26 25 smadiadetg0 ⊢M∈BaseNMatifR∈CRingRℂfld∧K∈N∧S∈BaseifR∈CRingRℂfld→NmaDetifR∈CRingRℂfld⁡KMNmatRRepifR∈CRingRℂfldSK=S⋅ifR∈CRingRℂfldN∖KmaDetifR∈CRingRℂfld⁡KNsubMatifR∈CRingRℂfld⁡MK
27 23 26 dedth ⊢R∈CRing→M∈BaseNMatR∧K∈N∧S∈BaseR→NmaDetR⁡KMNmatRRepRSK=S⋅RN∖KmaDetR⁡KNsubMatR⁡MK
28 27 impl ⊢R∈CRing∧M∈BaseNMatR∧K∈N∧S∈BaseR→NmaDetR⁡KMNmatRRepRSK=S⋅RN∖KmaDetR⁡KNsubMatR⁡MK