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-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44900) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | resvplusg 30901 | +g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻)) | ||
Theorem | resvvsca 30902 | ·𝑠 is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ · = ( ·𝑠 ‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘𝐻)) | ||
Theorem | resvmulr 30903 | ·𝑠 is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ · = (.r‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝐻)) | ||
Theorem | resv0g 30904 | 0g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 0 = (0g‘𝐻)) | ||
Theorem | resv1r 30905 | 1r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ 1 = (1r‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 1 = (1r‘𝐻)) | ||
Theorem | resvcmn 30906 | Scalar restriction preserves commutative monoids. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
⊢ 𝐻 = (𝐺 ↾v 𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐺 ∈ CMnd ↔ 𝐻 ∈ CMnd)) | ||
Theorem | gzcrng 30907 | The gaussian integers form a commutative ring. (Contributed by Thierry Arnoux, 18-Mar-2018.) |
⊢ (ℂfld ↾s ℤ[i]) ∈ CRing | ||
Theorem | reofld 30908 | The real numbers form an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
⊢ ℝfld ∈ oField | ||
Theorem | nn0omnd 30909 | The nonnegative integers form an ordered monoid. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
⊢ (ℂfld ↾s ℕ0) ∈ oMnd | ||
Theorem | rearchi 30910 | The field of the real numbers is Archimedean. See also arch 11888. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
⊢ ℝfld ∈ Archi | ||
Theorem | nn0archi 30911 | The monoid of the nonnegative integers is Archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018.) |
⊢ (ℂfld ↾s ℕ0) ∈ Archi | ||
Theorem | xrge0slmod 30912 | 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 | qusker 30913* | The kernel of a quotient map. (Contributed by Thierry Arnoux, 20-May-2023.) |
⊢ 𝑉 = (Base‘𝑀) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥](𝑀 ~QG 𝐺)) & ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺)) & ⊢ 0 = (0g‘𝑁) ⇒ ⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → (◡𝐹 “ { 0 }) = 𝐺) | ||
Theorem | eqgvscpbl 30914 | The left coset equivalence relation is compatible with the scalar multiplication operation. (Contributed by Thierry Arnoux, 18-May-2023.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ ∼ = (𝑀 ~QG 𝐺) & ⊢ 𝑆 = (Base‘(Scalar‘𝑀)) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀)) & ⊢ (𝜑 → 𝐾 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋 ∼ 𝑌 → (𝐾 · 𝑋) ∼ (𝐾 · 𝑌))) | ||
Theorem | qusvscpbl 30915* | The quotient map distributes over the scalar multiplication. (Contributed by Thierry Arnoux, 18-May-2023.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ ∼ = (𝑀 ~QG 𝐺) & ⊢ 𝑆 = (Base‘(Scalar‘𝑀)) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀)) & ⊢ (𝜑 → 𝐾 ∈ 𝑆) & ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺)) & ⊢ ∙ = ( ·𝑠 ‘𝑁) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [𝑥](𝑀 ~QG 𝐺)) & ⊢ (𝜑 → 𝑈 ∈ 𝐵) & ⊢ (𝜑 → 𝑉 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝐹‘𝑈) = (𝐹‘𝑉) → (𝐹‘(𝐾 · 𝑈)) = (𝐹‘(𝐾 · 𝑉)))) | ||
Theorem | qusscaval 30916 | Value of the scalar multiplication operation on the quotient structure. (Contributed by Thierry Arnoux, 18-May-2023.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ ∼ = (𝑀 ~QG 𝐺) & ⊢ 𝑆 = (Base‘(Scalar‘𝑀)) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀)) & ⊢ (𝜑 → 𝐾 ∈ 𝑆) & ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺)) & ⊢ ∙ = ( ·𝑠 ‘𝑁) ⇒ ⊢ ((𝜑 ∧ 𝐾 ∈ 𝑆 ∧ 𝑋 ∈ 𝐵) → (𝐾 ∙ [𝑋](𝑀 ~QG 𝐺)) = [(𝐾 · 𝑋)](𝑀 ~QG 𝐺)) | ||
Theorem | imaslmod 30917* | The image structure of a left module is a left module. (Contributed by Thierry Arnoux, 15-May-2023.) |
⊢ (𝜑 → 𝑁 = (𝐹 “s 𝑀)) & ⊢ 𝑉 = (Base‘𝑀) & ⊢ 𝑆 = (Base‘(Scalar‘𝑀)) & ⊢ + = (+g‘𝑀) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ 0 = (0g‘𝑀) & ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝐹‘𝑎) = (𝐹‘𝑏) → (𝐹‘(𝑘 · 𝑎)) = (𝐹‘(𝑘 · 𝑏)))) & ⊢ (𝜑 → 𝑀 ∈ LMod) ⇒ ⊢ (𝜑 → 𝑁 ∈ LMod) | ||
Theorem | quslmod 30918 | If 𝐺 is a submodule in 𝑀, then 𝑁 = 𝑀 / 𝐺 is a left module, called the quotient module of 𝑀 by 𝐺. (Contributed by Thierry Arnoux, 18-May-2023.) |
⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺)) & ⊢ 𝑉 = (Base‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀)) ⇒ ⊢ (𝜑 → 𝑁 ∈ LMod) | ||
Theorem | quslmhm 30919* | If 𝐺 is a submodule of 𝑀, then the "natural map" from elements to their cosets is a left module homomorphism from 𝑀 to 𝑀 / 𝐺. (Contributed by Thierry Arnoux, 18-May-2023.) |
⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺)) & ⊢ 𝑉 = (Base‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀)) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥](𝑀 ~QG 𝐺)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑀 LMHom 𝑁)) | ||
Theorem | ecxpid 30920 | The equivalence class of a cartesian product is the whole set. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
⊢ (𝑋 ∈ 𝐴 → [𝑋](𝐴 × 𝐴) = 𝐴) | ||
Theorem | eqg0el 30921 | Equivalence class of a quotient group for a subgroup. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
⊢ ∼ = (𝐺 ~QG 𝐻) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐻 ∈ (SubGrp‘𝐺)) → ([𝑋] ∼ = 𝐻 ↔ 𝑋 ∈ 𝐻)) | ||
Theorem | qsxpid 30922 | The quotient set of a cartesian product is trivial. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
⊢ (𝐴 ≠ ∅ → (𝐴 / (𝐴 × 𝐴)) = {𝐴}) | ||
Theorem | qusxpid 30923 | The Group quotient equivalence relation for the whole group is the cartesian product, i.e. all elements are in the same equivalence class. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → (𝐺 ~QG 𝐵) = (𝐵 × 𝐵)) | ||
Theorem | qustriv 30924 | The quotient of a group 𝐺 by itself is trivial. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐵)) ⇒ ⊢ (𝐺 ∈ Grp → (Base‘𝑄) = {𝐵}) | ||
Theorem | qustrivr 30925 | Converse of qustriv 30924. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐻)) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐻 ∈ (SubGrp‘𝐺) ∧ (Base‘𝑄) = {𝐻}) → 𝐻 = 𝐵) | ||
Theorem | fply1 30926 | Conditions for a function to be an univariate polynomial. (Contributed by Thierry Arnoux, 19-Aug-2023.) |
⊢ 0 = (0g‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (Base‘(Poly1‘𝑅)) & ⊢ (𝜑 → 𝐹:(ℕ0 ↑m 1o)⟶𝐵) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → 𝐹 ∈ 𝑃) | ||
Theorem | islinds5 30927* | A set is linearly independent if and only if it has no non-trivial representations of zero. (Contributed by Thierry Arnoux, 18-May-2023.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑂 = (0g‘𝑊) & ⊢ 0 = (0g‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵) → (𝑉 ∈ (LIndS‘𝑊) ↔ ∀𝑎 ∈ (𝐾 ↑m 𝑉)((𝑎 finSupp 0 ∧ (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣) · 𝑣))) = 𝑂) → 𝑎 = (𝑉 × { 0 })))) | ||
Theorem | ellspds 30928* | Variation on ellspd 20940. (Contributed by Thierry Arnoux, 18-May-2023.) |
⊢ 𝑁 = (LSpan‘𝑀) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 0 = (0g‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝑉 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝑁‘𝑉) ↔ ∃𝑎 ∈ (𝐾 ↑m 𝑉)(𝑎 finSupp 0 ∧ 𝑋 = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣) · 𝑣)))))) | ||
Theorem | 0ellsp 30929 | Zero is in all spans. (Contributed by Thierry Arnoux, 8-May-2023.) |
⊢ 0 = (0g‘𝑊) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑆 ⊆ 𝐵) → 0 ∈ (𝑁‘𝑆)) | ||
Theorem | 0nellinds 30930 | The group identity cannot be an element of an independent set. (Contributed by Thierry Arnoux, 8-May-2023.) |
⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) → ¬ 0 ∈ 𝐹) | ||
Theorem | rspsnel 30931* | Membership in a principal ideal. Analogous to lspsnel 19769. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝐼 ∈ (𝐾‘{𝑋}) ↔ ∃𝑥 ∈ 𝐵 𝐼 = (𝑥 · 𝑋))) | ||
Theorem | rspsnid 30932 | A principal ideal contains the element that generates it. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ (𝐾‘{𝐺})) | ||
Theorem | lbslsp 30933* | Any element of a left module 𝑀 can be expressed as a linear combination of the elements of a basis 𝑉 of 𝑀. (Contributed by Thierry Arnoux, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 0 = (0g‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝑉 ∈ (LBasis‘𝑀)) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐵 ↔ ∃𝑎 ∈ (𝐾 ↑m 𝑉)(𝑎 finSupp 0 ∧ 𝑋 = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣) · 𝑣)))))) | ||
Theorem | lindssn 30934 | Any singleton of a nonzero element is an independent set. (Contributed by Thierry Arnoux, 5-Aug-2023.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → {𝑋} ∈ (LIndS‘𝑊)) | ||
Theorem | lindflbs 30935 | Conditions for an independent family to be a basis. (Contributed by Thierry Arnoux, 21-Jul-2023.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑂 = (0g‘𝑊) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑆 ∈ NzRing) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼–1-1→𝐵) ⇒ ⊢ (𝜑 → (ran 𝐹 ∈ (LBasis‘𝑊) ↔ (𝐹 LIndF 𝑊 ∧ (𝑁‘ran 𝐹) = 𝐵))) | ||
Theorem | linds2eq 30936 | Deduce equality of elements in an independent set. (Contributed by Thierry Arnoux, 18-Jul-2023.) |
⊢ 𝐹 = (Base‘(Scalar‘𝑊)) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐵 ∈ (LIndS‘𝑊)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐾 ∈ 𝐹) & ⊢ (𝜑 → 𝐿 ∈ 𝐹) & ⊢ (𝜑 → 𝐾 ≠ 0 ) & ⊢ (𝜑 → (𝐾 · 𝑋) = (𝐿 · 𝑌)) ⇒ ⊢ (𝜑 → (𝑋 = 𝑌 ∧ 𝐾 = 𝐿)) | ||
Theorem | lindfpropd 30937* | Property deduction for linearly independent families. (Contributed by Thierry Arnoux, 16-Jul-2023.) |
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) & ⊢ (𝜑 → (Base‘(Scalar‘𝐾)) = (Base‘(Scalar‘𝐿))) & ⊢ (𝜑 → (0g‘(Scalar‘𝐾)) = (0g‘(Scalar‘𝐿))) & ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐾)) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥( ·𝑠 ‘𝐾)𝑦) ∈ (Base‘𝐾)) & ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐾)) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦)) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝐿 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑋 LIndF 𝐾 ↔ 𝑋 LIndF 𝐿)) | ||
Theorem | lindspropd 30938* | Property deduction for linearly independent sets. (Contributed by Thierry Arnoux, 16-Jul-2023.) |
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) & ⊢ (𝜑 → (Base‘(Scalar‘𝐾)) = (Base‘(Scalar‘𝐿))) & ⊢ (𝜑 → (0g‘(Scalar‘𝐾)) = (0g‘(Scalar‘𝐿))) & ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐾)) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥( ·𝑠 ‘𝐾)𝑦) ∈ (Base‘𝐾)) & ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐾)) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦)) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝐿 ∈ 𝑊) ⇒ ⊢ (𝜑 → (LIndS‘𝐾) = (LIndS‘𝐿)) | ||
The sumset (also called the Minkowski sum) of two subsets 𝐴 and 𝐵, is defined to be the set of all sums of an element from 𝐴 with an element from 𝐵. The sumset operation can be used for both group (additive) operations and ring (multiplicative) operations. | ||
Theorem | elgrplsmsn 30939* | Membership in a sumset with a singleton for a group operation. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝐴 ⊕ {𝑋}) ↔ ∃𝑥 ∈ 𝐴 𝑍 = (𝑥 + 𝑋))) | ||
Theorem | lsmsnorb 30940* | The sumset of a group with a single element is the element's orbit by the group action. See gaorb 18431. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ ∃𝑔 ∈ 𝐴 (𝑔 + 𝑥) = 𝑦)} & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ⊕ {𝑋}) = [𝑋] ∼ ) | ||
Theorem | elringlsm 30941* | Membership in a product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ × = (LSSum‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ⊆ 𝐵) & ⊢ (𝜑 → 𝐹 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝐸 × 𝐹) ↔ ∃𝑥 ∈ 𝐸 ∃𝑦 ∈ 𝐹 𝑍 = (𝑥 · 𝑦))) | ||
Theorem | ringlsmss 30942 | Closure of the product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ × = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐸 ⊆ 𝐵) & ⊢ (𝜑 → 𝐹 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐸 × 𝐹) ⊆ 𝐵) | ||
Theorem | lsmsnpridl 30943 | The product of the ring with a single element is equal to the principal ideal generated by that element. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ × = (LSSum‘𝐺) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐵 × {𝑋}) = (𝐾‘{𝑋})) | ||
Theorem | lsmsnidl 30944 | The product of the ring with a single element is a principal ideal. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ × = (LSSum‘𝐺) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐵 × {𝑋}) ∈ (LPIdeal‘𝑅)) | ||
Theorem | lsmidllsp 30945 | The sum of two ideals is the ideal generated by their union. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ⊕ = (LSSum‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝐽 ∈ (LIdeal‘𝑅)) ⇒ ⊢ (𝜑 → (𝐼 ⊕ 𝐽) = (𝐾‘(𝐼 ∪ 𝐽))) | ||
Theorem | lsmidl 30946 | The sum of two ideals is an ideal. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ⊕ = (LSSum‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝐽 ∈ (LIdeal‘𝑅)) ⇒ ⊢ (𝜑 → (𝐼 ⊕ 𝐽) ∈ (LIdeal‘𝑅)) | ||
Syntax | cprmidl 30947 | Extend class notation with the class of prime ideals. |
class PrmIdeal | ||
Definition | df-prmidl 30948* | Define the class of prime ideals of a ring 𝑅. A proper ideal 𝐼 of 𝑅 is prime if whenever 𝐴𝐵 ⊆ 𝐼 for ideals 𝐴 and 𝐵, either 𝐴 ⊆ 𝐼 or 𝐵 ⊆ 𝐼. The more familiar definition using elements rather than ideals is equivalent provided 𝑅 is commutative; see prmidl2 30953 and isprmidlc 30958. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 14-Jan-2024.) |
⊢ PrmIdeal = (𝑟 ∈ Ring ↦ {𝑖 ∈ (LIdeal‘𝑟) ∣ (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑎 ∈ (LIdeal‘𝑟)∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))}) | ||
Theorem | prmidlval 30949* | The class of prime ideals of a ring 𝑅. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (PrmIdeal‘𝑅) = {𝑖 ∈ (LIdeal‘𝑅) ∣ (𝑖 ≠ 𝐵 ∧ ∀𝑎 ∈ (LIdeal‘𝑅)∀𝑏 ∈ (LIdeal‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥 · 𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))}) | ||
Theorem | isprmidl 30950* | The predicate "is a prime ideal". (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝑃 ∈ (PrmIdeal‘𝑅) ↔ (𝑃 ∈ (LIdeal‘𝑅) ∧ 𝑃 ≠ 𝐵 ∧ ∀𝑎 ∈ (LIdeal‘𝑅)∀𝑏 ∈ (LIdeal‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥 · 𝑦) ∈ 𝑃 → (𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃))))) | ||
Theorem | prmidlnr 30951 | A prime ideal is a proper ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) → 𝑃 ≠ 𝐵) | ||
Theorem | prmidl 30952* | The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) ∧ (𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐽 ∈ (LIdeal‘𝑅))) ∧ ∀𝑥 ∈ 𝐼 ∀𝑦 ∈ 𝐽 (𝑥 · 𝑦) ∈ 𝑃) → (𝐼 ⊆ 𝑃 ∨ 𝐽 ⊆ 𝑃)) | ||
Theorem | prmidl2 30953* | A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 35342 for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝑃 ∈ (LIdeal‘𝑅)) ∧ (𝑃 ≠ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) ∈ 𝑃 → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃)))) → 𝑃 ∈ (PrmIdeal‘𝑅)) | ||
Theorem | pridln1 30954 | A proper ideal cannot contain the ring unity. (Contributed by Thierry Arnoux, 9-Apr-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐼 ≠ 𝐵) → ¬ 1 ∈ 𝐼) | ||
Theorem | prmidlidl 30955 | A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) → 𝑃 ∈ (LIdeal‘𝑅)) | ||
Theorem | lidlnsg 30956 | An ideal is a normal subgroup. (Contributed by Thierry Arnoux, 14-Jan-2024.) |
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝐼 ∈ (NrmSGrp‘𝑅)) | ||
Theorem | cringm4 30957 | Commutative/associative law for commutative ring. (Contributed by Thierry Arnoux, 14-Jan-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 · 𝑌) · (𝑍 · 𝑊)) = ((𝑋 · 𝑍) · (𝑌 · 𝑊))) | ||
Theorem | isprmidlc 30958* | The predicate "is prime ideal" for commutative rings. Alternate definition for commutative rings. See definition in [Lang] p. 92. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → (𝑃 ∈ (PrmIdeal‘𝑅) ↔ (𝑃 ∈ (LIdeal‘𝑅) ∧ 𝑃 ≠ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) ∈ 𝑃 → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃))))) | ||
Theorem | prmidlc 30959 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) ∧ (𝐼 ∈ 𝐵 ∧ 𝐽 ∈ 𝐵 ∧ (𝐼 · 𝐽) ∈ 𝑃)) → (𝐼 ∈ 𝑃 ∨ 𝐽 ∈ 𝑃)) | ||
Theorem | qsidomlem1 30960 | If the quotient ring of a commutative ring relative to an ideal is an integral domain, that ideal must be prime. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) → 𝐼 ∈ (PrmIdeal‘𝑅)) | ||
Theorem | qsidomlem2 30961 | A quotient by a prime ideal is an integral domain. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝑄 ∈ IDomn) | ||
Theorem | qsidom 30962 | An ideal 𝐼 in the commutative ring 𝑅 is prime if and only if the factor ring 𝑄 is an integral domain. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → (𝑄 ∈ IDomn ↔ 𝐼 ∈ (PrmIdeal‘𝑅))) | ||
Syntax | cmxidl 30963 | Extend class notation with the class of maximal ideals. |
class MaxIdeal | ||
Definition | df-mxidl 30964* | Define the class of maximal ideals of a ring 𝑅. A proper ideal is called maximal if it is maximal with respect to inclusion among proper ideals. (Contributed by Jeff Madsen, 5-Jan-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
⊢ MaxIdeal = (𝑟 ∈ Ring ↦ {𝑖 ∈ (LIdeal‘𝑟) ∣ (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑗 ∈ (LIdeal‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = (Base‘𝑟))))}) | ||
Theorem | mxidlval 30965* | The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (MaxIdeal‘𝑅) = {𝑖 ∈ (LIdeal‘𝑅) ∣ (𝑖 ≠ 𝐵 ∧ ∀𝑗 ∈ (LIdeal‘𝑅)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = 𝐵)))}) | ||
Theorem | ismxidl 30966* | The predicate "is a maximal ideal". (Contributed by Jeff Madsen, 5-Jan-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝑀 ∈ (MaxIdeal‘𝑅) ↔ (𝑀 ∈ (LIdeal‘𝑅) ∧ 𝑀 ≠ 𝐵 ∧ ∀𝑗 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑗 → (𝑗 = 𝑀 ∨ 𝑗 = 𝐵))))) | ||
Theorem | mxidlidl 30967 | A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ∈ (LIdeal‘𝑅)) | ||
Theorem | mxidlnr 30968 | A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ≠ 𝐵) | ||
Theorem | mxidlmax 30969 | A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ (𝐼 ∈ (LIdeal‘𝑅) ∧ 𝑀 ⊆ 𝐼)) → (𝐼 = 𝑀 ∨ 𝐼 = 𝐵)) | ||
Theorem | mxidln1 30970 | One is not contained in any maximal ideal. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → ¬ 1 ∈ 𝑀) | ||
Theorem | mxidlnzr 30971 | A ring with a maximal ideal is a nonzero ring. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑅 ∈ NzRing) | ||
Theorem | mxidlprm 30972 | Every maximal ideal is prime. Statement in [Lang] p. 92 (Contributed by Thierry Arnoux, 21-Jan-2024.) |
⊢ × = (LSSum‘(mulGrp‘𝑅)) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ∈ (PrmIdeal‘𝑅)) | ||
Theorem | ssmxidllem 30973* | The set 𝑃 used in the proof of ssmxidl 30974 satisfies the condition of Zorn's Lemma. (Contributed by Thierry Arnoux, 10-Apr-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ (𝑝 ≠ 𝐵 ∧ 𝐼 ⊆ 𝑝)} & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝐼 ≠ 𝐵) & ⊢ (𝜑 → 𝑍 ⊆ 𝑃) & ⊢ (𝜑 → 𝑍 ≠ ∅) & ⊢ (𝜑 → [⊊] Or 𝑍) ⇒ ⊢ (𝜑 → ∪ 𝑍 ∈ 𝑃) | ||
Theorem | ssmxidl 30974* | Let 𝑅 be a ring, and let 𝐼 be a proper ideal of 𝑅. Then there is a maximal ideal of 𝑅 containing 𝐼. (Contributed by Thierry Arnoux, 10-Apr-2024.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐼 ≠ 𝐵) → ∃𝑚 ∈ (MaxIdeal‘𝑅)𝐼 ⊆ 𝑚) | ||
Theorem | krull 30975* | Krull's theorem: Any nonzero ring has at least one maximal ideal. (Contributed by Thierry Arnoux, 10-Apr-2024.) |
⊢ (𝑅 ∈ NzRing → ∃𝑚 𝑚 ∈ (MaxIdeal‘𝑅)) | ||
Theorem | mxidlnzrb 30976* | A ring is nonzero if and only if it has maximal ideals. (Contributed by Thierry Arnoux, 10-Apr-2024.) |
⊢ (𝑅 ∈ Ring → (𝑅 ∈ NzRing ↔ ∃𝑚 𝑚 ∈ (MaxIdeal‘𝑅))) | ||
Syntax | cidlsrg 30977 | Extend class notation with the semiring of ideals of a ring. |
class IDLsrg | ||
Definition | df-idlsrg 30978* | Define a structure for the ideals of a ring. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
⊢ IDLsrg = (𝑟 ∈ Ring ↦ ⦋(LIdeal‘𝑟) / 𝑏⦌({〈(Base‘ndx), 𝑏〉, 〈(+g‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((+𝑓‘𝑟) “ (𝑖 × 𝑗)))〉, 〈(.r‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘((+𝑓‘(mulGrp‘𝑟)) “ (𝑖 × 𝑗))))〉} ∪ {〈(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ (𝑏 ∖ {𝑗 ∈ (PrmIdeal‘𝑟) ∣ 𝑗 ⊆ 𝑖}))〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}〉})) | ||
Syntax | crspec 30979 | Extend class notation with the spectrum of a ring. |
class Spec | ||
Definition | df-rspec 30980 | Define the spectrum of a ring. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
⊢ Spec = (𝑟 ∈ Ring ↦ ((IDLsrg‘𝑟) ↾s (PrmIdeal‘𝑟))) | ||
Theorem | sra1r 30981 | The multiplicative neutral element of a subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 1 = (1r‘𝑊)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → 1 = (1r‘𝐴)) | ||
Theorem | sraring 30982 | Condition for a subring algebra to be a ring. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑉 ⊆ 𝐵) → 𝐴 ∈ Ring) | ||
Theorem | sradrng 30983 | Condition for a subring algebra to be a division ring. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵) → 𝐴 ∈ DivRing) | ||
Theorem | srasubrg 30984 | A subring of the original structure is also a subring of the constructed subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝑊)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐴)) | ||
Theorem | sralvec 30985 | Given a sub division ring 𝐹 of a division ring 𝐸, 𝐸 may be considered as a vector space over 𝐹, which becomes the field of scalars. (Contributed by Thierry Arnoux, 24-May-2023.) |
⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) ⇒ ⊢ ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec) | ||
Theorem | srafldlvec 30986 | Given a subfield 𝐹 of a field 𝐸, 𝐸 may be considered as a vector space over 𝐹, which becomes the field of scalars. (Contributed by Thierry Arnoux, 24-May-2023.) |
⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) ⇒ ⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ Field ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec) | ||
Theorem | drgext0g 30987 | The additive neutral element of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) ⇒ ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐵)) | ||
Theorem | drgextvsca 30988 | The scalar multiplication operation of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) ⇒ ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘𝐵)) | ||
Theorem | drgext0gsca 30989 | The additive neutral element of the scalar field of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) ⇒ ⊢ (𝜑 → (0g‘𝐵) = (0g‘(Scalar‘𝐵))) | ||
Theorem | drgextsubrg 30990 | The scalar field is a subring of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) & ⊢ (𝜑 → 𝐹 ∈ DivRing) ⇒ ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐵)) | ||
Theorem | drgextlsp 30991 | The scalar field is a subspace of a subring algebra. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) & ⊢ (𝜑 → 𝐹 ∈ DivRing) ⇒ ⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝐵)) | ||
Theorem | drgextgsum 30992* | Group sum in a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ 𝑌)) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ 𝑌))) | ||
Theorem | lvecdimfi 30993 | Finite version of lvecdim 19923 which does not require the axiom of choice. The axiom of choice is used in acsmapd 17782, which is required in the infinite case. Suggested by Gérard Lang. (Contributed by Thierry Arnoux, 24-May-2023.) |
⊢ 𝐽 = (LBasis‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑆 ∈ 𝐽) & ⊢ (𝜑 → 𝑇 ∈ 𝐽) & ⊢ (𝜑 → 𝑆 ∈ Fin) ⇒ ⊢ (𝜑 → 𝑆 ≈ 𝑇) | ||
Syntax | cldim 30994 | Extend class notation with the dimension of a vector space. |
class dim | ||
Definition | df-dim 30995 | Define the dimension of a vector space as the cardinality of its bases. Note that by lvecdim 19923, all bases are equinumerous. (Contributed by Thierry Arnoux, 6-May-2023.) |
⊢ dim = (𝑓 ∈ V ↦ ∪ (♯ “ (LBasis‘𝑓))) | ||
Theorem | dimval 30996 | 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 30997 | The dimension of a vector space 𝐹 is the cardinality of one of its bases. This version of dimval 30996 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 30998 | Closure of the vector space dimension. (Contributed by Thierry Arnoux, 18-May-2023.) |
⊢ (𝑉 ∈ LVec → (dim‘𝑉) ∈ ℕ0*) | ||
Theorem | lvecdim0i 30999 | 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 31000 | 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 })) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |