Theorem mdetr0

Description: The determinant of a matrix with a row containing only 0's is 0. (Contributed by SO, 16-Jul-2018)

	Ref	Expression
Hypotheses	mdetr0.d	$$⊢D=N\mathrm{maDet}R$$
	mdetr0.k	$$⊢K={\mathrm{Base}}_R$$
	mdetr0.z	$$⊢\underset{\dot{}}{0}=0_R$$
	mdetr0.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	mdetr0.n	$$⊢\phi \to N\in \mathrm{Fin}$$
	mdetr0.x	$$⊢\left(\phi \wedge i\in N\wedge j\in N\right)\to X\in K$$
	mdetr0.i	$$⊢\phi \to I\in N$$
Assertion	mdetr0	$$⊢\phi \to D\left(\left(i\in N,j\in N⟼if\left(i=I,\underset{\dot{}}{0},X\right)\right)\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		mdetr0.d	$$⊢D=N\mathrm{maDet}R$$
2		mdetr0.k	$$⊢K={\mathrm{Base}}_R$$
3		mdetr0.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		mdetr0.r	$$⊢\phi \to R\in \mathrm{CRing}$$
5		mdetr0.n	$$⊢\phi \to N\in \mathrm{Fin}$$
6		mdetr0.x	$$⊢\left(\phi \wedge i\in N\wedge j\in N\right)\to X\in K$$
7		mdetr0.i	$$⊢\phi \to I\in N$$
8		eqid	$$⊢{\cdot }_R={\cdot }_R$$
9		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
10	4 9	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
11	2 3	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in K$$
12	10 11	syl	$$⊢\phi \to \underset{\dot{}}{0}\in K$$
13	12	3ad2ant1	$$⊢\left(\phi \wedge i\in N\wedge j\in N\right)\to \underset{\dot{}}{0}\in K$$
14	1 2 8 4 5 13 6 12 7	mdetrsca2	$$⊢\phi \to D\left(\left(i\in N,j\in N⟼if\left(i=I,\underset{\dot{}}{0}{\cdot }_R\underset{\dot{}}{0},X\right)\right)\right)=\underset{\dot{}}{0}{\cdot }_{R}D\left(\left(i\in N,j\in N⟼if\left(i=I,\underset{\dot{}}{0},X\right)\right)\right)$$
15	2 8 3	ringlz	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{0}\in K\right)\to \underset{\dot{}}{0}{\cdot }_R\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
16	10 12 15	syl2anc	$$⊢\phi \to \underset{\dot{}}{0}{\cdot }_R\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
17	16	ifeq1d	$$⊢\phi \to if\left(i=I,\underset{\dot{}}{0}{\cdot }_R\underset{\dot{}}{0},X\right)=if\left(i=I,\underset{\dot{}}{0},X\right)$$
18	17	mpoeq3dv	$$⊢\phi \to \left(i\in N,j\in N⟼if\left(i=I,\underset{\dot{}}{0}{\cdot }_R\underset{\dot{}}{0},X\right)\right)=\left(i\in N,j\in N⟼if\left(i=I,\underset{\dot{}}{0},X\right)\right)$$
19	18	fveq2d	$$⊢\phi \to D\left(\left(i\in N,j\in N⟼if\left(i=I,\underset{\dot{}}{0}{\cdot }_R\underset{\dot{}}{0},X\right)\right)\right)=D\left(\left(i\in N,j\in N⟼if\left(i=I,\underset{\dot{}}{0},X\right)\right)\right)$$
20		eqid	$$⊢N\mathrm{Mat}R=N\mathrm{Mat}R$$
21		eqid	$$⊢{\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}={\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}$$
22	1 20 21 2	mdetf	$$⊢R\in \mathrm{CRing}\to D:{\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}⟶K$$
23	4 22	syl	$$⊢\phi \to D:{\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}⟶K$$
24	13 6	ifcld	$$⊢\left(\phi \wedge i\in N\wedge j\in N\right)\to if\left(i=I,\underset{\dot{}}{0},X\right)\in K$$
25	20 2 21 5 4 24	matbas2d	$$⊢\phi \to \left(i\in N,j\in N⟼if\left(i=I,\underset{\dot{}}{0},X\right)\right)\in {\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}$$
26	23 25	ffvelrnd	$$⊢\phi \to D\left(\left(i\in N,j\in N⟼if\left(i=I,\underset{\dot{}}{0},X\right)\right)\right)\in K$$
27	2 8 3	ringlz	$$⊢\left(R\in \mathrm{Ring}\wedge D\left(\left(i\in N,j\in N⟼if\left(i=I,\underset{\dot{}}{0},X\right)\right)\right)\in K\right)\to \underset{\dot{}}{0}{\cdot }_{R}D\left(\left(i\in N,j\in N⟼if\left(i=I,\underset{\dot{}}{0},X\right)\right)\right)=\underset{\dot{}}{0}$$
28	10 26 27	syl2anc	$$⊢\phi \to \underset{\dot{}}{0}{\cdot }_{R}D\left(\left(i\in N,j\in N⟼if\left(i=I,\underset{\dot{}}{0},X\right)\right)\right)=\underset{\dot{}}{0}$$
29	14 19 28	3eqtr3d	$$⊢\phi \to D\left(\left(i\in N,j\in N⟼if\left(i=I,\underset{\dot{}}{0},X\right)\right)\right)=\underset{\dot{}}{0}$$