P. 339 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33801-33900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mplvrpmlem 33801*	Lemma for mplvrpmga 33803 and others. (Contributed by Thierry Arnoux, 11-Jan-2026.)
⊢ 𝑆 = (SymGrp‘𝐼)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑋 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})    ⇒   ⊢ (𝜑 → (𝑋 ∘ 𝐷) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
Theorem	mplvrpmfgalem 33802*	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 33803*	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 33804*	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 33805*	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 33806*	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 33807*	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 33808*	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 33809*	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 33810*	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 33811*	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 33812*	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.51  The ring of symmetric polynomials
Syntax	csply 33813	Extend class notation with the symmetric polynomials.
class SymPoly
Syntax	cesply 33814	Extend class notation with the elementary symmetric polynomials.
class eSymPoly
Definition	df-sply 33815*	Define symmetric polynomials. See splyval 33817 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 33816*	Define elementary symmetric polynomials. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ eSymPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑘 ∈ ℕ0 ↦ ((ℤRHom‘𝑟) ∘ ((𝟭‘{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0})‘((𝟭‘𝑖) “ {𝑐 ∈ 𝒫 𝑖 ∣ (♯‘𝑐) = 𝑘})))))
Theorem	splyval 33817*	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 33818*	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 33819*	Conditions for being a symmetric polynomial. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ 𝑆 = (SymGrp‘𝐼)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑀)    &   ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ 𝑥 ∈ 𝐷) → (𝐹‘(𝑥 ∘ 𝑝)) = (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐼SymPoly𝑅))
Theorem	esplyval 33820*	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 33821*	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 33822	The 0-th elementary symmetric polynomial is the constant 1. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝑈 = (1r‘(𝐼 mPoly 𝑅))    ⇒   ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘0) = 𝑈)
Theorem	esplyfval2 33823*	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 33824*	Lemma for esplyfv 33828 and others. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝟭‘𝐼) “ {𝑐 ∈ 𝒫 𝐼 ∣ (♯‘𝑐) = 𝐾}) ⊆ 𝐷)
Theorem	esplympl 33825*	Elementary symmetric polynomials are polynomials. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))    ⇒   ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘𝐾) ∈ 𝑀)
Theorem	esplymhp 33826*	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 33827*	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 33828*	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 33829*	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 33830*	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 33831	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 33832	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 33833*	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 33834*	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 33835	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 33836*	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 33837*	Lemma for vieta 33838: 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 33838*	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 26353 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.52  The subring algebra
Theorem	sra1r 33839	The unity element of a subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 1 = (1r‘𝑊))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → 1 = (1r‘𝐴))
Theorem	sradrng 33840	Condition for a subring algebra to be a division ring. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵) → 𝐴 ∈ DivRing)
Theorem	sraidom 33841	Condition for a subring algebra to be an integral domain. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝑉 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ IDomn)
Theorem	srasubrg 33842	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 33843	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 33844	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 33845	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 33846	A subring is a subspace of the subring algebra. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑊 = ((subringAlg ‘𝑅)‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑅)    &   ⊢ 𝑆 = (𝑅 ↾s 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝐶 ∈ (SubRing‘𝑆))    ⇒   ⊢ (𝜑 → 𝐵 ∈ (LSubSp‘𝑊))
Theorem	srapwov 33847	The "power" operation on a subring algebra. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ 𝐴 = ((subringAlg ‘𝑊)‘𝑆)    &   ⊢ (𝜑 → 𝑊 ∈ Ring)    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → (.g‘(mulGrp‘𝑊)) = (.g‘(mulGrp‘𝐴)))
21.3.10.53  Division Ring Extensions
Theorem	drgext0g 33848	The additive neutral element of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.)
⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ DivRing)    &   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸))    ⇒   ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐵))
Theorem	drgextvsca 33849	The scalar multiplication operation of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.)
⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ DivRing)    &   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸))    ⇒   ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘𝐵))
Theorem	drgext0gsca 33850	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 33851	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 33852	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 33853*	Group sum in a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.)
⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ DivRing)    &   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸))    &   ⊢ 𝐹 = (𝐸 ↾s 𝑈)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ 𝑌)) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ 𝑌)))
21.3.10.54  Vector Spaces
Theorem	lvecdimfi 33854	Finite version of lvecdim 21207 which does not require the axiom of choice. The axiom of choice is used in acsmapd 18569, which is required in the infinite case. Suggested by Gérard Lang. (Contributed by Thierry Arnoux, 24-May-2023.)
⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝑆 ≈ 𝑇)
Theorem	exsslsb 33855*	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 33856	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.55  Vector Space Dimension
Syntax	cldim 33857	Extend class notation with the dimension of a vector space.
class dim
Definition	df-dim 33858	Define the dimension of a vector space as the cardinality of its bases. Note that by lvecdim 21207, all bases are equinumerous. (Contributed by Thierry Arnoux, 6-May-2023.)
⊢ dim = (𝑓 ∈ V ↦ ∪ (♯ “ (LBasis‘𝑓)))
Theorem	dimval 33859	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 33860	The dimension of a vector space 𝐹 is the cardinality of one of its bases. This version of dimval 33859 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 33861	Closure of the vector space dimension. (Contributed by Thierry Arnoux, 18-May-2023.)
⊢ (𝑉 ∈ LVec → (dim‘𝑉) ∈ ℕ0*)
Theorem	lmimdim 33862	Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Feb-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝑆 LMIso 𝑇))    &   ⊢ (𝜑 → 𝑆 ∈ LVec)    ⇒   ⊢ (𝜑 → (dim‘𝑆) = (dim‘𝑇))
Theorem	lmicdim 33863	Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Mar-2025.)
⊢ (𝜑 → 𝑆 ≃𝑚 𝑇)    &   ⊢ (𝜑 → 𝑆 ∈ LVec)    ⇒   ⊢ (𝜑 → (dim‘𝑆) = (dim‘𝑇))
Theorem	lvecdim0i 33864	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 33865	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 33866	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 33867*	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‘𝐿))
Theorem	rlmdim 33868	The left vector space induced by a ring over itself has dimension 1. (Contributed by Thierry Arnoux, 5-Aug-2023.) Generalize to division rings. (Revised by SN, 22-Mar-2025.)
⊢ 𝑉 = (ringLMod‘𝐹)    ⇒   ⊢ (𝐹 ∈ DivRing → (dim‘𝑉) = 1)
Theorem	frlmdim 33869	Dimension of a free left module. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝐹 = (𝑅 freeLMod 𝐼)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉) → (dim‘𝐹) = (♯‘𝐼))
Theorem	tnglvec 33870	Augmenting a structure with a norm conserves left vector spaces. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 ∈ LVec ↔ 𝑇 ∈ LVec))
Theorem	tngdim 33871	Dimension of a left vector space augmented with a norm. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    ⇒   ⊢ ((𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉) → (dim‘𝐺) = (dim‘𝑇))
Theorem	rrxdim 33872	Dimension of the generalized Euclidean space. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝐻 = (ℝ^‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → (dim‘𝐻) = (♯‘𝐼))
Theorem	matdim 33873	Dimension of the space of square matrices. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝐴 = (𝐼 Mat 𝑅)    &   ⊢ 𝑁 = (♯‘𝐼)    ⇒   ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → (dim‘𝐴) = (𝑁 · 𝑁))
Theorem	lbslsat 33874	A nonzero vector 𝑋 is a basis of a line spanned by the singleton 𝑋. Spans of nonzero singletons are sometimes called "atoms", see df-lsatoms 39564 and for example lsatlspsn 39581. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑌 = (𝑊 ↾s (𝑁‘{𝑋}))    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → {𝑋} ∈ (LBasis‘𝑌))
Theorem	lsatdim 33875	A line, spanned by a nonzero singleton, has dimension 1. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑌 = (𝑊 ↾s (𝑁‘{𝑋}))    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (dim‘𝑌) = 1)
Theorem	drngdimgt0 33876	The dimension of a vector space that is also a division ring is greater than zero. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ ((𝐹 ∈ LVec ∧ 𝐹 ∈ DivRing) → 0 < (dim‘𝐹))
Theorem	lmhmlvec2 33877	A homomorphism of left vector spaces has a left vector space as codomain. (Contributed by Thierry Arnoux, 7-May-2023.)
⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝑈 ∈ LVec)
Theorem	kerlmhm 33878	The kernel of a vector space homomorphism is a vector space itself. (Contributed by Thierry Arnoux, 7-May-2023.)
⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐾 = (𝑉 ↾s (◡𝐹 “ { 0 }))    ⇒   ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝐾 ∈ LVec)
Theorem	imlmhm 33879	The image of a vector space homomorphism is a vector space itself. (Contributed by Thierry Arnoux, 7-May-2023.)
⊢ 𝐼 = (𝑈 ↾s ran 𝐹)    ⇒   ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝐼 ∈ LVec)
Theorem	ply1degltdimlem 33880*	Lemma for ply1degltdim 33881. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ 𝐸 = (𝑃 ↾s 𝑆)    &   ⊢ 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)))    ⇒   ⊢ (𝜑 → ran 𝐹 ∈ (LBasis‘𝐸))
Theorem	ply1degltdim 33881	The space 𝑆 of the univariate polynomials of degree less than 𝑁 has dimension 𝑁. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ 𝐸 = (𝑃 ↾s 𝑆)    ⇒   ⊢ (𝜑 → (dim‘𝐸) = 𝑁)
Theorem	lindsunlem 33882	Lemma for lindsun 33883. (Contributed by Thierry Arnoux, 9-May-2023.)
⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ (LIndS‘𝑊))    &   ⊢ (𝜑 → 𝑉 ∈ (LIndS‘𝑊))    &   ⊢ (𝜑 → ((𝑁‘𝑈) ∩ (𝑁‘𝑉)) = { 0 })    &   ⊢ 𝑂 = (0g‘(Scalar‘𝑊))    &   ⊢ 𝐹 = (Base‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐾 ∈ (𝐹 ∖ {𝑂}))    &   ⊢ (𝜑 → (𝐾( ·𝑠 ‘𝑊)𝐶) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝐶})))    ⇒   ⊢ (𝜑 → ⊥)
Theorem	lindsun 33883	Condition for the union of two independent sets to be an independent set. (Contributed by Thierry Arnoux, 9-May-2023.)
⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ (LIndS‘𝑊))    &   ⊢ (𝜑 → 𝑉 ∈ (LIndS‘𝑊))    &   ⊢ (𝜑 → ((𝑁‘𝑈) ∩ (𝑁‘𝑉)) = { 0 })    ⇒   ⊢ (𝜑 → (𝑈 ∪ 𝑉) ∈ (LIndS‘𝑊))
Theorem	lbsdiflsp0 33884	The linear spans of two disjunct independent sets only have a trivial intersection. This can be seen as the opposite direction of lindsun 33883. (Contributed by Thierry Arnoux, 17-May-2023.)
⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ∧ 𝑉 ⊆ 𝐵) → ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉)) = { 0 })
Theorem	dimkerim 33885	Given a linear map 𝐹 between vector spaces 𝑉 and 𝑈, the dimension of the vector space 𝑉 is the sum of the dimension of 𝐹 's kernel and the dimension of 𝐹's image. Second part of theorem 5.3 in [Lang] p. 141 This can also be described as the Rank-nullity theorem, (dim‘𝐼) being the rank of 𝐹 (the dimension of its image), and (dim‘𝐾) its nullity (the dimension of its kernel). (Contributed by Thierry Arnoux, 17-May-2023.)
⊢ 0 = (0g‘𝑈)    &   ⊢ 𝐾 = (𝑉 ↾s (◡𝐹 “ { 0 }))    &   ⊢ 𝐼 = (𝑈 ↾s ran 𝐹)    ⇒   ⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼)))
Theorem	qusdimsum 33886	Let 𝑊 be a vector space, and let 𝑋 be a subspace. Then the dimension of 𝑊 is the sum of the dimension of 𝑋 and the dimension of the quotient space of 𝑋. First part of theorem 5.3 in [Lang] p. 141. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑌 = (𝑊 /s (𝑊 ~QG 𝑈))    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝑈 ∈ (LSubSp‘𝑊)) → (dim‘𝑊) = ((dim‘𝑋) +𝑒 (dim‘𝑌)))
Theorem	fedgmullem1 33887*	Lemma for fedgmul 33889. (Contributed by Thierry Arnoux, 20-Jul-2023.)
⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑉)    &   ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)    &   ⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉)    &   ⊢ 𝐹 = (𝐸 ↾s 𝑈)    &   ⊢ 𝐾 = (𝐸 ↾s 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ DivRing)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝐾 ∈ DivRing)    &   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸))    &   ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐹))    &   ⊢ 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(.r‘𝐸)𝑗))    &   ⊢ 𝐻 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝐺‘𝑗)‘𝑖))    &   ⊢ (𝜑 → 𝑋 ∈ (LBasis‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (LBasis‘𝐵))    &   ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐴))    &   ⊢ (𝜑 → 𝐿:𝑌⟶(Base‘(Scalar‘𝐵)))    &   ⊢ (𝜑 → 𝐿 finSupp (0g‘(Scalar‘𝐵)))    &   ⊢ (𝜑 → 𝑍 = (𝐵 Σg (𝑗 ∈ 𝑌 ↦ ((𝐿‘𝑗)( ·𝑠 ‘𝐵)𝑗))))    &   ⊢ (𝜑 → 𝐺:𝑌⟶((Base‘(Scalar‘𝐶)) ↑m 𝑋))    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐺‘𝑗) finSupp (0g‘(Scalar‘𝐶)))    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑌) → (𝐿‘𝑗) = (𝐶 Σg (𝑖 ∈ 𝑋 ↦ (((𝐺‘𝑗)‘𝑖)( ·𝑠 ‘𝐶)𝑖))))    ⇒   ⊢ (𝜑 → (𝐻 finSupp (0g‘(Scalar‘𝐴)) ∧ 𝑍 = (𝐴 Σg (𝐻 ∘f ( ·𝑠 ‘𝐴)𝐷))))
Theorem	fedgmullem2 33888*	Lemma for fedgmul 33889. (Contributed by Thierry Arnoux, 20-Jul-2023.)
⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑉)    &   ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)    &   ⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉)    &   ⊢ 𝐹 = (𝐸 ↾s 𝑈)    &   ⊢ 𝐾 = (𝐸 ↾s 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ DivRing)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝐾 ∈ DivRing)    &   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸))    &   ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐹))    &   ⊢ 𝐷 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ (𝑖(.r‘𝐸)𝑗))    &   ⊢ 𝐻 = (𝑗 ∈ 𝑌, 𝑖 ∈ 𝑋 ↦ ((𝐺‘𝑗)‘𝑖))    &   ⊢ (𝜑 → 𝑋 ∈ (LBasis‘𝐶))    &   ⊢ (𝜑 → 𝑌 ∈ (LBasis‘𝐵))    &   ⊢ (𝜑 → 𝑊 ∈ (Base‘((Scalar‘𝐴) freeLMod (𝑌 × 𝑋))))    &   ⊢ (𝜑 → (𝐴 Σg (𝑊 ∘f ( ·𝑠 ‘𝐴)𝐷)) = (0g‘𝐴))    ⇒   ⊢ (𝜑 → 𝑊 = ((𝑌 × 𝑋) × {(0g‘(Scalar‘𝐴))}))
Theorem	fedgmul 33889	The multiplicativity formula for degrees of field extensions. Given 𝐸 a field extension of 𝐹, itself a field extension of 𝐾, we have [𝐸:𝐾] = [𝐸:𝐹][𝐹:𝐾]. Proposition 1.2 of [Lang], p. 224. Here (dim‘𝐴) is the degree of the extension 𝐸 of 𝐾, (dim‘𝐵) is the degree of the extension 𝐸 of 𝐹, and (dim‘𝐶) is the degree of the extension 𝐹 of 𝐾. This proof is valid for infinite dimensions, and is actually valid for division ring extensions, not just field extensions. (Contributed by Thierry Arnoux, 25-Jul-2023.)
⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑉)    &   ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)    &   ⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉)    &   ⊢ 𝐹 = (𝐸 ↾s 𝑈)    &   ⊢ 𝐾 = (𝐸 ↾s 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ DivRing)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝐾 ∈ DivRing)    &   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸))    &   ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐹))    ⇒   ⊢ (𝜑 → (dim‘𝐴) = ((dim‘𝐵) ·e (dim‘𝐶)))
Theorem	dimlssid 33890	If the dimension of a linear subspace 𝐿 is the dimension of the whole vector space 𝐸, then 𝐿 is the whole space. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ LVec)    &   ⊢ (𝜑 → (dim‘𝐸) ∈ ℕ0)    &   ⊢ (𝜑 → 𝐿 ∈ (LSubSp‘𝐸))    &   ⊢ (𝜑 → (dim‘(𝐸 ↾s 𝐿)) = (dim‘𝐸))    ⇒   ⊢ (𝜑 → 𝐿 = 𝐵)
Theorem	lvecendof1f1o 33891	If an endomorphism 𝑈 of a vector space 𝐸 of finite dimension is injective, then it is bijective. Item (b) of Corollary of Proposition 9 in [BourbakiAlg1] p. 298 . (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ LVec)    &   ⊢ (𝜑 → (dim‘𝐸) ∈ ℕ0)    &   ⊢ (𝜑 → 𝑈 ∈ (𝐸 LMHom 𝐸))    &   ⊢ (𝜑 → 𝑈:𝐵–1-1→𝐵)    ⇒   ⊢ (𝜑 → 𝑈:𝐵–1-1-onto→𝐵)
Theorem	lactlmhm 33892*	In an associative algebra 𝐴, left-multiplication by a fixed element of the algebra is a module homomorphism, analogous to ringlghm 20341. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = (.r‘𝐴)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐶 · 𝑥))    &   ⊢ (𝜑 → 𝐴 ∈ AssAlg)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐴 LMHom 𝐴))
Theorem	assalactf1o 33893*	In an associative algebra 𝐴, left-multiplication by a fixed element of the algebra is bijective. See also lactlmhm 33892. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = (.r‘𝐴)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐶 · 𝑥))    &   ⊢ (𝜑 → 𝐴 ∈ AssAlg)    &   ⊢ 𝐸 = (RLReg‘𝐴)    &   ⊢ 𝐾 = (Scalar‘𝐴)    &   ⊢ (𝜑 → 𝐾 ∈ DivRing)    &   ⊢ (𝜑 → (dim‘𝐴) ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐸)    ⇒   ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝐵)
Theorem	assarrginv 33894	If an element 𝑋 of an associative algebra 𝐴 over a division ring 𝐾 is regular, then it is a unit. Proposition 2. in Chapter 5. of [BourbakiAlg2] p. 113. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐸 = (RLReg‘𝐴)    &   ⊢ 𝑈 = (Unit‘𝐴)    &   ⊢ 𝐾 = (Scalar‘𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ AssAlg)    &   ⊢ (𝜑 → 𝐾 ∈ DivRing)    &   ⊢ (𝜑 → (dim‘𝐴) ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐸)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝑈)
Theorem	assafld 33895	If an algebra 𝐴 of finite degree over a division ring 𝐾 is an integral domain, then it is a field. Corollary of Proposition 2. in Chapter 5. of [BourbakiAlg2] p. 113. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐾 = (Scalar‘𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ AssAlg)    &   ⊢ (𝜑 → 𝐴 ∈ IDomn)    &   ⊢ (𝜑 → 𝐾 ∈ DivRing)    &   ⊢ (𝜑 → (dim‘𝐴) ∈ ℕ0)    ⇒   ⊢ (𝜑 → 𝐴 ∈ Field)
21.3.11  Field Extensions
Syntax	cfldext 33896	Syntax for the field extension relation.
class /FldExt
Syntax	cfinext 33897	Syntax for the finite field extension relation.
class /FinExt
Syntax	cextdg 33898	Syntax for the field extension degree operation.
class [:]
Definition	df-fldext 33899*	Definition of the field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ /FldExt = {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒 ↾s (Base‘𝑓)) ∧ (Base‘𝑓) ∈ (SubRing‘𝑒)))}
Definition	df-extdg 33900*	Definition of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ [:] = (𝑒 ∈ V, 𝑓 ∈ (/FldExt “ {𝑒}) ↦ (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓))))