HomeTheorem List (p. 337 of 506)
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. 337 of 506) | < 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-31236) |
Hilbert Space Explorer
(31237-32759) |
Users' Mathboxes
(32760-50572) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | fldgensdrg 33601 | A generated subfield is a sub-division-ring. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑆) ∈ (SubDRing‘𝐹)) | ||
| Theorem | fldgenssv 33602 | A generated subfield is a subset of the field's base. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑆) ⊆ 𝐵) | ||
| Theorem | fldgenss 33603 | Generated subfields preserve subset ordering. ( see lspss 21084 and spanss 31666) (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑇) ⊆ (𝐹 fldGen 𝑆)) | ||
| Theorem | fldgenidfld 33604 | The subfield generated by a subfield is the subfield itself. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ∈ (SubDRing‘𝐹)) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑆) = 𝑆) | ||
| Theorem | fldgenssp 33605 | The field generated by a set of elements in a division ring is contained in any sub-division-ring which contains those elements. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ∈ (SubDRing‘𝐹)) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑇) ⊆ 𝑆) | ||
| Theorem | fldgenid 33606 | The subfield of a field 𝐹 generated by the whole base set of 𝐹 is 𝐹 itself. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝐵) = 𝐵) | ||
| Theorem | fldgenfld 33607 | A generated subfield is a field. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ Field) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ↾s (𝐹 fldGen 𝑆)) ∈ Field) | ||
| Theorem | primefldgen1 33608 | The prime field of a division ring is the subfield generated by the multiplicative identity element. In general, we should write "prime division ring", but since most later usages are in the case where the ambient ring is commutative, we keep the term "prime field". (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) ⇒ ⊢ (𝜑 → ∩ (SubDRing‘𝑅) = (𝑅 fldGen { 1 })) | ||
| Theorem | 1fldgenq 33609 | The field of rational numbers ℚ is generated by 1 in ℂfld, that is, ℚ is the prime field of ℂfld. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ (ℂfld fldGen {1}) = ℚ | ||
| Theorem | rhmdvd 33610 | A ring homomorphism preserves ratios. (Contributed by Thierry Arnoux, 22-Oct-2017.) |
| ⊢ 𝑈 = (Unit‘𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ / = (/r‘𝑆) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) ∧ ((𝐹‘𝐵) ∈ 𝑈 ∧ (𝐹‘𝐶) ∈ 𝑈)) → ((𝐹‘𝐴) / (𝐹‘𝐵)) = ((𝐹‘(𝐴 · 𝐶)) / (𝐹‘(𝐵 · 𝐶)))) | ||
| Theorem | kerunit 33611 | 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 33612 | Extend class notation with the scalar restriction operation. |
| class ↾v | ||
| Definition | df-resv 33613* | 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 33614 | The scalar restriction is a proper operator, so it can be used with ovprc1 7449. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ Rel dom ↾v | ||
| Theorem | resvval 33615 | Value of structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet ⟨(Scalar‘ndx), (𝐹 ↾s 𝐴)⟩))) | ||
| Theorem | resvid2 33616 | General behavior of trivial restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊) | ||
| Theorem | resvval2 33617 | Value of nontrivial structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet ⟨(Scalar‘ndx), (𝐹 ↾s 𝐴)⟩)) | ||
| Theorem | resvsca 33618 | Base set of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐹 ↾s 𝐴) = (Scalar‘𝑅)) | ||
| Theorem | resvlem 33619 | Other elements of a scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐶 = (𝐸‘𝑊) & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝐸‘ndx) ≠ (Scalar‘ndx) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐶 = (𝐸‘𝑅)) | ||
| Theorem | resvbas 33620 | Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐵 = (Base‘𝐻)) | ||
| Theorem | resvplusg 33621 | +g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻)) | ||
| Theorem | resvvsca 33622 | ·𝑠 is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Proof shortened by AV, 31-Oct-2024.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ · = ( ·𝑠 ‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘𝐻)) | ||
| Theorem | resvmulr 33623 | .r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ · = (.r‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝐻)) | ||
| Theorem | resv0g 33624 | 0g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 0 = (0g‘𝐻)) | ||
| Theorem | resv1r 33625 | 1r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ 1 = (1r‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 1 = (1r‘𝐻)) | ||
| Theorem | resvcmn 33626 | Scalar restriction preserves commutative monoids. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐺 ∈ CMnd ↔ 𝐻 ∈ CMnd)) | ||
| Theorem | gzcrng 33627 | The gaussian integers form a commutative ring. (Contributed by Thierry Arnoux, 18-Mar-2018.) |
| ⊢ (ℂfld ↾s ℤ[i]) ∈ CRing | ||
| Theorem | cnfldfld 33628 | The complex numbers form a field. (Contributed by Thierry Arnoux, 6-Jul-2025.) |
| ⊢ ℂfld ∈ Field | ||
| Theorem | reofld 33629 | The real numbers form an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
| ⊢ ℝfld ∈ oField | ||
| Theorem | nn0omnd 33630 | The nonnegative integers form an ordered monoid. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| ⊢ (ℂfld ↾s ℕ0) ∈ oMnd | ||
| Theorem | gsumind 33631 | The group sum of an indicator function of the set 𝐴 gives the size of 𝐴. (Contributed by Thierry Arnoux, 18-Jan-2026.) |
| ⊢ (𝜑 → 𝑂 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ⊆ 𝑂) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → (ℂfld Σg ((𝟭‘𝑂)‘𝐴)) = (♯‘𝐴)) | ||
| Theorem | rearchi 33632 | The field of the real numbers is Archimedean. See also arch 12500. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
| ⊢ ℝfld ∈ Archi | ||
| Theorem | nn0archi 33633 | The monoid of the nonnegative integers is Archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018.) |
| ⊢ (ℂfld ↾s ℕ0) ∈ Archi | ||
| Theorem | xrge0slmod 33634 | 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 33635* | The kernel of a quotient map. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝑉 = (Base‘𝑀) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥](𝑀 ~QG 𝐺)) & ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺)) & ⊢ 0 = (0g‘𝑁) ⇒ ⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → (◡𝐹 “ { 0 }) = 𝐺) | ||
| Theorem | eqgvscpbl 33636 | 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 33637* | 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 | qusvsval 33638 | 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 33639* | 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 | imasmhm 33640* | Given a function 𝐹 with homomorphic properties, build the image of a monoid. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ + = (+g‘𝑊) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ (𝜑 → 𝑊 ∈ Mnd) ⇒ ⊢ (𝜑 → ((𝐹 “s 𝑊) ∈ Mnd ∧ 𝐹 ∈ (𝑊 MndHom (𝐹 “s 𝑊)))) | ||
| Theorem | imasghm 33641* | Given a function 𝐹 with homomorphic properties, build the image of a group. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ + = (+g‘𝑊) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ (𝜑 → 𝑊 ∈ Grp) ⇒ ⊢ (𝜑 → ((𝐹 “s 𝑊) ∈ Grp ∧ 𝐹 ∈ (𝑊 GrpHom (𝐹 “s 𝑊)))) | ||
| Theorem | imasrhm 33642* | Given a function 𝐹 with homomorphic properties, build the image of a ring. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ + = (+g‘𝑊) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ · = (.r‘𝑊) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)))) & ⊢ (𝜑 → 𝑊 ∈ Ring) ⇒ ⊢ (𝜑 → ((𝐹 “s 𝑊) ∈ Ring ∧ 𝐹 ∈ (𝑊 RingHom (𝐹 “s 𝑊)))) | ||
| Theorem | imaslmhm 33643* | Given a function 𝐹 with homomorphic properties, build the image of a left module. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ + = (+g‘𝑊) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ ((𝜑 ∧ (𝑘 ∈ 𝐾 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐹‘𝑎) = (𝐹‘𝑏) → (𝐹‘(𝑘 × 𝑎)) = (𝐹‘(𝑘 × 𝑏)))) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ × = ( ·𝑠 ‘𝑊) ⇒ ⊢ (𝜑 → ((𝐹 “s 𝑊) ∈ LMod ∧ 𝐹 ∈ (𝑊 LMHom (𝐹 “s 𝑊)))) | ||
| Theorem | quslmod 33644 | 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 33645* | 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 | quslvec 33646 | If 𝑆 is a vector subspace in 𝑊, then 𝑄 = 𝑊 / 𝑆 is a vector space, called the quotient space of 𝑊 by 𝑆. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ 𝑄 = (𝑊 /s (𝑊 ~QG 𝑆)) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑆 ∈ (LSubSp‘𝑊)) ⇒ ⊢ (𝜑 → 𝑄 ∈ LVec) | ||
| Theorem | znfermltl 33647 | Fermat's little theorem in ℤ/nℤ. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑃) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ ↑ = (.g‘(mulGrp‘𝑍)) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ 𝐵) → (𝑃 ↑ 𝐴) = 𝐴) | ||
| Theorem | islinds5 33648* | 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 33649* | Variation on ellspd 21931. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ 𝑁 = (LSpan‘𝑀) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 0 = (0g‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝑉 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝑁‘𝑉) ↔ ∃𝑎 ∈ (𝐾 ↑m 𝑉)(𝑎 finSupp 0 ∧ 𝑋 = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣) · 𝑣)))))) | ||
| Theorem | 0ellsp 33650 | Zero is in all spans. (Contributed by Thierry Arnoux, 8-May-2023.) |
| ⊢ 0 = (0g‘𝑊) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑆 ⊆ 𝐵) → 0 ∈ (𝑁‘𝑆)) | ||
| Theorem | 0nellinds 33651 | The group identity cannot be an element of an independent set. (Contributed by Thierry Arnoux, 8-May-2023.) |
| ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) → ¬ 0 ∈ 𝐹) | ||
| Theorem | elrsp 33652* | Write the elements of a ring span as finite linear combinations. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑁 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝑁‘𝐼) ↔ ∃𝑎 ∈ (𝐵 ↑m 𝐼)(𝑎 finSupp 0 ∧ 𝑋 = (𝑅 Σg (𝑖 ∈ 𝐼 ↦ ((𝑎‘𝑖) · 𝑖)))))) | ||
| Theorem | ellpi 33653 | Elementhood in a left principal ideal in terms of the "divides" relation. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑌 ∈ (𝐾‘{𝑋}) ↔ 𝑋 ∥ 𝑌)) | ||
| Theorem | lpirlidllpi 33654* | In a principal ideal ring, ideals are principal. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ LPIR) & ⊢ (𝜑 → 𝐽 ∈ 𝐼) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐽 = (𝐾‘{𝑥})) | ||
| Theorem | rspidlid 33655 | The ideal span of an ideal is the ideal itself. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝐾‘𝐼) = 𝐼) | ||
| Theorem | lbslsp 33656* | 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 33657 | 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 33658 | 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 | islbs5 33659* | An equivalent formulation of the basis predicate in a vector space, using a function 𝐹 for generating the base. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑂 = (0g‘𝑊) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑆 ∈ NzRing) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼–1-1→𝐵) ⇒ ⊢ (𝜑 → (ran 𝐹 ∈ (LBasis‘𝑊) ↔ (∀𝑎 ∈ (𝐾 ↑m 𝐼)((𝑎 finSupp 0 ∧ (𝑊 Σg (𝑎 ∘f · 𝐹)) = 𝑂) → 𝑎 = (𝐼 × { 0 })) ∧ (𝑁‘ran 𝐹) = 𝐵))) | ||
| Theorem | linds2eq 33660 | 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 33661* | 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 33662* | 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‘𝐿)) | ||
| Theorem | dvdsruassoi 33663 | If two elements 𝑋 and 𝑌 of a ring 𝑅 are unit multiples, then they are associates, i.e. each divides the other. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑉 ∈ 𝑈) & ⊢ (𝜑 → (𝑉 · 𝑋) = 𝑌) ⇒ ⊢ (𝜑 → (𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋)) | ||
| Theorem | dvdsruasso 33664* | Two elements 𝑋 and 𝑌 of a ring 𝑅 are associates, i.e. each divides the other, iff they are unit multiples of each other. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) ⇒ ⊢ (𝜑 → ((𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋) ↔ ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌)) | ||
| Theorem | dvdsruasso2 33665* | A reformulation of dvdsruasso 33664. (Proposed by Gerard Lang, 28-May-2025.) (Contributed by Thiery Arnoux, 29-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝜑 → ((𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋) ↔ ∃𝑢 ∈ 𝑈 ∃𝑣 ∈ 𝑈 ((𝑢 · 𝑋) = 𝑌 ∧ (𝑣 · 𝑌) = 𝑋 ∧ (𝑢 · 𝑣) = 1 ))) | ||
| Theorem | dvdsrspss 33666 | In a ring, an element 𝑋 divides 𝑌 iff the ideal generated by 𝑌 is a subset of the ideal generated by 𝑋. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (𝑋 ∥ 𝑌 ↔ (𝐾‘{𝑌}) ⊆ (𝐾‘{𝑋}))) | ||
| Theorem | rspsnasso 33667 | Two elements 𝑋 and 𝑌 of a ring 𝑅 are associates, i.e. each divides the other, iff the ideals they generate are equal. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → ((𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋) ↔ (𝐾‘{𝑌}) = (𝐾‘{𝑋}))) | ||
| Theorem | unitprodclb 33668 | A finite product is a unit iff all factors are units. (Contributed by Thierry Arnoux, 27-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐹 ∈ Word 𝐵) ⇒ ⊢ (𝜑 → ((𝑀 Σg 𝐹) ∈ 𝑈 ↔ ran 𝐹 ⊆ 𝑈)) | ||
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 33669* | Membership in a sumset with a singleton for a group operation. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝐴 ⊕ {𝑋}) ↔ ∃𝑥 ∈ 𝐴 𝑍 = (𝑥 + 𝑋))) | ||
| Theorem | lsmsnorb 33670* | The sumset of a group with a single element is the element's orbit by the group action. See gaorb 19376. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ ∃𝑔 ∈ 𝐴 (𝑔 + 𝑥) = 𝑦)} & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ⊕ {𝑋}) = [𝑋] ∼ ) | ||
| Theorem | lsmsnorb2 33671* | The sumset of a single element with a group is the element's orbit by the group action. See gaorb 19376. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ ∃𝑔 ∈ 𝐴 (𝑥 + 𝑔) = 𝑦)} & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ({𝑋} ⊕ 𝐴) = [𝑋] ∼ ) | ||
| Theorem | ringlsmss 33672 | Closure of the product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ × = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐸 ⊆ 𝐵) & ⊢ (𝜑 → 𝐹 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐸 × 𝐹) ⊆ 𝐵) | ||
| Theorem | ringlsmss1 33673 | The product of an ideal 𝐼 of a commutative ring 𝑅 with some set E is a subset of the ideal. (Contributed by Thierry Arnoux, 8-Jun-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ × = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐸 ⊆ 𝐵) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) ⇒ ⊢ (𝜑 → (𝐼 × 𝐸) ⊆ 𝐼) | ||
| Theorem | ringlsmss2 33674 | The product with an ideal of a ring is a subset of that ideal. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ × = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐸 ⊆ 𝐵) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) ⇒ ⊢ (𝜑 → (𝐸 × 𝐼) ⊆ 𝐼) | ||
| Theorem | lsmsnpridl 33675 | 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 33676 | 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 | lsmssass 33677 | Group sum is associative, subset version (see lsmass 19738). (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝑅 ⊆ 𝐵) & ⊢ (𝜑 → 𝑇 ⊆ 𝐵) & ⊢ (𝜑 → 𝑈 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ((𝑅 ⊕ 𝑇) ⊕ 𝑈) = (𝑅 ⊕ (𝑇 ⊕ 𝑈))) | ||
| Theorem | grplsm0l 33678 | Sumset with the identity singleton is the original set. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → ({ 0 } ⊕ 𝐴) = 𝐴) | ||
| Theorem | grplsmid 33679 | The direct sum of an element 𝑋 of a subgroup 𝐴 is the subgroup itself. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
| ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝐴) → ({𝑋} ⊕ 𝐴) = 𝐴) | ||
| Theorem | quslsm 33680 | Express the image by the quotient map in terms of direct sum. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → [𝑋](𝐺 ~QG 𝑆) = ({𝑋} ⊕ 𝑆)) | ||
| Theorem | qusbas2 33681* | Alternate definition of the group quotient set, as the set of all cosets of the form ({𝑥} ⊕ 𝑁). (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ (SubGrp‘𝐺)) ⇒ ⊢ (𝜑 → (𝐵 / (𝐺 ~QG 𝑁)) = ran (𝑥 ∈ 𝐵 ↦ ({𝑥} ⊕ 𝑁))) | ||
| Theorem | qus0g 33682 | The identity element of a quotient group. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) ⇒ ⊢ (𝑁 ∈ (NrmSGrp‘𝐺) → (0g‘𝑄) = 𝑁) | ||
| Theorem | qusima 33683* | The image of a subgroup by the natural map from elements to their cosets. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [𝑥](𝐺 ~QG 𝑁)) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) & ⊢ (𝜑 → 𝐻 ∈ 𝑆) & ⊢ (𝜑 → 𝑆 ⊆ (SubGrp‘𝐺)) ⇒ ⊢ (𝜑 → (𝐸‘𝐻) = (𝐹 “ 𝐻)) | ||
| Theorem | qusrn 33684* | The natural map from elements to their cosets is surjective. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑈 = (𝐵 / (𝐺 ~QG 𝑁)) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [𝑥](𝐺 ~QG 𝑁)) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) ⇒ ⊢ (𝜑 → ran 𝐹 = 𝑈) | ||
| Theorem | nsgqus0 33685 | A normal subgroup 𝑁 is a member of all subgroups 𝐹 of the quotient group by 𝑁. In fact, it is the identity element of the quotient group. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
| ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) ⇒ ⊢ ((𝑁 ∈ (NrmSGrp‘𝐺) ∧ 𝐹 ∈ (SubGrp‘𝑄)) → 𝑁 ∈ 𝐹) | ||
| Theorem | nsgmgclem 33686* | Lemma for nsgmgc 33687. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) & ⊢ (𝜑 → 𝐹 ∈ (SubGrp‘𝑄)) ⇒ ⊢ (𝜑 → {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹} ∈ (SubGrp‘𝐺)) | ||
| Theorem | nsgmgc 33687* | There is a monotone Galois connection between the lattice of subgroups of a group 𝐺 containing a normal subgroup 𝑁 and the lattice of subgroups of the quotient group 𝐺 / 𝑁. This is sometimes called the lattice theorem. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ} & ⊢ 𝑇 = (SubGrp‘𝑄) & ⊢ 𝐽 = (𝑉MGalConn𝑊) & ⊢ 𝑉 = (toInc‘𝑆) & ⊢ 𝑊 = (toInc‘𝑇) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))) & ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) ⇒ ⊢ (𝜑 → 𝐸𝐽𝐹) | ||
| Theorem | nsgqusf1olem1 33688* | Lemma for nsgqusf1o 33691. (Contributed by Thierry Arnoux, 4-Aug-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ} & ⊢ 𝑇 = (SubGrp‘𝑄) & ⊢ ≤ = (le‘(toInc‘𝑆)) & ⊢ ≲ = (le‘(toInc‘𝑇)) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))) & ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) ⇒ ⊢ (((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) → ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)) ∈ 𝑇) | ||
| Theorem | nsgqusf1olem2 33689* | Lemma for nsgqusf1o 33691. (Contributed by Thierry Arnoux, 4-Aug-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ} & ⊢ 𝑇 = (SubGrp‘𝑄) & ⊢ ≤ = (le‘(toInc‘𝑆)) & ⊢ ≲ = (le‘(toInc‘𝑇)) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))) & ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) ⇒ ⊢ (𝜑 → ran 𝐸 = 𝑇) | ||
| Theorem | nsgqusf1olem3 33690* | Lemma for nsgqusf1o 33691. (Contributed by Thierry Arnoux, 4-Aug-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ} & ⊢ 𝑇 = (SubGrp‘𝑄) & ⊢ ≤ = (le‘(toInc‘𝑆)) & ⊢ ≲ = (le‘(toInc‘𝑇)) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))) & ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) ⇒ ⊢ (𝜑 → ran 𝐹 = 𝑆) | ||
| Theorem | nsgqusf1o 33691* | The canonical projection homomorphism 𝐸 defines a bijective correspondence between the set 𝑆 of subgroups of 𝐺 containing a normal subgroup 𝑁 and the subgroups of the quotient group 𝐺 / 𝑁. This theorem is sometimes called the correspondence theorem, or the fourth isomorphism theorem. (Contributed by Thierry Arnoux, 4-Aug-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ} & ⊢ 𝑇 = (SubGrp‘𝑄) & ⊢ ≤ = (le‘(toInc‘𝑆)) & ⊢ ≲ = (le‘(toInc‘𝑇)) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))) & ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) ⇒ ⊢ (𝜑 → 𝐸:𝑆–1-1-onto→𝑇) | ||
| Theorem | lmhmqusker 33692* | A surjective module homomorphism 𝐹 from 𝐺 to 𝐻 induces an isomorphism 𝐽 from 𝑄 to 𝐻, where 𝑄 is the factor group of 𝐺 by 𝐹's kernel 𝐾. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| ⊢ 0 = (0g‘𝐻) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 LMHom 𝐻)) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾)) & ⊢ (𝜑 → ran 𝐹 = (Base‘𝐻)) & ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞)) ⇒ ⊢ (𝜑 → 𝐽 ∈ (𝑄 LMIso 𝐻)) | ||
| Theorem | lmicqusker 33693 | The image 𝐻 of a module homomorphism 𝐹 is isomorphic with the quotient module 𝑄 over 𝐹's kernel 𝐾. This is part of what is sometimes called the first isomorphism theorem for modules. (Contributed by Thierry Arnoux, 10-Mar-2025.) |
| ⊢ 0 = (0g‘𝐻) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 LMHom 𝐻)) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾)) & ⊢ (𝜑 → ran 𝐹 = (Base‘𝐻)) ⇒ ⊢ (𝜑 → 𝑄 ≃𝑚 𝐻) | ||
| Theorem | intlidl 33694 | The intersection of a nonempty collection of ideals is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 8-Jun-2024.) |
| ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅)) → ∩ 𝐶 ∈ (LIdeal‘𝑅)) | ||
| Theorem | inlidl 33695 | The intersection of two ideals is an ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by AV, 28-Jun-2026.) |
| ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐽 ∈ (LIdeal‘𝑅)) → (𝐼 ∩ 𝐽) ∈ (LIdeal‘𝑅)) | ||
| Theorem | pidlnzb 33696 | A principal ideal is nonzero iff it is generated by a nonzero elements (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑋 ≠ 0 ↔ (𝐾‘{𝑋}) ≠ { 0 })) | ||
| Theorem | lidlunitel 33697 | If an ideal 𝐼 contains a unit 𝐽, then it is the whole ring. (Contributed by Thierry Arnoux, 19-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ (𝜑 → 𝐽 ∈ 𝑈) & ⊢ (𝜑 → 𝐽 ∈ 𝐼) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) ⇒ ⊢ (𝜑 → 𝐼 = 𝐵) | ||
| Theorem | unitpidl1 33698 | The ideal 𝐼 generated by an element 𝑋 of a commutative ring 𝑅 is the unit ideal 𝐵 iff 𝑋 is a ring unit. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐼 = (𝐾‘{𝑋}) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → (𝐼 = 𝐵 ↔ 𝑋 ∈ 𝑈)) | ||
| Theorem | rhmquskerlem 33699* | The mapping 𝐽 induced by a ring homomorphism 𝐹 from the quotient group 𝑄 over 𝐹's kernel 𝐾 is a ring homomorphism. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 0 = (0g‘𝐻) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 RingHom 𝐻)) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾)) & ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞)) & ⊢ (𝜑 → 𝐺 ∈ CRing) ⇒ ⊢ (𝜑 → 𝐽 ∈ (𝑄 RingHom 𝐻)) | ||
| Theorem | rhmqusker 33700* | A surjective ring homomorphism 𝐹 from 𝐺 to 𝐻 induces an isomorphism 𝐽 from 𝑄 to 𝐻, where 𝑄 is the factor group of 𝐺 by 𝐹's kernel 𝐾. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| ⊢ 0 = (0g‘𝐻) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 RingHom 𝐻)) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾)) & ⊢ (𝜑 → ran 𝐹 = (Base‘𝐻)) & ⊢ (𝜑 → 𝐺 ∈ CRing) & ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞)) ⇒ ⊢ (𝜑 → 𝐽 ∈ (𝑄 RingIso 𝐻)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |