HomeTheorem List (p. 335 of 502)
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. 335 of 502) | < 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-31005) |
Hilbert Space Explorer
(31006-32528) |
Users' Mathboxes
(32529-50153) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | fracfld 33401 | The field of fractions of an integral domain is a field. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ IDomn) ⇒ ⊢ (𝜑 → ( Frac ‘𝑅) ∈ Field) | ||
| Theorem | idomsubr 33402* | Every integral domain is isomorphic with a subring of some field. (Proposed by Gerard Lang, 10-May-2025.) (Contributed by Thierry Arnoux, 10-May-2025.) |
| ⊢ (𝜑 → 𝑅 ∈ IDomn) ⇒ ⊢ (𝜑 → ∃𝑓 ∈ Field ∃𝑠 ∈ (SubRing‘𝑓)𝑅 ≃𝑟 (𝑓 ↾s 𝑠)) | ||
| Syntax | cfldgen 33403 | Syntax for a function generating sub-fields. |
| class fldGen | ||
| Definition | df-fldgen 33404* | Define a function generating the smallest sub-division-ring of a given ring containing a given set. If the base structure is a division ring, then this is also a division ring (see fldgensdrg 33407). If the base structure is a field, this is a subfield (see fldgenfld 33413 and fldsdrgfld 20743). In general this will be used in the context of fields, hence the name fldGen. (Contributed by Saveliy Skresanov and Thierry Arnoux, 9-Jan-2025.) |
| ⊢ fldGen = (𝑓 ∈ V, 𝑠 ∈ V ↦ ∩ {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠 ⊆ 𝑎}) | ||
| Theorem | fldgenval 33405* | Value of the field generating function: (𝐹 fldGen 𝑆) is the smallest sub-division-ring of 𝐹 containing 𝑆. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑆) = ∩ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎}) | ||
| Theorem | fldgenssid 33406 | The field generated by a set of elements contains those elements. See lspssid 20948. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝑆 ⊆ (𝐹 fldGen 𝑆)) | ||
| Theorem | fldgensdrg 33407 | A generated subfield is a sub-division-ring. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑆) ∈ (SubDRing‘𝐹)) | ||
| Theorem | fldgenssv 33408 | A generated subfield is a subset of the field's base. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑆) ⊆ 𝐵) | ||
| Theorem | fldgenss 33409 | Generated subfields preserve subset ordering. ( see lspss 20947 and spanss 31435) (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑇) ⊆ (𝐹 fldGen 𝑆)) | ||
| Theorem | fldgenidfld 33410 | The subfield generated by a subfield is the subfield itself. (Contributed by Thierry Arnoux, 15-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑆 ∈ (SubDRing‘𝐹)) ⇒ ⊢ (𝜑 → (𝐹 fldGen 𝑆) = 𝑆) | ||
| Theorem | fldgenssp 33411 | 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 33412 | 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 33413 | A generated subfield is a field. (Contributed by Thierry Arnoux, 11-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ Field) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ↾s (𝐹 fldGen 𝑆)) ∈ Field) | ||
| Theorem | primefldgen1 33414 | 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 33415 | 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 33416 | A ring homomorphism preserves ratios. (Contributed by Thierry Arnoux, 22-Oct-2017.) |
| ⊢ 𝑈 = (Unit‘𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ / = (/r‘𝑆) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) ∧ ((𝐹‘𝐵) ∈ 𝑈 ∧ (𝐹‘𝐶) ∈ 𝑈)) → ((𝐹‘𝐴) / (𝐹‘𝐵)) = ((𝐹‘(𝐴 · 𝐶)) / (𝐹‘(𝐵 · 𝐶)))) | ||
| Theorem | kerunit 33417 | 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 33418 | Extend class notation with the scalar restriction operation. |
| class ↾v | ||
| Definition | df-resv 33419* | 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 33420 | The scalar restriction is a proper operator, so it can be used with ovprc1 7407. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ Rel dom ↾v | ||
| Theorem | resvval 33421 | Value of structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet ⟨(Scalar‘ndx), (𝐹 ↾s 𝐴)⟩))) | ||
| Theorem | resvid2 33422 | General behavior of trivial restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊) | ||
| Theorem | resvval2 33423 | Value of nontrivial structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet ⟨(Scalar‘ndx), (𝐹 ↾s 𝐴)⟩)) | ||
| Theorem | resvsca 33424 | Base set of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝑅 = (𝑊 ↾v 𝐴) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐹 ↾s 𝐴) = (Scalar‘𝑅)) | ||
| Theorem | resvlem 33425 | 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 33426 | Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐵 = (Base‘𝐻)) | ||
| Theorem | resvplusg 33427 | +g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻)) | ||
| Theorem | resvvsca 33428 | ·𝑠 is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Proof shortened by AV, 31-Oct-2024.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ · = ( ·𝑠 ‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = ( ·𝑠 ‘𝐻)) | ||
| Theorem | resvmulr 33429 | .r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ · = (.r‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝐻)) | ||
| Theorem | resv0g 33430 | 0g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 0 = (0g‘𝐻)) | ||
| Theorem | resv1r 33431 | 1r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) & ⊢ 1 = (1r‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 1 = (1r‘𝐻)) | ||
| Theorem | resvcmn 33432 | Scalar restriction preserves commutative monoids. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐻 = (𝐺 ↾v 𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐺 ∈ CMnd ↔ 𝐻 ∈ CMnd)) | ||
| Theorem | gzcrng 33433 | The gaussian integers form a commutative ring. (Contributed by Thierry Arnoux, 18-Mar-2018.) |
| ⊢ (ℂfld ↾s ℤ[i]) ∈ CRing | ||
| Theorem | cnfldfld 33434 | The complex numbers form a field. (Contributed by Thierry Arnoux, 6-Jul-2025.) |
| ⊢ ℂfld ∈ Field | ||
| Theorem | reofld 33435 | The real numbers form an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
| ⊢ ℝfld ∈ oField | ||
| Theorem | nn0omnd 33436 | The nonnegative integers form an ordered monoid. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| ⊢ (ℂfld ↾s ℕ0) ∈ oMnd | ||
| Theorem | gsumind 33437 | 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 33438 | The field of the real numbers is Archimedean. See also arch 12410. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
| ⊢ ℝfld ∈ Archi | ||
| Theorem | nn0archi 33439 | The monoid of the nonnegative integers is Archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018.) |
| ⊢ (ℂfld ↾s ℕ0) ∈ Archi | ||
| Theorem | xrge0slmod 33440 | 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 33441* | The kernel of a quotient map. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝑉 = (Base‘𝑀) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥](𝑀 ~QG 𝐺)) & ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺)) & ⊢ 0 = (0g‘𝑁) ⇒ ⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → (◡𝐹 “ { 0 }) = 𝐺) | ||
| Theorem | eqgvscpbl 33442 | 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 33443* | 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 33444 | 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 33445* | 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 33446* | 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 33447* | 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 33448* | 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 33449* | 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 33450 | 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 33451* | 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 33452 | 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 | ecxpid 33453 | The equivalence class of a cartesian product is the whole set. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
| ⊢ (𝑋 ∈ 𝐴 → [𝑋](𝐴 × 𝐴) = 𝐴) | ||
| Theorem | qsxpid 33454 | The quotient set of a cartesian product is trivial. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
| ⊢ (𝐴 ≠ ∅ → (𝐴 / (𝐴 × 𝐴)) = {𝐴}) | ||
| Theorem | qusxpid 33455 | 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 33456 | The quotient of a group 𝐺 by itself is trivial. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐵)) ⇒ ⊢ (𝐺 ∈ Grp → (Base‘𝑄) = {𝐵}) | ||
| Theorem | qustrivr 33457 | Converse of qustriv 33456. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐻)) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐻 ∈ (SubGrp‘𝐺) ∧ (Base‘𝑄) = {𝐻}) → 𝐻 = 𝐵) | ||
| Theorem | znfermltl 33458 | Fermat's little theorem in ℤ/nℤ. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑃) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ ↑ = (.g‘(mulGrp‘𝑍)) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ 𝐵) → (𝑃 ↑ 𝐴) = 𝐴) | ||
| Theorem | islinds5 33459* | 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 33460* | Variation on ellspd 21769. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ 𝑁 = (LSpan‘𝑀) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 0 = (0g‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝑉 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝑁‘𝑉) ↔ ∃𝑎 ∈ (𝐾 ↑m 𝑉)(𝑎 finSupp 0 ∧ 𝑋 = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣) · 𝑣)))))) | ||
| Theorem | 0ellsp 33461 | Zero is in all spans. (Contributed by Thierry Arnoux, 8-May-2023.) |
| ⊢ 0 = (0g‘𝑊) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑆 ⊆ 𝐵) → 0 ∈ (𝑁‘𝑆)) | ||
| Theorem | 0nellinds 33462 | The group identity cannot be an element of an independent set. (Contributed by Thierry Arnoux, 8-May-2023.) |
| ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) → ¬ 0 ∈ 𝐹) | ||
| Theorem | rspsnid 33463 | A principal ideal contains the element that generates it. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ (𝐾‘{𝐺})) | ||
| Theorem | elrsp 33464* | 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 33465 | 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 33466* | In a principal ideal ring, ideals are principal. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ LPIR) & ⊢ (𝜑 → 𝐽 ∈ 𝐼) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐽 = (𝐾‘{𝑥})) | ||
| Theorem | rspidlid 33467 | The ideal span of an ideal is the ideal itself. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝐾‘𝐼) = 𝐼) | ||
| Theorem | pidlnz 33468 | A principal ideal generated by a nonzero element is not the zero ideal. (Contributed by Thierry Arnoux, 11-Apr-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝐾‘{𝑋}) ≠ { 0 }) | ||
| Theorem | lbslsp 33469* | 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 33470 | 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 33471 | 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 33472* | 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 33473 | 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 33474* | 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 33475* | 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 33476 | 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 33477* | 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 33478* | A reformulation of dvdsruasso 33477. (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 33479 | 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 33480 | 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 33481 | 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 33482* | Membership in a sumset with a singleton for a group operation. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝐴 ⊕ {𝑋}) ↔ ∃𝑥 ∈ 𝐴 𝑍 = (𝑥 + 𝑋))) | ||
| Theorem | lsmsnorb 33483* | The sumset of a group with a single element is the element's orbit by the group action. See gaorb 19248. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ ∃𝑔 ∈ 𝐴 (𝑔 + 𝑥) = 𝑦)} & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ⊕ {𝑋}) = [𝑋] ∼ ) | ||
| Theorem | lsmsnorb2 33484* | The sumset of a single element with a group is the element's orbit by the group action. See gaorb 19248. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ ∃𝑔 ∈ 𝐴 (𝑥 + 𝑔) = 𝑦)} & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ({𝑋} ⊕ 𝐴) = [𝑋] ∼ ) | ||
| Theorem | elringlsm 33485* | Membership in a product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ × = (LSSum‘𝐺) & ⊢ (𝜑 → 𝐸 ⊆ 𝐵) & ⊢ (𝜑 → 𝐹 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝐸 × 𝐹) ↔ ∃𝑥 ∈ 𝐸 ∃𝑦 ∈ 𝐹 𝑍 = (𝑥 · 𝑦))) | ||
| Theorem | elringlsmd 33486 | Membership in a product of two subsets of a ring, one direction. (Contributed by Thierry Arnoux, 13-Apr-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ × = (LSSum‘𝐺) & ⊢ (𝜑 → 𝐸 ⊆ 𝐵) & ⊢ (𝜑 → 𝐹 ⊆ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ (𝜑 → 𝑌 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ (𝐸 × 𝐹)) | ||
| Theorem | ringlsmss 33487 | Closure of the product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ × = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐸 ⊆ 𝐵) & ⊢ (𝜑 → 𝐹 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐸 × 𝐹) ⊆ 𝐵) | ||
| Theorem | ringlsmss1 33488 | 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 33489 | 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 33490 | 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 33491 | 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 33492 | 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 33493 | The sum of two ideals is an ideal. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⊕ = (LSSum‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝐽 ∈ (LIdeal‘𝑅)) ⇒ ⊢ (𝜑 → (𝐼 ⊕ 𝐽) ∈ (LIdeal‘𝑅)) | ||
| Theorem | lsmssass 33494 | Group sum is associative, subset version (see lsmass 19610). (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝑅 ⊆ 𝐵) & ⊢ (𝜑 → 𝑇 ⊆ 𝐵) & ⊢ (𝜑 → 𝑈 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ((𝑅 ⊕ 𝑇) ⊕ 𝑈) = (𝑅 ⊕ (𝑇 ⊕ 𝑈))) | ||
| Theorem | grplsm0l 33495 | Sumset with the identity singleton is the original set. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → ({ 0 } ⊕ 𝐴) = 𝐴) | ||
| Theorem | grplsmid 33496 | The direct sum of an element 𝑋 of a subgroup 𝐴 is the subgroup itself. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
| ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝐴) → ({𝑋} ⊕ 𝐴) = 𝐴) | ||
| Theorem | quslsm 33497 | 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 33498* | 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 33499 | The identity element of a quotient group. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) ⇒ ⊢ (𝑁 ∈ (NrmSGrp‘𝐺) → (0g‘𝑄) = 𝑁) | ||
| Theorem | qusima 33500* | 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‘𝐺)) ⇒ ⊢ (𝜑 → (𝐸‘𝐻) = (𝐹 “ 𝐻)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |