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	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
	mdetralt2.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	mdetralt2.z	⊢ 0 = ( 0_g ‘ 𝑅 )
	mdetralt2.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	mdetralt2.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
	mdetralt2.x	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑁 ) → 𝑋 ∈ 𝐾 )
	mdetralt2.y	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑌 ∈ 𝐾 )
	mdetralt2.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
	mdetralt2.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑁 )
	mdetralt2.ij	⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
Assertion	mdetralt2	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑋 , 𝑌 ) ) ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		mdetralt2.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
2		mdetralt2.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
3		mdetralt2.z	⊢ 0 = ( 0_g ‘ 𝑅 )
4		mdetralt2.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
5		mdetralt2.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
6		mdetralt2.x	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑁 ) → 𝑋 ∈ 𝐾 )
7		mdetralt2.y	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑌 ∈ 𝐾 )
8		mdetralt2.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
9		mdetralt2.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑁 )
10		mdetralt2.ij	⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
11		eqid	⊢ ( 𝑁 Mat 𝑅 ) = ( 𝑁 Mat 𝑅 )
12		eqid	⊢ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
13	6	3adant2	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑋 ∈ 𝐾 )
14	13 7	ifcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → if ( 𝑖 = 𝐽 , 𝑋 , 𝑌 ) ∈ 𝐾 )
15	13 14	ifcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑋 , 𝑌 ) ) ∈ 𝐾 )
16	11 2 12 5 4 15	matbas2d	⊢ ( 𝜑 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑋 , 𝑌 ) ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
17		eqidd	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑁 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑋 , 𝑌 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑋 , 𝑌 ) ) ) )
18		iftrue	⊢ ( 𝑖 = 𝐼 → if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑋 , 𝑌 ) ) = 𝑋 )
19	18	ad2antrl	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑁 ) ∧ ( 𝑖 = 𝐼 ∧ 𝑗 = 𝑤 ) ) → if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑋 , 𝑌 ) ) = 𝑋 )
20		csbeq1a	⊢ ( 𝑗 = 𝑤 → 𝑋 = ⦋ 𝑤 / 𝑗 ⦌ 𝑋 )
21	20	ad2antll	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑁 ) ∧ ( 𝑖 = 𝐼 ∧ 𝑗 = 𝑤 ) ) → 𝑋 = ⦋ 𝑤 / 𝑗 ⦌ 𝑋 )
22	19 21	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑁 ) ∧ ( 𝑖 = 𝐼 ∧ 𝑗 = 𝑤 ) ) → if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑋 , 𝑌 ) ) = ⦋ 𝑤 / 𝑗 ⦌ 𝑋 )
23		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑖 = 𝐼 ) → 𝑁 = 𝑁 )
24	8	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑁 ) → 𝐼 ∈ 𝑁 )
25		simpr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑁 ) → 𝑤 ∈ 𝑁 )
26		nfv	⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑤 ∈ 𝑁 )
27		nfcsb1v	⊢ Ⅎ 𝑗 ⦋ 𝑤 / 𝑗 ⦌ 𝑋
28	27	nfel1	⊢ Ⅎ 𝑗 ⦋ 𝑤 / 𝑗 ⦌ 𝑋 ∈ 𝐾
29	26 28	nfim	⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑤 ∈ 𝑁 ) → ⦋ 𝑤 / 𝑗 ⦌ 𝑋 ∈ 𝐾 )
30		eleq1w	⊢ ( 𝑗 = 𝑤 → ( 𝑗 ∈ 𝑁 ↔ 𝑤 ∈ 𝑁 ) )
31	30	anbi2d	⊢ ( 𝑗 = 𝑤 → ( ( 𝜑 ∧ 𝑗 ∈ 𝑁 ) ↔ ( 𝜑 ∧ 𝑤 ∈ 𝑁 ) ) )
32	20	eleq1d	⊢ ( 𝑗 = 𝑤 → ( 𝑋 ∈ 𝐾 ↔ ⦋ 𝑤 / 𝑗 ⦌ 𝑋 ∈ 𝐾 ) )
33	31 32	imbi12d	⊢ ( 𝑗 = 𝑤 → ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑁 ) → 𝑋 ∈ 𝐾 ) ↔ ( ( 𝜑 ∧ 𝑤 ∈ 𝑁 ) → ⦋ 𝑤 / 𝑗 ⦌ 𝑋 ∈ 𝐾 ) ) )
34	29 33 6	chvarfv	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑁 ) → ⦋ 𝑤 / 𝑗 ⦌ 𝑋 ∈ 𝐾 )
35		nfv	⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑤 ∈ 𝑁 )
36		nfcv	⊢ Ⅎ 𝑗 𝐼
37		nfcv	⊢ Ⅎ 𝑖 𝑤
38		nfcv	⊢ Ⅎ 𝑖 ⦋ 𝑤 / 𝑗 ⦌ 𝑋
39	17 22 23 24 25 34 35 26 36 37 38 27	ovmpodxf	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑁 ) → ( 𝐼 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑋 , 𝑌 ) ) ) 𝑤 ) = ⦋ 𝑤 / 𝑗 ⦌ 𝑋 )
40		iftrue	⊢ ( 𝑖 = 𝐽 → if ( 𝑖 = 𝐽 , 𝑋 , 𝑌 ) = 𝑋 )
41	40	ifeq2d	⊢ ( 𝑖 = 𝐽 → if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑋 , 𝑌 ) ) = if ( 𝑖 = 𝐼 , 𝑋 , 𝑋 ) )
42		ifid	⊢ if ( 𝑖 = 𝐼 , 𝑋 , 𝑋 ) = 𝑋
43	41 42	eqtrdi	⊢ ( 𝑖 = 𝐽 → if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑋 , 𝑌 ) ) = 𝑋 )
44	43	ad2antrl	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑁 ) ∧ ( 𝑖 = 𝐽 ∧ 𝑗 = 𝑤 ) ) → if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑋 , 𝑌 ) ) = 𝑋 )
45	20	ad2antll	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑁 ) ∧ ( 𝑖 = 𝐽 ∧ 𝑗 = 𝑤 ) ) → 𝑋 = ⦋ 𝑤 / 𝑗 ⦌ 𝑋 )
46	44 45	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑁 ) ∧ ( 𝑖 = 𝐽 ∧ 𝑗 = 𝑤 ) ) → if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑋 , 𝑌 ) ) = ⦋ 𝑤 / 𝑗 ⦌ 𝑋 )
47		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑁 ) ∧ 𝑖 = 𝐽 ) → 𝑁 = 𝑁 )
48	9	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑁 ) → 𝐽 ∈ 𝑁 )
49		nfcv	⊢ Ⅎ 𝑗 𝐽
50	17 46 47 48 25 34 35 26 49 37 38 27	ovmpodxf	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑁 ) → ( 𝐽 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑋 , 𝑌 ) ) ) 𝑤 ) = ⦋ 𝑤 / 𝑗 ⦌ 𝑋 )
51	39 50	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑁 ) → ( 𝐼 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑋 , 𝑌 ) ) ) 𝑤 ) = ( 𝐽 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑋 , 𝑌 ) ) ) 𝑤 ) )
52	51	ralrimiva	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑁 ( 𝐼 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑋 , 𝑌 ) ) ) 𝑤 ) = ( 𝐽 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑋 , 𝑌 ) ) ) 𝑤 ) )
53	1 11 12 3 4 16 8 9 10 52	mdetralt	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑋 , 𝑌 ) ) ) ) = 0 )

Metamath Proof Explorer

Theorem mdetralt2

Proof