This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
mdetero.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
mdetero.p ⊢ + = ( +g ‘ 𝑅 )
mdetero.t ⊢ · = ( .r ‘ 𝑅 )
mdetero.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
mdetero.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
mdetero.x ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑁 ) → 𝑋 ∈ 𝐾 )
mdetero.y ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑁 ) → 𝑌 ∈ 𝐾 )
mdetero.z ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑍 ∈ 𝐾 )
mdetero.w ⊢ ( 𝜑 → 𝑊 ∈ 𝐾 )
mdetero.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
mdetero.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑁 )
mdetero.ij ⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
Assertion mdetero ( 𝜑 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + ( 𝑊 · 𝑌 ) ) , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) = ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mdetero.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
2 mdetero.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
3 mdetero.p ⊢ + = ( +g ‘ 𝑅 )
4 mdetero.t ⊢ · = ( .r ‘ 𝑅 )
5 mdetero.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
6 mdetero.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
7 mdetero.x ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑁 ) → 𝑋 ∈ 𝐾 )
8 mdetero.y ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑁 ) → 𝑌 ∈ 𝐾 )
9 mdetero.z ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑍 ∈ 𝐾 )
10 mdetero.w ⊢ ( 𝜑 → 𝑊 ∈ 𝐾 )
11 mdetero.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
12 mdetero.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑁 )
13 mdetero.ij ⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
14 7 3adant2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑋 ∈ 𝐾 )
15 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
16 5 15 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
17 16 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
18 10 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑊 ∈ 𝐾 )
19 8 3adant2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑌 ∈ 𝐾 )
20 2 4 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑊 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) → ( 𝑊 · 𝑌 ) ∈ 𝐾 )
21 17 18 19 20 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑊 · 𝑌 ) ∈ 𝐾 )
22 19 9 ifcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ∈ 𝐾 )
23 1 2 3 5 6 14 21 22 11 mdetrlin2 ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + ( 𝑊 · 𝑌 ) ) , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) = ( ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) + ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑊 · 𝑌 ) , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) ) )
24 1 2 4 5 6 19 22 10 11 mdetrsca2 ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑊 · 𝑌 ) , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) = ( 𝑊 · ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) ) )
25 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
26 1 2 25 5 6 8 9 11 12 13 mdetralt2 ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) = ( 0g ‘ 𝑅 ) )
27 26 oveq2d ⊢ ( 𝜑 → ( 𝑊 · ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) ) = ( 𝑊 · ( 0g ‘ 𝑅 ) ) )
28 2 4 25 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑊 ∈ 𝐾 ) → ( 𝑊 · ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
29 16 10 28 syl2anc ⊢ ( 𝜑 → ( 𝑊 · ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
30 24 27 29 3eqtrd ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑊 · 𝑌 ) , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) = ( 0g ‘ 𝑅 ) )
31 30 oveq2d ⊢ ( 𝜑 → ( ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) + ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑊 · 𝑌 ) , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) ) = ( ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) + ( 0g ‘ 𝑅 ) ) )
32 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
33 16 32 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
34 eqid ⊢ ( 𝑁 Mat 𝑅 ) = ( 𝑁 Mat 𝑅 )
35 eqid ⊢ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
36 1 34 35 2 mdetf ⊢ ( 𝑅 ∈ CRing → 𝐷 : ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ⟶ 𝐾 )
37 5 36 syl ⊢ ( 𝜑 → 𝐷 : ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ⟶ 𝐾 )
38 14 22 ifcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ∈ 𝐾 )
39 34 2 35 6 5 38 matbas2d ⊢ ( 𝜑 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
40 37 39 ffvelcdmd ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) ∈ 𝐾 )
41 2 3 25 grprid ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) ∈ 𝐾 ) → ( ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) + ( 0g ‘ 𝑅 ) ) = ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) )
42 33 40 41 syl2anc ⊢ ( 𝜑 → ( ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) + ( 0g ‘ 𝑅 ) ) = ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) )
43 23 31 42 3eqtrd ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + ( 𝑊 · 𝑌 ) ) , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) = ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , if ( 𝑖 = 𝐽 , 𝑌 , 𝑍 ) ) ) ) )