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	rlmdim 33801	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 33802	Dimension of a free left module. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝐹 = (𝑅 freeLMod 𝐼)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉) → (dim‘𝐹) = (♯‘𝐼))
Theorem	tnglvec 33803	Augmenting a structure with a norm conserves left vector spaces. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 ∈ LVec ↔ 𝑇 ∈ LVec))
Theorem	tngdim 33804	Dimension of a left vector space augmented with a norm. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    ⇒   ⊢ ((𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉) → (dim‘𝐺) = (dim‘𝑇))
Theorem	rrxdim 33805	Dimension of the generalized Euclidean space. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝐻 = (ℝ^‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → (dim‘𝐻) = (♯‘𝐼))
Theorem	matdim 33806	Dimension of the space of square matrices. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝐴 = (𝐼 Mat 𝑅)    &   ⊢ 𝑁 = (♯‘𝐼)    ⇒   ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → (dim‘𝐴) = (𝑁 · 𝑁))
Theorem	lbslsat 33807	A nonzero vector 𝑋 is a basis of a line spanned by the singleton 𝑋. Spans of nonzero singletons are sometimes called "atoms", see df-lsatoms 39475 and for example lsatlspsn 39492. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑌 = (𝑊 ↾s (𝑁‘{𝑋}))    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → {𝑋} ∈ (LBasis‘𝑌))
Theorem	lsatdim 33808	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 33809	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 33810	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 33811	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 33812	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 33813*	Lemma for ply1degltdim 33814. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ 𝐸 = (𝑃 ↾s 𝑆)    &   ⊢ 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)))    ⇒   ⊢ (𝜑 → ran 𝐹 ∈ (LBasis‘𝐸))
Theorem	ply1degltdim 33814	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 33815	Lemma for lindsun 33816. (Contributed by Thierry Arnoux, 9-May-2023.)
⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ (LIndS‘𝑊))    &   ⊢ (𝜑 → 𝑉 ∈ (LIndS‘𝑊))    &   ⊢ (𝜑 → ((𝑁‘𝑈) ∩ (𝑁‘𝑉)) = { 0 })    &   ⊢ 𝑂 = (0g‘(Scalar‘𝑊))    &   ⊢ 𝐹 = (Base‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐾 ∈ (𝐹 ∖ {𝑂}))    &   ⊢ (𝜑 → (𝐾( ·𝑠 ‘𝑊)𝐶) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝐶})))    ⇒   ⊢ (𝜑 → ⊥)
Theorem	lindsun 33816	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 33817	The linear spans of two disjunct independent sets only have a trivial intersection. This can be seen as the opposite direction of lindsun 33816. (Contributed by Thierry Arnoux, 17-May-2023.)
⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ∧ 𝑉 ⊆ 𝐵) → ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉)) = { 0 })
Theorem	dimkerim 33818	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 33819	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 33820*	Lemma for fedgmul 33822. (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 33821*	Lemma for fedgmul 33822. (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 33822	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 33823	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 33824	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 33825*	In an associative algebra 𝐴, left-multiplication by a fixed element of the algebra is a module homomorphism, analogous to ringlghm 20291. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = (.r‘𝐴)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐶 · 𝑥))    &   ⊢ (𝜑 → 𝐴 ∈ AssAlg)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐴 LMHom 𝐴))
Theorem	assalactf1o 33826*	In an associative algebra 𝐴, left-multiplication by a fixed element of the algebra is bijective. See also lactlmhm 33825. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = (.r‘𝐴)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐶 · 𝑥))    &   ⊢ (𝜑 → 𝐴 ∈ AssAlg)    &   ⊢ 𝐸 = (RLReg‘𝐴)    &   ⊢ 𝐾 = (Scalar‘𝐴)    &   ⊢ (𝜑 → 𝐾 ∈ DivRing)    &   ⊢ (𝜑 → (dim‘𝐴) ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐸)    ⇒   ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝐵)
Theorem	assarrginv 33827	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 33828	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 33829	Syntax for the field extension relation.
class /FldExt
Syntax	cfinext 33830	Syntax for the finite field extension relation.
class /FinExt
Syntax	cextdg 33831	Syntax for the field extension degree operation.
class [:]
Definition	df-fldext 33832*	Definition of the field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ /FldExt = {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒 ↾s (Base‘𝑓)) ∧ (Base‘𝑓) ∈ (SubRing‘𝑒)))}
Definition	df-extdg 33833*	Definition of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ [:] = (𝑒 ∈ V, 𝑓 ∈ (/FldExt “ {𝑒}) ↦ (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓))))
Definition	df-finext 33834*	Definition of the finite field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ /FinExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)}
Theorem	relfldext 33835	The field extension is a relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ Rel /FldExt
Theorem	brfldext 33836	The field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ Field) → (𝐸/FldExt𝐹 ↔ (𝐹 = (𝐸 ↾s (Base‘𝐹)) ∧ (Base‘𝐹) ∈ (SubRing‘𝐸))))
Theorem	ccfldextrr 33837	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 33838	A field extension is only defined if the extension is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → 𝐸 ∈ Field)
Theorem	fldextfld2 33839	A field extension is only defined if the subfield is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → 𝐹 ∈ Field)
Theorem	fldextsubrg 33840	Field extension implies a subring relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ 𝑈 = (Base‘𝐹)    ⇒   ⊢ (𝐸/FldExt𝐹 → 𝑈 ∈ (SubRing‘𝐸))
Theorem	sdrgfldext 33841	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 33842	Field extension implies a structure restriction relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → 𝐹 = (𝐸 ↾s (Base‘𝐹)))
Theorem	brfinext 33843	The finite field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → (𝐸/FinExt𝐹 ↔ (𝐸[:]𝐹) ∈ ℕ0))
Theorem	extdgval 33844	Value of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) = (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
Theorem	fldextsdrg 33845	Deduce sub-division-ring from field extension. (Contributed by Thierry Arnoux, 26-Oct-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐸/FldExt𝐹)    ⇒   ⊢ (𝜑 → 𝐵 ∈ (SubDRing‘𝐸))
Theorem	fldextsralvec 33846	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 33847	Closure of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) ∈ ℕ0*)
Theorem	extdggt0 33848	Degrees of field extension are greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → 0 < (𝐸[:]𝐹))
Theorem	fldexttr 33849	Field extension is a transitive relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ ((𝐸/FldExt𝐹 ∧ 𝐹/FldExt𝐾) → 𝐸/FldExt𝐾)
Theorem	fldextid 33850	The field extension relation is reflexive. (Contributed by Thierry Arnoux, 30-Jul-2023.)
⊢ (𝐹 ∈ Field → 𝐹/FldExt𝐹)
Theorem	extdgid 33851	A trivial field extension has degree one. (Contributed by Thierry Arnoux, 4-Aug-2023.)
⊢ (𝐸 ∈ Field → (𝐸[:]𝐸) = 1)
Theorem	fldsdrgfldext 33852	A sub-division-ring of a field forms a field extension. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ 𝐺 = (𝐹 ↾s 𝐴)    &   ⊢ (𝜑 → 𝐹 ∈ Field)    &   ⊢ (𝜑 → 𝐴 ∈ (SubDRing‘𝐹))    ⇒   ⊢ (𝜑 → 𝐹/FldExt𝐺)
Theorem	fldsdrgfldext2 33853	A sub-sub-division-ring of a field forms a field extension. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ 𝐺 = (𝐹 ↾s 𝐴)    &   ⊢ (𝜑 → 𝐹 ∈ Field)    &   ⊢ (𝜑 → 𝐴 ∈ (SubDRing‘𝐹))    &   ⊢ (𝜑 → 𝐵 ∈ (SubDRing‘𝐺))    &   ⊢ 𝐻 = (𝐹 ↾s 𝐵)    ⇒   ⊢ (𝜑 → 𝐺/FldExt𝐻)
Theorem	extdgmul 33854	The multiplicativity formula for degrees of field extensions. Given 𝐸 a field extension of 𝐹, itself a field extension of 𝐾, the degree of the extension 𝐸/FldExt𝐾 is the product of the degrees of the extensions 𝐸/FldExt𝐹 and 𝐹/FldExt𝐾. Proposition 1.2 of [Lang], p. 224. (Contributed by Thierry Arnoux, 30-Jul-2023.)
⊢ ((𝐸/FldExt𝐹 ∧ 𝐹/FldExt𝐾) → (𝐸[:]𝐾) = ((𝐸[:]𝐹) ·e (𝐹[:]𝐾)))
Theorem	finextfldext 33855	A finite field extension is a field extension. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ (𝜑 → 𝐸/FinExt𝐹)    ⇒   ⊢ (𝜑 → 𝐸/FldExt𝐹)
Theorem	finexttrb 33856	The extension 𝐸 of 𝐾 is finite if and only if 𝐸 is finite over 𝐹 and 𝐹 is finite over 𝐾. Corollary 1.3 of [Lang] , p. 225. (Contributed by Thierry Arnoux, 30-Jul-2023.)
⊢ ((𝐸/FldExt𝐹 ∧ 𝐹/FldExt𝐾) → (𝐸/FinExt𝐾 ↔ (𝐸/FinExt𝐹 ∧ 𝐹/FinExt𝐾)))
Theorem	extdg1id 33857	If the degree of the extension 𝐸/FldExt𝐹 is 1, then 𝐸 and 𝐹 are identical. (Contributed by Thierry Arnoux, 6-Aug-2023.)
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → 𝐸 = 𝐹)
Theorem	extdg1b 33858	The degree of the extension 𝐸/FldExt𝐹 is 1 iff 𝐸 and 𝐹 are the same structure. (Contributed by Thierry Arnoux, 6-Aug-2023.)
⊢ (𝐸/FldExt𝐹 → ((𝐸[:]𝐹) = 1 ↔ 𝐸 = 𝐹))
Theorem	fldgenfldext 33859	A subfield 𝐹 extended with a set 𝐴 forms a field extension. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐾 = (𝐸 ↾s 𝐹)    &   ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ 𝐴)))    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝐿/FldExt𝐾)
Theorem	fldextchr 33860	The characteristic of a subfield is the same as the characteristic of the larger field. (Contributed by Thierry Arnoux, 20-Aug-2023.)
⊢ (𝐸/FldExt𝐹 → (chr‘𝐹) = (chr‘𝐸))
Theorem	evls1fldgencl 33861	Closure of the subring polynomial evaluation in the field extention. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝑂‘𝐺)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
Theorem	ccfldsrarelvec 33862	The subring algebra of the complex numbers over the real numbers is a left vector space. (Contributed by Thierry Arnoux, 20-Aug-2023.)
⊢ ((subringAlg ‘ℂfld)‘ℝ) ∈ LVec
Theorem	ccfldextdgrr 33863	The degree of the field extension of the complex numbers over the real numbers is 2. (Suggested by GL, 4-Aug-2023.) (Contributed by Thierry Arnoux, 20-Aug-2023.)
⊢ (ℂfld[:]ℝfld) = 2
Theorem	fldextrspunlsplem 33864*	Lemma for fldextrspunlsp 33865: First direction. Part of the proof of Proposition 5, Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ 𝐾 = (𝐿 ↾s 𝐹)    &   ⊢ 𝐼 = (𝐿 ↾s 𝐺)    &   ⊢ 𝐽 = (𝐿 ↾s 𝐻)    &   ⊢ (𝜑 → 𝐿 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))    &   ⊢ 𝑁 = (RingSpan‘𝐿)    &   ⊢ 𝐶 = (𝑁‘(𝐺 ∪ 𝐻))    &   ⊢ 𝐸 = (𝐿 ↾s 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝑃:𝐻⟶𝐺)    &   ⊢ (𝜑 → 𝑃 finSupp (0g‘𝐿))    &   ⊢ (𝜑 → 𝑋 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓))))    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏)))))
Theorem	fldextrspunlsp 33865	Lemma for fldextrspunfld 33867. The subring generated by the union of two field extensions 𝐺 and 𝐻 is the vector sub- 𝐺 space generated by a basis 𝐵 of 𝐻. Part of the proof of Proposition 5, Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ 𝐾 = (𝐿 ↾s 𝐹)    &   ⊢ 𝐼 = (𝐿 ↾s 𝐺)    &   ⊢ 𝐽 = (𝐿 ↾s 𝐻)    &   ⊢ (𝜑 → 𝐿 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))    &   ⊢ 𝑁 = (RingSpan‘𝐿)    &   ⊢ 𝐶 = (𝑁‘(𝐺 ∪ 𝐻))    &   ⊢ 𝐸 = (𝐿 ↾s 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹)))    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝐶 = ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝐵))
Theorem	fldextrspunlem1 33866	Lemma for fldextrspunfld 33867. Part of the proof of Proposition 5, Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ 𝐾 = (𝐿 ↾s 𝐹)    &   ⊢ 𝐼 = (𝐿 ↾s 𝐺)    &   ⊢ 𝐽 = (𝐿 ↾s 𝐻)    &   ⊢ (𝜑 → 𝐿 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0)    &   ⊢ 𝑁 = (RingSpan‘𝐿)    &   ⊢ 𝐶 = (𝑁‘(𝐺 ∪ 𝐻))    &   ⊢ 𝐸 = (𝐿 ↾s 𝐶)    ⇒   ⊢ (𝜑 → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (𝐽[:]𝐾))
Theorem	fldextrspunfld 33867	The ring generated by the union of two field extensions is a field. Part of the proof of Proposition 5, Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ 𝐾 = (𝐿 ↾s 𝐹)    &   ⊢ 𝐼 = (𝐿 ↾s 𝐺)    &   ⊢ 𝐽 = (𝐿 ↾s 𝐻)    &   ⊢ (𝜑 → 𝐿 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0)    &   ⊢ 𝑁 = (RingSpan‘𝐿)    &   ⊢ 𝐶 = (𝑁‘(𝐺 ∪ 𝐻))    &   ⊢ 𝐸 = (𝐿 ↾s 𝐶)    ⇒   ⊢ (𝜑 → 𝐸 ∈ Field)
Theorem	fldextrspunlem2 33868	Part of the proof of Proposition 5, Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ 𝐾 = (𝐿 ↾s 𝐹)    &   ⊢ 𝐼 = (𝐿 ↾s 𝐺)    &   ⊢ 𝐽 = (𝐿 ↾s 𝐻)    &   ⊢ (𝜑 → 𝐿 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0)    &   ⊢ 𝑁 = (RingSpan‘𝐿)    &   ⊢ 𝐶 = (𝑁‘(𝐺 ∪ 𝐻))    &   ⊢ 𝐸 = (𝐿 ↾s 𝐶)    ⇒   ⊢ (𝜑 → 𝐶 = (𝐿 fldGen (𝐺 ∪ 𝐻)))
Theorem	fldextrspundgle 33869	Inequality involving the degree of two different field extensions 𝐼 and 𝐽 of a same field 𝐹. Part of the proof of Proposition 5, Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ 𝐾 = (𝐿 ↾s 𝐹)    &   ⊢ 𝐼 = (𝐿 ↾s 𝐺)    &   ⊢ 𝐽 = (𝐿 ↾s 𝐻)    &   ⊢ (𝜑 → 𝐿 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0)    &   ⊢ 𝐸 = (𝐿 ↾s (𝐿 fldGen (𝐺 ∪ 𝐻)))    ⇒   ⊢ (𝜑 → (𝐸[:]𝐼) ≤ (𝐽[:]𝐾))
Theorem	fldextrspundglemul 33870	Given two field extensions 𝐼 / 𝐾 and 𝐽 / 𝐾 of the same field 𝐾, 𝐽 / 𝐾 being finite, and the composiste field 𝐸 = 𝐼𝐽, the degree of the extension of the composite field 𝐸 / 𝐾 is at most the product of the field extension degrees of 𝐼 / 𝐾 and 𝐽 / 𝐾. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ 𝐾 = (𝐿 ↾s 𝐹)    &   ⊢ 𝐼 = (𝐿 ↾s 𝐺)    &   ⊢ 𝐽 = (𝐿 ↾s 𝐻)    &   ⊢ (𝜑 → 𝐿 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0)    &   ⊢ 𝐸 = (𝐿 ↾s (𝐿 fldGen (𝐺 ∪ 𝐻)))    ⇒   ⊢ (𝜑 → (𝐸[:]𝐾) ≤ ((𝐼[:]𝐾) ·e (𝐽[:]𝐾)))
Theorem	fldextrspundgdvdslem 33871	Lemma for fldextrspundgdvds 33872. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ 𝐾 = (𝐿 ↾s 𝐹)    &   ⊢ 𝐼 = (𝐿 ↾s 𝐺)    &   ⊢ 𝐽 = (𝐿 ↾s 𝐻)    &   ⊢ (𝜑 → 𝐿 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0)    &   ⊢ 𝐸 = (𝐿 ↾s (𝐿 fldGen (𝐺 ∪ 𝐻)))    &   ⊢ (𝜑 → (𝐼[:]𝐾) ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐸[:]𝐼) ∈ ℕ0)
Theorem	fldextrspundgdvds 33872	Given two finite extensions 𝐼 / 𝐾 and 𝐽 / 𝐾 of the same field 𝐾, the degree of the extension 𝐼 / 𝐾 divides the degree of the extension 𝐸 / 𝐾, 𝐸 being the composite field 𝐼𝐽. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ 𝐾 = (𝐿 ↾s 𝐹)    &   ⊢ 𝐼 = (𝐿 ↾s 𝐺)    &   ⊢ 𝐽 = (𝐿 ↾s 𝐻)    &   ⊢ (𝜑 → 𝐿 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0)    &   ⊢ 𝐸 = (𝐿 ↾s (𝐿 fldGen (𝐺 ∪ 𝐻)))    &   ⊢ (𝜑 → (𝐼[:]𝐾) ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐼[:]𝐾) ∥ (𝐸[:]𝐾))
Theorem	fldext2rspun 33873*	Given two field extensions 𝐼 / 𝐾 and 𝐽 / 𝐾, 𝐼 / 𝐾 being a quadratic extension, and the degree of 𝐽 / 𝐾 being a power of 2, the degree of the extension 𝐸 / 𝐾 is a power of 2 , 𝐸 being the composite field 𝐼𝐽. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ 𝐾 = (𝐿 ↾s 𝐹)    &   ⊢ 𝐼 = (𝐿 ↾s 𝐺)    &   ⊢ 𝐽 = (𝐿 ↾s 𝐻)    &   ⊢ (𝜑 → 𝐿 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → (𝐼[:]𝐾) = 2)    &   ⊢ (𝜑 → (𝐽[:]𝐾) = (2↑𝑁))    &   ⊢ 𝐸 = (𝐿 ↾s (𝐿 fldGen (𝐺 ∪ 𝐻)))    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ℕ0 (𝐸[:]𝐾) = (2↑𝑛))
21.3.11.1  Algebraic numbers
Syntax	cirng 33874	Integral subring of a ring.
class IntgRing
Definition	df-irng 33875*	Define the subring of elements of a ring 𝑟 integral over a subset 𝑠. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Thierry Arnoux, 28-Jan-2025.)
⊢ IntgRing = (𝑟 ∈ V, 𝑠 ∈ V ↦ ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡((𝑟 evalSub1 𝑠)‘𝑓) “ {(0g‘𝑟)}))
Theorem	irngval 33876*	The elements of a field 𝑅 integral over a subset 𝑆. In the case of a subfield, those are the algebraic numbers over the field 𝑆 within the field 𝑅. That is, the numbers 𝑋 which are roots of monic polynomials 𝑃(𝑋) with coefficients in 𝑆. (Contributed by Thierry Arnoux, 28-Jan-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑈 = (𝑅 ↾s 𝑆)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑅 IntgRing 𝑆) = ∪ 𝑓 ∈ (Monic1p‘𝑈)(◡(𝑂‘𝑓) “ { 0 }))
Theorem	elirng 33877*	Property for an element 𝑋 of a field 𝑅 to be integral over a subring 𝑆. (Contributed by Thierry Arnoux, 28-Jan-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑈 = (𝑅 ↾s 𝑆)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝑅 IntgRing 𝑆) ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑓 ∈ (Monic1p‘𝑈)((𝑂‘𝑓)‘𝑋) = 0 )))
Theorem	irngss 33878	All elements of a subring 𝑆 are integral over 𝑆. This is only true in the case of a nonzero ring, since there are no integral elements in a zero ring (see 0ringirng 33880). (Contributed by Thierry Arnoux, 28-Jan-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑈 = (𝑅 ↾s 𝑆)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    ⇒   ⊢ (𝜑 → 𝑆 ⊆ (𝑅 IntgRing 𝑆))
Theorem	irngssv 33879	An integral element is an element of the base set. (Contributed by Thierry Arnoux, 28-Jan-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑈 = (𝑅 ↾s 𝑆)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    ⇒   ⊢ (𝜑 → (𝑅 IntgRing 𝑆) ⊆ 𝐵)
Theorem	0ringirng 33880	A zero ring 𝑅 has no integral elements. (Contributed by Thierry Arnoux, 5-Feb-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑈 = (𝑅 ↾s 𝑆)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → ¬ 𝑅 ∈ NzRing)    ⇒   ⊢ (𝜑 → (𝑅 IntgRing 𝑆) = ∅)
Theorem	irngnzply1lem 33881	In the case of a field 𝐸, a root 𝑋 of some nonzero polynomial 𝑃 with coefficients in a subfield 𝐹 is integral over 𝐹. (Contributed by Thierry Arnoux, 5-Feb-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑍 = (0g‘(Poly1‘𝐸))    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝑃 ∈ dom 𝑂)    &   ⊢ (𝜑 → 𝑃 ≠ 𝑍)    &   ⊢ (𝜑 → ((𝑂‘𝑃)‘𝑋) = 0 )    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐸 IntgRing 𝐹))
Theorem	irngnzply1 33882*	In the case of a field 𝐸, the roots of nonzero polynomials 𝑝 with coefficients in a subfield 𝐹 are exactly the integral elements over 𝐹. Roots of nonzero polynomials are called algebraic numbers, so this shows that in the case of a field, elements integral over 𝐹 are exactly the algebraic numbers. In this formula, dom 𝑂 represents the polynomials, and 𝑍 the zero polynomial. (Contributed by Thierry Arnoux, 5-Feb-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑍 = (0g‘(Poly1‘𝐸))    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    ⇒   ⊢ (𝜑 → (𝐸 IntgRing 𝐹) = ∪ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 }))
Theorem	extdgfialglem1 33883*	Lemma for extdgfialg 33885. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐷 = (dim‘((subringAlg ‘𝐸)‘𝐹))    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    &   ⊢ 𝑍 = (0g‘𝐸)    &   ⊢ · = (.r‘𝐸)    &   ⊢ 𝐺 = (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ (𝐹 ↑m (0...𝐷))(𝑎 finSupp 𝑍 ∧ ((𝐸 Σg (𝑎 ∘f · 𝐺)) = 𝑍 ∧ 𝑎 ≠ ((0...𝐷) × {𝑍}))))
Theorem	extdgfialglem2 33884*	Lemma for extdgfialg 33885. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐷 = (dim‘((subringAlg ‘𝐸)‘𝐹))    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    &   ⊢ 𝑍 = (0g‘𝐸)    &   ⊢ · = (.r‘𝐸)    &   ⊢ 𝐺 = (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴:(0...𝐷)⟶𝐹)    &   ⊢ (𝜑 → 𝐴 finSupp 𝑍)    &   ⊢ (𝜑 → (𝐸 Σg (𝐴 ∘f · 𝐺)) = 𝑍)    &   ⊢ (𝜑 → 𝐴 ≠ ((0...𝐷) × {𝑍}))    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐸 IntgRing 𝐹))
Theorem	extdgfialg 33885	A finite field extension 𝐸 / 𝐹 is algebraic. Part of the proof of Proposition 1.1 of [Lang], p. 224. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐷 = (dim‘((subringAlg ‘𝐸)‘𝐹))    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐸 IntgRing 𝐹) = 𝐵)
21.3.11.2  Algebraic extensions
Syntax	calgext 33886	Syntax for the algebraic field extension relation.
class /AlgExt
Definition	df-algext 33887*	Definition of the algebraic extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ /AlgExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒 IntgRing (Base‘𝑓)) = (Base‘𝑒))}
Theorem	bralgext 33888	Express the fact that a field extension 𝐸 / 𝐹 is algebraic. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝐶 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐸/AlgExt𝐹 ↔ (𝐸/FldExt𝐹 ∧ (𝐸 IntgRing 𝐶) = 𝐵)))
Theorem	finextalg 33889	A finite field extension is algebraic. Proposition 1.1 of [Lang], p. 224. (Contributed by Thierry Arnoux, 10-Jan-2026.)
⊢ (𝜑 → 𝐸/FinExt𝐹)    ⇒   ⊢ (𝜑 → 𝐸/AlgExt𝐹)
21.3.11.3  Minimal polynomials
Syntax	cminply 33890	Extend class notation with the minimal polynomial builder function.
class minPoly
Definition	df-minply 33891*	Define the minimal polynomial builder function. (Contributed by Thierry Arnoux, 19-Jan-2025.)
⊢ minPoly = (𝑒 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑒) ↦ ((idlGen1p‘(𝑒 ↾s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g‘𝑒)})))
Theorem	ply1annidllem 33892*	Write the set 𝑄 of polynomials annihilating an element 𝐴 as the kernel of the ring homomorphism 𝐹 mapping polynomials 𝑝 to their subring evaluation at a given point 𝐴. (Contributed by Thierry Arnoux, 9-Feb-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 }    &   ⊢ 𝐹 = (𝑝 ∈ (Base‘𝑃) ↦ ((𝑂‘𝑝)‘𝐴))    ⇒   ⊢ (𝜑 → 𝑄 = (◡𝐹 “ { 0 }))
Theorem	ply1annidl 33893*	The set 𝑄 of polynomials annihilating an element 𝐴 forms an ideal. (Contributed by Thierry Arnoux, 9-Feb-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 }    ⇒   ⊢ (𝜑 → 𝑄 ∈ (LIdeal‘𝑃))
Theorem	ply1annnr 33894*	The set 𝑄 of polynomials annihilating an element 𝐴 is not the whole polynomial ring. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 }    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    ⇒   ⊢ (𝜑 → 𝑄 ≠ 𝑈)
Theorem	ply1annig1p 33895*	The ideal 𝑄 of polynomials annihilating an element 𝐴 is generated by the ideal's canonical generator. (Contributed by Thierry Arnoux, 9-Feb-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 }    &   ⊢ 𝐾 = (RSpan‘𝑃)    &   ⊢ 𝐺 = (idlGen1p‘(𝐸 ↾s 𝐹))    ⇒   ⊢ (𝜑 → 𝑄 = (𝐾‘{(𝐺‘𝑄)}))
Theorem	minplyval 33896*	Expand the value of the minimal polynomial (𝑀‘𝐴) for a given element 𝐴. It is defined as the unique monic polynomial of minimal degree which annihilates 𝐴. By ply1annig1p 33895, that polynomial generates the ideal of the annihilators of 𝐴. (Contributed by Thierry Arnoux, 9-Feb-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 }    &   ⊢ 𝐾 = (RSpan‘𝑃)    &   ⊢ 𝐺 = (idlGen1p‘(𝐸 ↾s 𝐹))    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) = (𝐺‘𝑄))
Theorem	minplycl 33897*	The minimal polynomial is a polynomial. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 }    &   ⊢ 𝐾 = (RSpan‘𝑃)    &   ⊢ 𝐺 = (idlGen1p‘(𝐸 ↾s 𝐹))    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ∈ (Base‘𝑃))
Theorem	ply1annprmidl 33898*	The set 𝑄 of polynomials annihilating an element 𝐴 is a prime ideal. (Contributed by Thierry Arnoux, 9-Feb-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 }    ⇒   ⊢ (𝜑 → 𝑄 ∈ (PrmIdeal‘𝑃))
Theorem	minplymindeg 33899	The minimal polynomial of 𝐴 is minimal among the nonzero annihilators of 𝐴 with regard to degree. (Contributed by Thierry Arnoux, 22-Jun-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ 𝐷 = (deg1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ (𝜑 → ((𝑂‘𝐻)‘𝐴) = 0 )    &   ⊢ (𝜑 → 𝐻 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐻 ≠ 𝑍)    ⇒   ⊢ (𝜑 → (𝐷‘(𝑀‘𝐴)) ≤ (𝐷‘𝐻))
Theorem	minplyann 33900	The minimal polynomial for 𝐴 annihilates 𝐴. (Contributed by Thierry Arnoux, 25-Apr-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    ⇒   ⊢ (𝜑 → ((𝑂‘(𝑀‘𝐴))‘𝐴) = 0 )