![]() |
Metamath
Proof Explorer Theorem List (p. 411 of 478) | < 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: | ![]() (1-30149) |
![]() (30150-31672) |
![]() (31673-47754) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fnimasnd 41001 | The image of a function by a singleton whose element is in the domain of the function. (Contributed by Steven Nguyen, 7-Jun-2023.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝑆 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹 “ {𝑆}) = {(𝐹‘𝑆)}) | ||
Theorem | fvmptd4 41002* | Deduction version of fvmpt 6994 (where the substitution hypothesis does not have the antecedent 𝜑). (Contributed by SN, 26-Jul-2024.) |
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶) | ||
Theorem | eqresfnbd 41003 | Property of being the restriction of a function. Note that this is closer to funssres 6589 than fnssres 6670. (Contributed by SN, 11-Mar-2025.) |
⊢ (𝜑 → 𝐹 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑅 = (𝐹 ↾ 𝐴) ↔ (𝑅 Fn 𝐴 ∧ 𝑅 ⊆ 𝐹))) | ||
Theorem | f1o2d2 41004* | Sufficient condition for a binary function expressed in maps-to notation to be bijective. (Contributed by SN, 11-Mar-2025.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → 𝐼 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → 𝐽 ∈ 𝐵) & ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐷)) → ((𝑥 = 𝐼 ∧ 𝑦 = 𝐽) ↔ 𝑧 = 𝐶)) ⇒ ⊢ (𝜑 → 𝐹:(𝐴 × 𝐵)–1-1-onto→𝐷) | ||
Theorem | fmpocos 41005* | Composition of two functions. Variation of fmpoco 8076 with more context in the substitution hypothesis for 𝑇. (Contributed by SN, 14-Mar-2025.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ 𝐶) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅)) & ⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝐶 ↦ 𝑆)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ⦋𝑅 / 𝑧⦌𝑆 = 𝑇) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑇)) | ||
Theorem | ovmpogad 41006* | Value of an operation given by a maps-to rule. Deduction form of ovmpoga 7557. (Contributed by SN, 14-Mar-2025.) |
⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆) | ||
Theorem | ofun 41007 | A function operation of unions of disjoint functions is a union of function operations. (Contributed by SN, 16-Jun-2024.) |
⊢ (𝜑 → 𝐴 Fn 𝑀) & ⊢ (𝜑 → 𝐵 Fn 𝑀) & ⊢ (𝜑 → 𝐶 Fn 𝑁) & ⊢ (𝜑 → 𝐷 Fn 𝑁) & ⊢ (𝜑 → 𝑀 ∈ 𝑉) & ⊢ (𝜑 → 𝑁 ∈ 𝑊) & ⊢ (𝜑 → (𝑀 ∩ 𝑁) = ∅) ⇒ ⊢ (𝜑 → ((𝐴 ∪ 𝐶) ∘f 𝑅(𝐵 ∪ 𝐷)) = ((𝐴 ∘f 𝑅𝐵) ∪ (𝐶 ∘f 𝑅𝐷))) | ||
Theorem | dfqs2 41008* | Alternate definition of quotient set. (Contributed by Steven Nguyen, 7-Jun-2023.) |
⊢ (𝐴 / 𝑅) = ran (𝑥 ∈ 𝐴 ↦ [𝑥]𝑅) | ||
Theorem | dfqs3 41009* | Alternate definition of quotient set. (Contributed by Steven Nguyen, 7-Jun-2023.) |
⊢ (𝐴 / 𝑅) = ∪ 𝑥 ∈ 𝐴 {[𝑥]𝑅} | ||
Theorem | qseq12d 41010 | Equality theorem for quotient set, deduction form. (Contributed by Steven Nguyen, 30-Apr-2023.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 / 𝐶) = (𝐵 / 𝐷)) | ||
Theorem | qsalrel 41011* | The quotient set is equal to the singleton of 𝐴 when all elements are related and 𝐴 is nonempty. (Contributed by SN, 8-Jun-2023.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∼ 𝑦) & ⊢ (𝜑 → ∼ Er 𝐴) & ⊢ (𝜑 → 𝑁 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐴 / ∼ ) = {𝐴}) | ||
Theorem | fsuppfund 41012 | A finitely supported function is a function. (Contributed by SN, 8-Mar-2025.) |
⊢ (𝜑 → 𝐹 finSupp 𝑍) ⇒ ⊢ (𝜑 → Fun 𝐹) | ||
Theorem | fsuppsssuppgd 41013 | If the support of a function is a subset of a finite support, it is finite. Deduction associated with fsuppsssupp 9375. (Contributed by SN, 6-Mar-2025.) |
⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → 𝐹 finSupp 𝑂) & ⊢ (𝜑 → (𝐺 supp 𝑍) ⊆ (𝐹 supp 𝑂)) ⇒ ⊢ (𝜑 → 𝐺 finSupp 𝑍) | ||
Theorem | fsuppss 41014 | A subset of a finitely supported function is a finitely supported function. (Contributed by SN, 8-Mar-2025.) |
⊢ (𝜑 → 𝐹 ⊆ 𝐺) & ⊢ (𝜑 → 𝐺 finSupp 𝑍) ⇒ ⊢ (𝜑 → 𝐹 finSupp 𝑍) | ||
Theorem | elmapssresd 41015 | A restricted mapping is a mapping. EDITORIAL: Could be used to shorten elpm2r 8835 with some reordering involving mapsspm 8866. (Contributed by SN, 11-Mar-2025.) |
⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m 𝐶)) & ⊢ (𝜑 → 𝐷 ⊆ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ↾ 𝐷) ∈ (𝐵 ↑m 𝐷)) | ||
Theorem | mapcod 41016 | Compose two mappings. (Contributed by SN, 11-Mar-2025.) |
⊢ (𝜑 → 𝐹 ∈ (𝐴 ↑m 𝐵)) & ⊢ (𝜑 → 𝐺 ∈ (𝐵 ↑m 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺) ∈ (𝐴 ↑m 𝐶)) | ||
Theorem | fzosumm1 41017* | Separate out the last term in a finite sum. (Contributed by Steven Nguyen, 22-Aug-2023.) |
⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝐴 ∈ ℂ) & ⊢ (𝑘 = (𝑁 − 1) → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝐴 = (Σ𝑘 ∈ (𝑀..^(𝑁 − 1))𝐴 + 𝐵)) | ||
Theorem | ccatcan2d 41018 | Cancellation law for concatenation. (Contributed by SN, 6-Sep-2023.) |
⊢ (𝜑 → 𝐴 ∈ Word 𝑉) & ⊢ (𝜑 → 𝐵 ∈ Word 𝑉) & ⊢ (𝜑 → 𝐶 ∈ Word 𝑉) ⇒ ⊢ (𝜑 → ((𝐴 ++ 𝐶) = (𝐵 ++ 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | nelsubginvcld 41019 | The inverse of a non-subgroup-member is a non-subgroup-member. (Contributed by Steven Nguyen, 15-Apr-2023.) |
⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑆)) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ (𝜑 → (𝑁‘𝑋) ∈ (𝐵 ∖ 𝑆)) | ||
Theorem | nelsubgcld 41020 | A non-subgroup-member plus a subgroup member is a non-subgroup-member. (Contributed by Steven Nguyen, 15-Apr-2023.) |
⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑆)) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝐵 ∖ 𝑆)) | ||
Theorem | nelsubgsubcld 41021 | A non-subgroup-member minus a subgroup member is a non-subgroup-member. (Contributed by Steven Nguyen, 15-Apr-2023.) |
⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝑆)) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ − = (-g‘𝐺) ⇒ ⊢ (𝜑 → (𝑋 − 𝑌) ∈ (𝐵 ∖ 𝑆)) | ||
Theorem | rnasclg 41022 | The set of injected scalars is also interpretable as the span of the identity. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 𝐴 = (algSc‘𝑊) & ⊢ 1 = (1r‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) → ran 𝐴 = (𝑁‘{ 1 })) | ||
Theorem | frlmfielbas 41023 | The vectors of a finite free module are the functions from 𝐼 to 𝑁. (Contributed by SN, 31-Aug-2023.) |
⊢ 𝐹 = (𝑅 freeLMod 𝐼) & ⊢ 𝑁 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin) → (𝑋 ∈ 𝐵 ↔ 𝑋:𝐼⟶𝑁)) | ||
Theorem | frlmfzwrd 41024 | A vector of a module with indices from 0 to 𝑁 is a word over the scalars of the module. (Contributed by SN, 31-Aug-2023.) |
⊢ 𝑊 = (𝐾 freeLMod (0...𝑁)) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑆 = (Base‘𝐾) ⇒ ⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ Word 𝑆) | ||
Theorem | frlmfzowrd 41025 | A vector of a module with indices from 0 to 𝑁 − 1 is a word over the scalars of the module. (Contributed by SN, 31-Aug-2023.) |
⊢ 𝑊 = (𝐾 freeLMod (0..^𝑁)) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑆 = (Base‘𝐾) ⇒ ⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ Word 𝑆) | ||
Theorem | frlmfzolen 41026 | The dimension of a vector of a module with indices from 0 to 𝑁 − 1. (Contributed by SN, 1-Sep-2023.) |
⊢ 𝑊 = (𝐾 freeLMod (0..^𝑁)) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑆 = (Base‘𝐾) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → (♯‘𝑋) = 𝑁) | ||
Theorem | frlmfzowrdb 41027 | The vectors of a module with indices 0 to 𝑁 − 1 are the length- 𝑁 words over the scalars of the module. (Contributed by SN, 1-Sep-2023.) |
⊢ 𝑊 = (𝐾 freeLMod (0..^𝑁)) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑆 = (Base‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑋 ∈ 𝐵 ↔ (𝑋 ∈ Word 𝑆 ∧ (♯‘𝑋) = 𝑁))) | ||
Theorem | frlmfzoccat 41028 | The concatenation of two vectors of dimension 𝑁 and 𝑀 forms a vector of dimension 𝑁 + 𝑀. (Contributed by SN, 31-Aug-2023.) |
⊢ 𝑊 = (𝐾 freeLMod (0..^𝐿)) & ⊢ 𝑋 = (𝐾 freeLMod (0..^𝑀)) & ⊢ 𝑌 = (𝐾 freeLMod (0..^𝑁)) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐶 = (Base‘𝑋) & ⊢ 𝐷 = (Base‘𝑌) & ⊢ (𝜑 → 𝐾 ∈ 𝑍) & ⊢ (𝜑 → (𝑀 + 𝑁) = 𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑈 ∈ 𝐶) & ⊢ (𝜑 → 𝑉 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑈 ++ 𝑉) ∈ 𝐵) | ||
Theorem | frlmvscadiccat 41029 | Scalar multiplication distributes over concatenation. (Contributed by SN, 6-Sep-2023.) |
⊢ 𝑊 = (𝐾 freeLMod (0..^𝐿)) & ⊢ 𝑋 = (𝐾 freeLMod (0..^𝑀)) & ⊢ 𝑌 = (𝐾 freeLMod (0..^𝑁)) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐶 = (Base‘𝑋) & ⊢ 𝐷 = (Base‘𝑌) & ⊢ (𝜑 → 𝐾 ∈ 𝑍) & ⊢ (𝜑 → (𝑀 + 𝑁) = 𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑈 ∈ 𝐶) & ⊢ (𝜑 → 𝑉 ∈ 𝐷) & ⊢ 𝑂 = ( ·𝑠 ‘𝑊) & ⊢ ∙ = ( ·𝑠 ‘𝑋) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 𝑆 = (Base‘𝐾) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐴𝑂(𝑈 ++ 𝑉)) = ((𝐴 ∙ 𝑈) ++ (𝐴 · 𝑉))) | ||
Theorem | grpasscan2d 41030 | An associative cancellation law for groups. (Contributed by SN, 29-Jan-2025.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + (𝑁‘𝑌)) + 𝑌) = 𝑋) | ||
Theorem | grpcominv1 41031 | If two elements commute, then they commute with each other's inverses (case of the first element commuting with the inverse of the second element). (Contributed by SN, 29-Jan-2025.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋)) ⇒ ⊢ (𝜑 → (𝑋 + (𝑁‘𝑌)) = ((𝑁‘𝑌) + 𝑋)) | ||
Theorem | grpcominv2 41032 | If two elements commute, then they commute with each other's inverses (case of the second element commuting with the inverse of the first element). (Contributed by SN, 1-Feb-2025.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋)) ⇒ ⊢ (𝜑 → (𝑌 + (𝑁‘𝑋)) = ((𝑁‘𝑋) + 𝑌)) | ||
Theorem | finsubmsubg 41033 | A submonoid of a finite group is a subgroup. This does not extend to infinite groups, as the submonoid ℕ0 of the group (ℤ, + ) shows. Note also that the union of a submonoid and its inverses need not be a submonoid, as the submonoid (ℕ0 ∖ {1}) of the group (ℤ, + ) shows: 3 is in that submonoid, -2 is the inverse of 2, but 1 is not in their union. Or simply, the subgroup generated by (ℕ0 ∖ {1}) is ℤ, not (ℤ ∖ {1, -1}). (Contributed by SN, 31-Jan-2025.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺)) & ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) | ||
Theorem | ringlzd 41034 | The zero of a unital ring is a left-absorbing element. (Contributed by SN, 7-Mar-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ( 0 · 𝑋) = 0 ) | ||
Theorem | ringrzd 41035 | The zero of a unital ring is a right-absorbing element. (Contributed by SN, 7-Mar-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · 0 ) = 0 ) | ||
Theorem | crngcomd 41036 | Multiplication is commutative in a commutative ring. (Contributed by SN, 8-Mar-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) = (𝑌 · 𝑋)) | ||
Theorem | crng12d 41037 | Commutative/associative law that swaps the first two factors in a triple product. (Contributed by SN, 8-Mar-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · (𝑌 · 𝑍)) = (𝑌 · (𝑋 · 𝑍))) | ||
Theorem | imacrhmcl 41038 | The image of a commutative ring homomorphism is a commutative ring. (Contributed by SN, 10-Jan-2025.) |
⊢ 𝐶 = (𝑁 ↾s (𝐹 “ 𝑆)) & ⊢ (𝜑 → 𝐹 ∈ (𝑀 RingHom 𝑁)) & ⊢ (𝜑 → 𝑀 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑀)) ⇒ ⊢ (𝜑 → 𝐶 ∈ CRing) | ||
Theorem | rimrcl1 41039 | Reverse closure of a ring isomorphism. (Contributed by SN, 19-Feb-2025.) |
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝑅 ∈ Ring) | ||
Theorem | rimrcl2 41040 | Reverse closure of a ring isomorphism. (Contributed by SN, 19-Feb-2025.) |
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝑆 ∈ Ring) | ||
Theorem | rimcnv 41041 | The converse of a ring isomorphism is a ring isomorphism. (Contributed by SN, 10-Jan-2025.) |
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → ◡𝐹 ∈ (𝑆 RingIso 𝑅)) | ||
Theorem | rimco 41042 | The composition of ring isomorphisms is a ring isomorphism. (Contributed by SN, 17-Jan-2025.) |
⊢ ((𝐹 ∈ (𝑆 RingIso 𝑇) ∧ 𝐺 ∈ (𝑅 RingIso 𝑆)) → (𝐹 ∘ 𝐺) ∈ (𝑅 RingIso 𝑇)) | ||
Theorem | ricsym 41043 | Ring isomorphism is symmetric. (Contributed by SN, 10-Jan-2025.) |
⊢ (𝑅 ≃𝑟 𝑆 → 𝑆 ≃𝑟 𝑅) | ||
Theorem | rictr 41044 | Ring isomorphism is transitive. (Contributed by SN, 17-Jan-2025.) |
⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑆 ≃𝑟 𝑇) → 𝑅 ≃𝑟 𝑇) | ||
Theorem | riccrng1 41045 | Ring isomorphism preserves (multiplicative) commutativity. (Contributed by SN, 10-Jan-2025.) |
⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ CRing) → 𝑆 ∈ CRing) | ||
Theorem | riccrng 41046 | A ring is commutative if and only if an isomorphic ring is commutative. (Contributed by SN, 10-Jan-2025.) |
⊢ (𝑅 ≃𝑟 𝑆 → (𝑅 ∈ CRing ↔ 𝑆 ∈ CRing)) | ||
Theorem | drnginvrn0d 41047 | A multiplicative inverse in a division ring is nonzero. (recne0d 11980 analog). (Contributed by SN, 14-Aug-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝐼‘𝑋) ≠ 0 ) | ||
Theorem | drngmulcanad 41048 | Cancellation of a nonzero factor on the left for multiplication. (mulcanad 11845 analog). (Contributed by SN, 14-Aug-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ≠ 0 ) & ⊢ (𝜑 → (𝑍 · 𝑋) = (𝑍 · 𝑌)) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | drngmulcan2ad 41049 | Cancellation of a nonzero factor on the right for multiplication. (mulcan2ad 11846 analog). (Contributed by SN, 14-Aug-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ≠ 0 ) & ⊢ (𝜑 → (𝑋 · 𝑍) = (𝑌 · 𝑍)) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | drnginvmuld 41050 | Inverse of a nonzero product. (Contributed by SN, 14-Aug-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑌 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝐼‘(𝑋 · 𝑌)) = ((𝐼‘𝑌) · (𝐼‘𝑋))) | ||
Theorem | ricdrng1 41051 | A ring isomorphism maps a division ring to a division ring. (Contributed by SN, 18-Feb-2025.) |
⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ DivRing) → 𝑆 ∈ DivRing) | ||
Theorem | ricdrng 41052 | A ring is a division ring if and only if an isomorphic ring is a division ring. (Contributed by SN, 18-Feb-2025.) |
⊢ (𝑅 ≃𝑟 𝑆 → (𝑅 ∈ DivRing ↔ 𝑆 ∈ DivRing)) | ||
Theorem | lmodvscld 41053 | Closure of scalar product for a left module. (Contributed by SN, 15-Mar-2025.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑅 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑅 · 𝑋) ∈ 𝑉) | ||
Theorem | flddrngd 41054 | A field is a division ring. (Contributed by SN, 17-Jan-2025.) |
⊢ (𝜑 → 𝑅 ∈ Field) ⇒ ⊢ (𝜑 → 𝑅 ∈ DivRing) | ||
Theorem | ricfld 41055 | A ring is a field if and only if an isomorphic ring is a field. (Contributed by SN, 18-Feb-2025.) |
⊢ (𝑅 ≃𝑟 𝑆 → (𝑅 ∈ Field ↔ 𝑆 ∈ Field)) | ||
Theorem | lvecgrp 41056 | A vector space is a group. (Contributed by SN, 28-May-2023.) |
⊢ (𝑊 ∈ LVec → 𝑊 ∈ Grp) | ||
Theorem | lvecgrpd 41057 | A vector space is a group. (Contributed by SN, 16-May-2024.) |
⊢ (𝜑 → 𝑊 ∈ LVec) ⇒ ⊢ (𝜑 → 𝑊 ∈ Grp) | ||
Theorem | lvecring 41058 | The scalar component of a vector space is a ring. (Contributed by SN, 28-May-2023.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec → 𝐹 ∈ Ring) | ||
Theorem | frlm0vald 41059 | All coordinates of the zero vector are zero. (Contributed by SN, 14-Aug-2024.) |
⊢ 𝐹 = (𝑅 freeLMod 𝐼) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝐽 ∈ 𝐼) ⇒ ⊢ (𝜑 → ((0g‘𝐹)‘𝐽) = 0 ) | ||
Theorem | frlmsnic 41060* | Given a free module with a singleton as the index set, that is, a free module of one-dimensional vectors, the function that maps each vector to its coordinate is a module isomorphism from that module to its ring of scalars seen as a module. (Contributed by Steven Nguyen, 18-Aug-2023.) |
⊢ 𝑊 = (𝐾 freeLMod {𝐼}) & ⊢ 𝐹 = (𝑥 ∈ (Base‘𝑊) ↦ (𝑥‘𝐼)) ⇒ ⊢ ((𝐾 ∈ Ring ∧ 𝐼 ∈ V) → 𝐹 ∈ (𝑊 LMIso (ringLMod‘𝐾))) | ||
Theorem | uvccl 41061 | A unit vector is a vector. (Contributed by Steven Nguyen, 16-Jul-2023.) |
⊢ 𝑈 = (𝑅 unitVec 𝐼) & ⊢ 𝑌 = (𝑅 freeLMod 𝐼) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼) → (𝑈‘𝐽) ∈ 𝐵) | ||
Theorem | uvcn0 41062 | A unit vector is nonzero. (Contributed by Steven Nguyen, 16-Jul-2023.) |
⊢ 𝑈 = (𝑅 unitVec 𝐼) & ⊢ 𝑌 = (𝑅 freeLMod 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 0 = (0g‘𝑌) ⇒ ⊢ ((𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼) → (𝑈‘𝐽) ≠ 0 ) | ||
Theorem | pwselbasr 41063 | The reverse direction of pwselbasb 17430: a function between the index and base set of a structure is an element of the structure power. (Contributed by SN, 29-Jul-2024.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑉 = (Base‘𝑌) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) & ⊢ (𝜑 → 𝑋:𝐼⟶𝐵) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝑉) | ||
Theorem | pwsgprod 41064* | Finite products in a power structure are taken componentwise. Compare pwsgsum 19842. (Contributed by SN, 30-Jul-2024.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑌) & ⊢ 𝑀 = (mulGrp‘𝑌) & ⊢ 𝑇 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽)) → 𝑈 ∈ 𝐵) & ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) finSupp 1 ) ⇒ ⊢ (𝜑 → (𝑀 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ (𝑇 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)))) | ||
Theorem | psrbagres 41065* | Restrict a bag of variables in 𝐼 to a bag of variables in 𝐽 ⊆ 𝐼. (Contributed by SN, 10-Mar-2025.) |
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝐸 = {𝑔 ∈ (ℕ0 ↑m 𝐽) ∣ (◡𝑔 “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐽) ∈ 𝐸) | ||
Theorem | mpllmodd 41066 | The polynomial ring is a left module. (Contributed by SN, 12-Mar-2025.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝑃 ∈ LMod) | ||
Theorem | mplringd 41067 | The polynomial ring is a ring. (Contributed by SN, 7-Feb-2025.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → 𝑃 ∈ Ring) | ||
Theorem | mplcrngd 41068 | The polynomial ring is a commutative ring. (Contributed by SN, 7-Feb-2025.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → 𝑃 ∈ CRing) | ||
Theorem | mplsubrgcl 41069 | An element of a polynomial algebra over a subring is an element of the polynomial algebra. (Contributed by SN, 9-Feb-2025.) |
⊢ 𝑊 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑃 = (𝐼 mPoly 𝑆) & ⊢ 𝐶 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐹 ∈ 𝐶) | ||
Theorem | mhmcompl 41070 | The composition of a monoid homomorphism and a polynomial is a polynomial. (Contributed by SN, 7-Feb-2025.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑄 = (𝐼 mPoly 𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Base‘𝑄) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ (𝑅 MndHom 𝑆)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ 𝐶) | ||
Theorem | rhmmpllem1 41071* | Lemma for rhmmpl 41075. A subproof of psrmulcllem 21488. (Contributed by SN, 8-Feb-2025.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅)) & ⊢ (𝜑 → 𝑌:𝐷⟶(Base‘𝑅)) ⇒ ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) finSupp (0g‘𝑅)) | ||
Theorem | rhmmpllem2 41072* | Lemma for rhmmpl 41075. A subproof of psrmulcllem 21488. (Contributed by SN, 8-Feb-2025.) |
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅)) & ⊢ (𝜑 → 𝑌:𝐷⟶(Base‘𝑅)) ⇒ ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))) ∈ (Base‘𝑅)) | ||
Theorem | mhmcoaddmpl 41073 | Show that the ring homomorphism in rhmmpl 41075 preserves addition. (Contributed by SN, 8-Feb-2025.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑄 = (𝐼 mPoly 𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Base‘𝑄) & ⊢ + = (+g‘𝑃) & ⊢ ✚ = (+g‘𝑄) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ (𝑅 MndHom 𝑆)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐻 ∘ (𝐹 + 𝐺)) = ((𝐻 ∘ 𝐹) ✚ (𝐻 ∘ 𝐺))) | ||
Theorem | rhmcomulmpl 41074 | Show that the ring homomorphism in rhmmpl 41075 preserves multiplication. (Contributed by SN, 8-Feb-2025.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑄 = (𝐼 mPoly 𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Base‘𝑄) & ⊢ · = (.r‘𝑃) & ⊢ ∙ = (.r‘𝑄) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐻 ∘ (𝐹 · 𝐺)) = ((𝐻 ∘ 𝐹) ∙ (𝐻 ∘ 𝐺))) | ||
Theorem | rhmmpl 41075* | Provide a ring homomorphism between two polynomial algebras over their respective base rings given a ring homomorphism between the two base rings. Compare pwsco2rhm 20267. TODO: Currently mhmvlin 21881 would have to be moved up. Investigate the usefulness of surrounding theorems like mndvcl 21875 and the difference between mhmvlin 21881, ofco 7688, and ofco2 21935. (Contributed by SN, 8-Feb-2025.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝑄 = (𝐼 mPoly 𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ (𝐻 ∘ 𝑝)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑄)) | ||
Theorem | mplascl0 41076 | The zero scalar as a polynomial. (Contributed by SN, 23-Nov-2024.) |
⊢ 𝑊 = (𝐼 mPoly 𝑅) & ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝑂 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (𝐴‘𝑂) = 0 ) | ||
Theorem | mplascl1 41077 | The one scalar as a polynomial. (Contributed by SN, 12-Mar-2025.) |
⊢ 𝑊 = (𝐼 mPoly 𝑅) & ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝑂 = (1r‘𝑅) & ⊢ 1 = (1r‘𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (𝐴‘𝑂) = 1 ) | ||
Theorem | mplmapghm 41078* | The function 𝐻 mapping polynomials 𝑝 to their coefficient given a bag of variables 𝐹 is a group homomorphism. (Contributed by SN, 15-Mar-2025.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝐻 = (𝑝 ∈ 𝐵 ↦ (𝑝‘𝐹)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Grp) & ⊢ (𝜑 → 𝐹 ∈ 𝐷) ⇒ ⊢ (𝜑 → 𝐻 ∈ (𝑃 GrpHom 𝑅)) | ||
Theorem | evl0 41079 | The zero polynomial evaluates to zero. (Contributed by SN, 23-Nov-2024.) |
⊢ 𝑄 = (𝐼 eval 𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑊 = (𝐼 mPoly 𝑅) & ⊢ 𝑂 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → (𝑄‘ 0 ) = ((𝐵 ↑m 𝐼) × {𝑂})) | ||
Theorem | evlscl 41080 | A polynomial over the ring 𝑅 evaluates to an element in 𝑅. (Contributed by SN, 12-Mar-2025.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑅)‘𝑆) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑅 ↾s 𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → ((𝑄‘𝐹)‘𝐴) ∈ 𝐾) | ||
Theorem | evlsval3 41081* | Give a formula for the polynomial evaluation homomorphism. (Contributed by SN, 26-Jul-2024.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝑇 = (𝑆 ↑s (𝐾 ↑m 𝐼)) & ⊢ 𝑀 = (mulGrp‘𝑇) & ⊢ ↑ = (.g‘𝑀) & ⊢ · = (.r‘𝑇) & ⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑇 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑀 Σg (𝑏 ∘f ↑ 𝐺)))))) & ⊢ 𝐹 = (𝑥 ∈ 𝑅 ↦ ((𝐾 ↑m 𝐼) × {𝑥})) & ⊢ 𝐺 = (𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥))) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) ⇒ ⊢ (𝜑 → 𝑄 = 𝐸) | ||
Theorem | evlsvval 41082* | Give a formula for the evaluation of a polynomial. (Contributed by SN, 9-Feb-2025.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝑇 = (𝑆 ↑s (𝐾 ↑m 𝐼)) & ⊢ 𝑀 = (mulGrp‘𝑇) & ⊢ ↑ = (.g‘𝑀) & ⊢ · = (.r‘𝑇) & ⊢ 𝐹 = (𝑥 ∈ 𝑅 ↦ ((𝐾 ↑m 𝐼) × {𝑥})) & ⊢ 𝐺 = (𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥))) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑄‘𝐴) = (𝑇 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝐴‘𝑏)) · (𝑀 Σg (𝑏 ∘f ↑ 𝐺)))))) | ||
Theorem | evlsvvvallem 41083* | Lemma for evlsvvval 41085 akin to psrbagev2 21622. (Contributed by SN, 6-Mar-2025.) |
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑀 = (mulGrp‘𝑆) & ⊢ ↑ = (.g‘𝑀) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑀 Σg (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝐴‘𝑣)))) ∈ 𝐾) | ||
Theorem | evlsvvvallem2 41084* | Lemma for theorems using evlsvvval 41085. (Contributed by SN, 8-Mar-2025.) |
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑀 = (mulGrp‘𝑆) & ⊢ ↑ = (.g‘𝑀) & ⊢ · = (.r‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑣 ∈ 𝐼 ↦ ((𝑏‘𝑣) ↑ (𝐴‘𝑣)))))) finSupp (0g‘𝑆)) | ||
Theorem | evlsvvval 41085* | Give a formula for the evaluation of a polynomial given assignments from variables to values. This is the sum of the evaluations for each term (corresponding to a bag of variables), that is, the coefficient times the product of each variable raised to the corresponding power. (Contributed by SN, 5-Mar-2025.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑀 = (mulGrp‘𝑆) & ⊢ ↑ = (.g‘𝑀) & ⊢ · = (.r‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → ((𝑄‘𝐹)‘𝐴) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))))) | ||
Theorem | evlsscaval 41086 | Polynomial evaluation builder for a scalar. Compare evl1scad 21836. Note that scalar multiplication by 𝑋 is the same as vector multiplication by (𝐴‘𝑋) by asclmul1 21422. (Contributed by SN, 27-Jul-2024.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑅) & ⊢ (𝜑 → 𝐿 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → ((𝐴‘𝑋) ∈ 𝐵 ∧ ((𝑄‘(𝐴‘𝑋))‘𝐿) = 𝑋)) | ||
Theorem | evlsvarval 41087 | Polynomial evaluation builder for a variable. (Contributed by SN, 27-Jul-2024.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑉 = (𝐼 mVar 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → ((𝑉‘𝑋) ∈ 𝐵 ∧ ((𝑄‘(𝑉‘𝑋))‘𝐴) = (𝐴‘𝑋))) | ||
Theorem | evlsbagval 41088* | Polynomial evaluation builder for a bag of variables. EDITORIAL: This theorem should stay in my mathbox until there's another use, since 0 and 1 using 𝑈 instead of 𝑆 may not be convenient. (Contributed by SN, 29-Jul-2024.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝑊 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑀 = (mulGrp‘𝑆) & ⊢ ↑ = (.g‘𝑀) & ⊢ 0 = (0g‘𝑈) & ⊢ 1 = (1r‘𝑈) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝐹 = (𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝐵, 1 , 0 )) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝐹 ∈ 𝑊 ∧ ((𝑄‘𝐹)‘𝐴) = (𝑀 Σg (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝐴‘𝑣)))))) | ||
Theorem | evlsexpval 41089 | Polynomial evaluation builder for exponentiation. (Contributed by SN, 27-Jul-2024.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) & ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉)) & ⊢ ∙ = (.g‘(mulGrp‘𝑃)) & ⊢ ↑ = (.g‘(mulGrp‘𝑆)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝑁 ∙ 𝑀) ∈ 𝐵 ∧ ((𝑄‘(𝑁 ∙ 𝑀))‘𝐴) = (𝑁 ↑ 𝑉))) | ||
Theorem | evlsaddval 41090 | Polynomial evaluation builder for addition. (Contributed by SN, 27-Jul-2024.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) & ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊)) & ⊢ ✚ = (+g‘𝑃) & ⊢ + = (+g‘𝑆) ⇒ ⊢ (𝜑 → ((𝑀 ✚ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ✚ 𝑁))‘𝐴) = (𝑉 + 𝑊))) | ||
Theorem | evlsmulval 41091 | Polynomial evaluation builder for multiplication. (Contributed by SN, 27-Jul-2024.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) & ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊)) & ⊢ ∙ = (.r‘𝑃) & ⊢ · = (.r‘𝑆) ⇒ ⊢ (𝜑 → ((𝑀 ∙ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ∙ 𝑁))‘𝐴) = (𝑉 · 𝑊))) | ||
Theorem | evlsmaprhm 41092* | The function 𝐹 mapping polynomials 𝑝 to their subring evaluation at a given point 𝑋 is a ring homomorphism. Compare evls1maprhm 32703. (Contributed by SN, 12-Mar-2025.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑅)‘𝑆) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑅 ↾s 𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ ((𝑄‘𝑝)‘𝐴)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑅)) | ||
Theorem | evlsevl 41093 | Evaluation in a subring is the same as evaluation in the ring itself. (Contributed by SN, 9-Feb-2025.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝑂 = (𝐼 eval 𝑆) & ⊢ 𝑊 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑄‘𝐹) = (𝑂‘𝐹)) | ||
Theorem | evlcl 41094 | A polynomial over the ring 𝑅 evaluates to an element in 𝑅. (Contributed by SN, 12-Mar-2025.) |
⊢ 𝑄 = (𝐼 eval 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → ((𝑄‘𝐹)‘𝐴) ∈ 𝐾) | ||
Theorem | evlvvval 41095* | Give a formula for the evaluation of a polynomial given assignments from variables to values. (Contributed by SN, 5-Mar-2025.) |
⊢ 𝑄 = (𝐼 eval 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ ↑ = (.g‘𝑀) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → ((𝑄‘𝐹)‘𝐴) = (𝑅 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))))) | ||
Theorem | evlvvvallem 41096* | Lemma for theorems using evlvvval 41095. Version of evlsvvvallem2 41084 using df-evl 21618. (Contributed by SN, 11-Mar-2025.) |
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ ↑ = (.g‘𝑀) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑣 ∈ 𝐼 ↦ ((𝑏‘𝑣) ↑ (𝐴‘𝑣)))))) finSupp (0g‘𝑅)) | ||
Theorem | evladdval 41097 | Polynomial evaluation builder for addition. (Contributed by SN, 9-Feb-2025.) |
⊢ 𝑄 = (𝐼 eval 𝑆) & ⊢ 𝑃 = (𝐼 mPoly 𝑆) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ ✚ = (+g‘𝑃) & ⊢ + = (+g‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) & ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊)) ⇒ ⊢ (𝜑 → ((𝑀 ✚ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ✚ 𝑁))‘𝐴) = (𝑉 + 𝑊))) | ||
Theorem | evlmulval 41098 | Polynomial evaluation builder for multiplication. (Contributed by SN, 18-Feb-2025.) |
⊢ 𝑄 = (𝐼 eval 𝑆) & ⊢ 𝑃 = (𝐼 mPoly 𝑆) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ ∙ = (.r‘𝑃) & ⊢ · = (.r‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) & ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊)) ⇒ ⊢ (𝜑 → ((𝑀 ∙ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ∙ 𝑁))‘𝐴) = (𝑉 · 𝑊))) | ||
Theorem | selvcllem1 41099 | 𝑇 is an associative algebra. For simplicity, 𝐼 stands for (𝐼 ∖ 𝐽) and we have 𝐽 ∈ 𝑊 instead of 𝐽 ⊆ 𝐼. TODO-SN: In practice, this "simplification" makes the lemmas harder to use. (Contributed by SN, 15-Dec-2023.) |
⊢ 𝑈 = (𝐼 mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → 𝑇 ∈ AssAlg) | ||
Theorem | selvcllem2 41100 | 𝐷 is a ring homomorphism. (Contributed by SN, 15-Dec-2023.) |
⊢ 𝑈 = (𝐼 mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ 𝐶 = (algSc‘𝑇) & ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → 𝐷 ∈ (𝑅 RingHom 𝑇)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |