P. 415 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 41401-41500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	riccrng1 41401	Ring isomorphism preserves (multiplicative) commutativity. (Contributed by SN, 10-Jan-2025.)
⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ CRing) → 𝑆 ∈ CRing)
Theorem	riccrng 41402	A ring is commutative if and only if an isomorphic ring is commutative. (Contributed by SN, 10-Jan-2025.)
⊢ (𝑅 ≃𝑟 𝑆 → (𝑅 ∈ CRing ↔ 𝑆 ∈ CRing))
Theorem	drnginvrn0d 41403	A multiplicative inverse in a division ring is nonzero. (recne0d 11989 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐼‘𝑋) ≠ 0 )
Theorem	drngmulcanad 41404	Cancellation of a nonzero factor on the left for multiplication. (mulcanad 11854 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ≠ 0 )    &   ⊢ (𝜑 → (𝑍 · 𝑋) = (𝑍 · 𝑌))    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	drngmulcan2ad 41405	Cancellation of a nonzero factor on the right for multiplication. (mulcan2ad 11855 analog). (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ≠ 0 )    &   ⊢ (𝜑 → (𝑋 · 𝑍) = (𝑌 · 𝑍))    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	drnginvmuld 41406	Inverse of a nonzero product. (Contributed by SN, 14-Aug-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐼 = (invr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ≠ 0 )    &   ⊢ (𝜑 → 𝑌 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐼‘(𝑋 · 𝑌)) = ((𝐼‘𝑌) · (𝐼‘𝑋)))
Theorem	ricdrng1 41407	A ring isomorphism maps a division ring to a division ring. (Contributed by SN, 18-Feb-2025.)
⊢ ((𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ DivRing) → 𝑆 ∈ DivRing)
Theorem	ricdrng 41408	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 41409	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 41410	A vector space is a group. (Contributed by SN, 28-May-2023.)
⊢ (𝑊 ∈ LVec → 𝑊 ∈ Grp)
Theorem	lvecring 41411	The scalar component of a vector space is a ring. (Contributed by SN, 28-May-2023.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ LVec → 𝐹 ∈ Ring)
Theorem	frlm0vald 41412	All coordinates of the zero vector are zero. (Contributed by SN, 14-Aug-2024.)
⊢ 𝐹 = (𝑅 freeLMod 𝐼)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐼)    ⇒   ⊢ (𝜑 → ((0g‘𝐹)‘𝐽) = 0 )
Theorem	frlmsnic 41413*	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 41414	A unit vector is a vector. (Contributed by Steven Nguyen, 16-Jul-2023.)
⊢ 𝑈 = (𝑅 unitVec 𝐼)    &   ⊢ 𝑌 = (𝑅 freeLMod 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼) → (𝑈‘𝐽) ∈ 𝐵)
Theorem	uvcn0 41415	A unit vector is nonzero. (Contributed by Steven Nguyen, 16-Jul-2023.)
⊢ 𝑈 = (𝑅 unitVec 𝐼)    &   ⊢ 𝑌 = (𝑅 freeLMod 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 0 = (0g‘𝑌)    ⇒   ⊢ ((𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼) → (𝑈‘𝐽) ≠ 0 )
Theorem	pwselbasr 41416	The reverse direction of pwselbasb 17439: 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 41417*	Finite products in a power structure are taken componentwise. Compare pwsgsum 19892. (Contributed by SN, 30-Jul-2024.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 1 = (1r‘𝑌)    &   ⊢ 𝑀 = (mulGrp‘𝑌)    &   ⊢ 𝑇 = (mulGrp‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽)) → 𝑈 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) finSupp 1 )    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ (𝑇 Σg (𝑦 ∈ 𝐽 ↦ 𝑈))))
Theorem	psrbagres 41418*	Restrict a bag of variables in 𝐼 to a bag of variables in 𝐽 ⊆ 𝐼. (Contributed by SN, 10-Mar-2025.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝐸 = {𝑔 ∈ (ℕ0 ↑m 𝐽) ∣ (◡𝑔 “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐽) ∈ 𝐸)
Theorem	mpllmodd 41419	The polynomial ring is a left module. (Contributed by SN, 12-Mar-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑃 ∈ LMod)
Theorem	mplringd 41420	The polynomial ring is a ring. (Contributed by SN, 7-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑃 ∈ Ring)
Theorem	mplcrngd 41421	The polynomial ring is a commutative ring. (Contributed by SN, 7-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → 𝑃 ∈ CRing)
Theorem	mplsubrgcl 41422	An element of a polynomial algebra over a subring is an element of the polynomial algebra. (Contributed by SN, 9-Feb-2025.)
⊢ 𝑊 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐶 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝐶)
Theorem	mhmcompl 41423	The composition of a monoid homomorphism and a polynomial is a polynomial. (Contributed by SN, 7-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑄 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 MndHom 𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈ 𝐶)
Theorem	rhmmpllem1 41424*	Lemma for rhmmpl 41428. A subproof of psrmulcllem 21726. (Contributed by SN, 8-Feb-2025.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅))    &   ⊢ (𝜑 → 𝑌:𝐷⟶(Base‘𝑅))    ⇒   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥)))) finSupp (0g‘𝑅))
Theorem	rhmmpllem2 41425*	Lemma for rhmmpl 41428. A subproof of psrmulcllem 21726. (Contributed by SN, 8-Feb-2025.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅))    &   ⊢ (𝜑 → 𝑌:𝐷⟶(Base‘𝑅))    ⇒   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑋‘𝑥)(.r‘𝑅)(𝑌‘(𝑘 ∘f − 𝑥))))) ∈ (Base‘𝑅))
Theorem	mhmcoaddmpl 41426	Show that the ring homomorphism in rhmmpl 41428 preserves addition. (Contributed by SN, 8-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑄 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ + = (+g‘𝑃)    &   ⊢ ✚ = (+g‘𝑄)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 MndHom 𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻 ∘ (𝐹 + 𝐺)) = ((𝐻 ∘ 𝐹) ✚ (𝐻 ∘ 𝐺)))
Theorem	rhmcomulmpl 41427	Show that the ring homomorphism in rhmmpl 41428 preserves multiplication. (Contributed by SN, 8-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑄 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐶 = (Base‘𝑄)    &   ⊢ · = (.r‘𝑃)    &   ⊢ ∙ = (.r‘𝑄)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻 ∘ (𝐹 · 𝐺)) = ((𝐻 ∘ 𝐹) ∙ (𝐻 ∘ 𝐺)))
Theorem	rhmmpl 41428*	Provide a ring homomorphism between two polynomial algebras over their respective base rings given a ring homomorphism between the two base rings. Compare pwsco2rhm 20395. TODO: Currently mhmvlin 22120 would have to be moved up. Investigate the usefulness of surrounding theorems like mndvcl 22114 and the difference between mhmvlin 22120, ofco 7696, and ofco2 22174. (Contributed by SN, 8-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑄 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ (𝐻 ∘ 𝑝))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑄))
Theorem	mplascl0 41429	The zero scalar as a polynomial. (Contributed by SN, 23-Nov-2024.)
⊢ 𝑊 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝑂 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → (𝐴‘𝑂) = 0 )
Theorem	mplascl1 41430	The one scalar as a polynomial. (Contributed by SN, 12-Mar-2025.)
⊢ 𝑊 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ 𝑂 = (1r‘𝑅)    &   ⊢ 1 = (1r‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → (𝐴‘𝑂) = 1 )
Theorem	mplmapghm 41431*	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 41432	The zero polynomial evaluates to zero. (Contributed by SN, 23-Nov-2024.)
⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑂 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → (𝑄‘ 0 ) = ((𝐵 ↑m 𝐼) × {𝑂}))
Theorem	evlscl 41433	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 41434*	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 41435*	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 41436*	Lemma for evlsvvval 41438 akin to psrbagev2 21860. (Contributed by SN, 6-Mar-2025.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑀 = (mulGrp‘𝑆)    &   ⊢ ↑ = (.g‘𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝑣 ∈ 𝐼 ↦ ((𝐵‘𝑣) ↑ (𝐴‘𝑣)))) ∈ 𝐾)
Theorem	evlsvvvallem2 41437*	Lemma for theorems using evlsvvval 41438. (Contributed by SN, 8-Mar-2025.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝑀 = (mulGrp‘𝑆)    &   ⊢ ↑ = (.g‘𝑀)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑣 ∈ 𝐼 ↦ ((𝑏‘𝑣) ↑ (𝐴‘𝑣)))))) finSupp (0g‘𝑆))
Theorem	evlsvvval 41438*	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 41439	Polynomial evaluation builder for a scalar. Compare evl1scad 22075. Note that scalar multiplication by 𝑋 is the same as vector multiplication by (𝐴‘𝑋) by asclmul1 21660. (Contributed by SN, 27-Jul-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑅)    &   ⊢ (𝜑 → 𝐿 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((𝐴‘𝑋) ∈ 𝐵 ∧ ((𝑄‘(𝐴‘𝑋))‘𝐿) = 𝑋))
Theorem	evlsvarval 41440	Polynomial evaluation builder for a variable. (Contributed by SN, 27-Jul-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑉 = (𝐼 mVar 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((𝑉‘𝑋) ∈ 𝐵 ∧ ((𝑄‘(𝑉‘𝑋))‘𝐴) = (𝐴‘𝑋)))
Theorem	evlsbagval 41441*	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 41442	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 41443	Polynomial evaluation builder for addition. (Contributed by SN, 27-Jul-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    &   ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉))    &   ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊))    &   ⊢ ✚ = (+g‘𝑃)    &   ⊢ + = (+g‘𝑆)    ⇒   ⊢ (𝜑 → ((𝑀 ✚ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ✚ 𝑁))‘𝐴) = (𝑉 + 𝑊)))
Theorem	evlsmulval 41444	Polynomial evaluation builder for multiplication. (Contributed by SN, 27-Jul-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    &   ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉))    &   ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊))    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ · = (.r‘𝑆)    ⇒   ⊢ (𝜑 → ((𝑀 ∙ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ∙ 𝑁))‘𝐴) = (𝑉 · 𝑊)))
Theorem	evlsmaprhm 41445*	The function 𝐹 mapping polynomials 𝑝 to their subring evaluation at a given point 𝑋 is a ring homomorphism. Compare evls1maprhm 33045. (Contributed by SN, 12-Mar-2025.)
⊢ 𝑄 = ((𝐼 evalSub 𝑅)‘𝑆)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑈)    &   ⊢ 𝑈 = (𝑅 ↾s 𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ ((𝑄‘𝑝)‘𝐴))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingHom 𝑅))
Theorem	evlsevl 41446	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 41447	A polynomial over the ring 𝑅 evaluates to an element in 𝑅. (Contributed by SN, 12-Mar-2025.)
⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → ((𝑄‘𝐹)‘𝐴) ∈ 𝐾)
Theorem	evlvvval 41448*	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 41449*	Lemma for theorems using evlvvval 41448. Version of evlsvvvallem2 41437 using df-evl 21856. (Contributed by SN, 11-Mar-2025.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ ↑ = (.g‘𝑀)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    ⇒   ⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑣 ∈ 𝐼 ↦ ((𝑏‘𝑣) ↑ (𝐴‘𝑣)))))) finSupp (0g‘𝑅))
Theorem	evladdval 41450	Polynomial evaluation builder for addition. (Contributed by SN, 9-Feb-2025.)
⊢ 𝑄 = (𝐼 eval 𝑆)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ ✚ = (+g‘𝑃)    &   ⊢ + = (+g‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    &   ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉))    &   ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊))    ⇒   ⊢ (𝜑 → ((𝑀 ✚ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ✚ 𝑁))‘𝐴) = (𝑉 + 𝑊)))
Theorem	evlmulval 41451	Polynomial evaluation builder for multiplication. (Contributed by SN, 18-Feb-2025.)
⊢ 𝑄 = (𝐼 eval 𝑆)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    &   ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉))    &   ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ ((𝑄‘𝑁)‘𝐴) = 𝑊))    ⇒   ⊢ (𝜑 → ((𝑀 ∙ 𝑁) ∈ 𝐵 ∧ ((𝑄‘(𝑀 ∙ 𝑁))‘𝐴) = (𝑉 · 𝑊)))
Theorem	selvcllem1 41452	𝑇 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 41453	𝐷 is a ring homomorphism. (Contributed by SN, 15-Dec-2023.)
⊢ 𝑈 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐶 = (algSc‘𝑇)    &   ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → 𝐷 ∈ (𝑅 RingHom 𝑇))
Theorem	selvcllem3 41454	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 41455	Apply the third argument (selvcllem3 41454) 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 41456	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 41457*	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 41458	Closure of the "variable selection" function. (Contributed by SN, 22-Feb-2024.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐸 = (Base‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) ∈ 𝐸)
Theorem	selvval2 41459*	Value of the "variable selection" function. Convert selvval 21901 into a simpler form by using evlsevl 41446. (Contributed by SN, 9-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐶 = (algSc‘𝑇)    &   ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) = (((𝐼 eval 𝑇)‘(𝐷 ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))))
Theorem	selvvvval 41460*	Recover the original polynomial from a selectVars application. (Contributed by SN, 15-Mar-2025.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (((((𝐼 selectVars 𝑅)‘𝐽)‘𝐹)‘(𝑌 ↾ 𝐽))‘(𝑌 ↾ (𝐼 ∖ 𝐽))) = (𝐹‘𝑌))
Theorem	evlselvlem 41461*	Lemma for evlselv 41462. 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 41462	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 41463	The "variable selection" function is additive. (Contributed by SN, 7-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ + = (+g‘𝑃)    &   ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ ✚ = (+g‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘(𝐹 + 𝐺)) = ((((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) ✚ (((𝐼 selectVars 𝑅)‘𝐽)‘𝐺)))
Theorem	selvmul 41464	The "variable selection" function is multiplicative. (Contributed by SN, 18-Feb-2025.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ · = (.r‘𝑃)    &   ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ ∙ = (.r‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘(𝐹 · 𝐺)) = ((((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) ∙ (((𝐼 selectVars 𝑅)‘𝐽)‘𝐺)))
Theorem	fsuppind 41465*	Induction on functions 𝐹:𝐴⟶𝐵 with finite support, or in other words the base set of the free module (see frlmelbas 21531 and frlmplusgval 21539). This theorem is structurally general for polynomial proof usage (see mplelbas 21770 and mpladd 21788). 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 41466*	Lemma for fsuppssind 41468. Functions are zero outside of their support. (Contributed by SN, 15-Jul-2024.)
⊢ (𝜑 → 0 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐼⟶𝐵)    &   ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝑆)    ⇒   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, ((𝐹 ↾ 𝑆)‘𝑥), 0 )))
Theorem	fsuppssindlem2 41467*	Lemma for fsuppssind 41468. Write a function as a union. (Contributed by SN, 15-Jul-2024.)
⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐼)    ⇒   ⊢ (𝜑 → (𝐹 ∈ {𝑓 ∈ (𝐵 ↑m 𝑆) ∣ (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑆, (𝑓‘𝑥), 0 )) ∈ 𝐻} ↔ (𝐹:𝑆⟶𝐵 ∧ (𝐹 ∪ ((𝐼 ∖ 𝑆) × { 0 })) ∈ 𝐻)))
Theorem	fsuppssind 41468*	Induction on functions 𝐹:𝐴⟶𝐵 with finite support (see fsuppind 41465) 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 41469*	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 41470*	Give a formula for the evaluation of a homogeneous polynomial given assignments from variables to values. The difference between this and evlsvvval 41438 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 41471*	Lemma for mhphf 41472. 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 41472	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 41473	A homogeneous polynomial defines a homogeneous function; this is mhphf 41472 with simpler notation in the conclusion in exchange for a complex definition of ∙, which is based on frlmvscafval 21541 but without the finite support restriction (frlmpws 21525, frlmbas 21530) on the assignments 𝐴 from variables to values. TODO?: Polynomials (df-mpl 21684) 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 41474	A homogeneous polynomial defines a homogeneous function; this is mhphf2 41473 with the finite support restriction (frlmpws 21525, frlmbas 21530) on the assignments 𝐴 from variables to values. See comment of mhphf2 41473. (Contributed by SN, 23-Nov-2024.)
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   ⊢ 𝐻 = (𝐼 mHomP 𝑈)    &   ⊢ 𝑈 = (𝑆 ↾s 𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐹 = (𝑆 freeLMod 𝐼)    &   ⊢ 𝑀 = (Base‘𝐹)    &   ⊢ ∙ = ( ·𝑠 ‘𝐹)    &   ⊢ · = (.r‘𝑆)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑆))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))    &   ⊢ (𝜑 → 𝐿 ∈ 𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑀)    ⇒   ⊢ (𝜑 → ((𝑄‘𝑋)‘(𝐿 ∙ 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)))
Theorem	mhphf4 41475	A homogeneous polynomial defines a homogeneous function; this is mhphf3 41474 with evalSub collapsed to eval. (Contributed by SN, 23-Nov-2024.)
⊢ 𝑄 = (𝐼 eval 𝑆)    &   ⊢ 𝐻 = (𝐼 mHomP 𝑆)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐹 = (𝑆 freeLMod 𝐼)    &   ⊢ 𝑀 = (Base‘𝐹)    &   ⊢ ∙ = ( ·𝑠 ‘𝐹)    &   ⊢ · = (.r‘𝑆)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑆))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐿 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑀)    ⇒   ⊢ (𝜑 → ((𝑄‘𝑋)‘(𝐿 ∙ 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)))
21.28.3  Arithmetic theorems 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 11183 is used in mulrid 11217 related theorems, so one could trade off the extra axioms in mulrid 11217 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 11170; in the other direction, real number closure laws can be avoided by using ax-resscn 11170 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 11178, ax-1cn 11171, and ax-addcl 11173. (And in practice, the expression isn't fully expanded into ones.) Multiplication by 1 requires either mullidi 11224 or (ax-1rid 11183 and 1re 11219) as seen in 1t1e1 12379 and 1t1e1ALT 41479. Multiplying with greater natural numbers uses ax-distr 11180. 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 11177 (see readdrid 41585 and readdlid 41579).
Theorem	c0exALT 41476	Alternate proof of c0ex 11213 using more set theory axioms but fewer complex number axioms (add ax-10 2136, ax-11 2153, ax-13 2370, ax-nul 5307, and remove ax-1cn 11171, ax-icn 11172, ax-addcl 11173, and ax-mulcl 11175). (Contributed by Steven Nguyen, 4-Dec-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 0 ∈ V
Theorem	0cnALT3 41477	Alternate proof of 0cn 11211 using ax-resscn 11170, ax-addrcl 11174, ax-rnegex 11184, ax-cnre 11186 instead of ax-icn 11172, ax-addcl 11173, ax-mulcl 11175, ax-i2m1 11181. Version of 0cnALT 11453 using ax-1cn 11171 instead of ax-icn 11172. (Contributed by Steven Nguyen, 7-Jan-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 0 ∈ ℂ
Theorem	elre0re 41478	Specialized version of 0red 11222 without using ax-1cn 11171 and ax-cnre 11186. (Contributed by Steven Nguyen, 28-Jan-2023.)
⊢ (𝐴 ∈ ℝ → 0 ∈ ℝ)
Theorem	1t1e1ALT 41479	Alternate proof of 1t1e1 12379 using a different set of axioms (add ax-mulrcl 11176, ax-i2m1 11181, ax-1ne0 11182, ax-rrecex 11185 and remove ax-resscn 11170, ax-mulcom 11177, ax-mulass 11179, ax-distr 11180). (Contributed by Steven Nguyen, 20-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (1 · 1) = 1
Theorem	remulcan2d 41480	mulcan2d 11853 for real numbers using fewer axioms. (Contributed by Steven Nguyen, 15-Apr-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ 𝐴 = 𝐵))
Theorem	readdridaddlidd 41481	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 11393, 𝐴 is the right additive identity. (Contributed by Steven Nguyen, 14-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝐵 + 𝐴) = 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ ℝ) → (𝐴 + 𝐶) = 𝐶)
Theorem	sn-1ne2 41482	A proof of 1ne2 12425 without using ax-mulcom 11177, ax-mulass 11179, ax-pre-mulgt0 11190. Based on mul02lem2 11396. (Contributed by SN, 13-Dec-2023.)
⊢ 1 ≠ 2
Theorem	nnn1suc 41483*	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 41484	Addition with 1 is commutative for natural numbers. (Contributed by Steven Nguyen, 9-Dec-2022.)
⊢ (𝐴 ∈ ℕ → (𝐴 + 1) = (1 + 𝐴))
Theorem	nnaddcom 41485	Addition is commutative for natural numbers. Uses fewer axioms than addcom 11405. (Contributed by Steven Nguyen, 9-Dec-2022.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	nnaddcomli 41486	Version of addcomli 11411 for natural numbers. (Contributed by Steven Nguyen, 1-Aug-2023.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ (𝐴 + 𝐵) = 𝐶    ⇒   ⊢ (𝐵 + 𝐴) = 𝐶
Theorem	nnadddir 41487	Right-distributivity for natural numbers without ax-mulcom 11177. (Contributed by SN, 5-Feb-2024.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Theorem	nnmul1com 41488	Multiplication with 1 is commutative for natural numbers, without ax-mulcom 11177. Since (𝐴 · 1) is 𝐴 by ax-1rid 11183, this is equivalent to remullid 41609 for natural numbers, but using fewer axioms (avoiding ax-resscn 11170, ax-addass 11178, ax-mulass 11179, ax-rnegex 11184, ax-pre-lttri 11187, ax-pre-lttrn 11188, ax-pre-ltadd 11189). (Contributed by SN, 5-Feb-2024.)
⊢ (𝐴 ∈ ℕ → (1 · 𝐴) = (𝐴 · 1))
Theorem	nnmulcom 41489	Multiplication is commutative for natural numbers. (Contributed by SN, 5-Feb-2024.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	mvrrsubd 41490	Move a subtraction in the RHS to a right-addition in the LHS. Converse of mvlraddd 11629. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = (𝐵 − 𝐶))    ⇒   ⊢ (𝜑 → (𝐴 + 𝐶) = 𝐵)
Theorem	laddrotrd 41491	Rotate the variables right in an equation with addition on the left, converting it into a subtraction. Version of mvlladdd 11630 with a commuted consequent, and of mvrladdd 11632 with a commuted hypothesis. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → (𝐶 − 𝐴) = 𝐵)
Theorem	raddcom12d 41492	Swap the first two variables in an equation with addition on the right, converting it into a subtraction. Version of mvrraddd 11631 with a commuted consequent, and of mvlraddd 11629 with a commuted hypothesis. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = (𝐵 + 𝐶))    ⇒   ⊢ (𝜑 → 𝐵 = (𝐴 − 𝐶))
Theorem	lsubrotld 41493	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 41494	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 41495	Relation between sums and differences. (Contributed by Steven Nguyen, 5-Jan-2023.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐴 − 𝐶) = (𝐷 − 𝐵)))
Theorem	sqsumi 41496	A sum squared. (Contributed by Steven Nguyen, 16-Sep-2022.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) · (𝐴 + 𝐵)) = (((𝐴 · 𝐴) + (𝐵 · 𝐵)) + (2 · (𝐴 · 𝐵)))
Theorem	negn0nposznnd 41497	Lemma for dffltz 41679. (Contributed by Steven Nguyen, 27-Feb-2023.)
⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → ¬ 0 < 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → -𝐴 ∈ ℕ)
Theorem	sqmid3api 41498	Value of the square of the middle term of a 3-term arithmetic progression. (Contributed by Steven Nguyen, 20-Sep-2022.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝑁 ∈ ℂ    &   ⊢ (𝐴 + 𝑁) = 𝐵    &   ⊢ (𝐵 + 𝑁) = 𝐶    ⇒   ⊢ (𝐵 · 𝐵) = ((𝐴 · 𝐶) + (𝑁 · 𝑁))
Theorem	decaddcom 41499	Commute ones place in addition. (Contributed by Steven Nguyen, 29-Jan-2023.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    ⇒   ⊢ (;𝐴𝐵 + 𝐶) = (;𝐴𝐶 + 𝐵)
Theorem	sqn5i 41500	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