Home | Metamath
Proof Explorer Theorem List (p. 310 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dimval 30901 | The dimension of a vector space 𝐹 is the cardinality of one of its bases. (Contributed by Thierry Arnoux, 6-May-2023.) |
⊢ 𝐽 = (LBasis‘𝐹) ⇒ ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) → (dim‘𝐹) = (♯‘𝑆)) | ||
Theorem | dimvalfi 30902 | The dimension of a vector space 𝐹 is the cardinality of one of its bases. This version of dimval 30901 does not depend on the axiom of choice, but it is limited to the case where the base 𝑆 is finite. (Contributed by Thierry Arnoux, 24-May-2023.) |
⊢ 𝐽 = (LBasis‘𝐹) ⇒ ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) → (dim‘𝐹) = (♯‘𝑆)) | ||
Theorem | dimcl 30903 | Closure of the vector space dimension. (Contributed by Thierry Arnoux, 18-May-2023.) |
⊢ (𝑉 ∈ LVec → (dim‘𝑉) ∈ ℕ0*) | ||
Theorem | lvecdim0i 30904 | A vector space of dimension zero is reduced to its identity element. (Contributed by Thierry Arnoux, 31-Jul-2023.) |
⊢ 0 = (0g‘𝑉) ⇒ ⊢ ((𝑉 ∈ LVec ∧ (dim‘𝑉) = 0) → (Base‘𝑉) = { 0 }) | ||
Theorem | lvecdim0 30905 | A vector space of dimension zero is reduced to its identity element, biconditional version. (Contributed by Thierry Arnoux, 31-Jul-2023.) |
⊢ 0 = (0g‘𝑉) ⇒ ⊢ (𝑉 ∈ LVec → ((dim‘𝑉) = 0 ↔ (Base‘𝑉) = { 0 })) | ||
Theorem | lssdimle 30906 | The dimension of a linear subspace is less than or equal to the dimension of the parent vector space. This is corollary 5.4 of [Lang] p. 141 (Contributed by Thierry Arnoux, 20-May-2023.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝑈 ∈ (LSubSp‘𝑊)) → (dim‘𝑋) ≤ (dim‘𝑊)) | ||
Theorem | dimpropd 30907* | If two structures have the same components (properties), they have the same dimension. (Contributed by Thierry Arnoux, 18-May-2023.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → 𝐵 ⊆ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦)) & ⊢ 𝐹 = (Scalar‘𝐾) & ⊢ 𝐺 = (Scalar‘𝐿) & ⊢ (𝜑 → 𝑃 = (Base‘𝐹)) & ⊢ (𝜑 → 𝑃 = (Base‘𝐺)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑥(+g‘𝐹)𝑦) = (𝑥(+g‘𝐺)𝑦)) & ⊢ (𝜑 → 𝐾 ∈ LVec) & ⊢ (𝜑 → 𝐿 ∈ LVec) ⇒ ⊢ (𝜑 → (dim‘𝐾) = (dim‘𝐿)) | ||
Theorem | rgmoddim 30908 | The left vector space induced by a ring over itself has dimension 1. (Contributed by Thierry Arnoux, 5-Aug-2023.) |
⊢ 𝑉 = (ringLMod‘𝐹) ⇒ ⊢ (𝐹 ∈ Field → (dim‘𝑉) = 1) | ||
Theorem | frlmdim 30909 | Dimension of a free left module. (Contributed by Thierry Arnoux, 20-May-2023.) |
⊢ 𝐹 = (𝑅 freeLMod 𝐼) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉) → (dim‘𝐹) = (♯‘𝐼)) | ||
Theorem | tnglvec 30910 | Augmenting a structure with a norm conserves left vector spaces. (Contributed by Thierry Arnoux, 20-May-2023.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝐺 ∈ LVec ↔ 𝑇 ∈ LVec)) | ||
Theorem | tngdim 30911 | Dimension of a left vector space augmented with a norm. (Contributed by Thierry Arnoux, 20-May-2023.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) ⇒ ⊢ ((𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉) → (dim‘𝐺) = (dim‘𝑇)) | ||
Theorem | rrxdim 30912 | Dimension of the generalized Euclidean space. (Contributed by Thierry Arnoux, 20-May-2023.) |
⊢ 𝐻 = (ℝ^‘𝐼) ⇒ ⊢ (𝐼 ∈ 𝑉 → (dim‘𝐻) = (♯‘𝐼)) | ||
Theorem | matdim 30913 | Dimension of the space of square matrices. (Contributed by Thierry Arnoux, 20-May-2023.) |
⊢ 𝐴 = (𝐼 Mat 𝑅) & ⊢ 𝑁 = (♯‘𝐼) ⇒ ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → (dim‘𝐴) = (𝑁 · 𝑁)) | ||
Theorem | lbslsat 30914 | A nonzero vector 𝑋 is a basis of a line spanned by the singleton 𝑋. Spans of nonzero singletons are sometimes called "atoms", see df-lsatoms 35994 and for example lsatlspsn 36011. (Contributed by Thierry Arnoux, 20-May-2023.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑌 = (𝑊 ↾s (𝑁‘{𝑋})) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → {𝑋} ∈ (LBasis‘𝑌)) | ||
Theorem | lsatdim 30915 | A line, spanned by a nonzero singleton, has dimension 1. (Contributed by Thierry Arnoux, 20-May-2023.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑌 = (𝑊 ↾s (𝑁‘{𝑋})) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (dim‘𝑌) = 1) | ||
Theorem | drngdimgt0 30916 | The dimension of a vector space that is also a division ring is greater than zero. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ ((𝐹 ∈ LVec ∧ 𝐹 ∈ DivRing) → 0 < (dim‘𝐹)) | ||
Theorem | lmhmlvec2 30917 | A homomorphism of left vector spaces has a left vector space as codomain. (Contributed by Thierry Arnoux, 7-May-2023.) |
⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝑈 ∈ LVec) | ||
Theorem | kerlmhm 30918 | The kernel of a vector space homomorphism is a vector space itself. (Contributed by Thierry Arnoux, 7-May-2023.) |
⊢ 0 = (0g‘𝑈) & ⊢ 𝐾 = (𝑉 ↾s (◡𝐹 “ { 0 })) ⇒ ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝐾 ∈ LVec) | ||
Theorem | imlmhm 30919 | The image of a vector space homomorphism is a vector space itself. (Contributed by Thierry Arnoux, 7-May-2023.) |
⊢ 𝐼 = (𝑈 ↾s ran 𝐹) ⇒ ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝐼 ∈ LVec) | ||
Theorem | lindsunlem 30920 | Lemma for lindsun 30921. (Contributed by Thierry Arnoux, 9-May-2023.) |
⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ (LIndS‘𝑊)) & ⊢ (𝜑 → 𝑉 ∈ (LIndS‘𝑊)) & ⊢ (𝜑 → ((𝑁‘𝑈) ∩ (𝑁‘𝑉)) = { 0 }) & ⊢ 𝑂 = (0g‘(Scalar‘𝑊)) & ⊢ 𝐹 = (Base‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐾 ∈ (𝐹 ∖ {𝑂})) & ⊢ (𝜑 → (𝐾( ·𝑠 ‘𝑊)𝐶) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝐶}))) ⇒ ⊢ (𝜑 → ⊥) | ||
Theorem | lindsun 30921 | Condition for the union of two independent sets to be an independent set. (Contributed by Thierry Arnoux, 9-May-2023.) |
⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ (LIndS‘𝑊)) & ⊢ (𝜑 → 𝑉 ∈ (LIndS‘𝑊)) & ⊢ (𝜑 → ((𝑁‘𝑈) ∩ (𝑁‘𝑉)) = { 0 }) ⇒ ⊢ (𝜑 → (𝑈 ∪ 𝑉) ∈ (LIndS‘𝑊)) | ||
Theorem | lbsdiflsp0 30922 | The linear spans of two disjunct independent sets only have a trivial intersection. This can be seen as the opposite direction of lindsun 30921. (Contributed by Thierry Arnoux, 17-May-2023.) |
⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ∧ 𝑉 ⊆ 𝐵) → ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉)) = { 0 }) | ||
Theorem | dimkerim 30923 | Given a linear map 𝐹 between vector spaces 𝑉 and 𝑈, the dimension of the vector space 𝑉 is the sum of the dimension of 𝐹 's kernel and the dimension of 𝐹's image. Second part of theorem 5.3 in [Lang] p. 141 This can also be described as the Rank-nullity theorem, (dim‘𝐼) being the rank of 𝐹 (the dimension of its image), and (dim‘𝐾) its nullity (the dimension of its kernel). (Contributed by Thierry Arnoux, 17-May-2023.) |
⊢ 0 = (0g‘𝑈) & ⊢ 𝐾 = (𝑉 ↾s (◡𝐹 “ { 0 })) & ⊢ 𝐼 = (𝑈 ↾s ran 𝐹) ⇒ ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼))) | ||
Theorem | qusdimsum 30924 | Let 𝑊 be a vector space, and let 𝑋 be a subspace. Then the dimension of 𝑊 is the sum of the dimension of 𝑋 and the dimension of the quotient space of 𝑋. First part of theorem 5.3 in [Lang] p. 141 (Contributed by Thierry Arnoux, 20-May-2023.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑌 = (𝑊 /s (𝑊 ~QG 𝑈)) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝑈 ∈ (LSubSp‘𝑊)) → (dim‘𝑊) = ((dim‘𝑋) +𝑒 (dim‘𝑌))) | ||
Theorem | fedgmullem1 30925* | Lemma for fedgmul 30927 (Contributed by Thierry Arnoux, 20-Jul-2023.) |
⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑉) & ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) & ⊢ 𝐾 = (𝐸 ↾s 𝑉) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝐾 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) & ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐹)) & ⊢ 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(.r‘𝐸)𝑗)) & ⊢ 𝐻 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝐺‘𝑗)‘𝑖)) & ⊢ (𝜑 → 𝑋 ∈ (LBasis‘𝐶)) & ⊢ (𝜑 → 𝑌 ∈ (LBasis‘𝐵)) & ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐴)) & ⊢ (𝜑 → 𝐿:𝑌⟶(Base‘(Scalar‘𝐵))) & ⊢ (𝜑 → 𝐿 finSupp (0g‘(Scalar‘𝐵))) & ⊢ (𝜑 → 𝑍 = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗)))) & ⊢ (𝜑 → 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋)) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐺‘𝑗) finSupp (0g‘(Scalar‘𝐶))) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐿‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖)))) ⇒ ⊢ (𝜑 → (𝐻 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑍 = (𝐴 Σg (𝐻 ∘f ( ·𝑠 ‘𝐴)𝐷)))) | ||
Theorem | fedgmullem2 30926* | Lemma for fedgmul 30927 (Contributed by Thierry Arnoux, 20-Jul-2023.) |
⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑉) & ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) & ⊢ 𝐾 = (𝐸 ↾s 𝑉) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝐾 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) & ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐹)) & ⊢ 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(.r‘𝐸)𝑗)) & ⊢ 𝐻 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝐺‘𝑗)‘𝑖)) & ⊢ (𝜑 → 𝑋 ∈ (LBasis‘𝐶)) & ⊢ (𝜑 → 𝑌 ∈ (LBasis‘𝐵)) & ⊢ (𝜑 → 𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋)))) & ⊢ (𝜑 → (𝐴 Σg (𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)) = (0g‘𝐴)) ⇒ ⊢ (𝜑 → 𝑊 = ((𝑌 × 𝑋) × {(0g‘(Scalar‘𝐴))})) | ||
Theorem | fedgmul 30927 | The multiplicativity formula for degrees of field extensions. Given 𝐸 a field extension of 𝐹, itself a field extension of 𝐾, we have [𝐸:𝐾] = [𝐸:𝐹][𝐹:𝐾]. Proposition 1.2 of [Lang], p. 224. Here (dim‘𝐴) is the degree of the extension 𝐸 of 𝐾, (dim‘𝐵) is the degree of the extension 𝐸 of 𝐹, and (dim‘𝐶) is the degree of the extension 𝐹 of 𝐾. This proof is valid for infinite dimensions, and is actually valid for division ring extensions, not just field extensions. (Contributed by Thierry Arnoux, 25-Jul-2023.) |
⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑉) & ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) & ⊢ 𝐾 = (𝐸 ↾s 𝑉) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝐾 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) & ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐹)) ⇒ ⊢ (𝜑 → (dim‘𝐴) = ((dim‘𝐵) ·e (dim‘𝐶))) | ||
Syntax | cfldext 30928 | Syntax for the field extension relation. |
class /FldExt | ||
Syntax | cfinext 30929 | Syntax for the finite field extension relation. |
class /FinExt | ||
Syntax | calgext 30930 | Syntax for the algebraic field extension relation. |
class /AlgExt | ||
Syntax | cextdg 30931 | Syntax for the field extension degree operation. |
class [:] | ||
Definition | df-fldext 30932* | Definition of the field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ /FldExt = {〈𝑒, 𝑓〉 ∣ ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒 ↾s (Base‘𝑓)) ∧ (Base‘𝑓) ∈ (SubRing‘𝑒)))} | ||
Definition | df-extdg 30933* | Definition of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ [:] = (𝑒 ∈ V, 𝑓 ∈ (/FldExt “ {𝑒}) ↦ (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓)))) | ||
Definition | df-finext 30934* | Definition of the finite field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ /FinExt = {〈𝑒, 𝑓〉 ∣ (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)} | ||
Definition | df-algext 30935* | Definition of the algebraic extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ /AlgExt = {〈𝑒, 𝑓〉 ∣ (𝑒/FldExt𝑓 ∧ ∀𝑥 ∈ (Base‘𝑒)∃𝑝 ∈ (Poly1‘𝑓)(((eval1‘𝑓)‘𝑝)‘𝑥) = (0g‘𝑒))} | ||
Theorem | relfldext 30936 | The field extension is a relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ Rel /FldExt | ||
Theorem | brfldext 30937 | The field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ Field) → (𝐸/FldExt𝐹 ↔ (𝐹 = (𝐸 ↾s (Base‘𝐹)) ∧ (Base‘𝐹) ∈ (SubRing‘𝐸)))) | ||
Theorem | ccfldextrr 30938 | The field of the complex numbers is an extension of the field of the real numbers. (Contributed by Thierry Arnoux, 20-Jul-2023.) |
⊢ ℂfld/FldExtℝfld | ||
Theorem | fldextfld1 30939 | A field extension is only defined if the extension is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ (𝐸/FldExt𝐹 → 𝐸 ∈ Field) | ||
Theorem | fldextfld2 30940 | A field extension is only defined if the subfield is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ (𝐸/FldExt𝐹 → 𝐹 ∈ Field) | ||
Theorem | fldextsubrg 30941 | Field extension implies a subring relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ 𝑈 = (Base‘𝐹) ⇒ ⊢ (𝐸/FldExt𝐹 → 𝑈 ∈ (SubRing‘𝐸)) | ||
Theorem | fldextress 30942 | Field extension implies a structure restriction relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ (𝐸/FldExt𝐹 → 𝐹 = (𝐸 ↾s (Base‘𝐹))) | ||
Theorem | brfinext 30943 | The finite field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ (𝐸/FldExt𝐹 → (𝐸/FinExt𝐹 ↔ (𝐸[:]𝐹) ∈ ℕ0)) | ||
Theorem | extdgval 30944 | Value of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) = (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) | ||
Theorem | fldextsralvec 30945 | The subring algebra associated with a field extension is a vector space. (Contributed by Thierry Arnoux, 3-Aug-2023.) |
⊢ (𝐸/FldExt𝐹 → ((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec) | ||
Theorem | extdgcl 30946 | Closure of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) ∈ ℕ0*) | ||
Theorem | extdggt0 30947 | Degrees of field extension are greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
⊢ (𝐸/FldExt𝐹 → 0 < (𝐸[:]𝐹)) | ||
Theorem | fldexttr 30948 | Field extension is a transitive relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ ((𝐸/FldExt𝐹 ∧ 𝐹/FldExt𝐾) → 𝐸/FldExt𝐾) | ||
Theorem | fldextid 30949 | The field extension relation is reflexive. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
⊢ (𝐹 ∈ Field → 𝐹/FldExt𝐹) | ||
Theorem | extdgid 30950 | A trivial field extension has degree one. (Contributed by Thierry Arnoux, 4-Aug-2023.) |
⊢ (𝐸 ∈ Field → (𝐸[:]𝐸) = 1) | ||
Theorem | extdgmul 30951 | The multiplicativity formula for degrees of field extensions. Given 𝐸 a field extension of 𝐹, itself a field extension of 𝐾, the degree of the extension 𝐸/FldExt𝐾 is the product of the degrees of the extensions 𝐸/FldExt𝐹 and 𝐹/FldExt𝐾. Proposition 1.2 of [Lang], p. 224. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
⊢ ((𝐸/FldExt𝐹 ∧ 𝐹/FldExt𝐾) → (𝐸[:]𝐾) = ((𝐸[:]𝐹) ·e (𝐹[:]𝐾))) | ||
Theorem | finexttrb 30952 | The extension 𝐸 of 𝐾 is finite if and only if 𝐸 is finite over 𝐹 and 𝐹 is finite over 𝐾. Corollary 1.3 of [Lang] , p. 225. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
⊢ ((𝐸/FldExt𝐹 ∧ 𝐹/FldExt𝐾) → (𝐸/FinExt𝐾 ↔ (𝐸/FinExt𝐹 ∧ 𝐹/FinExt𝐾))) | ||
Theorem | extdg1id 30953 | If the degree of the extension 𝐸/FldExt𝐹 is 1, then 𝐸 and 𝐹 are identical. (Contributed by Thierry Arnoux, 6-Aug-2023.) |
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → 𝐸 = 𝐹) | ||
Theorem | extdg1b 30954 | The degree of the extension 𝐸/FldExt𝐹 is 1 iff 𝐸 and 𝐹 are the same structure. (Contributed by Thierry Arnoux, 6-Aug-2023.) |
⊢ (𝐸/FldExt𝐹 → ((𝐸[:]𝐹) = 1 ↔ 𝐸 = 𝐹)) | ||
Theorem | fldextchr 30955 | The characteristic of a subfield is the same as the characteristic of the larger field. (Contributed by Thierry Arnoux, 20-Aug-2023.) |
⊢ (𝐸/FldExt𝐹 → (chr‘𝐹) = (chr‘𝐸)) | ||
Theorem | ccfldsrarelvec 30956 | The subring algebra of the complex numbers over the real numbers is a left vector space. (Contributed by Thierry Arnoux, 20-Aug-2023.) |
⊢ ((subringAlg ‘ℂfld)‘ℝ) ∈ LVec | ||
Theorem | ccfldextdgrr 30957 | The degree of the field extension of the complex numbers over the real numbers is 2. (Suggested by GL, 4-Aug-2023.) (Contributed by Thierry Arnoux, 20-Aug-2023.) |
⊢ (ℂfld[:]ℝfld) = 2 | ||
Syntax | csmat 30958 | Syntax for a function generating submatrices. |
class subMat1 | ||
Definition | df-smat 30959* | 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 21116. (Contributed by Thierry Arnoux, 18-Aug-2020.) |
⊢ subMat1 = (𝑚 ∈ V ↦ (𝑘 ∈ ℕ, 𝑙 ∈ ℕ ↦ (𝑚 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))〉)))) | ||
Theorem | smatfval 30960* | Value of the submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
⊢ ((𝐾 ∈ ℕ ∧ 𝐿 ∈ ℕ ∧ 𝑀 ∈ 𝑉) → (𝐾(subMat1‘𝑀)𝐿) = (𝑀 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉))) | ||
Theorem | smatrcl 30961 | Closure of the rectangular submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) ⇒ ⊢ (𝜑 → 𝑆 ∈ (𝐵 ↑m ((1...(𝑀 − 1)) × (1...(𝑁 − 1))))) | ||
Theorem | smatlem 30962 | Lemma for the next theorems. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐽 ∈ ℕ) & ⊢ (𝜑 → if(𝐼 < 𝐾, 𝐼, (𝐼 + 1)) = 𝑋) & ⊢ (𝜑 → if(𝐽 < 𝐿, 𝐽, (𝐽 + 1)) = 𝑌) ⇒ ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝑋𝐴𝑌)) | ||
Theorem | smattl 30963 | Entries of a submatrix, top left. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) & ⊢ (𝜑 → 𝐼 ∈ (1..^𝐾)) & ⊢ (𝜑 → 𝐽 ∈ (1..^𝐿)) ⇒ ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝐼𝐴𝐽)) | ||
Theorem | smattr 30964 | Entries of a submatrix, top right. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) & ⊢ (𝜑 → 𝐼 ∈ (𝐾...𝑀)) & ⊢ (𝜑 → 𝐽 ∈ (1..^𝐿)) ⇒ ⊢ (𝜑 → (𝐼𝑆𝐽) = ((𝐼 + 1)𝐴𝐽)) | ||
Theorem | smatbl 30965 | Entries of a submatrix, bottom left. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) & ⊢ (𝜑 → 𝐼 ∈ (1..^𝐾)) & ⊢ (𝜑 → 𝐽 ∈ (𝐿...𝑁)) ⇒ ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝐼𝐴(𝐽 + 1))) | ||
Theorem | smatbr 30966 | Entries of a submatrix, bottom right. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) & ⊢ (𝜑 → 𝐼 ∈ (𝐾...𝑀)) & ⊢ (𝜑 → 𝐽 ∈ (𝐿...𝑁)) ⇒ ⊢ (𝜑 → (𝐼𝑆𝐽) = ((𝐼 + 1)𝐴(𝐽 + 1))) | ||
Theorem | smatcl 30967 | Closure of the square submatrix: if 𝑀 is a square matrix of dimension 𝑁 with indices 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 | matmpo 30968* | Write a square matrix as a mapping operation. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ (𝑀 ∈ 𝐵 → 𝑀 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖𝑀𝑗))) | ||
Theorem | 1smat1 30969 | The submatrix of the identity matrix obtained by removing the ith row and the ith column is an identity matrix. Cf. 1marepvsma1 21122. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
⊢ 1 = (1r‘((1...𝑁) Mat 𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) ⇒ ⊢ (𝜑 → (𝐼(subMat1‘ 1 )𝐼) = (1r‘((1...(𝑁 − 1)) Mat 𝑅))) | ||
Theorem | submat1n 30970 | 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 30971 | 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 30972 | Lemma for submateq 30974. (Contributed by Thierry Arnoux, 25-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1))) & ⊢ (𝜑 → 𝐾 ≤ 𝑀) ⇒ ⊢ (𝜑 → (𝑀 ∈ (𝐾...𝑁) ∧ (𝑀 + 1) ∈ ((1...𝑁) ∖ {𝐾}))) | ||
Theorem | submateqlem2 30973 | Lemma for submateq 30974. (Contributed by Thierry Arnoux, 26-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1))) & ⊢ (𝜑 → 𝑀 < 𝐾) ⇒ ⊢ (𝜑 → (𝑀 ∈ (1..^𝐾) ∧ 𝑀 ∈ ((1...𝑁) ∖ {𝐾}))) | ||
Theorem | submateq 30974* | 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 30975 | 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 30976 | Extend class notation with the literal matrix conversion function. |
class litMat | ||
Definition | df-lmat 30977* | 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 30978* | Value of the literal matrix conversion function. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
⊢ (𝑀 ∈ 𝑉 → (litMat‘𝑀) = (𝑖 ∈ (1...(♯‘𝑀)), 𝑗 ∈ (1...(♯‘(𝑀‘0))) ↦ ((𝑀‘(𝑖 − 1))‘(𝑗 − 1)))) | ||
Theorem | lmatfval 30979* | Entries of a literal matrix. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
⊢ 𝑀 = (litMat‘𝑊) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑊 ∈ Word Word 𝑉) & ⊢ (𝜑 → (♯‘𝑊) = 𝑁) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (♯‘(𝑊‘𝑖)) = 𝑁) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) ⇒ ⊢ (𝜑 → (𝐼𝑀𝐽) = ((𝑊‘(𝐼 − 1))‘(𝐽 − 1))) | ||
Theorem | lmatfvlem 30980* | 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 30981* | Closure of the literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
⊢ 𝑀 = (litMat‘𝑊) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑊 ∈ Word Word 𝑉) & ⊢ (𝜑 → (♯‘𝑊) = 𝑁) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (♯‘(𝑊‘𝑖)) = 𝑁) & ⊢ 𝑉 = (Base‘𝑅) & ⊢ 𝑂 = ((1...𝑁) Mat 𝑅) & ⊢ 𝑃 = (Base‘𝑂) & ⊢ (𝜑 → 𝑅 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝑀 ∈ 𝑃) | ||
Theorem | lmat22lem 30982* | Lemma for lmat22e11 30983 and co. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
⊢ 𝑀 = (litMat‘〈“〈“𝐴𝐵”〉〈“𝐶𝐷”〉”〉) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^2)) → (♯‘(〈“〈“𝐴𝐵”〉〈“𝐶𝐷”〉”〉‘𝑖)) = 2) | ||
Theorem | lmat22e11 30983 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
⊢ 𝑀 = (litMat‘〈“〈“𝐴𝐵”〉〈“𝐶𝐷”〉”〉) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (1𝑀1) = 𝐴) | ||
Theorem | lmat22e12 30984 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
⊢ 𝑀 = (litMat‘〈“〈“𝐴𝐵”〉〈“𝐶𝐷”〉”〉) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (1𝑀2) = 𝐵) | ||
Theorem | lmat22e21 30985 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
⊢ 𝑀 = (litMat‘〈“〈“𝐴𝐵”〉〈“𝐶𝐷”〉”〉) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (2𝑀1) = 𝐶) | ||
Theorem | lmat22e22 30986 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
⊢ 𝑀 = (litMat‘〈“〈“𝐴𝐵”〉〈“𝐶𝐷”〉”〉) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (2𝑀2) = 𝐷) | ||
Theorem | lmat22det 30987 | 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 30988* | 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 30989* | 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 30990* | 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 30991* | 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 30992* | Lemma for madjusmdet 30996. (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 30993* | Lemma for madjusmdet 30996. (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 30994* | Lemma for madjusmdet 30996. (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 30995* | Lemma for madjusmdet 30996. (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 30996 | Express the cofactor of the matrix, i.e. the entries of its adjunct matrix, using determinant of submatrices. (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 30997* | 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 | txomap 30998* | Given two open maps 𝐹 and 𝐺, 𝐻 mapping pairs of sets, is also an open map for the product topology. (Contributed by Thierry Arnoux, 29-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝑋⟶𝑍) & ⊢ (𝜑 → 𝐺:𝑌⟶𝑇) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) & ⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑇)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ 𝐿) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 “ 𝑦) ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ (𝐽 ×t 𝐾)) & ⊢ 𝐻 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) ⇒ ⊢ (𝜑 → (𝐻 “ 𝐴) ∈ (𝐿 ×t 𝑀)) | ||
Theorem | qtopt1 30999* | If every equivalence class is closed, then the quotient space is T1 . (Contributed by Thierry Arnoux, 5-Jan-2020.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐽 ∈ Fre) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (◡𝐹 “ {𝑥}) ∈ (Clsd‘𝐽)) ⇒ ⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ Fre) | ||
Theorem | qtophaus 31000* | If an open map's graph in the product space (𝐽 ×t 𝐽) is closed, then its quotient topology is Hausdorff. (Contributed by Thierry Arnoux, 4-Jan-2020.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ ∼ = (◡𝐹 ∘ 𝐹) & ⊢ 𝐻 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) & ⊢ (𝜑 → 𝐽 ∈ Haus) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹)) & ⊢ (𝜑 → ∼ ∈ (Clsd‘(𝐽 ×t 𝐽))) ⇒ ⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ Haus) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |