Theorem mdetero

Description: The determinant function is multilinear (additive and homogeneous for each row (matrices are given explicitly by their entries). Corollary 4.9 in Lang p. 515. (Contributed by SO, 16-Jul-2018)

	Ref	Expression
Hypotheses	mdetero.d	$$⊢D=N\mathrm{maDet}R$$
	mdetero.k	$$⊢K={\mathrm{Base}}_R$$
	mdetero.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	mdetero.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	mdetero.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	mdetero.n	$$⊢\phi \to N\in \mathrm{Fin}$$
	mdetero.x	$$⊢\left(\phi \wedge j\in N\right)\to X\in K$$
	mdetero.y	$$⊢\left(\phi \wedge j\in N\right)\to Y\in K$$
	mdetero.z	$$⊢\left(\phi \wedge i\in N\wedge j\in N\right)\to Z\in K$$
	mdetero.w	$$⊢\phi \to W\in K$$
	mdetero.i	$$⊢\phi \to I\in N$$
	mdetero.j	$$⊢\phi \to J\in N$$
	mdetero.ij	$$⊢\phi \to I\ne J$$
Assertion	mdetero	$$⊢\phi \to D\left(\left(i\in N,j\in N⟼if\left(i=I,X\underset{\dot{}}{+}\left(W\underset{\dot{}}{·}Y\right),if\left(i=J,Y,Z\right)\right)\right)\right)=D\left(\left(i\in N,j\in N⟼if\left(i=I,X,if\left(i=J,Y,Z\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mdetero.d	$$⊢D=N\mathrm{maDet}R$$
2		mdetero.k	$$⊢K={\mathrm{Base}}_R$$
3		mdetero.p	$$⊢\underset{\dot{}}{+}={+}_R$$
4		mdetero.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
5		mdetero.r	$$⊢\phi \to R\in \mathrm{CRing}$$
6		mdetero.n	$$⊢\phi \to N\in \mathrm{Fin}$$
7		mdetero.x	$$⊢\left(\phi \wedge j\in N\right)\to X\in K$$
8		mdetero.y	$$⊢\left(\phi \wedge j\in N\right)\to Y\in K$$
9		mdetero.z	$$⊢\left(\phi \wedge i\in N\wedge j\in N\right)\to Z\in K$$
10		mdetero.w	$$⊢\phi \to W\in K$$
11		mdetero.i	$$⊢\phi \to I\in N$$
12		mdetero.j	$$⊢\phi \to J\in N$$
13		mdetero.ij	$$⊢\phi \to I\ne J$$
14	7	3adant2	$$⊢\left(\phi \wedge i\in N\wedge j\in N\right)\to X\in K$$
15		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
16	5 15	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
17	16	3ad2ant1	$$⊢\left(\phi \wedge i\in N\wedge j\in N\right)\to R\in \mathrm{Ring}$$
18	10	3ad2ant1	$$⊢\left(\phi \wedge i\in N\wedge j\in N\right)\to W\in K$$
19	8	3adant2	$$⊢\left(\phi \wedge i\in N\wedge j\in N\right)\to Y\in K$$
20	2 4	ringcl	$$⊢\left(R\in \mathrm{Ring}\wedge W\in K\wedge Y\in K\right)\to W\underset{\dot{}}{·}Y\in K$$
21	17 18 19 20	syl3anc	$$⊢\left(\phi \wedge i\in N\wedge j\in N\right)\to W\underset{\dot{}}{·}Y\in K$$
22	19 9	ifcld	$$⊢\left(\phi \wedge i\in N\wedge j\in N\right)\to if\left(i=J,Y,Z\right)\in K$$
23	1 2 3 5 6 14 21 22 11	mdetrlin2	$$⊢\phi \to D\left(\left(i\in N,j\in N⟼if\left(i=I,X\underset{\dot{}}{+}\left(W\underset{\dot{}}{·}Y\right),if\left(i=J,Y,Z\right)\right)\right)\right)=D\left(\left(i\in N,j\in N⟼if\left(i=I,X,if\left(i=J,Y,Z\right)\right)\right)\right)\underset{\dot{}}{+}D\left(\left(i\in N,j\in N⟼if\left(i=I,W\underset{\dot{}}{·}Y,if\left(i=J,Y,Z\right)\right)\right)\right)$$
24	1 2 4 5 6 19 22 10 11	mdetrsca2	$$⊢\phi \to D\left(\left(i\in N,j\in N⟼if\left(i=I,W\underset{\dot{}}{·}Y,if\left(i=J,Y,Z\right)\right)\right)\right)=W\underset{\dot{}}{·}D\left(\left(i\in N,j\in N⟼if\left(i=I,Y,if\left(i=J,Y,Z\right)\right)\right)\right)$$
25		eqid	$$⊢0_R=0_R$$
26	1 2 25 5 6 8 9 11 12 13	mdetralt2	$$⊢\phi \to D\left(\left(i\in N,j\in N⟼if\left(i=I,Y,if\left(i=J,Y,Z\right)\right)\right)\right)=0_R$$
27	26	oveq2d	$$⊢\phi \to W\underset{\dot{}}{·}D\left(\left(i\in N,j\in N⟼if\left(i=I,Y,if\left(i=J,Y,Z\right)\right)\right)\right)=W\underset{\dot{}}{·}{0}_R$$
28	2 4 25	ringrz	$$⊢\left(R\in \mathrm{Ring}\wedge W\in K\right)\to W\underset{\dot{}}{·}{0}_R=0_R$$
29	16 10 28	syl2anc	$$⊢\phi \to W\underset{\dot{}}{·}{0}_R=0_R$$
30	24 27 29	3eqtrd	$$⊢\phi \to D\left(\left(i\in N,j\in N⟼if\left(i=I,W\underset{\dot{}}{·}Y,if\left(i=J,Y,Z\right)\right)\right)\right)=0_R$$
31	30	oveq2d	$$⊢\phi \to D\left(\left(i\in N,j\in N⟼if\left(i=I,X,if\left(i=J,Y,Z\right)\right)\right)\right)\underset{\dot{}}{+}D\left(\left(i\in N,j\in N⟼if\left(i=I,W\underset{\dot{}}{·}Y,if\left(i=J,Y,Z\right)\right)\right)\right)=D\left(\left(i\in N,j\in N⟼if\left(i=I,X,if\left(i=J,Y,Z\right)\right)\right)\right)\underset{\dot{}}{+}{0}_R$$
32		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
33	16 32	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
34		eqid	$$⊢N\mathrm{Mat}R=N\mathrm{Mat}R$$
35		eqid	$$⊢{\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}={\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}$$
36	1 34 35 2	mdetf	$$⊢R\in \mathrm{CRing}\to D:{\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}⟶K$$
37	5 36	syl	$$⊢\phi \to D:{\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}⟶K$$
38	14 22	ifcld	$$⊢\left(\phi \wedge i\in N\wedge j\in N\right)\to if\left(i=I,X,if\left(i=J,Y,Z\right)\right)\in K$$
39	34 2 35 6 5 38	matbas2d	$$⊢\phi \to \left(i\in N,j\in N⟼if\left(i=I,X,if\left(i=J,Y,Z\right)\right)\right)\in {\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}$$
40	37 39	ffvelcdmd	$$⊢\phi \to D\left(\left(i\in N,j\in N⟼if\left(i=I,X,if\left(i=J,Y,Z\right)\right)\right)\right)\in K$$
41	2 3 25	grprid	$$⊢\left(R\in \mathrm{Grp}\wedge D\left(\left(i\in N,j\in N⟼if\left(i=I,X,if\left(i=J,Y,Z\right)\right)\right)\right)\in K\right)\to D\left(\left(i\in N,j\in N⟼if\left(i=I,X,if\left(i=J,Y,Z\right)\right)\right)\right)\underset{\dot{}}{+}{0}_R=D\left(\left(i\in N,j\in N⟼if\left(i=I,X,if\left(i=J,Y,Z\right)\right)\right)\right)$$
42	33 40 41	syl2anc	$$⊢\phi \to D\left(\left(i\in N,j\in N⟼if\left(i=I,X,if\left(i=J,Y,Z\right)\right)\right)\right)\underset{\dot{}}{+}{0}_R=D\left(\left(i\in N,j\in N⟼if\left(i=I,X,if\left(i=J,Y,Z\right)\right)\right)\right)$$
43	23 31 42	3eqtrd	$$⊢\phi \to D\left(\left(i\in N,j\in N⟼if\left(i=I,X\underset{\dot{}}{+}\left(W\underset{\dot{}}{·}Y\right),if\left(i=J,Y,Z\right)\right)\right)\right)=D\left(\left(i\in N,j\in N⟼if\left(i=I,X,if\left(i=J,Y,Z\right)\right)\right)\right)$$