![]() |
Metamath
Proof Explorer Theorem List (p. 420 of 485) | < 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-30800) |
![]() (30801-32323) |
![]() (32324-48421) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ricfld 41901 | 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 41902 | A vector space is a group. (Contributed by SN, 28-May-2023.) |
⊢ (𝑊 ∈ LVec → 𝑊 ∈ Grp) | ||
Theorem | lvecring 41903 | The scalar component of a vector space is a ring. (Contributed by SN, 28-May-2023.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec → 𝐹 ∈ Ring) | ||
Theorem | frlm0vald 41904 | All coordinates of the zero vector are zero. (Contributed by SN, 14-Aug-2024.) |
⊢ 𝐹 = (𝑅 freeLMod 𝐼) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝐽 ∈ 𝐼) ⇒ ⊢ (𝜑 → ((0g‘𝐹)‘𝐽) = 0 ) | ||
Theorem | frlmsnic 41905* | 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 41906 | A unit vector is a vector. (Contributed by Steven Nguyen, 16-Jul-2023.) |
⊢ 𝑈 = (𝑅 unitVec 𝐼) & ⊢ 𝑌 = (𝑅 freeLMod 𝐼) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼) → (𝑈‘𝐽) ∈ 𝐵) | ||
Theorem | uvcn0 41907 | A unit vector is nonzero. (Contributed by Steven Nguyen, 16-Jul-2023.) |
⊢ 𝑈 = (𝑅 unitVec 𝐼) & ⊢ 𝑌 = (𝑅 freeLMod 𝐼) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 0 = (0g‘𝑌) ⇒ ⊢ ((𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼) → (𝑈‘𝐽) ≠ 0 ) | ||
Theorem | pwselbasr 41908 | The reverse direction of pwselbasb 17473: 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 41909* | Finite products in a power structure are taken componentwise. Compare pwsgsum 19949. (Contributed by SN, 30-Jul-2024.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑌) & ⊢ 𝑀 = (mulGrp‘𝑌) & ⊢ 𝑇 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽)) → 𝑈 ∈ 𝐵) & ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) finSupp 1 ) ⇒ ⊢ (𝜑 → (𝑀 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ (𝑇 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)))) | ||
Theorem | psrmnd 41910 | The ring of power series is a monoid. (Contributed by SN, 25-Apr-2025.) |
⊢ 𝑆 = (𝐼 mPwSer 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Mnd) ⇒ ⊢ (𝜑 → 𝑆 ∈ Mnd) | ||
Theorem | psrbagres 41911* | 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 41912 | The polynomial ring is a commutative ring. (Contributed by SN, 7-Feb-2025.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → 𝑃 ∈ CRing) | ||
Theorem | mplsubrgcl 41913 | 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 41914 | 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 41915 | Show that the ring homomorphism in rhmpsr 41917 preserves addition. (Contributed by SN, 18-May-2025.) |
⊢ 𝑃 = (𝐼 mPwSer 𝑅) & ⊢ 𝑄 = (𝐼 mPwSer 𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Base‘𝑄) & ⊢ + = (+g‘𝑃) & ⊢ ✚ = (+g‘𝑄) & ⊢ (𝜑 → 𝐻 ∈ (𝑅 MndHom 𝑆)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐻 ∘ (𝐹 + 𝐺)) = ((𝐻 ∘ 𝐹) ✚ (𝐻 ∘ 𝐺))) | ||
Theorem | rhmcomulpsr 41916 | Show that the ring homomorphism in rhmpsr 41917 preserves multiplication. (Contributed by SN, 18-May-2025.) |
⊢ 𝑃 = (𝐼 mPwSer 𝑅) & ⊢ 𝑄 = (𝐼 mPwSer 𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐶 = (Base‘𝑄) & ⊢ · = (.r‘𝑃) & ⊢ ∙ = (.r‘𝑄) & ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐻 ∘ (𝐹 · 𝐺)) = ((𝐻 ∘ 𝐹) ∙ (𝐻 ∘ 𝐺))) | ||
Theorem | rhmpsr 41917* | 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 41918* | 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 41919 | The zero scalar as a polynomial. (Contributed by SN, 23-Nov-2024.) |
⊢ 𝑊 = (𝐼 mPoly 𝑅) & ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝑂 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (𝐴‘𝑂) = 0 ) | ||
Theorem | mplascl1 41920 | The one scalar as a polynomial. (Contributed by SN, 12-Mar-2025.) |
⊢ 𝑊 = (𝐼 mPoly 𝑅) & ⊢ 𝐴 = (algSc‘𝑊) & ⊢ 𝑂 = (1r‘𝑅) & ⊢ 1 = (1r‘𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (𝐴‘𝑂) = 1 ) | ||
Theorem | mplmapghm 41921* | 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 41922 | The zero polynomial evaluates to zero. (Contributed by SN, 23-Nov-2024.) |
⊢ 𝑄 = (𝐼 eval 𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑊 = (𝐼 mPoly 𝑅) & ⊢ 𝑂 = (0g‘𝑅) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → (𝑄‘ 0 ) = ((𝐵 ↑m 𝐼) × {𝑂})) | ||
Theorem | evlscl 41923 | 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 41924* | 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 41925* | 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 41926* | Lemma for evlsvvval 41928 akin to psrbagev2 22045. (Contributed by SN, 6-Mar-2025.) |
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑀 = (mulGrp‘𝑆) & ⊢ ↑ = (.g‘𝑀) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑀 Σg (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝐴‘𝑣)))) ∈ 𝐾) | ||
Theorem | evlsvvvallem2 41927* | Lemma for theorems using evlsvvval 41928. (Contributed by SN, 8-Mar-2025.) |
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑀 = (mulGrp‘𝑆) & ⊢ ↑ = (.g‘𝑀) & ⊢ · = (.r‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑣 ∈ 𝐼 ↦ ((𝑏‘𝑣) ↑ (𝐴‘𝑣)))))) finSupp (0g‘𝑆)) | ||
Theorem | evlsvvval 41928* | 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 41929 | Polynomial evaluation builder for a scalar. Compare evl1scad 22279. Note that scalar multiplication by 𝑋 is the same as vector multiplication by (𝐴‘𝑋) by asclmul1 21836. (Contributed by SN, 27-Jul-2024.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝑅) & ⊢ (𝜑 → 𝐿 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → ((𝐴‘𝑋) ∈ 𝐵 ∧ ((𝑄‘(𝐴‘𝑋))‘𝐿) = 𝑋)) | ||
Theorem | evlsvarval 41930 | Polynomial evaluation builder for a variable. (Contributed by SN, 27-Jul-2024.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑉 = (𝐼 mVar 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → ((𝑉‘𝑋) ∈ 𝐵 ∧ ((𝑄‘(𝑉‘𝑋))‘𝐴) = (𝐴‘𝑋))) | ||
Theorem | evlsbagval 41931* | 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 41932 | 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 41933 | Polynomial evaluation builder for addition. (Contributed by SN, 27-Jul-2024.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) & ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊)) & ⊢ ✚ = (+g‘𝑃) & ⊢ + = (+g‘𝑆) ⇒ ⊢ (𝜑 → ((𝑀 ✚ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ✚ 𝑁))‘𝐴) = (𝑉 + 𝑊))) | ||
Theorem | evlsmulval 41934 | Polynomial evaluation builder for multiplication. (Contributed by SN, 27-Jul-2024.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) & ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊)) & ⊢ ∙ = (.r‘𝑃) & ⊢ · = (.r‘𝑆) ⇒ ⊢ (𝜑 → ((𝑀 ∙ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ∙ 𝑁))‘𝐴) = (𝑉 · 𝑊))) | ||
Theorem | evlsmaprhm 41935* | The function 𝐹 mapping polynomials 𝑝 to their subring evaluation at a given point 𝑋 is a ring homomorphism. Compare evls1maprhm 22320. (Contributed by SN, 12-Mar-2025.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑅)‘𝑆) & ⊢ 𝑃 = (𝐼 mPoly 𝑈) & ⊢ 𝑈 = (𝑅 ↾s 𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ ((𝑄‘𝑝)‘𝐴)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑅)) | ||
Theorem | evlsevl 41936 | 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 41937 | A polynomial over the ring 𝑅 evaluates to an element in 𝑅. (Contributed by SN, 12-Mar-2025.) |
⊢ 𝑄 = (𝐼 eval 𝑅) & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → ((𝑄‘𝐹)‘𝐴) ∈ 𝐾) | ||
Theorem | evlvvval 41938* | 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 41939* | Lemma for theorems using evlvvval 41938. Version of evlsvvvallem2 41927 using df-evl 22041. (Contributed by SN, 11-Mar-2025.) |
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ ↑ = (.g‘𝑀) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑣 ∈ 𝐼 ↦ ((𝑏‘𝑣) ↑ (𝐴‘𝑣)))))) finSupp (0g‘𝑅)) | ||
Theorem | evladdval 41940 | Polynomial evaluation builder for addition. (Contributed by SN, 9-Feb-2025.) |
⊢ 𝑄 = (𝐼 eval 𝑆) & ⊢ 𝑃 = (𝐼 mPoly 𝑆) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ ✚ = (+g‘𝑃) & ⊢ + = (+g‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) & ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊)) ⇒ ⊢ (𝜑 → ((𝑀 ✚ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ✚ 𝑁))‘𝐴) = (𝑉 + 𝑊))) | ||
Theorem | evlmulval 41941 | Polynomial evaluation builder for multiplication. (Contributed by SN, 18-Feb-2025.) |
⊢ 𝑄 = (𝐼 eval 𝑆) & ⊢ 𝑃 = (𝐼 mPoly 𝑆) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ ∙ = (.r‘𝑃) & ⊢ · = (.r‘𝑆) & ⊢ (𝜑 → 𝐼 ∈ 𝑍) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) & ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉)) & ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊)) ⇒ ⊢ (𝜑 → ((𝑀 ∙ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ∙ 𝑁))‘𝐴) = (𝑉 · 𝑊))) | ||
Theorem | selvcllem1 41942 | 𝑇 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 41943 | 𝐷 is a ring homomorphism. (Contributed by SN, 15-Dec-2023.) |
⊢ 𝑈 = (𝐼 mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ 𝐶 = (algSc‘𝑇) & ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ CRing) ⇒ ⊢ (𝜑 → 𝐷 ∈ (𝑅 RingHom 𝑇)) | ||
Theorem | selvcllem3 41944 | 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 41945 | Apply the third argument (selvcllem3 41944) 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 41946 | 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 41947* | 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 41948 | Closure of the "variable selection" function. (Contributed by SN, 22-Feb-2024.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ 𝐸 = (Base‘𝑇) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) ∈ 𝐸) | ||
Theorem | selvval2 41949* | Value of the "variable selection" function. Convert selvval 22083 into a simpler form by using evlsevl 41936. (Contributed by SN, 9-Feb-2025.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ 𝐶 = (algSc‘𝑇) & ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈)) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) = (((𝐼 eval 𝑇)‘(𝐷 ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥)))))) | ||
Theorem | selvvvval 41950* | Recover the original polynomial from a selectVars application. (Contributed by SN, 15-Mar-2025.) |
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} & ⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐷) ⇒ ⊢ (𝜑 → (((((𝐼 selectVars 𝑅)‘𝐽)‘𝐹)‘(𝑌 ↾ 𝐽))‘(𝑌 ↾ (𝐼 ∖ 𝐽))) = (𝐹‘𝑌)) | ||
Theorem | evlselvlem 41951* | Lemma for evlselv 41952. 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 41952 | 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 41953 | The "variable selection" function is additive. (Contributed by SN, 7-Feb-2025.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ + = (+g‘𝑃) & ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ ✚ = (+g‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘(𝐹 + 𝐺)) = ((((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) ✚ (((𝐼 selectVars 𝑅)‘𝐽)‘𝐺))) | ||
Theorem | selvmul 41954 | The "variable selection" function is multiplicative. (Contributed by SN, 18-Feb-2025.) |
⊢ 𝑃 = (𝐼 mPoly 𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ · = (.r‘𝑃) & ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅) & ⊢ 𝑇 = (𝐽 mPoly 𝑈) & ⊢ ∙ = (.r‘𝑇) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐽 ⊆ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘(𝐹 · 𝐺)) = ((((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) ∙ (((𝐼 selectVars 𝑅)‘𝐽)‘𝐺))) | ||
Theorem | fsuppind 41955* | Induction on functions 𝐹:𝐴⟶𝐵 with finite support, or in other words the base set of the free module (see frlmelbas 21707 and frlmplusgval 21715). This theorem is structurally general for polynomial proof usage (see mplelbas 21953 and mpladd 21971). 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 41956* | Lemma for fsuppssind 41958. Functions are zero outside of their support. (Contributed by SN, 15-Jul-2024.) |
⊢ (𝜑 → 0 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝑆) ⇒ ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, ((𝐹 ↾ 𝑆)‘𝑥), 0 ))) | ||
Theorem | fsuppssindlem2 41957* | Lemma for fsuppssind 41958. Write a function as a union. (Contributed by SN, 15-Jul-2024.) |
⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ⊆ 𝐼) ⇒ ⊢ (𝜑 → (𝐹 ∈ {𝑓 ∈ (𝐵 ↑m 𝑆) ∣ (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, (𝑓‘𝑥), 0 )) ∈ 𝐻} ↔ (𝐹:𝑆⟶𝐵 ∧ (𝐹 ∪ ((𝐼 ∖ 𝑆) × { 0 })) ∈ 𝐻))) | ||
Theorem | fsuppssind 41958* | Induction on functions 𝐹:𝐴⟶𝐵 with finite support (see fsuppind 41955) 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 41959* | 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) & ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁)) & ⊢ (𝜑 → (𝐷 × { 0 }) ∈ 𝐺) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) → (𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) ∈ 𝐺) & ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐻‘𝑁) ∩ 𝐺) ∧ 𝑦 ∈ ((𝐻‘𝑁) ∩ 𝐺))) → (𝑥 + 𝑦) ∈ 𝐺) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝐺) | ||
Theorem | evlsmhpvvval 41960* | Give a formula for the evaluation of a homogeneous polynomial given assignments from variables to values. The difference between this and evlsvvval 41928 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‘𝑆)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐹 ∈ (𝐻‘𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → ((𝑄‘𝐹)‘𝐴) = (𝑆 Σg (𝑏 ∈ 𝐺 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))))) | ||
Theorem | mhphflem 41961* | Lemma for mhphf 41962. 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 41962 | 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‘𝑆)) & ⊢ (𝜑 → 𝐿 ∈ 𝑅) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴))) | ||
Theorem | mhphf2 41963 |
A homogeneous polynomial defines a homogeneous function; this is mhphf 41962
with simpler notation in the conclusion in exchange for a complex
definition of ∙, which is
based on frlmvscafval 21717 but without the
finite support restriction (frlmpws 21701, frlmbas 21706) on the assignments
𝐴 from variables to values.
TODO?: Polynomials (df-mpl 21861) 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‘𝑆)) & ⊢ (𝜑 → 𝐿 ∈ 𝑅) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) ⇒ ⊢ (𝜑 → ((𝑄‘𝑋)‘(𝐿 ∙ 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴))) | ||
Theorem | mhphf3 41964 | A homogeneous polynomial defines a homogeneous function; this is mhphf2 41963 with the finite support restriction (frlmpws 21701, frlmbas 21706) on the assignments 𝐴 from variables to values. See comment of mhphf2 41963. (Contributed by SN, 23-Nov-2024.) |
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) & ⊢ 𝐻 = (𝐼 mHomP 𝑈) & ⊢ 𝑈 = (𝑆 ↾s 𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐹 = (𝑆 freeLMod 𝐼) & ⊢ 𝑀 = (Base‘𝐹) & ⊢ ∙ = ( ·𝑠 ‘𝐹) & ⊢ · = (.r‘𝑆) & ⊢ ↑ = (.g‘(mulGrp‘𝑆)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) & ⊢ (𝜑 → 𝐿 ∈ 𝑅) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁)) & ⊢ (𝜑 → 𝐴 ∈ 𝑀) ⇒ ⊢ (𝜑 → ((𝑄‘𝑋)‘(𝐿 ∙ 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴))) | ||
Theorem | mhphf4 41965 | A homogeneous polynomial defines a homogeneous function; this is mhphf3 41964 with evalSub collapsed to eval. (Contributed by SN, 23-Nov-2024.) |
⊢ 𝑄 = (𝐼 eval 𝑆) & ⊢ 𝐻 = (𝐼 mHomP 𝑆) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐹 = (𝑆 freeLMod 𝐼) & ⊢ 𝑀 = (Base‘𝐹) & ⊢ ∙ = ( ·𝑠 ‘𝐹) & ⊢ · = (.r‘𝑆) & ⊢ ↑ = (.g‘(mulGrp‘𝑆)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐿 ∈ 𝐾) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁)) & ⊢ (𝜑 → 𝐴 ∈ 𝑀) ⇒ ⊢ (𝜑 → ((𝑄‘𝑋)‘(𝐿 ∙ 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴))) | ||
Towards the start of this section are several proofs regarding the different complex number axioms that could be used to prove some results. For example, ax-1rid 11210 is used in mulrid 11244 related theorems, so one could trade off the extra axioms in mulrid 11244 for the axioms needed to prove that something is a real number. Another example is avoiding complex number closure laws by using real number closure laws and then using ax-resscn 11197; in the other direction, real number closure laws can be avoided by using ax-resscn 11197 and then the complex number closure laws. (This only works if the result of (𝐴 + 𝐵) only needs to be a complex number). The natural numbers are especially amenable to axiom reductions, as the set ℕ is the recursive set {1, (1 + 1), ((1 + 1) + 1)}, etc., i.e. the set of numbers formed by only additions of 1. The digits 2 through 9 are defined so that they expand into additions of 1. This conveniently allows for adding natural numbers by rearranging parentheses, as shown below: (4 + 3) = 7 ((3 + 1) + (2 + 1)) = (6 + 1) ((((1 + 1) + 1) + 1) + ((1 + 1) + 1)) = ((((((1 + 1) + 1) + 1) + 1) + 1) + 1) This only requires ax-addass 11205, ax-1cn 11198, and ax-addcl 11200. (And in practice, the expression isn't fully expanded into ones.) Multiplication by 1 requires either mullidi 11251 or (ax-1rid 11210 and 1re 11246) as seen in 1t1e1 12407 and 1t1e1ALT 41969. Multiplying with greater natural numbers uses ax-distr 11207. Still, this takes fewer axioms than adding zero, which is often implicit in theorems such as (9 + 1) = ;10. Adding zero uses almost every complex number axiom, though notably not ax-mulcom 11204 (see readdrid 42096 and readdlid 42090). | ||
Theorem | c0exALT 41966 | Alternate proof of c0ex 11240 using more set theory axioms but fewer complex number axioms (add ax-10 2129, ax-11 2146, ax-13 2365, ax-nul 5307, and remove ax-1cn 11198, ax-icn 11199, ax-addcl 11200, and ax-mulcl 11202). (Contributed by Steven Nguyen, 4-Dec-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 0 ∈ V | ||
Theorem | 0cnALT3 41967 | Alternate proof of 0cn 11238 using ax-resscn 11197, ax-addrcl 11201, ax-rnegex 11211, ax-cnre 11213 instead of ax-icn 11199, ax-addcl 11200, ax-mulcl 11202, ax-i2m1 11208. Version of 0cnALT 11480 using ax-1cn 11198 instead of ax-icn 11199. (Contributed by Steven Nguyen, 7-Jan-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 0 ∈ ℂ | ||
Theorem | elre0re 41968 | Specialized version of 0red 11249 without using ax-1cn 11198 and ax-cnre 11213. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → 0 ∈ ℝ) | ||
Theorem | 1t1e1ALT 41969 | Alternate proof of 1t1e1 12407 using a different set of axioms (add ax-mulrcl 11203, ax-i2m1 11208, ax-1ne0 11209, ax-rrecex 11212 and remove ax-resscn 11197, ax-mulcom 11204, ax-mulass 11206, ax-distr 11207). (Contributed by Steven Nguyen, 20-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (1 · 1) = 1 | ||
Theorem | remulcan2d 41970 | mulcan2d 11880 for real numbers using fewer axioms. (Contributed by Steven Nguyen, 15-Apr-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | readdridaddlidd 41971 | Given some real number 𝐵 where 𝐴 acts like a right additive identity, derive that 𝐴 is a left additive identity. Note that the hypothesis is weaker than proving that 𝐴 is a right additive identity (for all numbers). Although, if there is a right additive identity, then by readdcan 11420, 𝐴 is the right additive identity. (Contributed by Steven Nguyen, 14-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐵 + 𝐴) = 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ ℝ) → (𝐴 + 𝐶) = 𝐶) | ||
Theorem | sn-1ne2 41972 | A proof of 1ne2 12453 without using ax-mulcom 11204, ax-mulass 11206, ax-pre-mulgt0 11217. Based on mul02lem2 11423. (Contributed by SN, 13-Dec-2023.) |
⊢ 1 ≠ 2 | ||
Theorem | nnn1suc 41973* | A positive integer that is not 1 is a successor of some other positive integer. (Contributed by Steven Nguyen, 19-Aug-2023.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐴 ≠ 1) → ∃𝑥 ∈ ℕ (𝑥 + 1) = 𝐴) | ||
Theorem | nnadd1com 41974 | Addition with 1 is commutative for natural numbers. (Contributed by Steven Nguyen, 9-Dec-2022.) |
⊢ (𝐴 ∈ ℕ → (𝐴 + 1) = (1 + 𝐴)) | ||
Theorem | nnaddcom 41975 | Addition is commutative for natural numbers. Uses fewer axioms than addcom 11432. (Contributed by Steven Nguyen, 9-Dec-2022.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Theorem | nnaddcomli 41976 | Version of addcomli 11438 for natural numbers. (Contributed by Steven Nguyen, 1-Aug-2023.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ & ⊢ (𝐴 + 𝐵) = 𝐶 ⇒ ⊢ (𝐵 + 𝐴) = 𝐶 | ||
Theorem | nnadddir 41977 | Right-distributivity for natural numbers without ax-mulcom 11204. (Contributed by SN, 5-Feb-2024.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))) | ||
Theorem | nnmul1com 41978 | Multiplication with 1 is commutative for natural numbers, without ax-mulcom 11204. Since (𝐴 · 1) is 𝐴 by ax-1rid 11210, this is equivalent to remullid 42120 for natural numbers, but using fewer axioms (avoiding ax-resscn 11197, ax-addass 11205, ax-mulass 11206, ax-rnegex 11211, ax-pre-lttri 11214, ax-pre-lttrn 11215, ax-pre-ltadd 11216). (Contributed by SN, 5-Feb-2024.) |
⊢ (𝐴 ∈ ℕ → (1 · 𝐴) = (𝐴 · 1)) | ||
Theorem | nnmulcom 41979 | Multiplication is commutative for natural numbers. (Contributed by SN, 5-Feb-2024.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Theorem | readdrcl2d 41980 | Reverse closure for addition: the second addend is real if the first addend is real and the sum is real. (Contributed by SN, 25-Apr-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐵 ∈ ℝ) | ||
Theorem | mvrrsubd 41981 | Move a subtraction in the RHS to a right-addition in the LHS. Converse of mvlraddd 11656. (Contributed by SN, 21-Aug-2024.) |
⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 = (𝐵 − 𝐶)) ⇒ ⊢ (𝜑 → (𝐴 + 𝐶) = 𝐵) | ||
Theorem | laddrotrd 41982 | Rotate the variables right in an equation with addition on the left, converting it into a subtraction. Version of mvlladdd 11657 with a commuted consequent, and of mvrladdd 11659 with a commuted hypothesis. (Contributed by SN, 21-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → (𝐶 − 𝐴) = 𝐵) | ||
Theorem | raddcom12d 41983 | Swap the first two variables in an equation with addition on the right, converting it into a subtraction. Version of mvrraddd 11658 with a commuted consequent, and of mvlraddd 11656 with a commuted hypothesis. (Contributed by SN, 21-Aug-2024.) |
⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 = (𝐵 + 𝐶)) ⇒ ⊢ (𝜑 → 𝐵 = (𝐴 − 𝐶)) | ||
Theorem | lsubrotld 41984 | Rotate the variables left in an equation with subtraction on the left, converting it into an addition. (Contributed by SN, 21-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 − 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → (𝐵 + 𝐶) = 𝐴) | ||
Theorem | lsubcom23d 41985 | Swap the second and third variables in an equation with subtraction on the left, converting it into an addition. (Contributed by SN, 23-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 − 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → (𝐴 − 𝐶) = 𝐵) | ||
Theorem | addsubeq4com 41986 | Relation between sums and differences. (Contributed by Steven Nguyen, 5-Jan-2023.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐴 − 𝐶) = (𝐷 − 𝐵))) | ||
Theorem | sqsumi 41987 | A sum squared. (Contributed by Steven Nguyen, 16-Sep-2022.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) · (𝐴 + 𝐵)) = (((𝐴 · 𝐴) + (𝐵 · 𝐵)) + (2 · (𝐴 · 𝐵))) | ||
Theorem | negn0nposznnd 41988 | Lemma for dffltz 42190. (Contributed by Steven Nguyen, 27-Feb-2023.) |
⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → ¬ 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ∈ ℤ) ⇒ ⊢ (𝜑 → -𝐴 ∈ ℕ) | ||
Theorem | sqmid3api 41989 | Value of the square of the middle term of a 3-term arithmetic progression. (Contributed by Steven Nguyen, 20-Sep-2022.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝑁 ∈ ℂ & ⊢ (𝐴 + 𝑁) = 𝐵 & ⊢ (𝐵 + 𝑁) = 𝐶 ⇒ ⊢ (𝐵 · 𝐵) = ((𝐴 · 𝐶) + (𝑁 · 𝑁)) | ||
Theorem | decaddcom 41990 | Commute ones place in addition. (Contributed by Steven Nguyen, 29-Jan-2023.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 ⇒ ⊢ (;𝐴𝐵 + 𝐶) = (;𝐴𝐶 + 𝐵) | ||
Theorem | sqn5i 41991 | The square of a number ending in 5. This shortcut only works because 5 is half of 10. (Contributed by Steven Nguyen, 16-Sep-2022.) |
⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ (;𝐴5 · ;𝐴5) = ;;(𝐴 · (𝐴 + 1))25 | ||
Theorem | sqn5ii 41992 | The square of a number ending in 5. This shortcut only works because 5 is half of 10. (Contributed by Steven Nguyen, 16-Sep-2022.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ (𝐴 + 1) = 𝐵 & ⊢ (𝐴 · 𝐵) = 𝐶 ⇒ ⊢ (;𝐴5 · ;𝐴5) = ;;𝐶25 | ||
Theorem | decpmulnc 41993 | Partial products algorithm for two digit multiplication, no carry. Compare muladdi 11697. (Contributed by Steven Nguyen, 9-Dec-2022.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ (𝐴 · 𝐶) = 𝐸 & ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹 & ⊢ (𝐵 · 𝐷) = 𝐺 ⇒ ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;;𝐸𝐹𝐺 | ||
Theorem | decpmul 41994 | Partial products algorithm for two digit multiplication. (Contributed by Steven Nguyen, 10-Dec-2022.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ (𝐴 · 𝐶) = 𝐸 & ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹 & ⊢ (𝐵 · 𝐷) = ;𝐺𝐻 & ⊢ (;𝐸𝐺 + 𝐹) = 𝐼 & ⊢ 𝐺 ∈ ℕ0 & ⊢ 𝐻 ∈ ℕ0 ⇒ ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;𝐼𝐻 | ||
Theorem | sqdeccom12 41995 | The square of a number in terms of its digits switched. (Contributed by Steven Nguyen, 3-Jan-2023.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 ⇒ ⊢ ((;𝐴𝐵 · ;𝐴𝐵) − (;𝐵𝐴 · ;𝐵𝐴)) = (;99 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) | ||
Theorem | sq3deccom12 41996 | Variant of sqdeccom12 41995 with a three digit square. (Contributed by Steven Nguyen, 3-Jan-2023.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ (𝐴 + 𝐶) = 𝐷 ⇒ ⊢ ((;;𝐴𝐵𝐶 · ;;𝐴𝐵𝐶) − (;𝐷𝐵 · ;𝐷𝐵)) = (;99 · ((;𝐴𝐵 · ;𝐴𝐵) − (𝐶 · 𝐶))) | ||
Theorem | 4t5e20 41997 | 4 times 5 equals 20. (Contributed by SN, 30-Mar-2025.) |
⊢ (4 · 5) = ;20 | ||
Theorem | sq9 41998 | The square of 9 is 81. (Contributed by SN, 30-Mar-2025.) |
⊢ (9↑2) = ;81 | ||
Theorem | 235t711 41999 |
Calculate a product by long multiplication as a base comparison with other
multiplication algorithms.
Conveniently, 711 has two ones which greatly simplifies calculations like 235 · 1. There isn't a higher level mulcomli 11255 saving the lower level uses of mulcomli 11255 within 235 · 7 since mulcom2 doesn't exist, but if commuted versions of theorems like 7t2e14 12819 are added then this proof would benefit more than ex-decpmul 42000. For practicality, this proof doesn't have "e167085" at the end of its name like 2p2e4 12380 or 8t7e56 12830. (Contributed by Steven Nguyen, 10-Dec-2022.) (New usage is discouraged.) |
⊢ (;;235 · ;;711) = ;;;;;167085 | ||
Theorem | ex-decpmul 42000 | Example usage of decpmul 41994. This proof is significantly longer than 235t711 41999. There is more unnecessary carrying compared to 235t711 41999. Although saving 5 visual steps, using mulcomli 11255 early on increases the compressed proof length. (Contributed by Steven Nguyen, 10-Dec-2022.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (;;235 · ;;711) = ;;;;;167085 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |