HomeTheorem List (p. 299 of 426)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 299 of 426) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | orngogrp 29801 | An ordered ring is an ordered group. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| ⊢ (𝑅 ∈ oRing → 𝑅 ∈ oGrp) | ||
| Theorem | isofld 29802 | An ordered field is a field with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| ⊢ (𝐹 ∈ oField ↔ (𝐹 ∈ Field ∧ 𝐹 ∈ oRing)) | ||
| Theorem | orngmul 29803 | In an ordered ring, the ordering is compatible with the ring multiplication operation. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ≤ = (le‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ oRing ∧ (𝑋 ∈ 𝐵 ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ 𝐵 ∧ 0 ≤ 𝑌)) → 0 ≤ (𝑋 · 𝑌)) | ||
| Theorem | orngsqr 29804 | In an ordered ring, all squares are positive. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ≤ = (le‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵) → 0 ≤ (𝑋 · 𝑋)) | ||
| Theorem | ornglmulle 29805 | In an ordered ring, multiplication with a positive does not change comparison. (Contributed by Thierry Arnoux, 10-Apr-2018.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ oRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ ≤ = (le‘𝑅) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → 0 ≤ 𝑍) ⇒ ⊢ (𝜑 → (𝑍 · 𝑋) ≤ (𝑍 · 𝑌)) | ||
| Theorem | orngrmulle 29806 | In an ordered ring, multiplication with a positive does not change comparison. (Contributed by Thierry Arnoux, 10-Apr-2018.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ oRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ ≤ = (le‘𝑅) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) & ⊢ (𝜑 → 0 ≤ 𝑍) ⇒ ⊢ (𝜑 → (𝑋 · 𝑍) ≤ (𝑌 · 𝑍)) | ||
| Theorem | ornglmullt 29807 | In an ordered ring, multiplication with a positive does not change strict comparison. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ oRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ < = (lt‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 < 𝑌) & ⊢ (𝜑 → 0 < 𝑍) ⇒ ⊢ (𝜑 → (𝑍 · 𝑋) < (𝑍 · 𝑌)) | ||
| Theorem | orngrmullt 29808 | In an ordered ring, multiplication with a positive does not change strict comparison. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ oRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ < = (lt‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 < 𝑌) & ⊢ (𝜑 → 0 < 𝑍) ⇒ ⊢ (𝜑 → (𝑋 · 𝑍) < (𝑌 · 𝑍)) | ||
| Theorem | orngmullt 29809 | In an ordered ring, the strict ordering is compatible with the ring multiplication operation. (Contributed by Thierry Arnoux, 9-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ < = (lt‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ oRing) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 0 < 𝑋) & ⊢ (𝜑 → 0 < 𝑌) ⇒ ⊢ (𝜑 → 0 < (𝑋 · 𝑌)) | ||
| Theorem | ofldfld 29810 | An ordered field is a field. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
| ⊢ (𝐹 ∈ oField → 𝐹 ∈ Field) | ||
| Theorem | ofldtos 29811 | An ordered field is a totally ordered set. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
| ⊢ (𝐹 ∈ oField → 𝐹 ∈ Toset) | ||
| Theorem | orng0le1 29812 | In an ordered ring, the ring unit is positive. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
| ⊢ 0 = (0g‘𝐹) & ⊢ 1 = (1r‘𝐹) & ⊢ ≤ = (le‘𝐹) ⇒ ⊢ (𝐹 ∈ oRing → 0 ≤ 1 ) | ||
| Theorem | ofldlt1 29813 | In an ordered field, the ring unit is strictly positive. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
| ⊢ 0 = (0g‘𝐹) & ⊢ 1 = (1r‘𝐹) & ⊢ < = (lt‘𝐹) ⇒ ⊢ (𝐹 ∈ oField → 0 < 1 ) | ||
| Theorem | ofldchr 29814 | The characteristic of an ordered field is zero. (Contributed by Thierry Arnoux, 21-Jan-2018.) (Proof shortened by AV, 6-Oct-2020.) |
| ⊢ (𝐹 ∈ oField → (chr‘𝐹) = 0) | ||
| Theorem | suborng 29815 | Every subring of an ordered ring is also an ordered ring. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
| ⊢ ((𝑅 ∈ oRing ∧ (𝑅 ↾s 𝐴) ∈ Ring) → (𝑅 ↾s 𝐴) ∈ oRing) | ||
| Theorem | subofld 29816 | Every subfield of an ordered field is also an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
| ⊢ ((𝐹 ∈ oField ∧ (𝐹 ↾s 𝐴) ∈ Field) → (𝐹 ↾s 𝐴) ∈ oField) | ||
| Theorem | isarchiofld 29817* | Axiom of Archimedes : a characterization of the Archimedean property for ordered fields. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐻 = (ℤRHom‘𝑊) & ⊢ < = (lt‘𝑊) ⇒ ⊢ (𝑊 ∈ oField → (𝑊 ∈ Archi ↔ ∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛))) | ||
| Theorem | rhmdvdsr 29818 | A ring homomorphism preserves the divisibility relation. (Contributed by Thierry Arnoux, 22-Oct-2017.) |
| ⊢ 𝑋 = (Base‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ / = (∥r‘𝑆) ⇒ ⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ∥ 𝐵) → (𝐹‘𝐴) / (𝐹‘𝐵)) | ||
| Theorem | rhmopp 29819 | A ring homomorphism is also a ring homomorphism for the opposite rings. (Contributed by Thierry Arnoux, 27-Oct-2017.) |
| ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ ((oppr‘𝑅) RingHom (oppr‘𝑆))) | ||
| Theorem | elrhmunit 29820 | Ring homomorphisms preserve unit elements. (Contributed by Thierry Arnoux, 23-Oct-2017.) |
| ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (𝐹‘𝐴) ∈ (Unit‘𝑆)) | ||
| Theorem | rhmdvd 29821 | A ring homomorphism preserves ratios. (Contributed by Thierry Arnoux, 22-Oct-2017.) |
| ⊢ 𝑈 = (Unit‘𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ / = (/r‘𝑆) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) ∧ ((𝐹‘𝐵) ∈ 𝑈 ∧ (𝐹‘𝐶) ∈ 𝑈)) → ((𝐹‘𝐴) / (𝐹‘𝐵)) = ((𝐹‘(𝐴 · 𝐶)) / (𝐹‘(𝐵 · 𝐶)))) | ||
| Theorem | rhmunitinv 29822 | Ring homomorphisms preserve the inverse of unit elements. (Contributed by Thierry Arnoux, 23-Oct-2017.) |
| ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐴 ∈ (Unit‘𝑅)) → (𝐹‘((invr‘𝑅)‘𝐴)) = ((invr‘𝑆)‘(𝐹‘𝐴))) | ||
| Theorem | kerunit 29823 | If a unit element lies in the kernel of a ring homomorphism, then 0 = 1, i.e. the target ring is the zero ring. (Contributed by Thierry Arnoux, 24-Oct-2017.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 0 = (0g‘𝑆) & ⊢ 1 = (1r‘𝑆) ⇒ ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ (𝑈 ∩ (◡𝐹 “ { 0 })) ≠ ∅) → 1 = 0 ) | ||
| Syntax | cresv 29824 | Extend class notation with the scalar restriction operation. |
| class ↾v | ||
| Definition | df-resv 29825* | Define an operator to restrict the scalar field component of an extended structure. (Contributed by Thierry Arnoux, 5-Sep-2018.) |
| ⊢ ↾v = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘(Scalar‘𝑤)) ⊆ 𝑥, 𝑤, (𝑤 sSet ⟨(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)⟩))) | ||
| Theorem | reldmresv 29826 | The scalar restriction is a proper operator, so it can be used with ovprc1 6684. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ Rel dom ↾v | ||
| Theorem | resvval 29827 | Value of structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet ⟨(Scalar‘ndx), (𝐹 ↾s 𝐴)⟩))) | ||
| Theorem | resvid2 29828 | General behavior of trivial restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊) | ||
| Theorem | resvval2 29829 | Value of nontrivial structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet ⟨(Scalar‘ndx), (𝐹 ↾s 𝐴)⟩)) | ||
| Theorem | resvsca 29830 | Base set of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐹 ↾s 𝐴) = (Scalar‘𝑅)) | ||
| Theorem | resvlem 29831 | Other elements of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐶 = (𝐸‘𝑊) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 ≠ 5 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐶 = (𝐸‘𝑅)) | ||
| Theorem | resvbas 29832 | Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐵 = (Base‘𝐻)) | ||
| Theorem | resvplusg 29833 | +g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻)) | ||
| Theorem | resvvsca 29834 | ·𝑠 is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ · = ( ·𝑠 ‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘𝐻)) | ||
| Theorem | resvmulr 29835 | ·𝑠 is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ · = (.r‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝐻)) | ||
| Theorem | resv0g 29836 | 0g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 0 = (0g‘𝐻)) | ||
| Theorem | resv1r 29837 | 1r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ 1 = (1r‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 1 = (1r‘𝐻)) | ||
| Theorem | resvcmn 29838 | Scalar restriction preserves commutative monoids. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐺 ∈ CMnd ↔ 𝐻 ∈ CMnd)) | ||
| Theorem | gzcrng 29839 | The gaussian integers form a commutative ring. (Contributed by Thierry Arnoux, 18-Mar-2018.) |
| ⊢ (ℂfld ↾s ℤ[i]) ∈ CRing | ||
| Theorem | reofld 29840 | The real numbers form an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
| ⊢ ℝfld ∈ oField | ||
| Theorem | nn0omnd 29841 | The nonnegative integers form an ordered monoid. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| ⊢ (ℂfld ↾s ℕ0) ∈ oMnd | ||
| Theorem | rearchi 29842 | The field of the real numbers is Archimedean. See also arch 11289. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
| ⊢ ℝfld ∈ Archi | ||
| Theorem | nn0archi 29843 | The monoid of the nonnegative integers is Archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018.) |
| ⊢ (ℂfld ↾s ℕ0) ∈ Archi | ||
| Theorem | xrge0slmod 29844 | The extended nonnegative real numbers form a semiring left module. One could also have used subringAlg to get the same structure. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐺 = (ℝ*𝑠 ↾s (0[,]+∞)) & ⊢ 𝑊 = (𝐺 ↾v (0[,)+∞)) ⇒ ⊢ 𝑊 ∈ SLMod | ||
| Theorem | symgfcoeu 29845* | Uniqueness property of permutations. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝐺 = (Base‘(SymGrp‘𝐷)) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → ∃!𝑝 ∈ 𝐺 𝑄 = (𝑃 ∘ 𝑝)) | ||
| Theorem | psgndmfi 29846 | For a finite base set, the permutation sign is defined for all permutations. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝑆 = (pmSgn‘𝐷) & ⊢ 𝐺 = (Base‘(SymGrp‘𝐷)) ⇒ ⊢ (𝐷 ∈ Fin → 𝑆 Fn 𝐺) | ||
| Theorem | psgnid 29847 | Permutation sign of the identity. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
| ⊢ 𝑆 = (pmSgn‘𝐷) ⇒ ⊢ (𝐷 ∈ Fin → (𝑆‘( I ↾ 𝐷)) = 1) | ||
| Theorem | pmtrprfv2 29848 | In a transposition of two given points, each maps to the other. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑇‘{𝑋, 𝑌})‘𝑌) = 𝑋) | ||
| Theorem | pmtrto1cl 29849 | Useful lemma for the following theorems. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
| ⊢ 𝐷 = (1...𝑁) & ⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝑇‘{𝐾, (𝐾 + 1)}) ∈ ran 𝑇) | ||
| Theorem | psgnfzto1stlem 29850* | Lemma for psgnfzto1st 29855. Our permutation of rank (𝑛 + 1) can be written as a permutation of rank 𝑛 composed with a transposition. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
| ⊢ 𝐷 = (1...𝑁) ⇒ ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖))) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∘ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))))) | ||
| Theorem | fzto1stfv1 29851* | Value of our permutation 𝑃 at 1. (Contributed by Thierry Arnoux, 23-Aug-2020.) |
| ⊢ 𝐷 = (1...𝑁) & ⊢ 𝑃 = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) ⇒ ⊢ (𝐼 ∈ 𝐷 → (𝑃‘1) = 𝐼) | ||
| Theorem | fzto1st1 29852* | Special case where the permutation defined in psgnfzto1st 29855 is the identity. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
| ⊢ 𝐷 = (1...𝑁) & ⊢ 𝑃 = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) ⇒ ⊢ (𝐼 = 1 → 𝑃 = ( I ↾ 𝐷)) | ||
| Theorem | fzto1st 29853* | The function moving one element to the first position (and shifting all elements before it) is a permutation. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
| ⊢ 𝐷 = (1...𝑁) & ⊢ 𝑃 = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) & ⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐼 ∈ 𝐷 → 𝑃 ∈ 𝐵) | ||
| Theorem | fzto1stinvn 29854* | Value of the inverse of our permutation 𝑃 at 𝐼 (Contributed by Thierry Arnoux, 23-Aug-2020.) |
| ⊢ 𝐷 = (1...𝑁) & ⊢ 𝑃 = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) & ⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐼 ∈ 𝐷 → (◡𝑃‘𝐼) = 1) | ||
| Theorem | psgnfzto1st 29855* | The permutation sign for moving one element to the first position. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
| ⊢ 𝐷 = (1...𝑁) & ⊢ 𝑃 = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) & ⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑆 = (pmSgn‘𝐷) ⇒ ⊢ (𝐼 ∈ 𝐷 → (𝑆‘𝑃) = (-1↑(𝐼 + 1))) | ||
| Theorem | pmtridf1o 29856 | Transpositions of 𝑋 and 𝑌 (understood to be the identity when 𝑋 = 𝑌), are bijections. (Contributed by Thierry Arnoux, 1-Jan-2022.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ 𝑇 = if(𝑋 = 𝑌, ( I ↾ 𝐴), ((pmTrsp‘𝐴)‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → 𝑇:𝐴–1-1-onto→𝐴) | ||
| Theorem | pmtridfv1 29857 | Value at X of the transposition of 𝑋 and 𝑌 (understood to be the identity when X = Y ). (Contributed by Thierry Arnoux, 3-Jan-2022.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ 𝑇 = if(𝑋 = 𝑌, ( I ↾ 𝐴), ((pmTrsp‘𝐴)‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → (𝑇‘𝑋) = 𝑌) | ||
| Theorem | pmtridfv2 29858 | Value at Y of the transposition of 𝑋 and 𝑌 (understood to be the identity when X = Y ). (Contributed by Thierry Arnoux, 3-Jan-2022.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ 𝑇 = if(𝑋 = 𝑌, ( I ↾ 𝐴), ((pmTrsp‘𝐴)‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → (𝑇‘𝑌) = 𝑋) | ||
| Syntax | csmat 29859 | Syntax for a function generating submatrixes. |
| class subMat1 | ||
| Definition | df-smat 29860* | Define a function generating submatrices of an integer-indexed matrix. The function maps an index in ((1...𝑀) × (1...𝑁)) into a new index in ((1...(𝑀 − 1)) × (1...(𝑁 − 1))). A submatrix is obtained by deleting a row and a column of the original matrix. Because this function re-indexes the matrix, the resulting submatrix still has the same index set for rows and columns, and its determinent is defined, unlike the current df-subma 20383. (Contributed by Thierry Arnoux, 18-Aug-2020.) |
| ⊢ subMat1 = (𝑚 ∈ V ↦ (𝑘 ∈ ℕ, 𝑙 ∈ ℕ ↦ (𝑚 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩)))) | ||
| Theorem | smatfval 29861* | Value of the submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ ((𝐾 ∈ ℕ ∧ 𝐿 ∈ ℕ ∧ 𝑀 ∈ 𝑉) → (𝐾(subMat1‘𝑀)𝐿) = (𝑀 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩))) | ||
| Theorem | smatrcl 29862 | Closure of the rectangular submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑𝑚 ((1...𝑀) × (1...𝑁)))) ⇒ ⊢ (𝜑 → 𝑆 ∈ (𝐵 ↑𝑚 ((1...(𝑀 − 1)) × (1...(𝑁 − 1))))) | ||
| Theorem | smatlem 29863 | Lemma for the next theorems. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑𝑚 ((1...𝑀) × (1...𝑁)))) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐽 ∈ ℕ) & ⊢ (𝜑 → if(𝐼 < 𝐾, 𝐼, (𝐼 + 1)) = 𝑋) & ⊢ (𝜑 → if(𝐽 < 𝐿, 𝐽, (𝐽 + 1)) = 𝑌) ⇒ ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝑋𝐴𝑌)) | ||
| Theorem | smattl 29864 | Entries of a submatrix, top left. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑𝑚 ((1...𝑀) × (1...𝑁)))) & ⊢ (𝜑 → 𝐼 ∈ (1..^𝐾)) & ⊢ (𝜑 → 𝐽 ∈ (1..^𝐿)) ⇒ ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝐼𝐴𝐽)) | ||
| Theorem | smattr 29865 | Entries of a submatrix, top right. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑𝑚 ((1...𝑀) × (1...𝑁)))) & ⊢ (𝜑 → 𝐼 ∈ (𝐾...𝑀)) & ⊢ (𝜑 → 𝐽 ∈ (1..^𝐿)) ⇒ ⊢ (𝜑 → (𝐼𝑆𝐽) = ((𝐼 + 1)𝐴𝐽)) | ||
| Theorem | smatbl 29866 | Entries of a submatrix, bottom left. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑𝑚 ((1...𝑀) × (1...𝑁)))) & ⊢ (𝜑 → 𝐼 ∈ (1..^𝐾)) & ⊢ (𝜑 → 𝐽 ∈ (𝐿...𝑁)) ⇒ ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝐼𝐴(𝐽 + 1))) | ||
| Theorem | smatbr 29867 | Entries of a submatrix, bottom right. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑𝑚 ((1...𝑀) × (1...𝑁)))) & ⊢ (𝜑 → 𝐼 ∈ (𝐾...𝑀)) & ⊢ (𝜑 → 𝐽 ∈ (𝐿...𝑁)) ⇒ ⊢ (𝜑 → (𝐼𝑆𝐽) = ((𝐼 + 1)𝐴(𝐽 + 1))) | ||
| Theorem | smatcl 29868 | Closure of the square submatrix: if 𝑀 is a square matrix of dimension 𝑁 with indexes in (1...𝑁), then a submatrix of 𝑀 is of dimension (𝑁 − 1). (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐶 = (Base‘((1...(𝑁 − 1)) Mat 𝑅)) & ⊢ 𝑆 = (𝐾(subMat1‘𝑀)𝐿) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑆 ∈ 𝐶) | ||
| Theorem | matmpt2 29869* | Write a square matrix as a mapping operation. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ (𝑀 ∈ 𝐵 → 𝑀 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖𝑀𝑗))) | ||
| Theorem | 1smat1 29870 | The submatrix of the identity matrix obtained by removing the ith row and the ith column is an identity matrix. Cf. 1marepvsma1 20389. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ 1 = (1r‘((1...𝑁) Mat 𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) ⇒ ⊢ (𝜑 → (𝐼(subMat1‘ 1 )𝐼) = (1r‘((1...(𝑁 − 1)) Mat 𝑅))) | ||
| Theorem | submat1n 29871 | One case where the submatrix with integer indices, subMat1, and the general submatrix subMat, agree. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) → (𝑁(subMat1‘𝑀)𝑁) = (𝑁(((1...𝑁) subMat 𝑅)‘𝑀)𝑁)) | ||
| Theorem | submatres 29872 | Special case where the submatrix is a restriction of the initial matrix, and no renumbering occurs. (Contributed by Thierry Arnoux, 26-Aug-2020.) |
| ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) → (𝑁(subMat1‘𝑀)𝑁) = (𝑀 ↾ ((1...(𝑁 − 1)) × (1...(𝑁 − 1))))) | ||
| Theorem | submateqlem1 29873 | Lemma for submateq 29875. (Contributed by Thierry Arnoux, 25-Aug-2020.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1))) & ⊢ (𝜑 → 𝐾 ≤ 𝑀) ⇒ ⊢ (𝜑 → (𝑀 ∈ (𝐾...𝑁) ∧ (𝑀 + 1) ∈ ((1...𝑁) ∖ {𝐾}))) | ||
| Theorem | submateqlem2 29874 | Lemma for submateq 29875. (Contributed by Thierry Arnoux, 26-Aug-2020.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1))) & ⊢ (𝜑 → 𝑀 < 𝐾) ⇒ ⊢ (𝜑 → (𝑀 ∈ (1..^𝐾) ∧ 𝑀 ∈ ((1...𝑁) ∖ {𝐾}))) | ||
| Theorem | submateq 29875* | Sufficient condition for two submatrices to be equal. (Contributed by Thierry Arnoux, 25-Aug-2020.) |
| ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐸 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝐽})) → (𝑖𝐸𝑗) = (𝑖𝐹𝑗)) ⇒ ⊢ (𝜑 → (𝐼(subMat1‘𝐸)𝐽) = (𝐼(subMat1‘𝐹)𝐽)) | ||
| Theorem | submatminr1 29876 | If we take a submatrix by removing the row 𝐼 and column 𝐽, then the result is the same on the matrix with row 𝐼 and column 𝐽 modified by the minMatR1 operator. (Contributed by Thierry Arnoux, 25-Aug-2020.) |
| ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ 𝐸 = (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) ⇒ ⊢ (𝜑 → (𝐼(subMat1‘𝑀)𝐽) = (𝐼(subMat1‘𝐸)𝐽)) | ||
| Syntax | clmat 29877 | Extend class notation with the literal matrix conversion function. |
| class litMat | ||
| Definition | df-lmat 29878* | Define a function converting words of words into matrices. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
| ⊢ litMat = (𝑚 ∈ V ↦ (𝑖 ∈ (1...(#‘𝑚)), 𝑗 ∈ (1...(#‘(𝑚‘0))) ↦ ((𝑚‘(𝑖 − 1))‘(𝑗 − 1)))) | ||
| Theorem | lmatval 29879* | Value of the literal matrix conversion function. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
| ⊢ (𝑀 ∈ 𝑉 → (litMat‘𝑀) = (𝑖 ∈ (1...(#‘𝑀)), 𝑗 ∈ (1...(#‘(𝑀‘0))) ↦ ((𝑀‘(𝑖 − 1))‘(𝑗 − 1)))) | ||
| Theorem | lmatfval 29880* | Entries of a literal matrix. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
| ⊢ 𝑀 = (litMat‘𝑊) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑊 ∈ Word Word 𝑉) & ⊢ (𝜑 → (#‘𝑊) = 𝑁) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (#‘(𝑊‘𝑖)) = 𝑁) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) ⇒ ⊢ (𝜑 → (𝐼𝑀𝐽) = ((𝑊‘(𝐼 − 1))‘(𝐽 − 1))) | ||
| Theorem | lmatfvlem 29881* | Useful lemma to extract literal matrix entries. Suggested by Mario Carneiro. (Contributed by Thierry Arnoux, 3-Sep-2020.) |
| ⊢ 𝑀 = (litMat‘𝑊) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑊 ∈ Word Word 𝑉) & ⊢ (𝜑 → (#‘𝑊) = 𝑁) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (#‘(𝑊‘𝑖)) = 𝑁) & ⊢ 𝐾 ∈ ℕ0 & ⊢ 𝐿 ∈ ℕ0 & ⊢ 𝐼 ≤ 𝑁 & ⊢ 𝐽 ≤ 𝑁 & ⊢ (𝐾 + 1) = 𝐼 & ⊢ (𝐿 + 1) = 𝐽 & ⊢ (𝑊‘𝐾) = 𝑋 & ⊢ (𝜑 → (𝑋‘𝐿) = 𝑌) ⇒ ⊢ (𝜑 → (𝐼𝑀𝐽) = 𝑌) | ||
| Theorem | lmatcl 29882* | Closure of the literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
| ⊢ 𝑀 = (litMat‘𝑊) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑊 ∈ Word Word 𝑉) & ⊢ (𝜑 → (#‘𝑊) = 𝑁) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (#‘(𝑊‘𝑖)) = 𝑁) & ⊢ 𝑉 = (Base‘𝑅) & ⊢ 𝑂 = ((1...𝑁) Mat 𝑅) & ⊢ 𝑃 = (Base‘𝑂) & ⊢ (𝜑 → 𝑅 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝑀 ∈ 𝑃) | ||
| Theorem | lmat22lem 29883* | Lemma for lmat22e11 29884 and co. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
| ⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^2)) → (#‘(⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩‘𝑖)) = 2) | ||
| Theorem | lmat22e11 29884 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
| ⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (1𝑀1) = 𝐴) | ||
| Theorem | lmat22e12 29885 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
| ⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (1𝑀2) = 𝐵) | ||
| Theorem | lmat22e21 29886 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
| ⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (2𝑀1) = 𝐶) | ||
| Theorem | lmat22e22 29887 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
| ⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (2𝑀2) = 𝐷) | ||
| Theorem | lmat22det 29888 | The determinant of a literal 2x2 complex matrix. (Contributed by Thierry Arnoux, 1-Sep-2020.) |
| ⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ · = (.r‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ 𝑉 = (Base‘𝑅) & ⊢ 𝐽 = ((1...2) maDet 𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (𝐽‘𝑀) = ((𝐴 · 𝐷) − (𝐶 · 𝐵))) | ||
| Theorem | mdetpmtr1 29889* | The determinant of a matrix with permuted rows is the determinant of the original matrix multiplied by the sign of the permutation. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐺 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀𝑗)) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝐷‘𝐸))) | ||
| Theorem | mdetpmtr2 29890* | The determinant of a matrix with permuted columns is the determinant of the original matrix multiplied by the sign of the permutation. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐺 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖𝑀(𝑃‘𝑗))) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝐷‘𝐸))) | ||
| Theorem | mdetpmtr12 29891* | The determinant of a matrix with permuted rows and columns is the determinant of the original matrix multiplied by the product of the signs of the permutations. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐺 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀(𝑄‘𝑗))) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ (𝜑 → 𝑃 ∈ 𝐺) & ⊢ (𝜑 → 𝑄 ∈ 𝐺) ⇒ ⊢ (𝜑 → (𝐷‘𝑀) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐷‘𝐸))) | ||
| Theorem | mdetlap1 29892* | A Laplace expansion of the determinant of a matrix, using the adjunct (cofactor) matrix. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐾 = (𝑁 maAdju 𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁) → (𝐷‘𝑀) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝐼𝑀𝑗) · (𝑗(𝐾‘𝑀)𝐼))))) | ||
| Theorem | madjusmdetlem1 29893* | Lemma for madjusmdet 29897. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐷 = ((1...𝑁) maDet 𝑅) & ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ 𝐺 = (Base‘(SymGrp‘(1...𝑁))) & ⊢ 𝑆 = (pmSgn‘(1...𝑁)) & ⊢ 𝑈 = (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) & ⊢ 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)𝑈(𝑄‘𝑗))) & ⊢ (𝜑 → 𝑃 ∈ 𝐺) & ⊢ (𝜑 → 𝑄 ∈ 𝐺) & ⊢ (𝜑 → (𝑃‘𝑁) = 𝐼) & ⊢ (𝜑 → (𝑄‘𝑁) = 𝐽) & ⊢ (𝜑 → (𝐼(subMat1‘𝑈)𝐽) = (𝑁(subMat1‘𝑊)𝑁)) ⇒ ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽)))) | ||
| Theorem | madjusmdetlem2 29894* | Lemma for madjusmdet 29897. (Contributed by Thierry Arnoux, 26-Aug-2020.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐷 = ((1...𝑁) maDet 𝑅) & ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ 𝑃 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) & ⊢ 𝑆 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝑁, if(𝑖 ≤ 𝑁, (𝑖 − 1), 𝑖))) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)) = ((𝑃 ∘ ◡𝑆)‘𝑋)) | ||
| Theorem | madjusmdetlem3 29895* | Lemma for madjusmdet 29897. (Contributed by Thierry Arnoux, 27-Aug-2020.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐷 = ((1...𝑁) maDet 𝑅) & ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ 𝑃 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) & ⊢ 𝑆 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝑁, if(𝑖 ≤ 𝑁, (𝑖 − 1), 𝑖))) & ⊢ 𝑄 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝐽, if(𝑗 ≤ 𝐽, (𝑗 − 1), 𝑗))) & ⊢ 𝑇 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝑁, if(𝑗 ≤ 𝑁, (𝑗 − 1), 𝑗))) & ⊢ 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ (((𝑃 ∘ ◡𝑆)‘𝑖)𝑈((𝑄 ∘ ◡𝑇)‘𝑗))) & ⊢ (𝜑 → 𝑈 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼(subMat1‘𝑈)𝐽) = (𝑁(subMat1‘𝑊)𝑁)) | ||
| Theorem | madjusmdetlem4 29896* | Lemma for madjusmdet 29897. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐷 = ((1...𝑁) maDet 𝑅) & ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ 𝑃 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) & ⊢ 𝑆 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝑁, if(𝑖 ≤ 𝑁, (𝑖 − 1), 𝑖))) & ⊢ 𝑄 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝐽, if(𝑗 ≤ 𝐽, (𝑗 − 1), 𝑗))) & ⊢ 𝑇 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝑁, if(𝑗 ≤ 𝑁, (𝑗 − 1), 𝑗))) ⇒ ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘(-1↑(𝐼 + 𝐽))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽)))) | ||
| Theorem | madjusmdet 29897 | Express the cofactor of the matrix, i.e. the entries of its adjunct matrix, using determinant of submatrixes. (Contributed by Thierry Arnoux, 23-Aug-2020.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐷 = ((1...𝑁) maDet 𝑅) & ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘(-1↑(𝐼 + 𝐽))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽)))) | ||
| Theorem | mdetlap 29898* | Laplace expansion of the determinant of a square matrix. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐷 = ((1...𝑁) maDet 𝑅) & ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐷‘𝑀) = (𝑅 Σg (𝑗 ∈ (1...𝑁) ↦ ((𝑍‘(-1↑(𝐼 + 𝑗))) · ((𝐼𝑀𝑗) · (𝐸‘(𝐼(subMat1‘𝑀)𝑗))))))) | ||
| Theorem | fvproj 29899* | Value of a function on pairs, given two projections 𝐹 and 𝐺. (Contributed by Thierry Arnoux, 30-Dec-2019.) |
| ⊢ 𝐻 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐻‘⟨𝑋, 𝑌⟩) = ⟨(𝐹‘𝑋), (𝐺‘𝑌)⟩) | ||
| Theorem | fimaproj 29900* | Image of a cartesian product for a function on pairs, given two projections 𝐹 and 𝐺. (Contributed by Thierry Arnoux, 30-Dec-2019.) |
| ⊢ 𝐻 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝑋 ⊆ 𝐴) & ⊢ (𝜑 → 𝑌 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐻 “ (𝑋 × 𝑌)) = ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |