P. 337 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33601-33700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	evl1deg1 33601	Evaluation of a univariate polynomial of degree 1. (Contributed by Thierry Arnoux, 8-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ · = (.r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ 𝐶 = (coe1‘𝑀)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝐴 = (𝐶‘1)    &   ⊢ 𝐵 = (𝐶‘0)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑈)    &   ⊢ (𝜑 → (𝐷‘𝑀) = 1)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑂‘𝑀)‘𝑋) = ((𝐴 · 𝑋) + 𝐵))
Theorem	evl1deg2 33602	Evaluation of a univariate polynomial of degree 2. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ · = (.r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    &   ⊢ 𝐹 = (coe1‘𝑀)    &   ⊢ 𝐸 = (deg1‘𝑅)    &   ⊢ 𝐴 = (𝐹‘2)    &   ⊢ 𝐵 = (𝐹‘1)    &   ⊢ 𝐶 = (𝐹‘0)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑈)    &   ⊢ (𝜑 → (𝐸‘𝑀) = 2)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑂‘𝑀)‘𝑋) = ((𝐴 · (2 ↑ 𝑋)) + ((𝐵 · 𝑋) + 𝐶)))
Theorem	evl1deg3 33603	Evaluation of a univariate polynomial of degree 3. (Contributed by Thierry Arnoux, 14-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ · = (.r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    &   ⊢ 𝐹 = (coe1‘𝑀)    &   ⊢ 𝐸 = (deg1‘𝑅)    &   ⊢ 𝐴 = (𝐹‘3)    &   ⊢ 𝐵 = (𝐹‘2)    &   ⊢ 𝐶 = (𝐹‘1)    &   ⊢ 𝐷 = (𝐹‘0)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑈)    &   ⊢ (𝜑 → (𝐸‘𝑀) = 3)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝑂‘𝑀)‘𝑋) = (((𝐴 · (3 ↑ 𝑋)) + (𝐵 · (2 ↑ 𝑋))) + ((𝐶 · 𝑋) + 𝐷)))
Theorem	ply1dg1rt 33604	Express the root − 𝐵 / 𝐴 of a polynomial 𝐴 · 𝑋 + 𝐵 of degree 1 over a field. (Contributed by Thierry Arnoux, 8-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Field)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑈)    &   ⊢ (𝜑 → (𝐷‘𝐺) = 1)    &   ⊢ 𝑁 = (invg‘𝑅)    &   ⊢ / = (/r‘𝑅)    &   ⊢ 𝐶 = (coe1‘𝐺)    &   ⊢ 𝐴 = (𝐶‘1)    &   ⊢ 𝐵 = (𝐶‘0)    &   ⊢ 𝑍 = ((𝑁‘𝐵) / 𝐴)    ⇒   ⊢ (𝜑 → (◡(𝑂‘𝐺) “ { 0 }) = {𝑍})
Theorem	ply1dg1rtn0 33605	Polynomials of degree 1 over a field always have some roots. (Contributed by Thierry Arnoux, 8-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Field)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑈)    &   ⊢ (𝜑 → (𝐷‘𝐺) = 1)    ⇒   ⊢ (𝜑 → (◡(𝑂‘𝐺) “ { 0 }) ≠ ∅)
Theorem	ply1mulrtss 33606	The roots of a factor 𝐹 are also roots of the product of polynomials (𝐹 · 𝐺). (Contributed by Thierry Arnoux, 8-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑂 = (eval1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑈)    &   ⊢ · = (.r‘𝑃)    ⇒   ⊢ (𝜑 → (◡(𝑂‘𝐹) “ { 0 }) ⊆ (◡(𝑂‘(𝐹 · 𝐺)) “ { 0 }))
Theorem	ply1dg3rt0irred 33607	If a cubic polynomial over a field has no roots, it is irreducible. (Proposed by Saveliy Skresanov, 5-Jun-2025.) (Contributed by Thierry Arnoux, 8-Jun-2025.)
⊢ 0 = (0g‘𝐹)    &   ⊢ 𝑂 = (eval1‘𝐹)    &   ⊢ 𝐷 = (deg1‘𝐹)    &   ⊢ 𝑃 = (Poly1‘𝐹)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ Field)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐵)    &   ⊢ (𝜑 → (◡(𝑂‘𝑄) “ { 0 }) = ∅)    &   ⊢ (𝜑 → (𝐷‘𝑄) = 3)    ⇒   ⊢ (𝜑 → 𝑄 ∈ (Irred‘𝑃))
Theorem	m1pmeq 33608	If two monic polynomials 𝐼 and 𝐽 differ by a unit factor 𝐾, then they are equal. (Contributed by Thierry Arnoux, 27-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝐹)    &   ⊢ 𝑀 = (Monic1p‘𝐹)    &   ⊢ 𝑈 = (Unit‘𝑃)    &   ⊢ · = (.r‘𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ Field)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑀)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐼 = (𝐾 · 𝐽))    ⇒   ⊢ (𝜑 → 𝐼 = 𝐽)
Theorem	ply1fermltl 33609	Fermat's little theorem for polynomials. If 𝑃 is prime, Then (𝑋 + 𝐴)↑𝑃 = ((𝑋↑𝑃) + 𝐴) modulo 𝑃. (Contributed by Thierry Arnoux, 24-Jul-2024.)
⊢ 𝑍 = (ℤ/nℤ‘𝑃)    &   ⊢ 𝑊 = (Poly1‘𝑍)    &   ⊢ 𝑋 = (var1‘𝑍)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (mulGrp‘𝑊)    &   ⊢ ↑ = (.g‘𝑁)    &   ⊢ 𝐶 = (algSc‘𝑊)    &   ⊢ 𝐴 = (𝐶‘((ℤRHom‘𝑍)‘𝐸))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝐸 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑃 ↑ (𝑋 + 𝐴)) = ((𝑃 ↑ 𝑋) + 𝐴))
Theorem	coe1mon 33610*	Coefficient vector of a monomial. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝜑 → (coe1‘(𝑁 ↑ 𝑋)) = (𝑘 ∈ ℕ0 ↦ if(𝑘 = 𝑁, 1 , 0 )))
Theorem	ply1moneq 33611	Two monomials are equal iff their powers are equal. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝑀 ↑ 𝑋) = (𝑁 ↑ 𝑋) ↔ 𝑀 = 𝑁))
Theorem	coe1zfv 33612	The coefficients of the zero univariate polynomial. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((coe1‘𝑍)‘𝑁) = 0 )
Theorem	coe1vr1 33613*	Polynomial coefficient of the variable. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ (𝜑 → (coe1‘𝑋) = (𝑘 ∈ ℕ0 ↦ if(𝑘 = 1, 1 , 0 )))
Theorem	deg1vr 33614	The degree of the variable polynomial is 1. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    ⇒   ⊢ (𝜑 → (𝐷‘𝑋) = 1)
Theorem	ply1degltel 33615	Characterize elementhood in the set 𝑆 of polynomials of degree less than 𝑁. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹 ∈ 𝐵 ∧ (𝐷‘𝐹) ≤ (𝑁 − 1))))
Theorem	ply1degleel 33616	Characterize elementhood in the set 𝑆 of polynomials of degree less than 𝑁. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑃)    ⇒   ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹 ∈ 𝐵 ∧ (𝐷‘𝐹) < 𝑁)))
Theorem	ply1degltlss 33617	The space 𝑆 of the univariate polynomials of degree less than 𝑁 forms a vector subspace. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → 𝑆 ∈ (LSubSp‘𝑃))
Theorem	gsummoncoe1fzo 33618*	A coefficient of the polynomial represented as a sum of scaled monomials is the coefficient of the corresponding scaled monomial. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ 𝑋 = (var1‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑃))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ ∗ = ( ·𝑠 ‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑁)𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐿 ∈ (0..^𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝑘 = 𝐿 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → ((coe1‘(𝑃 Σg (𝑘 ∈ (0..^𝑁) ↦ (𝐴 ∗ (𝑘 ↑ 𝑋)))))‘𝐿) = 𝐶)
Theorem	ply1gsumz 33619*	If a polynomial given as a sum of scaled monomials by factors 𝐴 is the zero polynomial, then all factors 𝐴 are zero. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)))    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ (𝜑 → 𝐴:(0..^𝑁)⟶𝐵)    &   ⊢ (𝜑 → (𝑃 Σg (𝐴 ∘f ( ·𝑠 ‘𝑃)𝐹)) = 𝑍)    ⇒   ⊢ (𝜑 → 𝐴 = ((0..^𝑁) × { 0 }))
Theorem	deg1addlt 33620	If both factors have degree bounded by 𝐿, then the sum of the polynomials also has degree bounded by 𝐿. See also deg1addle 26140. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑌 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ + = (+g‘𝑌)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐿 ∈ ℝ*)    &   ⊢ (𝜑 → (𝐷‘𝐹) < 𝐿)    &   ⊢ (𝜑 → (𝐷‘𝐺) < 𝐿)    ⇒   ⊢ (𝜑 → (𝐷‘(𝐹 + 𝐺)) < 𝐿)
Theorem	ig1pnunit 33621	The polynomial ideal generator is not a unit polynomial. (Contributed by Thierry Arnoux, 19-Mar-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (idlGen1p‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑃))    &   ⊢ (𝜑 → 𝐼 ≠ 𝑈)    ⇒   ⊢ (𝜑 → ¬ (𝐺‘𝐼) ∈ (Unit‘𝑃))
Theorem	ig1pmindeg 33622	The polynomial ideal generator is of minimum degree. (Contributed by Thierry Arnoux, 19-Mar-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐺 = (idlGen1p‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑃))    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐹 ≠ 0 )    ⇒   ⊢ (𝜑 → (𝐷‘(𝐺‘𝐼)) ≤ (𝐷‘𝐹))
21.3.10.47  Polynomial quotient and polynomial remainder
Theorem	q1pdir 33623	Distribution of univariate polynomial quotient over addition. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ / = (quot1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑁)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ + = (+g‘𝑃)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶)))
Theorem	q1pvsca 33624	Scalar multiplication property of the polynomial division. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ / = (quot1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑁)    &   ⊢ × = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝐵 × 𝐴) / 𝐶) = (𝐵 × (𝐴 / 𝐶)))
Theorem	r1pvsca 33625	Scalar multiplication property of the polynomial remainder operation. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑁)    &   ⊢ × = ( ·𝑠 ‘𝑃)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐾)    ⇒   ⊢ (𝜑 → ((𝐵 × 𝐴)𝐸𝐷) = (𝐵 × (𝐴𝐸𝐷)))
Theorem	r1p0 33626	Polynomial remainder operation of a division of the zero polynomial. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑁)    &   ⊢ 0 = (0g‘𝑃)    ⇒   ⊢ (𝜑 → ( 0 𝐸𝐷) = 0 )
Theorem	r1pcyc 33627	The polynomial remainder operation is periodic. See modcyc 13946. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ + = (+g‘𝑃)    &   ⊢ · = (.r‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑁)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝐴 + (𝐶 · 𝐵))𝐸𝐵) = (𝐴𝐸𝐵))
Theorem	r1padd1 33628	Addition property of the polynomial remainder operation, similar to modadd1 13948. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑁)    &   ⊢ (𝜑 → (𝐴𝐸𝐷) = (𝐵𝐸𝐷))    &   ⊢ + = (+g‘𝑃)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶)𝐸𝐷) = ((𝐵 + 𝐶)𝐸𝐷))
Theorem	r1pid2OLD 33629	Obsolete version of r1pid2 26201 as of 21-Jun-2025. (Contributed by Thierry Arnoux, 2-Apr-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑁)    ⇒   ⊢ (𝜑 → ((𝐴𝐸𝐵) = 𝐴 ↔ (𝐷‘𝐴) < (𝐷‘𝐵)))
Theorem	r1plmhm 33630*	The univariate polynomial remainder function 𝐹 is a module homomorphism. Its image (𝐹 “s 𝑃) is sometimes called the "ring of remainders" (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝐸 = (rem1p‘𝑅)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐹 = (𝑓 ∈ 𝑈 ↦ (𝑓𝐸𝑀))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑁)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑃 LMHom (𝐹 “s 𝑃)))
Theorem	r1pquslmic 33631*	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.48  The subring algebra
Theorem	sra1r 33632	The unity element of a subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023.)
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   ⊢ (𝜑 → 1 = (1r‘𝑊))    &   ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊))    ⇒   ⊢ (𝜑 → 1 = (1r‘𝐴))
Theorem	sradrng 33633	Condition for a subring algebra to be a division ring. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵) → 𝐴 ∈ DivRing)
Theorem	sraidom 33634	Condition for a subring algebra to be an integral domain. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ IDomn)    &   ⊢ (𝜑 → 𝑉 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ IDomn)
Theorem	srasubrg 33635	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 33636	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 33637	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 33638	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 33639	A subring is a subspace of the subring algebra. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑊 = ((subringAlg ‘𝑅)‘𝐶)    &   ⊢ 𝐴 = (Base‘𝑅)    &   ⊢ 𝑆 = (𝑅 ↾s 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝐶 ∈ (SubRing‘𝑆))    ⇒   ⊢ (𝜑 → 𝐵 ∈ (LSubSp‘𝑊))
21.3.10.49  Division Ring Extensions
Theorem	drgext0g 33640	The additive neutral element of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.)
⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ DivRing)    &   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸))    ⇒   ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐵))
Theorem	drgextvsca 33641	The scalar multiplication operation of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.)
⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ DivRing)    &   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸))    ⇒   ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘𝐵))
Theorem	drgext0gsca 33642	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 33643	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 33644	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 33645*	Group sum in a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.)
⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ DivRing)    &   ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸))    &   ⊢ 𝐹 = (𝐸 ↾s 𝑈)    &   ⊢ (𝜑 → 𝐹 ∈ DivRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ 𝑌)) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ 𝑌)))
21.3.10.50  Vector Spaces
Theorem	lvecdimfi 33646	Finite version of lvecdim 21159 which does not require the axiom of choice. The axiom of choice is used in acsmapd 18599, which is required in the infinite case. Suggested by Gérard Lang. (Contributed by Thierry Arnoux, 24-May-2023.)
⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝑆 ≈ 𝑇)
Theorem	exsslsb 33647*	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 33648	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.51  Vector Space Dimension
Syntax	cldim 33649	Extend class notation with the dimension of a vector space.
class dim
Definition	df-dim 33650	Define the dimension of a vector space as the cardinality of its bases. Note that by lvecdim 21159, all bases are equinumerous. (Contributed by Thierry Arnoux, 6-May-2023.)
⊢ dim = (𝑓 ∈ V ↦ ∪ (♯ “ (LBasis‘𝑓)))
Theorem	dimval 33651	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 33652	The dimension of a vector space 𝐹 is the cardinality of one of its bases. This version of dimval 33651 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 33653	Closure of the vector space dimension. (Contributed by Thierry Arnoux, 18-May-2023.)
⊢ (𝑉 ∈ LVec → (dim‘𝑉) ∈ ℕ0*)
Theorem	lmimdim 33654	Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Feb-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝑆 LMIso 𝑇))    &   ⊢ (𝜑 → 𝑆 ∈ LVec)    ⇒   ⊢ (𝜑 → (dim‘𝑆) = (dim‘𝑇))
Theorem	lmicdim 33655	Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Mar-2025.)
⊢ (𝜑 → 𝑆 ≃𝑚 𝑇)    &   ⊢ (𝜑 → 𝑆 ∈ LVec)    ⇒   ⊢ (𝜑 → (dim‘𝑆) = (dim‘𝑇))
Theorem	lvecdim0i 33656	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 33657	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 33658	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 33659*	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 33660	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	rgmoddimOLD 33661	Obsolete version of rlmdim 33660 as of 21-Mar-2025. (Contributed by Thierry Arnoux, 5-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑉 = (ringLMod‘𝐹)    ⇒   ⊢ (𝐹 ∈ Field → (dim‘𝑉) = 1)
Theorem	frlmdim 33662	Dimension of a free left module. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝐹 = (𝑅 freeLMod 𝐼)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉) → (dim‘𝐹) = (♯‘𝐼))
Theorem	tnglvec 33663	Augmenting a structure with a norm conserves left vector spaces. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 ∈ LVec ↔ 𝑇 ∈ LVec))
Theorem	tngdim 33664	Dimension of a left vector space augmented with a norm. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    ⇒   ⊢ ((𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉) → (dim‘𝐺) = (dim‘𝑇))
Theorem	rrxdim 33665	Dimension of the generalized Euclidean space. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝐻 = (ℝ^‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → (dim‘𝐻) = (♯‘𝐼))
Theorem	matdim 33666	Dimension of the space of square matrices. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝐴 = (𝐼 Mat 𝑅)    &   ⊢ 𝑁 = (♯‘𝐼)    ⇒   ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → (dim‘𝐴) = (𝑁 · 𝑁))
Theorem	lbslsat 33667	A nonzero vector 𝑋 is a basis of a line spanned by the singleton 𝑋. Spans of nonzero singletons are sometimes called "atoms", see df-lsatoms 38977 and for example lsatlspsn 38994. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑌 = (𝑊 ↾s (𝑁‘{𝑋}))    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → {𝑋} ∈ (LBasis‘𝑌))
Theorem	lsatdim 33668	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 33669	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 33670	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 33671	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 33672	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 33673*	Lemma for ply1degltdim 33674. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ 𝐸 = (𝑃 ↾s 𝑆)    &   ⊢ 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)))    ⇒   ⊢ (𝜑 → ran 𝐹 ∈ (LBasis‘𝐸))
Theorem	ply1degltdim 33674	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 33675	Lemma for lindsun 33676. (Contributed by Thierry Arnoux, 9-May-2023.)
⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ (LIndS‘𝑊))    &   ⊢ (𝜑 → 𝑉 ∈ (LIndS‘𝑊))    &   ⊢ (𝜑 → ((𝑁‘𝑈) ∩ (𝑁‘𝑉)) = { 0 })    &   ⊢ 𝑂 = (0g‘(Scalar‘𝑊))    &   ⊢ 𝐹 = (Base‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐾 ∈ (𝐹 ∖ {𝑂}))    &   ⊢ (𝜑 → (𝐾( ·𝑠 ‘𝑊)𝐶) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝐶})))    ⇒   ⊢ (𝜑 → ⊥)
Theorem	lindsun 33676	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 33677	The linear spans of two disjunct independent sets only have a trivial intersection. This can be seen as the opposite direction of lindsun 33676. (Contributed by Thierry Arnoux, 17-May-2023.)
⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ∧ 𝑉 ⊆ 𝐵) → ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉)) = { 0 })
Theorem	dimkerim 33678	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 33679	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 33680*	Lemma for fedgmul 33682. (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 33681*	Lemma for fedgmul 33682. (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 33682	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 33683	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 33684	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 33685*	In an associative algebra 𝐴, left-multiplication by a fixed element of the algebra is a module homomorphism, analogous to ringlghm 20309. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = (.r‘𝐴)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐶 · 𝑥))    &   ⊢ (𝜑 → 𝐴 ∈ AssAlg)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐴 LMHom 𝐴))
Theorem	assalactf1o 33686*	In an associative algebra 𝐴, left-multiplication by a fixed element of the algebra is bijective. See also lactlmhm 33685. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = (.r‘𝐴)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐶 · 𝑥))    &   ⊢ (𝜑 → 𝐴 ∈ AssAlg)    &   ⊢ 𝐸 = (RLReg‘𝐴)    &   ⊢ 𝐾 = (Scalar‘𝐴)    &   ⊢ (𝜑 → 𝐾 ∈ DivRing)    &   ⊢ (𝜑 → (dim‘𝐴) ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐸)    ⇒   ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝐵)
Theorem	assarrginv 33687	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 33688	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 33689	Syntax for the field extension relation.
class /FldExt
Syntax	cfinext 33690	Syntax for the finite field extension relation.
class /FinExt
Syntax	calgext 33691	Syntax for the algebraic field extension relation.
class /AlgExt
Syntax	cextdg 33692	Syntax for the field extension degree operation.
class [:]
Definition	df-fldext 33693*	Definition of the field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ /FldExt = {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒 ↾s (Base‘𝑓)) ∧ (Base‘𝑓) ∈ (SubRing‘𝑒)))}
Definition	df-extdg 33694*	Definition of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ [:] = (𝑒 ∈ V, 𝑓 ∈ (/FldExt “ {𝑒}) ↦ (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓))))
Definition	df-finext 33695*	Definition of the finite field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ /FinExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)}
Definition	df-algext 33696*	Definition of the algebraic extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ /AlgExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ ∀𝑥 ∈ (Base‘𝑒)∃𝑝 ∈ (Poly1‘𝑓)(((eval1‘𝑓)‘𝑝)‘𝑥) = (0g‘𝑒))}
Theorem	relfldext 33697	The field extension is a relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ Rel /FldExt
Theorem	brfldext 33698	The field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ Field) → (𝐸/FldExt𝐹 ↔ (𝐹 = (𝐸 ↾s (Base‘𝐹)) ∧ (Base‘𝐹) ∈ (SubRing‘𝐸))))
Theorem	ccfldextrr 33699	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 33700	A field extension is only defined if the extension is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → 𝐸 ∈ Field)