Description: According to the definition in Weierstrass p. 272, the determinant function is the unique multilinear, alternating and normalized function from the algebra of square matrices of the same dimension over a commutative ring to this ring. So for any multilinear (mdetuni.li and mdetuni.sc), alternating (mdetuni.al) and normalized (mdetuni.no) function D (mdetuni.ff) from the algebra of square matrices (mdetuni.a) to their underlying commutative ring (mdetuni.cr), the function value of this function D for a matrix F (mdetuni.f) is the determinant of this matrix. (Contributed by Stefan O'Rear, 15-Jul-2018) (Revised by Alexander van der Vekens, 8-Feb-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | mdetuni.a | ⊢ 𝐴 = ( 𝑁 Mat 𝑅 ) | |
| mdetuni.b | ⊢ 𝐵 = ( Base ‘ 𝐴 ) | ||
| mdetuni.k | ⊢ 𝐾 = ( Base ‘ 𝑅 ) | ||
| mdetuni.0g | ⊢ 0 = ( 0g ‘ 𝑅 ) | ||
| mdetuni.1r | ⊢ 1 = ( 1r ‘ 𝑅 ) | ||
| mdetuni.pg | ⊢ + = ( +g ‘ 𝑅 ) | ||
| mdetuni.tg | ⊢ · = ( .r ‘ 𝑅 ) | ||
| mdetuni.n | ⊢ ( 𝜑 → 𝑁 ∈ Fin ) | ||
| mdetuni.r | ⊢ ( 𝜑 → 𝑅 ∈ Ring ) | ||
| mdetuni.ff | ⊢ ( 𝜑 → 𝐷 : 𝐵 ⟶ 𝐾 ) | ||
| mdetuni.al | ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑁 ∀ 𝑧 ∈ 𝑁 ( ( 𝑦 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝑦 𝑥 𝑤 ) = ( 𝑧 𝑥 𝑤 ) ) → ( 𝐷 ‘ 𝑥 ) = 0 ) ) | ||
| mdetuni.li | ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( ( 𝐷 ‘ 𝑦 ) + ( 𝐷 ‘ 𝑧 ) ) ) ) | ||
| mdetuni.sc | ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ) ) | ||
| mdetuni.e | ⊢ 𝐸 = ( 𝑁 maDet 𝑅 ) | ||
| mdetuni.cr | ⊢ ( 𝜑 → 𝑅 ∈ CRing ) | ||
| mdetuni.f | ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 ) | ||
| mdetuni.no | ⊢ ( 𝜑 → ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) = 1 ) | ||
| Assertion | mdetuni | ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) = ( 𝐸 ‘ 𝐹 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mdetuni.a | ⊢ 𝐴 = ( 𝑁 Mat 𝑅 ) | |
| 2 | mdetuni.b | ⊢ 𝐵 = ( Base ‘ 𝐴 ) | |
| 3 | mdetuni.k | ⊢ 𝐾 = ( Base ‘ 𝑅 ) | |
| 4 | mdetuni.0g | ⊢ 0 = ( 0g ‘ 𝑅 ) | |
| 5 | mdetuni.1r | ⊢ 1 = ( 1r ‘ 𝑅 ) | |
| 6 | mdetuni.pg | ⊢ + = ( +g ‘ 𝑅 ) | |
| 7 | mdetuni.tg | ⊢ · = ( .r ‘ 𝑅 ) | |
| 8 | mdetuni.n | ⊢ ( 𝜑 → 𝑁 ∈ Fin ) | |
| 9 | mdetuni.r | ⊢ ( 𝜑 → 𝑅 ∈ Ring ) | |
| 10 | mdetuni.ff | ⊢ ( 𝜑 → 𝐷 : 𝐵 ⟶ 𝐾 ) | |
| 11 | mdetuni.al | ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑁 ∀ 𝑧 ∈ 𝑁 ( ( 𝑦 ≠ 𝑧 ∧ ∀ 𝑤 ∈ 𝑁 ( 𝑦 𝑥 𝑤 ) = ( 𝑧 𝑥 𝑤 ) ) → ( 𝐷 ‘ 𝑥 ) = 0 ) ) | |
| 12 | mdetuni.li | ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( 𝑦 ↾ ( { 𝑤 } × 𝑁 ) ) ∘f + ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑦 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( ( 𝐷 ‘ 𝑦 ) + ( 𝐷 ‘ 𝑧 ) ) ) ) | |
| 13 | mdetuni.sc | ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝑁 ( ( ( 𝑥 ↾ ( { 𝑤 } × 𝑁 ) ) = ( ( ( { 𝑤 } × 𝑁 ) × { 𝑦 } ) ∘f · ( 𝑧 ↾ ( { 𝑤 } × 𝑁 ) ) ) ∧ ( 𝑥 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) = ( 𝑧 ↾ ( ( 𝑁 ∖ { 𝑤 } ) × 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) = ( 𝑦 · ( 𝐷 ‘ 𝑧 ) ) ) ) | |
| 14 | mdetuni.e | ⊢ 𝐸 = ( 𝑁 maDet 𝑅 ) | |
| 15 | mdetuni.cr | ⊢ ( 𝜑 → 𝑅 ∈ CRing ) | |
| 16 | mdetuni.f | ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 ) | |
| 17 | mdetuni.no | ⊢ ( 𝜑 → ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) = 1 ) | |
| 18 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 | mdetuni0 | ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) = ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝐹 ) ) ) |
| 19 | 17 | oveq1d | ⊢ ( 𝜑 → ( ( 𝐷 ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐸 ‘ 𝐹 ) ) = ( 1 · ( 𝐸 ‘ 𝐹 ) ) ) |
| 20 | 14 1 2 3 | mdetcl | ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ) → ( 𝐸 ‘ 𝐹 ) ∈ 𝐾 ) |
| 21 | 15 16 20 | syl2anc | ⊢ ( 𝜑 → ( 𝐸 ‘ 𝐹 ) ∈ 𝐾 ) |
| 22 | 3 7 5 | ringlidm | ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐸 ‘ 𝐹 ) ∈ 𝐾 ) → ( 1 · ( 𝐸 ‘ 𝐹 ) ) = ( 𝐸 ‘ 𝐹 ) ) |
| 23 | 9 21 22 | syl2anc | ⊢ ( 𝜑 → ( 1 · ( 𝐸 ‘ 𝐹 ) ) = ( 𝐸 ‘ 𝐹 ) ) |
| 24 | 18 19 23 | 3eqtrd | ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) = ( 𝐸 ‘ 𝐹 ) ) |