P. 338 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33701-33800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	r1pquslmic 33701*	The univariate polynomial remainder ring (𝐹 “s 𝑃) is module isomorphic with the quotient ring. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐹 = (𝑓 ∈ 𝑈 ↦ (𝑓𝐸𝑀))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑁)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝐾))    ⇒   ⊢ (𝜑 → 𝑄 ≃𝑚 (𝐹 “s 𝑃))
21.3.10.49  Multivariate Polynomials
Theorem	psrbasfsupp 33702	Rewrite a finite support for nonnegative integers : For functions mapping a set 𝐼 to the nonnegative integers, having finite support can also be written as having a finite preimage of the positive integers. The latter expression is used for example in psrbas 21916, but with the former expression, theorems about finite support can be used more directly. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ 𝑓 finSupp 0}    ⇒   ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}
Theorem	psrnzr 33703	The ring of power series over a nonzero ring form a nonzero ring. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    ⇒   ⊢ (𝜑 → 𝑆 ∈ NzRing)
Theorem	mplnzr 33704	The multivariate polynomials over a nonzero ring form a nonzero ring. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    ⇒   ⊢ (𝜑 → 𝑃 ∈ NzRing)
Theorem	0mplrim 33705*	Build a ring isomorphism between multivariate polynomials with no variables and the underlying ring. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (∅ mPoly 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ (𝑝‘∅))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑃 RingIso 𝑅))
Theorem	0mplric 33706	Multivariate polynomials with no variables are isomorphic with the underlying ring. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (∅ mPoly 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑃 ≃𝑟 𝑅)
Theorem	mplasclco 33707*	Case where composing an algebra scalar lifting functions with a scalar leads to a scalar. This is useful when working with selectVars. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝑆 = (Base‘𝑅)    &   ⊢ 𝑂 = (𝐽 mPoly 𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑄 = (𝐼 mPoly 𝑂)    &   ⊢ 𝐴 = (algSc‘𝑂)    &   ⊢ 𝐵 = (algSc‘𝑃)    &   ⊢ 𝐶 = (algSc‘𝑄)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 𝐸 = {𝑗 ∈ (ℕ0 ↑m 𝐽) ∣ (◡𝑗 “ ℕ) ∈ Fin}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐴 ∘ (𝐵‘𝑋)) = (𝐶‘(𝐴‘𝑋)))
Theorem	selvascl 33708	The "variable selection" function evaluated at a scalar. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 𝐶 = (algSc‘𝑇)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)    &   ⊢ 𝑇 = (𝐽 mPoly 𝑈)    &   ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈))    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐽 ⊆ 𝐼)    ⇒   ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘(𝐴‘𝑋)) = (𝐷‘𝑋))
Theorem	selvply1rhmlema 33709*	Lemma for selvply1rhm 33716. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = ({𝑋} mPoly 𝑅)    &   ⊢ · = (.r‘𝑃)    &   ⊢ × = (.r‘𝑄)    &   ⊢ 𝑄 = (Poly1‘𝑅)    &   ⊢ 𝑀 = (𝑓 ∈ 𝐵 ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ (𝑓‘{⟨𝑋, (𝑛‘∅)⟩})))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑀‘𝐹) ∈ (Base‘𝑄))
Theorem	selvply1rhmlemb 33710*	Lemma for selvply1rhm 33716. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = ({𝑋} mPoly 𝑅)    &   ⊢ · = (.r‘𝑃)    &   ⊢ × = (.r‘𝑄)    &   ⊢ 𝑄 = (Poly1‘𝑅)    &   ⊢ 𝑀 = (𝑓 ∈ 𝐵 ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ (𝑓‘{⟨𝑋, (𝑛‘∅)⟩})))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑀‘(𝐹 · 𝐺)) = ((𝑀‘𝐹) × (𝑀‘𝐺)))
Theorem	selvply1rhmlem1 33711*	Lemma for selvply1rhm 33716. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑈 = ((𝐼 ∖ {𝑋}) mPoly 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝑈)    &   ⊢ 𝐻 = (𝑓 ∈ 𝐵 ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝑓)‘{⟨𝑋, (𝑛‘∅)⟩})))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → 𝐻:𝐵⟶(Base‘𝑄))
Theorem	selvply1rhmlem2 33712*	Lemma for selvply1rhm 33716: Image of the ring unit by the mapping 𝐻 (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑈 = ((𝐼 ∖ {𝑋}) mPoly 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝑈)    &   ⊢ 𝐻 = (𝑓 ∈ 𝐵 ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝑓)‘{⟨𝑋, (𝑛‘∅)⟩})))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → (𝐻‘(1r‘𝑃)) = (1r‘𝑄))
Theorem	selvply1rhmlem3 33713*	Lemma for selvply1rhm 33716. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑈 = ((𝐼 ∖ {𝑋}) mPoly 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝑈)    &   ⊢ 𝐻 = (𝑓 ∈ 𝐵 ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝑓)‘{⟨𝑋, (𝑛‘∅)⟩})))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑁 ∈ (ℕ0 ↑m 1o))    ⇒   ⊢ (𝜑 → ((𝐻‘𝐹)‘𝑁) = ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)‘{⟨𝑋, (𝑁‘∅)⟩}))
Theorem	selvply1rhmlem4 33714*	Lemma for selvply1rhm 33716: The mapping 𝐻 is linear. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑈 = ((𝐼 ∖ {𝑋}) mPoly 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝑈)    &   ⊢ 𝐻 = (𝑓 ∈ 𝐵 ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝑓)‘{⟨𝑋, (𝑛‘∅)⟩})))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐻‘(𝐹(+g‘𝑃)𝐺)) = ((𝐻‘𝐹)(+g‘𝑄)(𝐻‘𝐺)))
Theorem	selvply1rhmlem5 33715*	Lemma for selvply1rhm 33716. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑈 = ((𝐼 ∖ {𝑋}) mPoly 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝑈)    &   ⊢ 𝐻 = (𝑓 ∈ 𝐵 ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝑓)‘{⟨𝑋, (𝑛‘∅)⟩})))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ 𝑀 = (𝑞 ∈ (Base‘({𝑋} mPoly 𝑈)) ↦ (𝑠 ∈ (ℕ0 ↑m 1o) ↦ (𝑞‘{⟨𝑋, (𝑠‘∅)⟩})))    ⇒   ⊢ (𝜑 → (𝐻‘𝐹) = (𝑀‘(((𝐼 selectVars 𝑅)‘{𝑋})‘𝐹)))
Theorem	selvply1rhm 33716*	Build a ring homomorphism 𝐻 between the multivariate polynomials 𝑃 with variables in 𝐼 and the univariate polynomials 𝑄 in a single variable 𝑋 element of 𝐼. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑈 = ((𝐼 ∖ {𝑋}) mPoly 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝑈)    &   ⊢ 𝐻 = (𝑓 ∈ 𝐵 ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝑓)‘{⟨𝑋, (𝑛‘∅)⟩})))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    ⇒   ⊢ (𝜑 → 𝐻 ∈ (𝑃 RingHom 𝑄))
Theorem	selvply1rhm0 33717*	The ring homomorphism 𝐻 built in selvply1rhm 33716 is injective. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑈 = ((𝐼 ∖ {𝑋}) mPoly 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝑈)    &   ⊢ 𝐻 = (𝑓 ∈ 𝐵 ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ ((((𝐼 selectVars 𝑅)‘{𝑋})‘𝑓)‘{⟨𝑋, (𝑛‘∅)⟩})))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ 0 = (0g‘𝑄)    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐻‘𝐹) = 0 )    ⇒   ⊢ (𝜑 → 𝐹 = 𝑍)
Theorem	mplidomlem 33718*	Lemma for mplidom 33719. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ 𝐻 = (𝑓 ∈ 𝐶 ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ (((((𝑗 ∪ {𝑥}) selectVars 𝑅)‘{𝑥})‘𝑓)‘{⟨𝑥, (𝑛‘∅)⟩})))    &   ⊢ 𝐶 = (Base‘𝑆)    &   ⊢ 𝑆 = ((𝑗 ∪ {𝑥}) mPoly 𝑅)    &   ⊢ 𝑈 = (((𝑗 ∪ {𝑥}) ∖ {𝑥}) mPoly 𝑅)    &   ⊢ 𝑄 = (Poly1‘𝑈)    ⇒   ⊢ (𝜑 → 𝑃 ∈ IDomn)
Theorem	mplidom 33719	The multivariate polynomials over an integral domain form an integral domain. See ply1idom 26115. (Contributed by Thierry Arnoux, 4-May-2026.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    ⇒   ⊢ (𝜑 → 𝑃 ∈ IDomn)
Syntax	cextv 33720	Extend class notation with the "variable extension" function.
class extendVars
Definition	df-extv 33721*	Define the "variable extension" function. The function ((𝐼extendVars𝑅)‘𝐴) converts polynomials with variables indexed by (𝐼 ∖ {𝐴}) into polynomials indexed by 𝐼, and therefore maps elements of ((𝐼 ∖ {𝐴}) mPoly 𝑅) onto (𝐼 mPoly 𝑅). (Contributed by Thierry Arnoux, 20-Jan-2026.)
⊢ extendVars = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑎 ∈ 𝑖 ↦ (𝑓 ∈ (Base‘((𝑖 ∖ {𝑎}) mPoly 𝑟)) ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0} ↦ if((𝑥‘𝑎) = 0, (𝑓‘(𝑥 ↾ (𝑖 ∖ {𝑎}))), (0g‘𝑟))))))
Theorem	extvval 33722*	Value of the "variable extension" function. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ 𝐽 = (𝐼 ∖ {𝑎})    &   ⊢ 𝑀 = (Base‘(𝐽 mPoly 𝑅))    ⇒   ⊢ (𝜑 → (𝐼extendVars𝑅) = (𝑎 ∈ 𝐼 ↦ (𝑓 ∈ 𝑀 ↦ (𝑥 ∈ 𝐷 ↦ if((𝑥‘𝑎) = 0, (𝑓‘(𝑥 ↾ (𝐼 ∖ {𝑎}))), 0 )))))
Theorem	extvfval 33723*	The "variable extension" function evaluated for adding a variable with index 𝐴. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐼)    &   ⊢ 𝐽 = (𝐼 ∖ {𝐴})    &   ⊢ 𝑀 = (Base‘(𝐽 mPoly 𝑅))    ⇒   ⊢ (𝜑 → ((𝐼extendVars𝑅)‘𝐴) = (𝑓 ∈ 𝑀 ↦ (𝑥 ∈ 𝐷 ↦ if((𝑥‘𝐴) = 0, (𝑓‘(𝑥 ↾ 𝐽)), 0 ))))
Theorem	extvfv 33724*	The "variable extension" function evaluated for converting a given polynomial 𝐹 by adding a variable with index 𝐴. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐼)    &   ⊢ 𝐽 = (𝐼 ∖ {𝐴})    &   ⊢ 𝑀 = (Base‘(𝐽 mPoly 𝑅))    &   ⊢ (𝜑 → 𝐹 ∈ 𝑀)    ⇒   ⊢ (𝜑 → (((𝐼extendVars𝑅)‘𝐴)‘𝐹) = (𝑥 ∈ 𝐷 ↦ if((𝑥‘𝐴) = 0, (𝐹‘(𝑥 ↾ 𝐽)), 0 )))
Theorem	extvfvv 33725*	The "variable extension" function evaluated for converting a given polynomial 𝐹 by adding a variable with index 𝐴. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐼)    &   ⊢ 𝐽 = (𝐼 ∖ {𝐴})    &   ⊢ 𝑀 = (Base‘(𝐽 mPoly 𝑅))    &   ⊢ (𝜑 → 𝐹 ∈ 𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ((((𝐼extendVars𝑅)‘𝐴)‘𝐹)‘𝑋) = if((𝑋‘𝐴) = 0, (𝐹‘(𝑋 ↾ 𝐽)), 0 ))
Theorem	extvfvvcl 33726*	Closure for the "variable extension" function evaluated for converting a given polynomial 𝐹 by adding a variable with index 𝐴. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐽 = (𝐼 ∖ {𝐴})    &   ⊢ 𝑀 = (Base‘(𝐽 mPoly 𝑅))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ((((𝐼extendVars𝑅)‘𝐴)‘𝐹)‘𝑋) ∈ 𝐵)
Theorem	extvfvcl 33727*	Closure for the "variable extension" function evaluated for converting a given polynomial 𝐹 by adding a variable with index 𝐴. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐽 = (𝐼 ∖ {𝐴})    &   ⊢ 𝑀 = (Base‘(𝐽 mPoly 𝑅))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑀)    &   ⊢ 𝑁 = (Base‘(𝐼 mPoly 𝑅))    ⇒   ⊢ (𝜑 → (((𝐼extendVars𝑅)‘𝐴)‘𝐹) ∈ 𝑁)
Theorem	extvfvalf 33728*	The "variable extension" function maps polynomials with variables indexed in 𝐽 to polynomials with variables indexed in 𝐼. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐽 = (𝐼 ∖ {𝐴})    &   ⊢ 𝑀 = (Base‘(𝐽 mPoly 𝑅))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐼)    &   ⊢ 𝑁 = (Base‘(𝐼 mPoly 𝑅))    ⇒   ⊢ (𝜑 → ((𝐼extendVars𝑅)‘𝐴):𝑀⟶𝑁)
Theorem	mvrvalind 33729*	Value of the generating elements of the power series structure, expressed using the indicator function. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ 𝐴 = ((𝟭‘𝐼)‘{𝑋})    ⇒   ⊢ (𝜑 → ((𝑉‘𝑋)‘𝐹) = if(𝐹 = 𝐴, 1 , 0 ))
Theorem	mplmulmvr 33730*	Multiply a polynomial 𝐹 with a variable 𝑋 (i.e. with a monic monomial). (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑋 = ((𝐼 mVar 𝑅)‘𝑌)    &   ⊢ 𝑀 = (Base‘𝑃)    &   ⊢ · = (.r‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 𝐴 = ((𝟭‘𝐼)‘{𝑌})    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑀)    ⇒   ⊢ (𝜑 → (𝑋 · 𝐹) = (𝑏 ∈ 𝐷 ↦ if((𝑏‘𝑌) = 0, 0 , (𝐹‘(𝑏 ∘f − 𝐴)))))
Theorem	evlscaval 33731	Polynomial evaluation for scalars. See evlsscaval 22109. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝑊 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐿:𝐼⟶𝐵)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝐴‘𝑋))‘𝐿) = 𝑋)
Theorem	evlvarval 33732	Polynomial evaluation builder for a variable. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝑄 = (𝐼 eval 𝑆)    &   ⊢ 𝑃 = (𝐼 mPoly 𝑆)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼))    &   ⊢ 𝑉 = (𝐼 mVar 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐼)    ⇒   ⊢ (𝜑 → ((𝑉‘𝑋) ∈ 𝐵 ∧ ((𝑄‘(𝑉‘𝑋))‘𝐴) = (𝐴‘𝑋)))
Theorem	evlextv 33733	Evaluating a variable-extended polynomial is the same as evaluating the polynomial in the original set of variables (in both cases, the additionial variable is ignored). (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝑂 = (𝐽 eval 𝑅)    &   ⊢ 𝐽 = (𝐼 ∖ {𝑌})    &   ⊢ 𝑀 = (Base‘(𝐽 mPoly 𝑅))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐸 = (𝐼extendVars𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴:𝐼⟶𝐵)    ⇒   ⊢ (𝜑 → ((𝑄‘((𝐸‘𝑌)‘𝐹))‘𝐴) = ((𝑂‘𝐹)‘(𝐴 ↾ 𝐽)))
Theorem	mplvrpmlem 33734*	Lemma for mplvrpmga 33736 and others. (Contributed by Thierry Arnoux, 11-Jan-2026.)
⊢ 𝑆 = (SymGrp‘𝐼)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})    ⇒   ⊢ (𝜑 → (𝑋 ∘ 𝐷) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
Theorem	mplvrpmfgalem 33735*	Permuting variables in a multivariate polynomial conserves finite support. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ 𝑆 = (SymGrp‘𝐼)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))    &   ⊢ 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑀)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑃)    ⇒   ⊢ (𝜑 → (𝑄𝐴𝐹) finSupp 0 )
Theorem	mplvrpmga 33736*	The action of permuting variables in a multivariate polynomial is a group action. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ 𝑆 = (SymGrp‘𝐼)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))    &   ⊢ 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝑆 GrpAct 𝑀))
Theorem	mplvrpmmhm 33737*	The action of permuting variables in a multivariate polynomial is a monoid homomorphism. (Contributed by Thierry Arnoux, 11-Jan-2026.)
⊢ 𝑆 = (SymGrp‘𝐼)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))    &   ⊢ 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ 𝐹 = (𝑓 ∈ 𝑀 ↦ (𝐷𝐴𝑓))    &   ⊢ 𝑊 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑊 MndHom 𝑊))
Theorem	mplvrpmrhm 33738*	The action of permuting variables in a multivariate polynomial is a ring homomorphism. (Contributed by Thierry Arnoux, 15-Jan-2026.)
⊢ 𝑆 = (SymGrp‘𝐼)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))    &   ⊢ 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ 𝐹 = (𝑓 ∈ 𝑀 ↦ (𝐷𝐴𝑓))    &   ⊢ 𝑊 = (𝐼 mPoly 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑊 RingHom 𝑊))
Theorem	psrgsum 33739*	Finite commutative sums of power series are taken componentwise. (Contributed by Thierry Arnoux, 16-Mar-2026.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (𝑆 Σg 𝐹) = (𝑦 ∈ 𝐷 ↦ (𝑅 Σg (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)‘𝑦)))))
Theorem	psrmon 33740*	A monomial is a power series. (Contributed by Thierry Arnoux, 16-Mar-2026.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    ⇒   ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 )) ∈ 𝐵)
Theorem	psrmonmul 33741*	The product of two power series monomials adds the exponent vectors together. For example, the product of (𝑥↑2)(𝑦↑2) with (𝑦↑1)(𝑧↑3) is (𝑥↑2)(𝑦↑3)(𝑧↑3), where the exponent vectors ⟨2, 2, 0⟩ and ⟨0, 1, 3⟩ are added to give ⟨2, 3, 3⟩. (Contributed by Thierry Arnoux, 16-Mar-2026.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 )) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑋 ∘f + 𝑌), 1 , 0 )))
Theorem	psrmonmul2 33742*	The product of two power series monomials adds the exponent vectors together. Here, the function 𝐺 is a monomial builder, which maps a bag of variables with the monic monomial with only those variables. (Contributed by Thierry Arnoux, 16-Mar-2026.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ · = (.r‘𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐷)    &   ⊢ 𝐺 = (𝑦 ∈ 𝐷 ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 = 𝑦, 1 , 0 )))    ⇒   ⊢ (𝜑 → ((𝐺‘𝑋) · (𝐺‘𝑌)) = (𝐺‘(𝑋 ∘f + 𝑌)))
Theorem	psrmonprod 33743*	Finite product of bags of variables in a power series. Here the function 𝐺 maps a bag of variables to the corresponding monomial. (Contributed by Thierry Arnoux, 16-Mar-2026.)
⊢ 𝑆 = (𝐼 mPwSer 𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐷)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑆)    &   ⊢ 𝐺 = (𝑦 ∈ 𝐷 ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 = 𝑦, 1 , 0 )))    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝐺 ∘ 𝐹)) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)‘𝑖))))))
Theorem	mplgsum 33744*	Finite commutative sums of polynomials are taken componentwise. (Contributed by Thierry Arnoux, 16-Mar-2026.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (𝑃 Σg 𝐹) = (𝑦 ∈ 𝐷 ↦ (𝑅 Σg (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)‘𝑦)))))
Theorem	mplmonprod 33745*	Finite product of monomials. Here the function 𝐺 maps a bag of variables to the corresponding monomial. (Contributed by Thierry Arnoux, 16-Mar-2026.)
⊢ 𝑃 = (𝐼 mPoly 𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐷)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑀 = (mulGrp‘𝑃)    &   ⊢ 𝐺 = (𝑦 ∈ 𝐷 ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 = 𝑦, 1 , 0 )))    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝐺 ∘ 𝐹)) = (𝐺‘(𝑖 ∈ 𝐼 ↦ (ℂfld Σg (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)‘𝑖))))))
21.3.10.50  The ring of symmetric polynomials
Syntax	csply 33746	Extend class notation with the symmetric polynomials.
class SymPoly
Syntax	cesply 33747	Extend class notation with the elementary symmetric polynomials.
class eSymPoly
Definition	df-sply 33748*	Define symmetric polynomials. See splyval 33750 for a more readable expression. (Contributed by Thierry Arnoux, 11-Jan-2026.)
⊢ SymPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ ((Base‘(𝑖 mPoly 𝑟))FixPts(𝑑 ∈ (Base‘(SymGrp‘𝑖)), 𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))))
Definition	df-esply 33749*	Define elementary symmetric polynomials. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ eSymPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑘 ∈ ℕ0 ↦ ((ℤRHom‘𝑟) ∘ ((𝟭‘{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0})‘((𝟭‘𝑖) “ {𝑐 ∈ 𝒫 𝑖 ∣ (♯‘𝑐) = 𝑘})))))
Theorem	splyval 33750*	The symmetric polynomials for a given index 𝐼 of variables and base ring 𝑅. These are the fixed points of the action 𝐴 which permutes variables. (Contributed by Thierry Arnoux, 11-Jan-2026.)
⊢ 𝑆 = (SymGrp‘𝐼)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))    &   ⊢ 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐼SymPoly𝑅) = (𝑀FixPts𝐴))
Theorem	splysubrg 33751*	The symmetric polynomials form a subring of the ring of polynomials. (Contributed by Thierry Arnoux, 15-Jan-2026.)
⊢ 𝑆 = (SymGrp‘𝐼)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))    &   ⊢ 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → (𝐼SymPoly𝑅) ∈ (SubRing‘(𝐼 mPoly 𝑅)))
Theorem	issply 33752*	Conditions for being a symmetric polynomial. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ 𝑆 = (SymGrp‘𝐼)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑀)    &   ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ 𝑥 ∈ 𝐷) → (𝐹‘(𝑥 ∘ 𝑝)) = (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐼SymPoly𝑅))
Theorem	esplyval 33753*	The elementary polynomials for a given index 𝐼 of variables and base ring 𝑅. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐼eSymPoly𝑅) = (𝑘 ∈ ℕ0 ↦ ((ℤRHom‘𝑅) ∘ ((𝟭‘𝐷)‘((𝟭‘𝐼) “ {𝑐 ∈ 𝒫 𝐼 ∣ (♯‘𝑐) = 𝑘})))))
Theorem	esplyfval 33754*	The 𝐾-th elementary polynomial for a given index 𝐼 of variables and base ring 𝑅. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘𝐾) = ((ℤRHom‘𝑅) ∘ ((𝟭‘𝐷)‘((𝟭‘𝐼) “ {𝑐 ∈ 𝒫 𝐼 ∣ (♯‘𝑐) = 𝐾}))))
Theorem	esplyfval0 33755	The 0-th elementary symmetric polynomial is the constant 1. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝑈 = (1r‘(𝐼 mPoly 𝑅))    ⇒   ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘0) = 𝑈)
Theorem	esplyfval2 33756*	When 𝐾 is out-of-bounds, the 𝐾-th elementary symmetric polynomial is zero. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐾 ∈ (ℕ0 ∖ (0...(♯‘𝐼))))    &   ⊢ 𝑍 = (0g‘(𝐼 mPoly 𝑅))    ⇒   ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘𝐾) = 𝑍)
Theorem	esplylem 33757*	Lemma for esplyfv 33761 and others. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝟭‘𝐼) “ {𝑐 ∈ 𝒫 𝐼 ∣ (♯‘𝑐) = 𝐾}) ⊆ 𝐷)
Theorem	esplympl 33758*	Elementary symmetric polynomials are polynomials. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))    ⇒   ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘𝐾) ∈ 𝑀)
Theorem	esplymhp 33759*	The 𝐾-th elementary symmetric polynomial is homogeneous of degree 𝐾. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝐻 = (𝐼 mHomP 𝑅)    ⇒   ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘𝐾) ∈ (𝐻‘𝐾))
Theorem	esplyfv1 33760*	Coefficient for the 𝐾-th elementary symmetric polynomial and a bag of variables 𝐹 where variables are not raised to a power. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐾 ∈ (0...(♯‘𝐼)))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → ran 𝐹 ⊆ {0, 1})    ⇒   ⊢ (𝜑 → (((𝐼eSymPoly𝑅)‘𝐾)‘𝐹) = if((♯‘(𝐹 supp 0)) = 𝐾, 1 , 0 ))
Theorem	esplyfv 33761*	Coefficient for the 𝐾-th elementary symmetric polynomial and a bag of variables 𝐹: the coefficient is 1 for the bags of exactly 𝐾 variables, having exponent at most 1. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐾 ∈ (0...(♯‘𝐼)))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐷)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝜑 → (((𝐼eSymPoly𝑅)‘𝐾)‘𝐹) = if((ran 𝐹 ⊆ {0, 1} ∧ (♯‘(𝐹 supp 0)) = 𝐾), 1 , 0 ))
Theorem	esplysply 33762*	The 𝐾-th elementary symmetric polynomial is symmetric. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐾 ∈ (0...(♯‘𝐼)))    ⇒   ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘𝐾) ∈ (𝐼SymPoly𝑅))
Theorem	esplyfval3 33763*	Alternate expression for the value of the 𝐾-th elementary symmetric polynomial. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘𝐾) = (𝑓 ∈ 𝐷 ↦ if((ran 𝑓 ⊆ {0, 1} ∧ (♯‘(𝑓 supp 0)) = 𝐾), 1 , 0 )))
Theorem	esplyfval1 33764	The first elementary symmetric polynomial is the sum of all variables. (Contributed by Thierry Arnoux, 16-Mar-2026.)
⊢ 𝑊 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ 𝐸 = (𝐼eSymPoly𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → (𝐸‘1) = (𝑊 Σg 𝑉))
Theorem	esplyfvaln 33765	The last elementary symmetric polynomial is the product of all variables. (Contributed by Thierry Arnoux, 16-Mar-2026.)
⊢ 𝑊 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ 𝐸 = (𝐼eSymPoly𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ 𝑁 = (♯‘𝐼)    &   ⊢ 𝑀 = (mulGrp‘𝑊)    ⇒   ⊢ (𝜑 → (𝐸‘𝑁) = (𝑀 Σg 𝑉))
Theorem	esplyind 33766*	A recursive formula for the elementary symmetric polynomials. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ 𝑊 = (𝐼 mPoly 𝑅)    &   ⊢ 𝑉 = (𝐼 mVar 𝑅)    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = (.r‘𝑊)    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 𝐺 = ((𝐼extendVars𝑅)‘𝑌)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐼)    &   ⊢ 𝐽 = (𝐼 ∖ {𝑌})    &   ⊢ 𝐸 = (𝐽eSymPoly𝑅)    &   ⊢ (𝜑 → 𝐾 ∈ (1...(♯‘𝐼)))    &   ⊢ 𝐶 = {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}    ⇒   ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘𝐾) = (((𝑉‘𝑌) · (𝐺‘(𝐸‘(𝐾 − 1)))) + (𝐺‘(𝐸‘𝐾))))
Theorem	esplyindfv 33767*	A recursive formula for the elementary symmetric polynomials, evaluated at a given set of points 𝑍. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐼)    &   ⊢ 𝐽 = (𝐼 ∖ {𝑌})    &   ⊢ 𝐸 = (𝐽eSymPoly𝑅)    &   ⊢ (𝜑 → 𝐾 ∈ (0...(♯‘𝐽)))    &   ⊢ 𝐶 = {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}    &   ⊢ 𝐹 = ((𝐼eSymPoly𝑅)‘(𝐾 + 1))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝑂 = (𝐽 eval 𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ (𝜑 → 𝑍:𝐼⟶𝐵)    ⇒   ⊢ (𝜑 → ((𝑄‘𝐹)‘𝑍) = (((𝑍‘𝑌) · ((𝑂‘(𝐸‘𝐾))‘(𝑍 ↾ 𝐽))) + ((𝑂‘(𝐸‘(𝐾 + 1)))‘(𝑍 ↾ 𝐽))))
Theorem	esplyfvn 33768	Express the last elementary symmetric polynomial, evaluated at a given set of points 𝑍, in terms of the last elementary symmetric polynomial with one less variable. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝑂 = (𝐽 eval 𝑅)    &   ⊢ 𝐸 = (𝐼eSymPoly𝑅)    &   ⊢ 𝐹 = (𝐽eSymPoly𝑅)    &   ⊢ 𝐻 = (♯‘𝐼)    &   ⊢ 𝐾 = (♯‘𝐽)    &   ⊢ 𝐽 = (𝐼 ∖ {𝑌})    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑍:𝐼⟶𝐵)    ⇒   ⊢ (𝜑 → ((𝑄‘(𝐸‘𝐻))‘𝑍) = ((𝑍‘𝑌) · ((𝑂‘(𝐹‘𝐾))‘(𝑍 ↾ 𝐽))))
Theorem	vietadeg1 33769*	The degree of a product of 𝐻 of linear polynomials of the form 𝑋 − 𝑍 is 𝐻. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝑊 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 𝑀 = (mulGrp‘𝑊)    &   ⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝐸 = (𝐼eSymPoly𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    &   ⊢ 𝐻 = (♯‘𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝑍:𝐼⟶𝐵)    &   ⊢ 𝐹 = (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))    &   ⊢ 𝐷 = (deg1‘𝑅)    ⇒   ⊢ (𝜑 → (𝐷‘𝐹) = 𝐻)
Theorem	vietalem 33770*	Lemma for vieta 33771: induction step. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝑊 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 𝑀 = (mulGrp‘𝑊)    &   ⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝐸 = (𝐼eSymPoly𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    &   ⊢ 𝐻 = (♯‘𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝑍:𝐼⟶𝐵)    &   ⊢ 𝐹 = (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))    &   ⊢ (𝜑 → 𝐾 ∈ (0...𝐻))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐼)    &   ⊢ 𝐽 = (𝐼 ∖ {𝑌})    &   ⊢ (𝜑 → ∀𝑧 ∈ (𝐵 ↑m 𝐽)∀𝑘 ∈ (0...(♯‘𝐽))((coe1‘(𝑀 Σg (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝐽) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘𝑧)))    &   ⊢ (𝜑 → ((deg1‘𝑅)‘(𝑀 Σg (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)))))) = (♯‘𝐽))    ⇒   ⊢ (𝜑 → ((coe1‘𝐹)‘𝐾) = (((𝐻 − 𝐾) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝐾)))‘𝑍)))
Theorem	vieta 33771*	Vieta's Formulas: Coefficients of a monic polynomial 𝐹 expressed as a product of linear polynomials of the form 𝑋 − 𝑍 can be expressed in terms of elementary symmetric polynomials. The formulas appear in Chapter 6 of [Lang], p. 190. Theorem vieta1 26303 is a special case for the complex numbers, for the case 𝐾 = 1. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ 𝑊 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 𝑀 = (mulGrp‘𝑊)    &   ⊢ 𝑄 = (𝐼 eval 𝑅)    &   ⊢ 𝐸 = (𝐼eSymPoly𝑅)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑊)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    &   ⊢ 𝐻 = (♯‘𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝑍:𝐼⟶𝐵)    &   ⊢ 𝐹 = (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))    &   ⊢ (𝜑 → 𝐾 ∈ (0...𝐻))    &   ⊢ 𝐶 = (coe1‘𝐹)    ⇒   ⊢ (𝜑 → (𝐶‘(𝐻 − 𝐾)) = ((𝐾 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐾))‘𝑍)))
21.3.10.51  The subring algebra
Theorem	sra1r 33772	The unity element of a subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 1 = (1r‘𝑊))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → 1 = (1r‘𝐴))
Theorem	sradrng 33773	Condition for a subring algebra to be a division ring. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵) → 𝐴 ∈ DivRing)
Theorem	sraidom 33774	Condition for a subring algebra to be an integral domain. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝑉 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ IDomn)
Theorem	srasubrg 33775	A subring of the original structure is also a subring of the constructed subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝑊))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐴))
Theorem	sralvec 33776	Given a sub division ring 𝐹 of a division ring 𝐸, 𝐸 may be considered as a vector space over 𝐹, which becomes the field of scalars. (Contributed by Thierry Arnoux, 24-May-2023.)
⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑈)    &   ⊢ 𝐹 = (𝐸 ↾s 𝑈)    ⇒   ⊢ ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec)
Theorem	srafldlvec 33777	Given a subfield 𝐹 of a field 𝐸, 𝐸 may be considered as a vector space over 𝐹, which becomes the field of scalars. (Contributed by Thierry Arnoux, 24-May-2023.)
⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑈)    &   ⊢ 𝐹 = (𝐸 ↾s 𝑈)    ⇒   ⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ Field ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec)
Theorem	resssra 33778	The subring algebra of a restricted structure is the restriction of the subring algebra. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐴 = (Base‘𝑅)    &   ⊢ 𝑆 = (𝑅 ↾s 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((subringAlg ‘𝑆)‘𝐶) = (((subringAlg ‘𝑅)‘𝐶) ↾s 𝐵))
Theorem	lsssra 33779	A subring is a subspace of the subring algebra. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑊 = ((subringAlg ‘𝑅)‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑅)    &   ⊢ 𝑆 = (𝑅 ↾s 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝐶 ∈ (SubRing‘𝑆))    ⇒   ⊢ (𝜑 → 𝐵 ∈ (LSubSp‘𝑊))
Theorem	srapwov 33780	The "power" operation on a subring algebra. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ 𝐴 = ((subringAlg ‘𝑊)‘𝑆)    &   ⊢ (𝜑 → 𝑊 ∈ Ring)    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (.g‘(mulGrp‘𝑊)) = (.g‘(mulGrp‘𝐴)))
21.3.10.52  Division Ring Extensions
Theorem	drgext0g 33781	The additive neutral element of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.)
⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ DivRing)    &   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸))    ⇒   ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐵))
Theorem	drgextvsca 33782	The scalar multiplication operation of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.)
⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ DivRing)    &   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸))    ⇒   ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘𝐵))
Theorem	drgext0gsca 33783	The additive neutral element of the scalar field of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.)
⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ DivRing)    &   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸))    ⇒   ⊢ (𝜑 → (0g‘𝐵) = (0g‘(Scalar‘𝐵)))
Theorem	drgextsubrg 33784	The scalar field is a subring of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.)
⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ DivRing)    &   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸))    &   ⊢ 𝐹 = (𝐸 ↾s 𝑈)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    ⇒   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐵))
Theorem	drgextlsp 33785	The scalar field is a subspace of a subring algebra. (Contributed by Thierry Arnoux, 17-Jul-2023.)
⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ DivRing)    &   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸))    &   ⊢ 𝐹 = (𝐸 ↾s 𝑈)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    ⇒   ⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝐵))
Theorem	drgextgsum 33786*	Group sum in a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.)
⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ DivRing)    &   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸))    &   ⊢ 𝐹 = (𝐸 ↾s 𝑈)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ 𝑌)) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ 𝑌)))
21.3.10.53  Vector Spaces
Theorem	lvecdimfi 33787	Finite version of lvecdim 21157 which does not require the axiom of choice. The axiom of choice is used in acsmapd 18518, which is required in the infinite case. Suggested by Gérard Lang. (Contributed by Thierry Arnoux, 24-May-2023.)
⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝑆 ≈ 𝑇)
Theorem	exsslsb 33788*	Any finite generating set 𝑆 of a vector space 𝑊 contains a basis. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝐾 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ (𝜑 → (𝐾‘𝑆) = 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ 𝐽 𝑠 ⊆ 𝑆)
Theorem	lbslelsp 33789	The size of a basis 𝑋 of a vector space 𝑊 is less than the size of a generating set 𝑌. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝐾 = (LSpan‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝐵)    &   ⊢ (𝜑 → (𝐾‘𝑌) = 𝐵)    ⇒   ⊢ (𝜑 → (♯‘𝑋) ≤ (♯‘𝑌))
21.3.10.54  Vector Space Dimension
Syntax	cldim 33790	Extend class notation with the dimension of a vector space.
class dim
Definition	df-dim 33791	Define the dimension of a vector space as the cardinality of its bases. Note that by lvecdim 21157, all bases are equinumerous. (Contributed by Thierry Arnoux, 6-May-2023.)
⊢ dim = (𝑓 ∈ V ↦ ∪ (♯ “ (LBasis‘𝑓)))
Theorem	dimval 33792	The dimension of a vector space 𝐹 is the cardinality of one of its bases. (Contributed by Thierry Arnoux, 6-May-2023.)
⊢ 𝐽 = (LBasis‘𝐹)    ⇒   ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) → (dim‘𝐹) = (♯‘𝑆))
Theorem	dimvalfi 33793	The dimension of a vector space 𝐹 is the cardinality of one of its bases. This version of dimval 33792 does not depend on the axiom of choice, but it is limited to the case where the base 𝑆 is finite. (Contributed by Thierry Arnoux, 24-May-2023.)
⊢ 𝐽 = (LBasis‘𝐹)    ⇒   ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) → (dim‘𝐹) = (♯‘𝑆))
Theorem	dimcl 33794	Closure of the vector space dimension. (Contributed by Thierry Arnoux, 18-May-2023.)
⊢ (𝑉 ∈ LVec → (dim‘𝑉) ∈ ℕ0*)
Theorem	lmimdim 33795	Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Feb-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝑆 LMIso 𝑇))    &   ⊢ (𝜑 → 𝑆 ∈ LVec)    ⇒   ⊢ (𝜑 → (dim‘𝑆) = (dim‘𝑇))
Theorem	lmicdim 33796	Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Mar-2025.)
⊢ (𝜑 → 𝑆 ≃𝑚 𝑇)    &   ⊢ (𝜑 → 𝑆 ∈ LVec)    ⇒   ⊢ (𝜑 → (dim‘𝑆) = (dim‘𝑇))
Theorem	lvecdim0i 33797	A vector space of dimension zero is reduced to its identity element. (Contributed by Thierry Arnoux, 31-Jul-2023.)
⊢ 0 = (0g‘𝑉)    ⇒   ⊢ ((𝑉 ∈ LVec ∧ (dim‘𝑉) = 0) → (Base‘𝑉) = { 0 })
Theorem	lvecdim0 33798	A vector space of dimension zero is reduced to its identity element, biconditional version. (Contributed by Thierry Arnoux, 31-Jul-2023.)
⊢ 0 = (0g‘𝑉)    ⇒   ⊢ (𝑉 ∈ LVec → ((dim‘𝑉) = 0 ↔ (Base‘𝑉) = { 0 }))
Theorem	lssdimle 33799	The dimension of a linear subspace is less than or equal to the dimension of the parent vector space. This is corollary 5.4 of [Lang] p. 141. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝑈 ∈ (LSubSp‘𝑊)) → (dim‘𝑋) ≤ (dim‘𝑊))
Theorem	dimpropd 33800*	If two structures have the same components (properties), they have the same dimension. (Contributed by Thierry Arnoux, 18-May-2023.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦))    &   ⊢ 𝐹 = (Scalar‘𝐾)    &   ⊢ 𝐺 = (Scalar‘𝐿)    &   ⊢ (𝜑 → 𝑃 = (Base‘𝐹))    &   ⊢ (𝜑 → 𝑃 = (Base‘𝐺))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑥(+g‘𝐹)𝑦) = (𝑥(+g‘𝐺)𝑦))    &   ⊢ (𝜑 → 𝐾 ∈ LVec)    &   ⊢ (𝜑 → 𝐿 ∈ LVec)    ⇒   ⊢ (𝜑 → (dim‘𝐾) = (dim‘𝐿))