Theorem mdetralt2

Description: The determinant function is alternating regarding rows (matrix is given explicitly by its entries). (Contributed by SO, 16-Jul-2018)

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

Proof

Step	Hyp	Ref	Expression
1		mdetralt2.d	$$⊢D=N\mathrm{maDet}R$$
2		mdetralt2.k	$$⊢K={\mathrm{Base}}_R$$
3		mdetralt2.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		mdetralt2.r	$$⊢\phi \to R\in \mathrm{CRing}$$
5		mdetralt2.n	$$⊢\phi \to N\in \mathrm{Fin}$$
6		mdetralt2.x	$$⊢\left(\phi \wedge j\in N\right)\to X\in K$$
7		mdetralt2.y	$$⊢\left(\phi \wedge i\in N\wedge j\in N\right)\to Y\in K$$
8		mdetralt2.i	$$⊢\phi \to I\in N$$
9		mdetralt2.j	$$⊢\phi \to J\in N$$
10		mdetralt2.ij	$$⊢\phi \to I\ne J$$
11		eqid	$$⊢N\mathrm{Mat}R=N\mathrm{Mat}R$$
12		eqid	$$⊢{\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}={\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}$$
13	6	3adant2	$$⊢\left(\phi \wedge i\in N\wedge j\in N\right)\to X\in K$$
14	13 7	ifcld	$$⊢\left(\phi \wedge i\in N\wedge j\in N\right)\to if\left(i=J,X,Y\right)\in K$$
15	13 14	ifcld	$$⊢\left(\phi \wedge i\in N\wedge j\in N\right)\to if\left(i=I,X,if\left(i=J,X,Y\right)\right)\in K$$
16	11 2 12 5 4 15	matbas2d	$$⊢\phi \to \left(i\in N,j\in N⟼if\left(i=I,X,if\left(i=J,X,Y\right)\right)\right)\in {\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}$$
17		eqidd	$$⊢\left(\phi \wedge w\in N\right)\to \left(i\in N,j\in N⟼if\left(i=I,X,if\left(i=J,X,Y\right)\right)\right)=\left(i\in N,j\in N⟼if\left(i=I,X,if\left(i=J,X,Y\right)\right)\right)$$
18		iftrue	$$⊢i=I\to if\left(i=I,X,if\left(i=J,X,Y\right)\right)=X$$
19	18	ad2antrl	$$⊢\left(\left(\phi \wedge w\in N\right)\wedge \left(i=I\wedge j=w\right)\right)\to if\left(i=I,X,if\left(i=J,X,Y\right)\right)=X$$
20		csbeq1a	$$⊢j=w\to X=⦋w/j⦌X$$
21	20	ad2antll	$$⊢\left(\left(\phi \wedge w\in N\right)\wedge \left(i=I\wedge j=w\right)\right)\to X=⦋w/j⦌X$$
22	19 21	eqtrd	$$⊢\left(\left(\phi \wedge w\in N\right)\wedge \left(i=I\wedge j=w\right)\right)\to if\left(i=I,X,if\left(i=J,X,Y\right)\right)=⦋w/j⦌X$$
23		eqidd	$$⊢\left(\left(\phi \wedge w\in N\right)\wedge i=I\right)\to N=N$$
24	8	adantr	$$⊢\left(\phi \wedge w\in N\right)\to I\in N$$
25		simpr	$$⊢\left(\phi \wedge w\in N\right)\to w\in N$$
26		nfv	$$⊢Ⅎj\left(\phi \wedge w\in N\right)$$
27		nfcsb1v	$$⊢\underset{\_}{Ⅎ}j⦋w/j⦌X$$
28	27	nfel1	$$⊢Ⅎj⦋w/j⦌X\in K$$
29	26 28	nfim	$$⊢Ⅎj\left(\left(\phi \wedge w\in N\right)\to ⦋w/j⦌X\in K\right)$$
30		eleq1w	$$⊢j=w\to \left(j\in N\leftrightarrow w\in N\right)$$
31	30	anbi2d	$$⊢j=w\to \left(\left(\phi \wedge j\in N\right)\leftrightarrow \left(\phi \wedge w\in N\right)\right)$$
32	20	eleq1d	$$⊢j=w\to \left(X\in K\leftrightarrow ⦋w/j⦌X\in K\right)$$
33	31 32	imbi12d	$$⊢j=w\to \left(\left(\left(\phi \wedge j\in N\right)\to X\in K\right)\leftrightarrow \left(\left(\phi \wedge w\in N\right)\to ⦋w/j⦌X\in K\right)\right)$$
34	29 33 6	chvarfv	$$⊢\left(\phi \wedge w\in N\right)\to ⦋w/j⦌X\in K$$
35		nfv	$$⊢Ⅎi\left(\phi \wedge w\in N\right)$$
36		nfcv	$$⊢\underset{\_}{Ⅎ}jI$$
37		nfcv	$$⊢\underset{\_}{Ⅎ}iw$$
38		nfcv	$$⊢\underset{\_}{Ⅎ}i⦋w/j⦌X$$
39	17 22 23 24 25 34 35 26 36 37 38 27	ovmpodxf	$$⊢\left(\phi \wedge w\in N\right)\to I\left(i\in N,j\in N⟼if\left(i=I,X,if\left(i=J,X,Y\right)\right)\right)w=⦋w/j⦌X$$
40		iftrue	$$⊢i=J\to if\left(i=J,X,Y\right)=X$$
41	40	ifeq2d	$$⊢i=J\to if\left(i=I,X,if\left(i=J,X,Y\right)\right)=if\left(i=I,X,X\right)$$
42		ifid	$$⊢if\left(i=I,X,X\right)=X$$
43	41 42	syl6eq	$$⊢i=J\to if\left(i=I,X,if\left(i=J,X,Y\right)\right)=X$$
44	43	ad2antrl	$$⊢\left(\left(\phi \wedge w\in N\right)\wedge \left(i=J\wedge j=w\right)\right)\to if\left(i=I,X,if\left(i=J,X,Y\right)\right)=X$$
45	20	ad2antll	$$⊢\left(\left(\phi \wedge w\in N\right)\wedge \left(i=J\wedge j=w\right)\right)\to X=⦋w/j⦌X$$
46	44 45	eqtrd	$$⊢\left(\left(\phi \wedge w\in N\right)\wedge \left(i=J\wedge j=w\right)\right)\to if\left(i=I,X,if\left(i=J,X,Y\right)\right)=⦋w/j⦌X$$
47		eqidd	$$⊢\left(\left(\phi \wedge w\in N\right)\wedge i=J\right)\to N=N$$
48	9	adantr	$$⊢\left(\phi \wedge w\in N\right)\to J\in N$$
49		nfcv	$$⊢\underset{\_}{Ⅎ}jJ$$
50	17 46 47 48 25 34 35 26 49 37 38 27	ovmpodxf	$$⊢\left(\phi \wedge w\in N\right)\to J\left(i\in N,j\in N⟼if\left(i=I,X,if\left(i=J,X,Y\right)\right)\right)w=⦋w/j⦌X$$
51	39 50	eqtr4d	$$⊢\left(\phi \wedge w\in N\right)\to I\left(i\in N,j\in N⟼if\left(i=I,X,if\left(i=J,X,Y\right)\right)\right)w=J\left(i\in N,j\in N⟼if\left(i=I,X,if\left(i=J,X,Y\right)\right)\right)w$$
52	51	ralrimiva	$$⊢\phi \to \forall w\in NI\left(i\in N,j\in N⟼if\left(i=I,X,if\left(i=J,X,Y\right)\right)\right)w=J\left(i\in N,j\in N⟼if\left(i=I,X,if\left(i=J,X,Y\right)\right)\right)w$$
53	1 11 12 3 4 16 8 9 10 52	mdetralt	$$⊢\phi \to D\left(\left(i\in N,j\in N⟼if\left(i=I,X,if\left(i=J,X,Y\right)\right)\right)\right)=\underset{\dot{}}{0}$$