| Metamath
Proof Explorer Theorem List (p. 426 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | sn-sup2 42501* | sup2 12224 with exactly the same proof except for using sn-ltp1 42494 instead of ltp1 12107, saving ax-mulcom 11219. (Contributed by SN, 26-Jun-2024.) |
| ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | ||
| Theorem | sn-sup3d 42502* | sup3 12225 without ax-mulcom 11219, proven trivially from sn-sup2 42501. (Contributed by SN, 29-Jun-2025.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | ||
| Theorem | sn-suprcld 42503* | suprcld 12231 without ax-mulcom 11219, proven trivially from sn-sup3d 42502. (Contributed by SN, 29-Jun-2025.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈ ℝ) | ||
| Theorem | sn-suprubd 42504* | suprubd 12230 without ax-mulcom 11219, proven trivially from sn-suprcld 42503. (Contributed by SN, 29-Jun-2025.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ≤ sup(𝐴, ℝ, < )) | ||
| Theorem | sn-base0 42505 | Avoid axioms in base0 17252 by using the discouraged df-base 17248. This kind of axiom save is probably not worth it. (Contributed by SN, 16-Sep-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ∅ = (Base‘∅) | ||
| Theorem | nelsubginvcld 42506 | 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 42507 | 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 42508 | 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 42509 | 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 42510 | The vectors of a finite free module are the functions from 𝐼 to 𝑁. (Contributed by SN, 31-Aug-2023.) |
| ⊢ 𝐹 = (𝑅 freeLMod 𝐼) & ⊢ 𝑁 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝐹) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin) → (𝑋 ∈ 𝐵 ↔ 𝑋:𝐼⟶𝑁)) | ||
| Theorem | frlmfzwrd 42511 | 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 42512 | 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 42513 | 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 42514 | 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 42515 | 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 42516 | 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 42517 | An associative cancellation law for groups. (Contributed by SN, 29-Jan-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + (𝑁‘𝑌)) + 𝑌) = 𝑋) | ||
| Theorem | grpcominv1 42518 | 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 42519 | 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 42520 | 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 | opprmndb 42521 | A class is a monoid if and only if its opposite (ring) is a monoid. (Contributed by SN, 20-Jun-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ Mnd ↔ 𝑂 ∈ Mnd) | ||
| Theorem | opprgrpb 42522 | A class is a group if and only if its opposite (ring) is a group. (Contributed by SN, 20-Jun-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ Grp ↔ 𝑂 ∈ Grp) | ||
| Theorem | opprablb 42523 | A class is an Abelian group if and only if its opposite (ring) is an Abelian group. (Contributed by SN, 20-Jun-2025.) |
| ⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ Abel ↔ 𝑂 ∈ Abel) | ||
| Theorem | imacrhmcl 42524 | The image of a commutative ring homomorphism is a commutative ring. (Contributed by SN, 10-Jan-2025.) |
| ⊢ 𝐶 = (𝑁 ↾s (𝐹 “ 𝑆)) & ⊢ (𝜑 → 𝐹 ∈ (𝑀 RingHom 𝑁)) & ⊢ (𝜑 → 𝑀 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑀)) ⇒ ⊢ (𝜑 → 𝐶 ∈ CRing) | ||
| Theorem | rimrcl1 42525 | Reverse closure of a ring isomorphism. (Contributed by SN, 19-Feb-2025.) |
| ⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝑅 ∈ Ring) | ||
| Theorem | rimrcl2 42526 | Reverse closure of a ring isomorphism. (Contributed by SN, 19-Feb-2025.) |
| ⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝑆 ∈ Ring) | ||
| Theorem | rimcnv 42527 | The converse of a ring isomorphism is a ring isomorphism. (Contributed by SN, 10-Jan-2025.) |
| ⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → ◡𝐹 ∈ (𝑆 RingIso 𝑅)) | ||
| Theorem | rimco 42528 | The composition of ring isomorphisms is a ring isomorphism. (Contributed by SN, 17-Jan-2025.) |
| ⊢ ((𝐹 ∈ (𝑆 RingIso 𝑇) ∧ 𝐺 ∈ (𝑅 RingIso 𝑆)) → (𝐹 ∘ 𝐺) ∈ (𝑅 RingIso 𝑇)) | ||
| Theorem | ricsym 42529 | Ring isomorphism is symmetric. (Contributed by SN, 10-Jan-2025.) |
| ⊢ (𝑅 ≃𝑟 𝑆 → 𝑆 ≃𝑟 𝑅) | ||
| Theorem | rictr 42530 | Ring isomorphism is transitive. (Contributed by SN, 17-Jan-2025.) |
| ⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑆 ≃𝑟 𝑇) → 𝑅 ≃𝑟 𝑇) | ||
| Theorem | riccrng1 42531 | Ring isomorphism preserves (multiplicative) commutativity. (Contributed by SN, 10-Jan-2025.) |
| ⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ CRing) → 𝑆 ∈ CRing) | ||
| Theorem | riccrng 42532 | A ring is commutative if and only if an isomorphic ring is commutative. (Contributed by SN, 10-Jan-2025.) |
| ⊢ (𝑅 ≃𝑟 𝑆 → (𝑅 ∈ CRing ↔ 𝑆 ∈ CRing)) | ||
| Theorem | domnexpgn0cl 42533 | In a domain, a (nonnegative) power of a nonzero element is nonzero. (Contributed by SN, 6-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝑁 ↑ 𝑋) ∈ (𝐵 ∖ { 0 })) | ||
| Theorem | drnginvrn0d 42534 | A multiplicative inverse in a division ring is nonzero. (recne0d 12037 analog). (Contributed by SN, 14-Aug-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝐼‘𝑋) ≠ 0 ) | ||
| Theorem | drngmullcan 42535 | Cancellation of a nonzero factor on the left for multiplication. (mulcanad 11898 analog). (Contributed by SN, 14-Aug-2024.) (Proof shortened by SN, 25-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ≠ 0 ) & ⊢ (𝜑 → (𝑍 · 𝑋) = (𝑍 · 𝑌)) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
| Theorem | drngmulrcan 42536 | Cancellation of a nonzero factor on the right for multiplication. (mulcan2ad 11899 analog). (Contributed by SN, 14-Aug-2024.) (Proof shortened by SN, 25-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ≠ 0 ) & ⊢ (𝜑 → (𝑋 · 𝑍) = (𝑌 · 𝑍)) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
| Theorem | drnginvmuld 42537 | Inverse of a nonzero product. (Contributed by SN, 14-Aug-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑌 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝐼‘(𝑋 · 𝑌)) = ((𝐼‘𝑌) · (𝐼‘𝑋))) | ||
| Theorem | ricdrng1 42538 | A ring isomorphism maps a division ring to a division ring. (Contributed by SN, 18-Feb-2025.) |
| ⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ DivRing) → 𝑆 ∈ DivRing) | ||
| Theorem | ricdrng 42539 | 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 | ricfld 42540 | A ring is a field if and only if an isomorphic ring is a field. (Contributed by SN, 18-Feb-2025.) |
| ⊢ (𝑅 ≃𝑟 𝑆 → (𝑅 ∈ Field ↔ 𝑆 ∈ Field)) | ||
| Theorem | asclf1 42541* | Two ways of saying the scalar injection is one-to-one. (Contributed by SN, 3-Jul-2025.) |
| ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑁 = (0g‘𝑆) & ⊢ (𝜑 → 𝑊 ∈ Ring) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → (𝐴:𝐾–1-1→𝐵 ↔ ∀𝑠 ∈ 𝐾 ((𝐴‘𝑠) = 0 → 𝑠 = 𝑁))) | ||
| Theorem | abvexp 42542 | Move exponentiation in and out of absolute value. (Contributed by SN, 3-Jul-2025.) |
| ⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑅)) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝐹 ∈ 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐹‘(𝑁 ↑ 𝑋)) = ((𝐹‘𝑋)↑𝑁)) | ||
| Theorem | fimgmcyclem 42543* | Lemma for fimgmcyc 42544. (Contributed by SN, 7-Jul-2025.) |
| ⊢ (𝜑 → ∃𝑜 ∈ ℕ ∃𝑞 ∈ ℕ (𝑜 ≠ 𝑞 ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴))) ⇒ ⊢ (𝜑 → ∃𝑜 ∈ ℕ ∃𝑞 ∈ ℕ (𝑜 < 𝑞 ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴))) | ||
| Theorem | fimgmcyc 42544* | Version of odcl2 19583 for finite magmas: the multiples of an element 𝐴 ∈ 𝐵 are eventually periodic. (Contributed by SN, 3-Jul-2025.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ · = (.g‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ Mgm) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑜 ∈ ℕ ∃𝑝 ∈ ℕ (𝑜 · 𝐴) = ((𝑜 + 𝑝) · 𝐴)) | ||
| Theorem | fidomncyc 42545* | Version of odcl2 19583 for multiplicative groups of finite domains (that is, a finite monoid where nonzero elements are cancellable): one (1) is a multiple of any nonzero element. (Contributed by SN, 3-Jul-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ { 0 })) ⇒ ⊢ (𝜑 → ∃𝑛 ∈ ℕ (𝑛 ↑ 𝐴) = 1 ) | ||
| Theorem | fiabv 42546* | In a finite domain (a finite field), the only absolute value is the trivial one (abvtrivg 20834). (Contributed by SN, 3-Jul-2025.) |
| ⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑇 = (𝑥 ∈ 𝐵 ↦ if(𝑥 = 0 , 0, 1)) & ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → 𝐴 = {𝑇}) | ||
| Theorem | lvecgrp 42547 | A vector space is a group. (Contributed by SN, 28-May-2023.) |
| ⊢ (𝑊 ∈ LVec → 𝑊 ∈ Grp) | ||
| Theorem | lvecring 42548 | The scalar component of a vector space is a ring. (Contributed by SN, 28-May-2023.) |
| ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec → 𝐹 ∈ Ring) | ||
| Theorem | frlm0vald 42549 | All coordinates of the zero vector are zero. (Contributed by SN, 14-Aug-2024.) |
| ⊢ 𝐹 = (𝑅 freeLMod 𝐼) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝐽 ∈ 𝐼) ⇒ ⊢ (𝜑 → ((0g‘𝐹)‘𝐽) = 0 ) | ||
| Theorem | frlmsnic 42550* | 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 42551 | A unit vector is a vector. (Contributed by Steven Nguyen, 16-Jul-2023.) |
| ⊢ 𝑈 = (𝑅 unitVec 𝐼) & ⊢ 𝑌 = (𝑅 freeLMod 𝐼) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼) → (𝑈‘𝐽) ∈ 𝐵) | ||
| Theorem | uvcn0 42552 | A unit vector is nonzero. (Contributed by Steven Nguyen, 16-Jul-2023.) |
| ⊢ 𝑈 = (𝑅 unitVec 𝐼) & ⊢ 𝑌 = (𝑅 freeLMod 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 0 = (0g‘𝑌) ⇒ ⊢ ((𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼) → (𝑈‘𝐽) ≠ 0 ) | ||
| Theorem | pwselbasr 42553 | The reverse direction of pwselbasb 17533: 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 42554* | Finite products in a power structure are taken componentwise. Compare pwsgsum 20000. (Contributed by SN, 30-Jul-2024.) |
| ⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑌) & ⊢ 𝑀 = (mulGrp‘𝑌) & ⊢ 𝑇 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽)) → 𝑈 ∈ 𝐵) & ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) finSupp 1 ) ⇒ ⊢ (𝜑 → (𝑀 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ (𝑇 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)))) | ||
| Theorem | psrmnd 42555 | The ring of power series is a monoid. (Contributed by SN, 25-Apr-2025.) |
| ⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Mnd) ⇒ ⊢ (𝜑 → 𝑆 ∈ Mnd) | ||
| Theorem | psrbagres 42556* | 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 | mplcrngd 42557 | The polynomial ring is a commutative ring. (Contributed by SN, 7-Feb-2025.) |
| ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → 𝑃 ∈ CRing) | ||
| Theorem | mplsubrgcl 42558 | 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 | mhmcopsr 42559 | The composition of a monoid homomorphism and a power series is a power series. (Contributed by SN, 18-May-2025.) |
| ⊢ 𝑃 = (𝐼 mPwSer 𝑅) & ⊢ 𝑄 = (𝐼 mPwSer 𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Base‘𝑄) & ⊢ (𝜑 → 𝐻 ∈ (𝑅 MndHom 𝑆)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ 𝐶) | ||
| Theorem | mhmcoaddpsr 42560 | Show that the ring homomorphism in rhmpsr 42562 preserves addition. (Contributed by SN, 18-May-2025.) |
| ⊢ 𝑃 = (𝐼 mPwSer 𝑅) & ⊢ 𝑄 = (𝐼 mPwSer 𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Base‘𝑄) & ⊢ + = (+g‘𝑃) & ⊢ ✚ = (+g‘𝑄) & ⊢ (𝜑 → 𝐻 ∈ (𝑅 MndHom 𝑆)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐻 ∘ (𝐹 + 𝐺)) = ((𝐻 ∘ 𝐹) ✚ (𝐻 ∘ 𝐺))) | ||
| Theorem | rhmcomulpsr 42561 | Show that the ring homomorphism in rhmpsr 42562 preserves multiplication. (Contributed by SN, 18-May-2025.) |
| ⊢ 𝑃 = (𝐼 mPwSer 𝑅) & ⊢ 𝑄 = (𝐼 mPwSer 𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Base‘𝑄) & ⊢ · = (.r‘𝑃) & ⊢ ∙ = (.r‘𝑄) & ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐻 ∘ (𝐹 · 𝐺)) = ((𝐻 ∘ 𝐹) ∙ (𝐻 ∘ 𝐺))) | ||
| Theorem | rhmpsr 42562* | Provide a ring homomorphism between two power series algebras over their respective base rings given a ring homomorphism between the two base rings. (Contributed by SN, 8-Feb-2025.) |
| ⊢ 𝑃 = (𝐼 mPwSer 𝑅) & ⊢ 𝑄 = (𝐼 mPwSer 𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ (𝐻 ∘ 𝑝)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑄)) | ||
| Theorem | rhmpsr1 42563* | Provide a ring homomorphism between two univariate power series algebras over their respective base rings given a ring homomorphism between the two base rings. (Contributed by SN, 8-Feb-2025.) |
| ⊢ 𝑃 = (PwSer1‘𝑅) & ⊢ 𝑄 = (PwSer1‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ (𝐻 ∘ 𝑝)) & ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑄)) | ||
| Theorem | mplascl0 42564 | The zero scalar as a polynomial. (Contributed by SN, 23-Nov-2024.) |
| ⊢ 𝑊 = (𝐼 mPoly 𝑅) & ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝑂 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (𝐴‘𝑂) = 0 ) | ||
| Theorem | mplascl1 42565 | The one scalar as a polynomial. (Contributed by SN, 12-Mar-2025.) |
| ⊢ 𝑊 = (𝐼 mPoly 𝑅) & ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝑂 = (1r‘𝑅) & ⊢ 1 = (1r‘𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (𝐴‘𝑂) = 1 ) | ||
| Theorem | mplmapghm 42566* | 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 42567 | The zero polynomial evaluates to zero. (Contributed by SN, 23-Nov-2024.) |
| ⊢ 𝑄 = (𝐼 eval 𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑊 = (𝐼 mPoly 𝑅) & ⊢ 𝑂 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → (𝑄‘ 0 ) = ((𝐵 ↑m 𝐼) × {𝑂})) | ||
| Theorem | evlscl 42568 | 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 42569* | 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 42570* | 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 42571* | Lemma for evlsvvval 42573 akin to psrbagev2 22102. (Contributed by SN, 6-Mar-2025.) |
| ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑀 = (mulGrp‘𝑆) & ⊢ ↑ = (.g‘𝑀) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑀 Σg (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝐴‘𝑣)))) ∈ 𝐾) | ||
| Theorem | evlsvvvallem2 42572* | Lemma for theorems using evlsvvval 42573. (Contributed by SN, 8-Mar-2025.) |
| ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑀 = (mulGrp‘𝑆) & ⊢ ↑ = (.g‘𝑀) & ⊢ · = (.r‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑣 ∈ 𝐼 ↦ ((𝑏‘𝑣) ↑ (𝐴‘𝑣)))))) finSupp (0g‘𝑆)) | ||
| Theorem | evlsvvval 42573* | 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 42574 | Polynomial evaluation builder for a scalar. Compare evl1scad 22339. Note that scalar multiplication by 𝑋 is the same as vector multiplication by (𝐴‘𝑋) by asclmul1 21906. (Contributed by SN, 27-Jul-2024.) |
| ⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑅) & ⊢ (𝜑 → 𝐿 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → ((𝐴‘𝑋) ∈ 𝐵 ∧ ((𝑄‘(𝐴‘𝑋))‘𝐿) = 𝑋)) | ||
| Theorem | evlsvarval 42575 | Polynomial evaluation builder for a variable. (Contributed by SN, 27-Jul-2024.) |
| ⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑉 = (𝐼 mVar 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → ((𝑉‘𝑋) ∈ 𝐵 ∧ ((𝑄‘(𝑉‘𝑋))‘𝐴) = (𝐴‘𝑋))) | ||
| Theorem | evlsbagval 42576* | 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 42577 | 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 42578 | Polynomial evaluation builder for addition. (Contributed by SN, 27-Jul-2024.) |
| ⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) & ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊)) & ⊢ ✚ = (+g‘𝑃) & ⊢ + = (+g‘𝑆) ⇒ ⊢ (𝜑 → ((𝑀 ✚ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ✚ 𝑁))‘𝐴) = (𝑉 + 𝑊))) | ||
| Theorem | evlsmulval 42579 | Polynomial evaluation builder for multiplication. (Contributed by SN, 27-Jul-2024.) |
| ⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) & ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊)) & ⊢ ∙ = (.r‘𝑃) & ⊢ · = (.r‘𝑆) ⇒ ⊢ (𝜑 → ((𝑀 ∙ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ∙ 𝑁))‘𝐴) = (𝑉 · 𝑊))) | ||
| Theorem | evlsmaprhm 42580* | The function 𝐹 mapping polynomials 𝑝 to their subring evaluation at a given point 𝑋 is a ring homomorphism. Compare evls1maprhm 22380. (Contributed by SN, 12-Mar-2025.) |
| ⊢ 𝑄 = ((𝐼 evalSub 𝑅)‘𝑆) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑅 ↾s 𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ ((𝑄‘𝑝)‘𝐴)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑅)) | ||
| Theorem | evlsevl 42581 | 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 42582 | A polynomial over the ring 𝑅 evaluates to an element in 𝑅. (Contributed by SN, 12-Mar-2025.) |
| ⊢ 𝑄 = (𝐼 eval 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → ((𝑄‘𝐹)‘𝐴) ∈ 𝐾) | ||
| Theorem | evlvvval 42583* | 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 42584* | Lemma for theorems using evlvvval 42583. Version of evlsvvvallem2 42572 using df-evl 22099. (Contributed by SN, 11-Mar-2025.) |
| ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ ↑ = (.g‘𝑀) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑣 ∈ 𝐼 ↦ ((𝑏‘𝑣) ↑ (𝐴‘𝑣)))))) finSupp (0g‘𝑅)) | ||
| Theorem | evladdval 42585 | Polynomial evaluation builder for addition. (Contributed by SN, 9-Feb-2025.) |
| ⊢ 𝑄 = (𝐼 eval 𝑆) & ⊢ 𝑃 = (𝐼 mPoly 𝑆) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ ✚ = (+g‘𝑃) & ⊢ + = (+g‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) & ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊)) ⇒ ⊢ (𝜑 → ((𝑀 ✚ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ✚ 𝑁))‘𝐴) = (𝑉 + 𝑊))) | ||
| Theorem | evlmulval 42586 | Polynomial evaluation builder for multiplication. (Contributed by SN, 18-Feb-2025.) |
| ⊢ 𝑄 = (𝐼 eval 𝑆) & ⊢ 𝑃 = (𝐼 mPoly 𝑆) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ ∙ = (.r‘𝑃) & ⊢ · = (.r‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) & ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊)) ⇒ ⊢ (𝜑 → ((𝑀 ∙ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ∙ 𝑁))‘𝐴) = (𝑉 · 𝑊))) | ||
| Theorem | selvcllem1 42587 | 𝑇 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 42588 | 𝐷 is a ring homomorphism. (Contributed by SN, 15-Dec-2023.) |
| ⊢ 𝑈 = (𝐼 mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ 𝐶 = (algSc‘𝑇) & ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → 𝐷 ∈ (𝑅 RingHom 𝑇)) | ||
| Theorem | selvcllem3 42589 | The third argument passed to evalSub is in the domain. (Contributed by SN, 15-Dec-2023.) |
| ⊢ 𝑈 = (𝐼 mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ 𝐶 = (algSc‘𝑇) & ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → ran 𝐷 ∈ (SubRing‘𝑇)) | ||
| Theorem | selvcllemh 42590 | Apply the third argument (selvcllem3 42589) to show that 𝑄 is a (ring) homomorphism. (Contributed by SN, 5-Nov-2023.) |
| ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ 𝐶 = (algSc‘𝑇) & ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈)) & ⊢ 𝑄 = ((𝐼 evalSub 𝑇)‘ran 𝐷) & ⊢ 𝑊 = (𝐼 mPoly 𝑆) & ⊢ 𝑆 = (𝑇 ↾s ran 𝐷) & ⊢ 𝑋 = (𝑇 ↑s (𝐵 ↑m 𝐼)) & ⊢ 𝐵 = (Base‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) ⇒ ⊢ (𝜑 → 𝑄 ∈ (𝑊 RingHom 𝑋)) | ||
| Theorem | selvcllem4 42591 | The fourth argument passed to evalSub is in the domain (a polynomial in (𝐼 mPoly (𝐽 mPoly ((𝐼 ∖ 𝐽) mPoly 𝑅)))). (Contributed by SN, 5-Nov-2023.) |
| ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ 𝐶 = (algSc‘𝑇) & ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈)) & ⊢ 𝑆 = (𝑇 ↾s ran 𝐷) & ⊢ 𝑊 = (𝐼 mPoly 𝑆) & ⊢ 𝑋 = (Base‘𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐷 ∘ 𝐹) ∈ 𝑋) | ||
| Theorem | selvcllem5 42592* | The fifth argument passed to evalSub is in the domain (a function 𝐼⟶𝐸). (Contributed by SN, 22-Feb-2024.) |
| ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ 𝐶 = (algSc‘𝑇) & ⊢ 𝐸 = (Base‘𝑇) & ⊢ 𝐹 = (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥)))) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐸 ↑m 𝐼)) | ||
| Theorem | selvcl 42593 | Closure of the "variable selection" function. (Contributed by SN, 22-Feb-2024.) |
| ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ 𝐸 = (Base‘𝑇) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) ∈ 𝐸) | ||
| Theorem | selvval2 42594* | Value of the "variable selection" function. Convert selvval 22139 into a simpler form by using evlsevl 42581. (Contributed by SN, 9-Feb-2025.) |
| ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ 𝐶 = (algSc‘𝑇) & ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈)) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) = (((𝐼 eval 𝑇)‘(𝐷 ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥)))))) | ||
| Theorem | selvvvval 42595* | Recover the original polynomial from a selectVars application. (Contributed by SN, 15-Mar-2025.) |
| ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐷) ⇒ ⊢ (𝜑 → (((((𝐼 selectVars 𝑅)‘𝐽)‘𝐹)‘(𝑌 ↾ 𝐽))‘(𝑌 ↾ (𝐼 ∖ 𝐽))) = (𝐹‘𝑌)) | ||
| Theorem | evlselvlem 42596* | Lemma for evlselv 42597. Used to re-index to and from bags of variables in 𝐼 and bags of variables in the subsets 𝐽 and 𝐼 ∖ 𝐽. (Contributed by SN, 10-Mar-2025.) |
| ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝐸 = {𝑔 ∈ (ℕ0 ↑m 𝐽) ∣ (◡𝑔 “ ℕ) ∈ Fin} & ⊢ 𝐶 = {𝑓 ∈ (ℕ0 ↑m (𝐼 ∖ 𝐽)) ∣ (◡𝑓 “ ℕ) ∈ Fin} & ⊢ 𝐻 = (𝑐 ∈ 𝐶, 𝑒 ∈ 𝐸 ↦ (𝑐 ∪ 𝑒)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) ⇒ ⊢ (𝜑 → 𝐻:(𝐶 × 𝐸)–1-1-onto→𝐷) | ||
| Theorem | evlselv 42597 | Evaluating a selection of variable assignments, then evaluating the rest of the variables, is the same as evaluating with all assignments. (Contributed by SN, 10-Mar-2025.) |
| ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ 𝐿 = (algSc‘𝑈) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → ((((𝐼 ∖ 𝐽) eval 𝑅)‘(((𝐽 eval 𝑈)‘(((𝐼 selectVars 𝑅)‘𝐽)‘𝐹))‘(𝐿 ∘ (𝐴 ↾ 𝐽))))‘(𝐴 ↾ (𝐼 ∖ 𝐽))) = (((𝐼 eval 𝑅)‘𝐹)‘𝐴)) | ||
| Theorem | selvadd 42598 | The "variable selection" function is additive. (Contributed by SN, 7-Feb-2025.) |
| ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ + = (+g‘𝑃) & ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ ✚ = (+g‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘(𝐹 + 𝐺)) = ((((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) ✚ (((𝐼 selectVars 𝑅)‘𝐽)‘𝐺))) | ||
| Theorem | selvmul 42599 | The "variable selection" function is multiplicative. (Contributed by SN, 18-Feb-2025.) |
| ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ · = (.r‘𝑃) & ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ ∙ = (.r‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘(𝐹 · 𝐺)) = ((((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) ∙ (((𝐼 selectVars 𝑅)‘𝐽)‘𝐺))) | ||
| Theorem | fsuppind 42600* | Induction on functions 𝐹:𝐴⟶𝐵 with finite support, or in other words the base set of the free module (see frlmelbas 21776 and frlmplusgval 21784). This theorem is structurally general for polynomial proof usage (see mplelbas 22011 and mpladd 22029). Note that hypothesis 0 is redundant when 𝐼 is nonempty. (Contributed by SN, 18-May-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → (𝐼 × { 0 }) ∈ 𝐻) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 𝐵)) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 ∘f + 𝑦) ∈ 𝐻) ⇒ ⊢ ((𝜑 ∧ (𝑋:𝐼⟶𝐵 ∧ 𝑋 finSupp 0 )) → 𝑋 ∈ 𝐻) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |