![]() |
Metamath
Proof Explorer Theorem List (p. 426 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rimrcl1 42501 | Reverse closure of a ring isomorphism. (Contributed by SN, 19-Feb-2025.) |
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝑅 ∈ Ring) | ||
Theorem | rimrcl2 42502 | Reverse closure of a ring isomorphism. (Contributed by SN, 19-Feb-2025.) |
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → 𝑆 ∈ Ring) | ||
Theorem | rimcnv 42503 | The converse of a ring isomorphism is a ring isomorphism. (Contributed by SN, 10-Jan-2025.) |
⊢ (𝐹 ∈ (𝑅 RingIso 𝑆) → ◡𝐹 ∈ (𝑆 RingIso 𝑅)) | ||
Theorem | rimco 42504 | The composition of ring isomorphisms is a ring isomorphism. (Contributed by SN, 17-Jan-2025.) |
⊢ ((𝐹 ∈ (𝑆 RingIso 𝑇) ∧ 𝐺 ∈ (𝑅 RingIso 𝑆)) → (𝐹 ∘ 𝐺) ∈ (𝑅 RingIso 𝑇)) | ||
Theorem | ricsym 42505 | Ring isomorphism is symmetric. (Contributed by SN, 10-Jan-2025.) |
⊢ (𝑅 ≃𝑟 𝑆 → 𝑆 ≃𝑟 𝑅) | ||
Theorem | rictr 42506 | Ring isomorphism is transitive. (Contributed by SN, 17-Jan-2025.) |
⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑆 ≃𝑟 𝑇) → 𝑅 ≃𝑟 𝑇) | ||
Theorem | riccrng1 42507 | Ring isomorphism preserves (multiplicative) commutativity. (Contributed by SN, 10-Jan-2025.) |
⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ CRing) → 𝑆 ∈ CRing) | ||
Theorem | riccrng 42508 | A ring is commutative if and only if an isomorphic ring is commutative. (Contributed by SN, 10-Jan-2025.) |
⊢ (𝑅 ≃𝑟 𝑆 → (𝑅 ∈ CRing ↔ 𝑆 ∈ CRing)) | ||
Theorem | domnexpgn0cl 42509 | 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 42510 | A multiplicative inverse in a division ring is nonzero. (recne0d 12034 analog). (Contributed by SN, 14-Aug-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝐼‘𝑋) ≠ 0 ) | ||
Theorem | drngmullcan 42511 | Cancellation of a nonzero factor on the left for multiplication. (mulcanad 11895 analog). (Contributed by SN, 14-Aug-2024.) (Proof shortened by SN, 25-Jun-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ≠ 0 ) & ⊢ (𝜑 → (𝑍 · 𝑋) = (𝑍 · 𝑌)) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | drngmulrcan 42512 | Cancellation of a nonzero factor on the right for multiplication. (mulcan2ad 11896 analog). (Contributed by SN, 14-Aug-2024.) (Proof shortened by SN, 25-Jun-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ≠ 0 ) & ⊢ (𝜑 → (𝑋 · 𝑍) = (𝑌 · 𝑍)) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | drnginvmuld 42513 | Inverse of a nonzero product. (Contributed by SN, 14-Aug-2024.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑌 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝐼‘(𝑋 · 𝑌)) = ((𝐼‘𝑌) · (𝐼‘𝑋))) | ||
Theorem | ricdrng1 42514 | A ring isomorphism maps a division ring to a division ring. (Contributed by SN, 18-Feb-2025.) |
⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ DivRing) → 𝑆 ∈ DivRing) | ||
Theorem | ricdrng 42515 | 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 42516 | 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 42517* | 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 42518 | Move exponentiation in and out of absolute value. (Contributed by SN, 3-Jul-2025.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑅)) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝐹 ∈ 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐹‘(𝑁 ↑ 𝑋)) = ((𝐹‘𝑋)↑𝑁)) | ||
Theorem | fimgmcyclem 42519* | Lemma for fimgmcyc 42520. (Contributed by SN, 7-Jul-2025.) |
⊢ (𝜑 → ∃𝑜 ∈ ℕ ∃𝑞 ∈ ℕ (𝑜 ≠ 𝑞 ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴))) ⇒ ⊢ (𝜑 → ∃𝑜 ∈ ℕ ∃𝑞 ∈ ℕ (𝑜 < 𝑞 ∧ (𝑜 · 𝐴) = (𝑞 · 𝐴))) | ||
Theorem | fimgmcyc 42520* | Version of odcl2 19597 for finite magmas: the multiples of an element 𝐴 ∈ 𝐵 are eventually periodic. (Contributed by SN, 3-Jul-2025.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ · = (.g‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ Mgm) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑜 ∈ ℕ ∃𝑝 ∈ ℕ (𝑜 · 𝐴) = ((𝑜 + 𝑝) · 𝐴)) | ||
Theorem | fidomncyc 42521* | Version of odcl2 19597 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 42522* | In a finite domain (a finite field), the only absolute value is the trivial one (abvtrivg 20850). (Contributed by SN, 3-Jul-2025.) |
⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑇 = (𝑥 ∈ 𝐵 ↦ if(𝑥 = 0 , 0, 1)) & ⊢ (𝜑 → 𝑅 ∈ Domn) & ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → 𝐴 = {𝑇}) | ||
Theorem | lvecgrp 42523 | A vector space is a group. (Contributed by SN, 28-May-2023.) |
⊢ (𝑊 ∈ LVec → 𝑊 ∈ Grp) | ||
Theorem | lvecring 42524 | The scalar component of a vector space is a ring. (Contributed by SN, 28-May-2023.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec → 𝐹 ∈ Ring) | ||
Theorem | frlm0vald 42525 | All coordinates of the zero vector are zero. (Contributed by SN, 14-Aug-2024.) |
⊢ 𝐹 = (𝑅 freeLMod 𝐼) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝐽 ∈ 𝐼) ⇒ ⊢ (𝜑 → ((0g‘𝐹)‘𝐽) = 0 ) | ||
Theorem | frlmsnic 42526* | 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 42527 | A unit vector is a vector. (Contributed by Steven Nguyen, 16-Jul-2023.) |
⊢ 𝑈 = (𝑅 unitVec 𝐼) & ⊢ 𝑌 = (𝑅 freeLMod 𝐼) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼) → (𝑈‘𝐽) ∈ 𝐵) | ||
Theorem | uvcn0 42528 | A unit vector is nonzero. (Contributed by Steven Nguyen, 16-Jul-2023.) |
⊢ 𝑈 = (𝑅 unitVec 𝐼) & ⊢ 𝑌 = (𝑅 freeLMod 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 0 = (0g‘𝑌) ⇒ ⊢ ((𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼) → (𝑈‘𝐽) ≠ 0 ) | ||
Theorem | pwselbasr 42529 | The reverse direction of pwselbasb 17534: 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 42530* | Finite products in a power structure are taken componentwise. Compare pwsgsum 20014. (Contributed by SN, 30-Jul-2024.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑌) & ⊢ 𝑀 = (mulGrp‘𝑌) & ⊢ 𝑇 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽)) → 𝑈 ∈ 𝐵) & ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) finSupp 1 ) ⇒ ⊢ (𝜑 → (𝑀 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ (𝑇 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)))) | ||
Theorem | psrmnd 42531 | The ring of power series is a monoid. (Contributed by SN, 25-Apr-2025.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Mnd) ⇒ ⊢ (𝜑 → 𝑆 ∈ Mnd) | ||
Theorem | psrbagres 42532* | 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 42533 | The polynomial ring is a commutative ring. (Contributed by SN, 7-Feb-2025.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → 𝑃 ∈ CRing) | ||
Theorem | mplsubrgcl 42534 | 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 42535 | 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 42536 | Show that the ring homomorphism in rhmpsr 42538 preserves addition. (Contributed by SN, 18-May-2025.) |
⊢ 𝑃 = (𝐼 mPwSer 𝑅) & ⊢ 𝑄 = (𝐼 mPwSer 𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Base‘𝑄) & ⊢ + = (+g‘𝑃) & ⊢ ✚ = (+g‘𝑄) & ⊢ (𝜑 → 𝐻 ∈ (𝑅 MndHom 𝑆)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐻 ∘ (𝐹 + 𝐺)) = ((𝐻 ∘ 𝐹) ✚ (𝐻 ∘ 𝐺))) | ||
Theorem | rhmcomulpsr 42537 | Show that the ring homomorphism in rhmpsr 42538 preserves multiplication. (Contributed by SN, 18-May-2025.) |
⊢ 𝑃 = (𝐼 mPwSer 𝑅) & ⊢ 𝑄 = (𝐼 mPwSer 𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Base‘𝑄) & ⊢ · = (.r‘𝑃) & ⊢ ∙ = (.r‘𝑄) & ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐻 ∘ (𝐹 · 𝐺)) = ((𝐻 ∘ 𝐹) ∙ (𝐻 ∘ 𝐺))) | ||
Theorem | rhmpsr 42538* | 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 42539* | 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 42540 | The zero scalar as a polynomial. (Contributed by SN, 23-Nov-2024.) |
⊢ 𝑊 = (𝐼 mPoly 𝑅) & ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝑂 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (𝐴‘𝑂) = 0 ) | ||
Theorem | mplascl1 42541 | The one scalar as a polynomial. (Contributed by SN, 12-Mar-2025.) |
⊢ 𝑊 = (𝐼 mPoly 𝑅) & ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝑂 = (1r‘𝑅) & ⊢ 1 = (1r‘𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (𝐴‘𝑂) = 1 ) | ||
Theorem | mplmapghm 42542* | 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 42543 | The zero polynomial evaluates to zero. (Contributed by SN, 23-Nov-2024.) |
⊢ 𝑄 = (𝐼 eval 𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑊 = (𝐼 mPoly 𝑅) & ⊢ 𝑂 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → (𝑄‘ 0 ) = ((𝐵 ↑m 𝐼) × {𝑂})) | ||
Theorem | evlscl 42544 | 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 42545* | 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 42546* | 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 42547* | Lemma for evlsvvval 42549 akin to psrbagev2 22119. (Contributed by SN, 6-Mar-2025.) |
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑀 = (mulGrp‘𝑆) & ⊢ ↑ = (.g‘𝑀) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑀 Σg (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝐴‘𝑣)))) ∈ 𝐾) | ||
Theorem | evlsvvvallem2 42548* | Lemma for theorems using evlsvvval 42549. (Contributed by SN, 8-Mar-2025.) |
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑀 = (mulGrp‘𝑆) & ⊢ ↑ = (.g‘𝑀) & ⊢ · = (.r‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑣 ∈ 𝐼 ↦ ((𝑏‘𝑣) ↑ (𝐴‘𝑣)))))) finSupp (0g‘𝑆)) | ||
Theorem | evlsvvval 42549* | 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 42550 | Polynomial evaluation builder for a scalar. Compare evl1scad 22354. Note that scalar multiplication by 𝑋 is the same as vector multiplication by (𝐴‘𝑋) by asclmul1 21923. (Contributed by SN, 27-Jul-2024.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑅) & ⊢ (𝜑 → 𝐿 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → ((𝐴‘𝑋) ∈ 𝐵 ∧ ((𝑄‘(𝐴‘𝑋))‘𝐿) = 𝑋)) | ||
Theorem | evlsvarval 42551 | Polynomial evaluation builder for a variable. (Contributed by SN, 27-Jul-2024.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑉 = (𝐼 mVar 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → ((𝑉‘𝑋) ∈ 𝐵 ∧ ((𝑄‘(𝑉‘𝑋))‘𝐴) = (𝐴‘𝑋))) | ||
Theorem | evlsbagval 42552* | 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 42553 | 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 42554 | Polynomial evaluation builder for addition. (Contributed by SN, 27-Jul-2024.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) & ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊)) & ⊢ ✚ = (+g‘𝑃) & ⊢ + = (+g‘𝑆) ⇒ ⊢ (𝜑 → ((𝑀 ✚ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ✚ 𝑁))‘𝐴) = (𝑉 + 𝑊))) | ||
Theorem | evlsmulval 42555 | Polynomial evaluation builder for multiplication. (Contributed by SN, 27-Jul-2024.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) & ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊)) & ⊢ ∙ = (.r‘𝑃) & ⊢ · = (.r‘𝑆) ⇒ ⊢ (𝜑 → ((𝑀 ∙ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ∙ 𝑁))‘𝐴) = (𝑉 · 𝑊))) | ||
Theorem | evlsmaprhm 42556* | The function 𝐹 mapping polynomials 𝑝 to their subring evaluation at a given point 𝑋 is a ring homomorphism. Compare evls1maprhm 22395. (Contributed by SN, 12-Mar-2025.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑅)‘𝑆) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑅 ↾s 𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ ((𝑄‘𝑝)‘𝐴)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑅)) | ||
Theorem | evlsevl 42557 | 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 42558 | A polynomial over the ring 𝑅 evaluates to an element in 𝑅. (Contributed by SN, 12-Mar-2025.) |
⊢ 𝑄 = (𝐼 eval 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → ((𝑄‘𝐹)‘𝐴) ∈ 𝐾) | ||
Theorem | evlvvval 42559* | 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 42560* | Lemma for theorems using evlvvval 42559. Version of evlsvvvallem2 42548 using df-evl 22116. (Contributed by SN, 11-Mar-2025.) |
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ ↑ = (.g‘𝑀) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑣 ∈ 𝐼 ↦ ((𝑏‘𝑣) ↑ (𝐴‘𝑣)))))) finSupp (0g‘𝑅)) | ||
Theorem | evladdval 42561 | Polynomial evaluation builder for addition. (Contributed by SN, 9-Feb-2025.) |
⊢ 𝑄 = (𝐼 eval 𝑆) & ⊢ 𝑃 = (𝐼 mPoly 𝑆) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ ✚ = (+g‘𝑃) & ⊢ + = (+g‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) & ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊)) ⇒ ⊢ (𝜑 → ((𝑀 ✚ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ✚ 𝑁))‘𝐴) = (𝑉 + 𝑊))) | ||
Theorem | evlmulval 42562 | Polynomial evaluation builder for multiplication. (Contributed by SN, 18-Feb-2025.) |
⊢ 𝑄 = (𝐼 eval 𝑆) & ⊢ 𝑃 = (𝐼 mPoly 𝑆) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ ∙ = (.r‘𝑃) & ⊢ · = (.r‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) & ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊)) ⇒ ⊢ (𝜑 → ((𝑀 ∙ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ∙ 𝑁))‘𝐴) = (𝑉 · 𝑊))) | ||
Theorem | selvcllem1 42563 | 𝑇 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 42564 | 𝐷 is a ring homomorphism. (Contributed by SN, 15-Dec-2023.) |
⊢ 𝑈 = (𝐼 mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ 𝐶 = (algSc‘𝑇) & ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → 𝐷 ∈ (𝑅 RingHom 𝑇)) | ||
Theorem | selvcllem3 42565 | 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 42566 | Apply the third argument (selvcllem3 42565) 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 42567 | 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 42568* | 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 42569 | Closure of the "variable selection" function. (Contributed by SN, 22-Feb-2024.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ 𝐸 = (Base‘𝑇) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) ∈ 𝐸) | ||
Theorem | selvval2 42570* | Value of the "variable selection" function. Convert selvval 22156 into a simpler form by using evlsevl 42557. (Contributed by SN, 9-Feb-2025.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ 𝐶 = (algSc‘𝑇) & ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈)) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) = (((𝐼 eval 𝑇)‘(𝐷 ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥)))))) | ||
Theorem | selvvvval 42571* | Recover the original polynomial from a selectVars application. (Contributed by SN, 15-Mar-2025.) |
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐷) ⇒ ⊢ (𝜑 → (((((𝐼 selectVars 𝑅)‘𝐽)‘𝐹)‘(𝑌 ↾ 𝐽))‘(𝑌 ↾ (𝐼 ∖ 𝐽))) = (𝐹‘𝑌)) | ||
Theorem | evlselvlem 42572* | Lemma for evlselv 42573. 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 42573 | 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 42574 | The "variable selection" function is additive. (Contributed by SN, 7-Feb-2025.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ + = (+g‘𝑃) & ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ ✚ = (+g‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘(𝐹 + 𝐺)) = ((((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) ✚ (((𝐼 selectVars 𝑅)‘𝐽)‘𝐺))) | ||
Theorem | selvmul 42575 | The "variable selection" function is multiplicative. (Contributed by SN, 18-Feb-2025.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ · = (.r‘𝑃) & ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ ∙ = (.r‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘(𝐹 · 𝐺)) = ((((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) ∙ (((𝐼 selectVars 𝑅)‘𝐽)‘𝐺))) | ||
Theorem | fsuppind 42576* | Induction on functions 𝐹:𝐴⟶𝐵 with finite support, or in other words the base set of the free module (see frlmelbas 21793 and frlmplusgval 21801). This theorem is structurally general for polynomial proof usage (see mplelbas 22028 and mpladd 22046). 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 )) → 𝑋 ∈ 𝐻) | ||
Theorem | fsuppssindlem1 42577* | Lemma for fsuppssind 42579. Functions are zero outside of their support. (Contributed by SN, 15-Jul-2024.) |
⊢ (𝜑 → 0 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝑆) ⇒ ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, ((𝐹 ↾ 𝑆)‘𝑥), 0 ))) | ||
Theorem | fsuppssindlem2 42578* | Lemma for fsuppssind 42579. Write a function as a union. (Contributed by SN, 15-Jul-2024.) |
⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐼) ⇒ ⊢ (𝜑 → (𝐹 ∈ {𝑓 ∈ (𝐵 ↑m 𝑆) ∣ (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, (𝑓‘𝑥), 0 )) ∈ 𝐻} ↔ (𝐹:𝑆⟶𝐵 ∧ (𝐹 ∪ ((𝐼 ∖ 𝑆) × { 0 })) ∈ 𝐻))) | ||
Theorem | fsuppssind 42579* | Induction on functions 𝐹:𝐴⟶𝐵 with finite support (see fsuppind 42576) whose supports are subsets of 𝑆. (Contributed by SN, 15-Jun-2024.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐼) & ⊢ (𝜑 → (𝐼 × { 0 }) ∈ 𝐻) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) → (𝑠 ∈ 𝐼 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) ∈ 𝐻) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 ∘f + 𝑦) ∈ 𝐻) & ⊢ (𝜑 → 𝑋:𝐼⟶𝐵) & ⊢ (𝜑 → 𝑋 finSupp 0 ) & ⊢ (𝜑 → (𝑋 supp 0 ) ⊆ 𝑆) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐻) | ||
Theorem | mhpind 42580* | The homogeneous polynomials of degree 𝑁 are generated by the terms of degree 𝑁 and addition. (Contributed by SN, 28-Jul-2024.) |
⊢ 𝐻 = (𝐼 mHomP 𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ + = (+g‘𝑃) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝑆 = {𝑔 ∈ 𝐷 ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} & ⊢ (𝜑 → 𝑅 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁)) & ⊢ (𝜑 → (𝐷 × { 0 }) ∈ 𝐺) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) → (𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) ∈ 𝐺) & ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐻‘𝑁) ∩ 𝐺) ∧ 𝑦 ∈ ((𝐻‘𝑁) ∩ 𝐺))) → (𝑥 + 𝑦) ∈ 𝐺) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐺) | ||
Theorem | evlsmhpvvval 42581* | Give a formula for the evaluation of a homogeneous polynomial given assignments from variables to values. The difference between this and evlsvvval 42549 is that 𝑏 ∈ 𝐷 is restricted to 𝑏 ∈ 𝐺, that is, we can evaluate an 𝑁-th degree homogeneous polynomial over just the terms where the sum of all variable degrees is 𝑁. (Contributed by SN, 5-Mar-2025.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝐻 = (𝐼 mHomP 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝐺 = {𝑔 ∈ 𝐷 ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑀 = (mulGrp‘𝑆) & ⊢ ↑ = (.g‘𝑀) & ⊢ · = (.r‘𝑆) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐹 ∈ (𝐻‘𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → ((𝑄‘𝐹)‘𝐴) = (𝑆 Σg (𝑏 ∈ 𝐺 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))))) | ||
Theorem | mhphflem 42582* | Lemma for mhphf 42583. Add several multiples of 𝐿 together, in a case where the total amount of multiplies is 𝑁. (Contributed by SN, 30-Jul-2024.) |
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝐻 = {𝑔 ∈ 𝐷 ∣ ((ℂfld ↾s ℕ0) Σg 𝑔) = 𝑁} & ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐿 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐻) → (𝐺 Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) · 𝐿))) = (𝑁 · 𝐿)) | ||
Theorem | mhphf 42583 | A homogeneous polynomial defines a homogeneous function. Equivalently, an algebraic form is a homogeneous function. (An algebraic form is the function corresponding to a homogeneous polynomial, which in this case is the (𝑄‘𝑋) which corresponds to 𝑋). (Contributed by SN, 28-Jul-2024.) (Proof shortened by SN, 8-Mar-2025.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝐻 = (𝐼 mHomP 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ · = (.r‘𝑆) & ⊢ ↑ = (.g‘(mulGrp‘𝑆)) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐿 ∈ 𝑅) & ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴))) | ||
Theorem | mhphf2 42584 |
A homogeneous polynomial defines a homogeneous function; this is mhphf 42583
with simpler notation in the conclusion in exchange for a complex
definition of ∙, which is
based on frlmvscafval 21803 but without the
finite support restriction (frlmpws 21787, frlmbas 21792) on the assignments
𝐴 from variables to values.
TODO?: Polynomials (df-mpl 21948) are defined to have a finite amount of terms (of finite degree). As such, any assignment may be replaced by an assignment with finite support (as only a finite amount of variables matter in a given polynomial, even if the set of variables is infinite). So the finite support restriction can be assumed without loss of generality. (Contributed by SN, 11-Nov-2024.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝐻 = (𝐼 mHomP 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ ∙ = ( ·𝑠 ‘((ringLMod‘𝑆) ↑s 𝐼)) & ⊢ · = (.r‘𝑆) & ⊢ ↑ = (.g‘(mulGrp‘𝑆)) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐿 ∈ 𝑅) & ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → ((𝑄‘𝑋)‘(𝐿 ∙ 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴))) | ||
Theorem | mhphf3 42585 | A homogeneous polynomial defines a homogeneous function; this is mhphf2 42584 with the finite support restriction (frlmpws 21787, frlmbas 21792) on the assignments 𝐴 from variables to values. See comment of mhphf2 42584. (Contributed by SN, 23-Nov-2024.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝐻 = (𝐼 mHomP 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐹 = (𝑆 freeLMod 𝐼) & ⊢ 𝑀 = (Base‘𝐹) & ⊢ ∙ = ( ·𝑠 ‘𝐹) & ⊢ · = (.r‘𝑆) & ⊢ ↑ = (.g‘(mulGrp‘𝑆)) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐿 ∈ 𝑅) & ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁)) & ⊢ (𝜑 → 𝐴 ∈ 𝑀) ⇒ ⊢ (𝜑 → ((𝑄‘𝑋)‘(𝐿 ∙ 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴))) | ||
Theorem | mhphf4 42586 | A homogeneous polynomial defines a homogeneous function; this is mhphf3 42585 with evalSub collapsed to eval. (Contributed by SN, 23-Nov-2024.) |
⊢ 𝑄 = (𝐼 eval 𝑆) & ⊢ 𝐻 = (𝐼 mHomP 𝑆) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐹 = (𝑆 freeLMod 𝐼) & ⊢ 𝑀 = (Base‘𝐹) & ⊢ ∙ = ( ·𝑠 ‘𝐹) & ⊢ · = (.r‘𝑆) & ⊢ ↑ = (.g‘(mulGrp‘𝑆)) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐿 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁)) & ⊢ (𝜑 → 𝐴 ∈ 𝑀) ⇒ ⊢ (𝜑 → ((𝑄‘𝑋)‘(𝐿 ∙ 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴))) | ||
Looking at a corner in 3D space, one can see three right angles. It is impossible to draw three lines in 2D space such that any two of these lines are perpendicular, but a good enough representation is made by casting lines from the 2D surface. Points along the same cast line are collapsed into one point on the 2D surface. In many cases, the 2D surface is smaller than whatever needs to be represented. If the lines cast were perpendicular to the 2D surface, then only areas as small as the 2D surface could be represented. To fix this, the lines need to get further apart as they go farther from the 2D surface. On the other side of the 2D surface the lines will get closer together and intersect at a point (because it's defined that way). From this perspective, two parallel lines in 3D space will be represented by two lines that seem to intersect at a point "at infinity". Considering all maximal classes of parallel lines on a 2D plane in 3D space, these classes will all appear to intersect at different points at infinity, forming a line at infinity. Therefore the real projective plane can be thought of as the real affine plane together with the line at infinity. The projective plane takes care of some exceptions that may be found in the affine plane. For example, consider the curve that is the zeroes of 𝑦 = 𝑥↑2. Any line connecting the point (0, 1) to the x-axis intersects with the curve twice, except for the vertical line between (0, 1) and (0, 0). In the projective plane, the curve becomes an ellipse and there is no exception. While it may not seem like it, points at infinity and points corresponding to the affine plane are the same type of point. Consider a line going through the origin in 3D (affine) space. Either it intersects the plane 𝑧 = 1 once, or it is entirely within the plane 𝑧 = 0. If it is entirely within the plane 𝑧 = 0, then it corresponds to the point at infinity intersecting all lines on the plane 𝑧 = 1 with the same slope. Else it corresponds to the point in the 2D plane 𝑧 = 1 that it intersects. So there is a bijection between 3D lines through the origin and points on the real projective plane. The concept of projective spaces generalizes the projective plane to any dimension. | ||
Syntax | cprjsp 42587 | Extend class notation with the projective space function. |
class ℙ𝕣𝕠𝕛 | ||
Definition | df-prjsp 42588* | Define the projective space function. In the bijection between 3D lines through the origin and points in the projective plane (see section comment), this is equivalent to making any two 3D points (excluding the origin) equivalent iff one is a multiple of another. This definition does not quite give all the properties needed, since the scalars of a left vector space can be "less dense" than the vectors (for example, making equivalent rational multiples of real numbers). Compare df-lsatoms 38957. (Contributed by BJ and SN, 29-Apr-2023.) |
⊢ ℙ𝕣𝕠𝕛 = (𝑣 ∈ LVec ↦ ⦋((Base‘𝑣) ∖ {(0g‘𝑣)}) / 𝑏⦌(𝑏 / {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑣))𝑥 = (𝑙( ·𝑠 ‘𝑣)𝑦))})) | ||
Theorem | prjspval 42589* | Value of the projective space function, which is also known as the projectivization of 𝑉. (Contributed by Steven Nguyen, 29-Apr-2023.) |
⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ (𝑉 ∈ LVec → (ℙ𝕣𝕠𝕛‘𝑉) = (𝐵 / {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))})) | ||
Theorem | prjsprel 42590* | Utility theorem regarding the relation used in ℙ𝕣𝕠𝕛. (Contributed by Steven Nguyen, 29-Apr-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} ⇒ ⊢ (𝑋 ∼ 𝑌 ↔ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝐾 𝑋 = (𝑚 · 𝑌))) | ||
Theorem | prjspertr 42591* | The relation in ℙ𝕣𝕠𝕛 is transitive. (Contributed by Steven Nguyen, 1-May-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ ((𝑉 ∈ LMod ∧ (𝑋 ∼ 𝑌 ∧ 𝑌 ∼ 𝑍)) → 𝑋 ∼ 𝑍) | ||
Theorem | prjsperref 42592* | The relation in ℙ𝕣𝕠𝕛 is reflexive. (Contributed by Steven Nguyen, 30-Apr-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ (𝑉 ∈ LMod → (𝑋 ∈ 𝐵 ↔ 𝑋 ∼ 𝑋)) | ||
Theorem | prjspersym 42593* | The relation in ℙ𝕣𝕠𝕛 is symmetric. (Contributed by Steven Nguyen, 1-May-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∼ 𝑌) → 𝑌 ∼ 𝑋) | ||
Theorem | prjsper 42594* | The relation used to define ℙ𝕣𝕠𝕛 is an equivalence relation. (Contributed by Steven Nguyen, 1-May-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ (𝑉 ∈ LVec → ∼ Er 𝐵) | ||
Theorem | prjspreln0 42595* | Two nonzero vectors are equivalent by a nonzero scalar. (Contributed by Steven Nguyen, 31-May-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑆) ⇒ ⊢ (𝑉 ∈ LVec → (𝑋 ∼ 𝑌 ↔ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ (𝐾 ∖ { 0 })𝑋 = (𝑚 · 𝑌)))) | ||
Theorem | prjspvs 42596* | A nonzero multiple of a vector is equivalent to the vector. (Contributed by Steven Nguyen, 6-Jun-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑆) ⇒ ⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ (𝐾 ∖ { 0 })) → (𝑁 · 𝑋) ∼ 𝑋) | ||
Theorem | prjsprellsp 42597* | Two vectors are equivalent iff their spans are equal. (Contributed by Steven Nguyen, 31-May-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑁 = (LSpan‘𝑉) ⇒ ⊢ ((𝑉 ∈ LVec ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∼ 𝑌 ↔ (𝑁‘{𝑋}) = (𝑁‘{𝑌}))) | ||
Theorem | prjspeclsp 42598* | The vectors equivalent to a vector 𝑋 are the nonzero vectors in the span of 𝑋. (Contributed by Steven Nguyen, 6-Jun-2023.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝐾 𝑥 = (𝑙 · 𝑦))} & ⊢ 𝐵 = ((Base‘𝑉) ∖ {(0g‘𝑉)}) & ⊢ 𝑆 = (Scalar‘𝑉) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑁 = (LSpan‘𝑉) ⇒ ⊢ ((𝑉 ∈ LVec ∧ 𝑋 ∈ 𝐵) → [𝑋] ∼ = ((𝑁‘{𝑋}) ∖ {(0g‘𝑉)})) | ||
Theorem | prjspval2 42599* | Alternate definition of projective space. (Contributed by Steven Nguyen, 7-Jun-2023.) |
⊢ 0 = (0g‘𝑉) & ⊢ 𝐵 = ((Base‘𝑉) ∖ { 0 }) & ⊢ 𝑁 = (LSpan‘𝑉) ⇒ ⊢ (𝑉 ∈ LVec → (ℙ𝕣𝕠𝕛‘𝑉) = ∪ 𝑧 ∈ 𝐵 {((𝑁‘{𝑧}) ∖ { 0 })}) | ||
Syntax | cprjspn 42600 | Extend class notation with the n-dimensional projective space function. |
class ℙ𝕣𝕠𝕛n |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |