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
Definition	df-sply 33701*	Define symmetric polynomials. See splyval 33703 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 33702*	Define elementary symmetric polynomials. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ eSymPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑘 ∈ ℕ0 ↦ ((ℤRHom‘𝑟) ∘ ((𝟭‘{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0})‘((𝟭‘𝑖) “ {𝑐 ∈ 𝒫 𝑖 ∣ (♯‘𝑐) = 𝑘})))))
Theorem	splyval 33703*	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 33704*	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 33705*	Conditions for being a symmetric polynomial. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ 𝑆 = (SymGrp‘𝐼)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))    &   ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑀)    &   ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑃) ∧ 𝑥 ∈ 𝐷) → (𝐹‘(𝑥 ∘ 𝑝)) = (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐼SymPoly𝑅))
Theorem	esplyval 33706*	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 33707*	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 33708	The 0-th elementary symmetric polynomial is the constant 1. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝑈 = (1r‘(𝐼 mPoly 𝑅))    ⇒   ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘0) = 𝑈)
Theorem	esplyfval2 33709*	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 33710*	Lemma for esplyfv 33714 and others. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝟭‘𝐼) “ {𝑐 ∈ 𝒫 𝐼 ∣ (♯‘𝑐) = 𝐾}) ⊆ 𝐷)
Theorem	esplympl 33711*	Elementary symmetric polynomials are polynomials. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))    ⇒   ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘𝐾) ∈ 𝑀)
Theorem	esplymhp 33712*	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 33713*	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 33714*	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 33715*	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 33716*	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 33717	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 33718	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 33719*	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 33720*	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 33721	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 33722*	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 33723*	Lemma for vieta 33724: 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 33724*	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 26278 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 33725	The unity element of a subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 1 = (1r‘𝑊))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → 1 = (1r‘𝐴))
Theorem	sradrng 33726	Condition for a subring algebra to be a division ring. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵) → 𝐴 ∈ DivRing)
Theorem	sraidom 33727	Condition for a subring algebra to be an integral domain. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝑉 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ IDomn)
Theorem	srasubrg 33728	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 33729	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 33730	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 33731	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 33732	A subring is a subspace of the subring algebra. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑊 = ((subringAlg ‘𝑅)‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑅)    &   ⊢ 𝑆 = (𝑅 ↾s 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝐶 ∈ (SubRing‘𝑆))    ⇒   ⊢ (𝜑 → 𝐵 ∈ (LSubSp‘𝑊))
Theorem	srapwov 33733	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 33734	The additive neutral element of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.)
⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ DivRing)    &   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸))    ⇒   ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐵))
Theorem	drgextvsca 33735	The scalar multiplication operation of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.)
⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ DivRing)    &   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸))    ⇒   ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘𝐵))
Theorem	drgext0gsca 33736	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 33737	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 33738	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 33739*	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 33740	Finite version of lvecdim 21155 which does not require the axiom of choice. The axiom of choice is used in acsmapd 18520, which is required in the infinite case. Suggested by Gérard Lang. (Contributed by Thierry Arnoux, 24-May-2023.)
⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝑆 ≈ 𝑇)
Theorem	exsslsb 33741*	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 33742	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 33743	Extend class notation with the dimension of a vector space.
class dim
Definition	df-dim 33744	Define the dimension of a vector space as the cardinality of its bases. Note that by lvecdim 21155, all bases are equinumerous. (Contributed by Thierry Arnoux, 6-May-2023.)
⊢ dim = (𝑓 ∈ V ↦ ∪ (♯ “ (LBasis‘𝑓)))
Theorem	dimval 33745	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 33746	The dimension of a vector space 𝐹 is the cardinality of one of its bases. This version of dimval 33745 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 33747	Closure of the vector space dimension. (Contributed by Thierry Arnoux, 18-May-2023.)
⊢ (𝑉 ∈ LVec → (dim‘𝑉) ∈ ℕ0*)
Theorem	lmimdim 33748	Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Feb-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝑆 LMIso 𝑇))    &   ⊢ (𝜑 → 𝑆 ∈ LVec)    ⇒   ⊢ (𝜑 → (dim‘𝑆) = (dim‘𝑇))
Theorem	lmicdim 33749	Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Mar-2025.)
⊢ (𝜑 → 𝑆 ≃𝑚 𝑇)    &   ⊢ (𝜑 → 𝑆 ∈ LVec)    ⇒   ⊢ (𝜑 → (dim‘𝑆) = (dim‘𝑇))
Theorem	lvecdim0i 33750	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 33751	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 33752	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 33753*	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 33754	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 33755	Dimension of a free left module. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝐹 = (𝑅 freeLMod 𝐼)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉) → (dim‘𝐹) = (♯‘𝐼))
Theorem	tnglvec 33756	Augmenting a structure with a norm conserves left vector spaces. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 ∈ LVec ↔ 𝑇 ∈ LVec))
Theorem	tngdim 33757	Dimension of a left vector space augmented with a norm. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    ⇒   ⊢ ((𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉) → (dim‘𝐺) = (dim‘𝑇))
Theorem	rrxdim 33758	Dimension of the generalized Euclidean space. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝐻 = (ℝ^‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → (dim‘𝐻) = (♯‘𝐼))
Theorem	matdim 33759	Dimension of the space of square matrices. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝐴 = (𝐼 Mat 𝑅)    &   ⊢ 𝑁 = (♯‘𝐼)    ⇒   ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → (dim‘𝐴) = (𝑁 · 𝑁))
Theorem	lbslsat 33760	A nonzero vector 𝑋 is a basis of a line spanned by the singleton 𝑋. Spans of nonzero singletons are sometimes called "atoms", see df-lsatoms 39422 and for example lsatlspsn 39439. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑌 = (𝑊 ↾s (𝑁‘{𝑋}))    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → {𝑋} ∈ (LBasis‘𝑌))
Theorem	lsatdim 33761	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 33762	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 33763	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 33764	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 33765	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 33766*	Lemma for ply1degltdim 33767. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ 𝐸 = (𝑃 ↾s 𝑆)    &   ⊢ 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)))    ⇒   ⊢ (𝜑 → ran 𝐹 ∈ (LBasis‘𝐸))
Theorem	ply1degltdim 33767	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 33768	Lemma for lindsun 33769. (Contributed by Thierry Arnoux, 9-May-2023.)
⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ (LIndS‘𝑊))    &   ⊢ (𝜑 → 𝑉 ∈ (LIndS‘𝑊))    &   ⊢ (𝜑 → ((𝑁‘𝑈) ∩ (𝑁‘𝑉)) = { 0 })    &   ⊢ 𝑂 = (0g‘(Scalar‘𝑊))    &   ⊢ 𝐹 = (Base‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐾 ∈ (𝐹 ∖ {𝑂}))    &   ⊢ (𝜑 → (𝐾( ·𝑠 ‘𝑊)𝐶) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝐶})))    ⇒   ⊢ (𝜑 → ⊥)
Theorem	lindsun 33769	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 33770	The linear spans of two disjunct independent sets only have a trivial intersection. This can be seen as the opposite direction of lindsun 33769. (Contributed by Thierry Arnoux, 17-May-2023.)
⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ∧ 𝑉 ⊆ 𝐵) → ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉)) = { 0 })
Theorem	dimkerim 33771	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 33772	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 33773*	Lemma for fedgmul 33775. (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 33774*	Lemma for fedgmul 33775. (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 33775	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 33776	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 33777	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 33778*	In an associative algebra 𝐴, left-multiplication by a fixed element of the algebra is a module homomorphism, analogous to ringlghm 20293. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = (.r‘𝐴)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐶 · 𝑥))    &   ⊢ (𝜑 → 𝐴 ∈ AssAlg)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐴 LMHom 𝐴))
Theorem	assalactf1o 33779*	In an associative algebra 𝐴, left-multiplication by a fixed element of the algebra is bijective. See also lactlmhm 33778. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = (.r‘𝐴)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐶 · 𝑥))    &   ⊢ (𝜑 → 𝐴 ∈ AssAlg)    &   ⊢ 𝐸 = (RLReg‘𝐴)    &   ⊢ 𝐾 = (Scalar‘𝐴)    &   ⊢ (𝜑 → 𝐾 ∈ DivRing)    &   ⊢ (𝜑 → (dim‘𝐴) ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐸)    ⇒   ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝐵)
Theorem	assarrginv 33780	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 33781	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 33782	Syntax for the field extension relation.
class /FldExt
Syntax	cfinext 33783	Syntax for the finite field extension relation.
class /FinExt
Syntax	cextdg 33784	Syntax for the field extension degree operation.
class [:]
Definition	df-fldext 33785*	Definition of the field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ /FldExt = {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒 ↾s (Base‘𝑓)) ∧ (Base‘𝑓) ∈ (SubRing‘𝑒)))}
Definition	df-extdg 33786*	Definition of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ [:] = (𝑒 ∈ V, 𝑓 ∈ (/FldExt “ {𝑒}) ↦ (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓))))
Definition	df-finext 33787*	Definition of the finite field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ /FinExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)}
Theorem	relfldext 33788	The field extension is a relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ Rel /FldExt
Theorem	brfldext 33789	The field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ Field) → (𝐸/FldExt𝐹 ↔ (𝐹 = (𝐸 ↾s (Base‘𝐹)) ∧ (Base‘𝐹) ∈ (SubRing‘𝐸))))
Theorem	ccfldextrr 33790	The field of the complex numbers is an extension of the field of the real numbers. (Contributed by Thierry Arnoux, 20-Jul-2023.)
⊢ ℂfld/FldExtℝfld
Theorem	fldextfld1 33791	A field extension is only defined if the extension is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → 𝐸 ∈ Field)
Theorem	fldextfld2 33792	A field extension is only defined if the subfield is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → 𝐹 ∈ Field)
Theorem	fldextsubrg 33793	Field extension implies a subring relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ 𝑈 = (Base‘𝐹)    ⇒   ⊢ (𝐸/FldExt𝐹 → 𝑈 ∈ (SubRing‘𝐸))
Theorem	sdrgfldext 33794	A field 𝐸 and any sub-division-ring 𝐹 of 𝐸 form a field extension. (Contributed by Thierry Arnoux, 26-Oct-2025.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    ⇒   ⊢ (𝜑 → 𝐸/FldExt(𝐸 ↾s 𝐹))
Theorem	fldextress 33795	Field extension implies a structure restriction relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → 𝐹 = (𝐸 ↾s (Base‘𝐹)))
Theorem	brfinext 33796	The finite field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → (𝐸/FinExt𝐹 ↔ (𝐸[:]𝐹) ∈ ℕ0))
Theorem	extdgval 33797	Value of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) = (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
Theorem	fldextsdrg 33798	Deduce sub-division-ring from field extension. (Contributed by Thierry Arnoux, 26-Oct-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐸/FldExt𝐹)    ⇒   ⊢ (𝜑 → 𝐵 ∈ (SubDRing‘𝐸))
Theorem	fldextsralvec 33799	The subring algebra associated with a field extension is a vector space. (Contributed by Thierry Arnoux, 3-Aug-2023.)
⊢ (𝐸/FldExt𝐹 → ((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec)
Theorem	extdgcl 33800	Closure of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) ∈ ℕ0*)