Metamath Proof Explorer

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 ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
mdetralt2.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
mdetralt2.z ⊢ 0 = ( 0g ‘ 𝑅 )
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 = ( 0g ‘ 𝑅 )
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 )