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	matdim 33601	Dimension of the space of square matrices. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝐴 = (𝐼 Mat 𝑅)    &   ⊢ 𝑁 = (♯‘𝐼)    ⇒   ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → (dim‘𝐴) = (𝑁 · 𝑁))
Theorem	lbslsat 33602	A nonzero vector 𝑋 is a basis of a line spanned by the singleton 𝑋. Spans of nonzero singletons are sometimes called "atoms", see df-lsatoms 38940 and for example lsatlspsn 38957. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑌 = (𝑊 ↾s (𝑁‘{𝑋}))    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → {𝑋} ∈ (LBasis‘𝑌))
Theorem	lsatdim 33603	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 33604	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 33605	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 33606	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 33607	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 33608*	Lemma for ply1degltdim 33609. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑅 ∈ DivRing)    &   ⊢ 𝐸 = (𝑃 ↾s 𝑆)    &   ⊢ 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)))    ⇒   ⊢ (𝜑 → ran 𝐹 ∈ (LBasis‘𝐸))
Theorem	ply1degltdim 33609	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 33610	Lemma for lindsun 33611. (Contributed by Thierry Arnoux, 9-May-2023.)
⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ (LIndS‘𝑊))    &   ⊢ (𝜑 → 𝑉 ∈ (LIndS‘𝑊))    &   ⊢ (𝜑 → ((𝑁‘𝑈) ∩ (𝑁‘𝑉)) = { 0 })    &   ⊢ 𝑂 = (0g‘(Scalar‘𝑊))    &   ⊢ 𝐹 = (Base‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐾 ∈ (𝐹 ∖ {𝑂}))    &   ⊢ (𝜑 → (𝐾( ·𝑠 ‘𝑊)𝐶) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝐶})))    ⇒   ⊢ (𝜑 → ⊥)
Theorem	lindsun 33611	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 33612	The linear spans of two disjunct independent sets only have a trivial intersection. This can be seen as the opposite direction of lindsun 33611. (Contributed by Thierry Arnoux, 17-May-2023.)
⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ∧ 𝑉 ⊆ 𝐵) → ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉)) = { 0 })
Theorem	dimkerim 33613	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 33614	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 33615*	Lemma for fedgmul 33617. (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 33616*	Lemma for fedgmul 33617. (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 33617	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 33618	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 33619	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 33620*	In an associative algebra 𝐴, left-multiplication by a fixed element of the algebra is a module homomorphism, analogous to ringlghm 20270. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = (.r‘𝐴)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐶 · 𝑥))    &   ⊢ (𝜑 → 𝐴 ∈ AssAlg)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐴 LMHom 𝐴))
Theorem	assalactf1o 33621*	In an associative algebra 𝐴, left-multiplication by a fixed element of the algebra is bijective. See also lactlmhm 33620. (Contributed by Thierry Arnoux, 3-Aug-2025.)
⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = (.r‘𝐴)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐶 · 𝑥))    &   ⊢ (𝜑 → 𝐴 ∈ AssAlg)    &   ⊢ 𝐸 = (RLReg‘𝐴)    &   ⊢ 𝐾 = (Scalar‘𝐴)    &   ⊢ (𝜑 → 𝐾 ∈ DivRing)    &   ⊢ (𝜑 → (dim‘𝐴) ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐸)    ⇒   ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝐵)
Theorem	assarrginv 33622	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 33623	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 33624	Syntax for the field extension relation.
class /FldExt
Syntax	cfinext 33625	Syntax for the finite field extension relation.
class /FinExt
Syntax	calgext 33626	Syntax for the algebraic field extension relation.
class /AlgExt
Syntax	cextdg 33627	Syntax for the field extension degree operation.
class [:]
Definition	df-fldext 33628*	Definition of the field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ /FldExt = {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒 ↾s (Base‘𝑓)) ∧ (Base‘𝑓) ∈ (SubRing‘𝑒)))}
Definition	df-extdg 33629*	Definition of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ [:] = (𝑒 ∈ V, 𝑓 ∈ (/FldExt “ {𝑒}) ↦ (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓))))
Definition	df-finext 33630*	Definition of the finite field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ /FinExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)}
Definition	df-algext 33631*	Definition of the algebraic extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ /AlgExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ ∀𝑥 ∈ (Base‘𝑒)∃𝑝 ∈ (Poly1‘𝑓)(((eval1‘𝑓)‘𝑝)‘𝑥) = (0g‘𝑒))}
Theorem	relfldext 33632	The field extension is a relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ Rel /FldExt
Theorem	brfldext 33633	The field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ Field) → (𝐸/FldExt𝐹 ↔ (𝐹 = (𝐸 ↾s (Base‘𝐹)) ∧ (Base‘𝐹) ∈ (SubRing‘𝐸))))
Theorem	ccfldextrr 33634	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 33635	A field extension is only defined if the extension is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → 𝐸 ∈ Field)
Theorem	fldextfld2 33636	A field extension is only defined if the subfield is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → 𝐹 ∈ Field)
Theorem	fldextsubrg 33637	Field extension implies a subring relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ 𝑈 = (Base‘𝐹)    ⇒   ⊢ (𝐸/FldExt𝐹 → 𝑈 ∈ (SubRing‘𝐸))
Theorem	sdrgfldext 33638	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 33639	Field extension implies a structure restriction relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → 𝐹 = (𝐸 ↾s (Base‘𝐹)))
Theorem	brfinext 33640	The finite field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → (𝐸/FinExt𝐹 ↔ (𝐸[:]𝐹) ∈ ℕ0))
Theorem	extdgval 33641	Value of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) = (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
Theorem	fldextsdrg 33642	Deduce sub-division-ring from field extension. (Contributed by Thierry Arnoux, 26-Oct-2025.)
⊢ 𝐵 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝐸/FldExt𝐹)    ⇒   ⊢ (𝜑 → 𝐵 ∈ (SubDRing‘𝐸))
Theorem	fldextsralvec 33643	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 33644	Closure of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) ∈ ℕ0*)
Theorem	extdggt0 33645	Degrees of field extension are greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → 0 < (𝐸[:]𝐹))
Theorem	fldexttr 33646	Field extension is a transitive relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ ((𝐸/FldExt𝐹 ∧ 𝐹/FldExt𝐾) → 𝐸/FldExt𝐾)
Theorem	fldextid 33647	The field extension relation is reflexive. (Contributed by Thierry Arnoux, 30-Jul-2023.)
⊢ (𝐹 ∈ Field → 𝐹/FldExt𝐹)
Theorem	extdgid 33648	A trivial field extension has degree one. (Contributed by Thierry Arnoux, 4-Aug-2023.)
⊢ (𝐸 ∈ Field → (𝐸[:]𝐸) = 1)
Theorem	fldsdrgfldext 33649	A sub-division-ring of a field forms a field extension. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ 𝐺 = (𝐹 ↾s 𝐴)    &   ⊢ (𝜑 → 𝐹 ∈ Field)    &   ⊢ (𝜑 → 𝐴 ∈ (SubDRing‘𝐹))    ⇒   ⊢ (𝜑 → 𝐹/FldExt𝐺)
Theorem	fldsdrgfldext2 33650	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 33651	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	finexttrb 33652	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 33653	If the degree of the extension 𝐸/FldExt𝐹 is 1, then 𝐸 and 𝐹 are identical. (Contributed by Thierry Arnoux, 6-Aug-2023.)
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → 𝐸 = 𝐹)
Theorem	extdg1b 33654	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 33655	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 33656	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 33657	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 33658	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 33659	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 33660*	Lemma for fldextrspunlsp 33661: 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 33661	Lemma for fldextrspunfld 33663. 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 33662	Lemma for fldextrspunfld 33663. 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 33663	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 33664	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 33665	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 33666	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 33667	Lemma for fldextrspundgdvds 33668. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ 𝐾 = (𝐿 ↾s 𝐹)    &   ⊢ 𝐼 = (𝐿 ↾s 𝐺)    &   ⊢ 𝐽 = (𝐿 ↾s 𝐻)    &   ⊢ (𝜑 → 𝐿 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼))    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿))    &   ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0)    &   ⊢ 𝐸 = (𝐿 ↾s (𝐿 fldGen (𝐺 ∪ 𝐻)))    &   ⊢ (𝜑 → (𝐼[:]𝐾) ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐸[:]𝐼) ∈ ℕ0)
Theorem	fldextrspundgdvds 33668	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 33669*	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 33670	Integral subring of a ring.
class IntgRing
Definition	df-irng 33671*	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 33672*	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 33673*	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 33674	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 33676). (Contributed by Thierry Arnoux, 28-Jan-2025.)
⊢ 𝑂 = (𝑅 evalSub1 𝑆)    &   ⊢ 𝑈 = (𝑅 ↾s 𝑆)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ NzRing)    ⇒   ⊢ (𝜑 → 𝑆 ⊆ (𝑅 IntgRing 𝑆))
Theorem	irngssv 33675	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 33676	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 33677	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 33678*	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 }))
21.3.11.2  Minimal polynomials
Syntax	cminply 33679	Extend class notation with the minimal polynomial builder function.
class minPoly
Definition	df-minply 33680*	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 33681*	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 33682*	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 33683*	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 33684*	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 33685*	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 33684, 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 33686*	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 33687*	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 33688	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 33689	The minimal polynomial for 𝐴 annihilates 𝐴 (Contributed by Thierry Arnoux, 25-Apr-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    ⇒   ⊢ (𝜑 → ((𝑂‘(𝑀‘𝐴))‘𝐴) = 0 )
Theorem	minplyirredlem 33690	Lemma for minplyirred 33691. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍)    &   ⊢ (𝜑 → 𝐺 ∈ (Base‘𝑃))    &   ⊢ (𝜑 → 𝐻 ∈ (Base‘𝑃))    &   ⊢ (𝜑 → (𝐺(.r‘𝑃)𝐻) = (𝑀‘𝐴))    &   ⊢ (𝜑 → ((𝑂‘𝐺)‘𝐴) = (0g‘𝐸))    &   ⊢ (𝜑 → 𝐺 ≠ 𝑍)    &   ⊢ (𝜑 → 𝐻 ≠ 𝑍)    ⇒   ⊢ (𝜑 → 𝐻 ∈ (Unit‘𝑃))
Theorem	minplyirred 33691	A nonzero minimal polynomial is irreducible. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ∈ (Irred‘𝑃))
Theorem	irngnminplynz 33692	Integral elements have nonzero minimal polynomials. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 𝑍 = (0g‘(Poly1‘𝐸))    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍)
Theorem	minplym1p 33693	A minimal polynomial is monic. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝑍 = (0g‘(Poly1‘𝐸))    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    &   ⊢ 𝑈 = (Monic1p‘(𝐸 ↾s 𝐹))    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ∈ 𝑈)
Theorem	minplynzm1p 33694	If a minimal polynomial is nonzero, then it is monic. (Contributed by Thierry Arnoux, 26-Oct-2025.)
⊢ 𝐵 = (Base‘𝐸)    &   ⊢ 𝑍 = (0g‘(Poly1‘𝐸))    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍)    &   ⊢ 𝑈 = (Monic1p‘(𝐸 ↾s 𝐹))    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ∈ 𝑈)
Theorem	minplyelirng 33695	If the minimial polynomial 𝐹 of an element 𝑋 of a field 𝑅 has nonnegative degree, then 𝑋 is integral. (Contributed by Thierry Arnoux, 26-Oct-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑀 = (𝑅 minPoly 𝑆)    &   ⊢ 𝐷 = (deg1‘(𝑅 ↾s 𝑆))    &   ⊢ (𝜑 → 𝑅 ∈ Field)    &   ⊢ (𝜑 → 𝑆 ∈ (SubDRing‘𝑅))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐷‘(𝑀‘𝐴)) ∈ ℕ0)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝑅 IntgRing 𝑆))
Theorem	irredminply 33696	An irreducible, monic, annihilating polynomial is the minimal polynomial. (Contributed by Thierry Arnoux, 27-Apr-2025.)
⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))    &   ⊢ 𝐵 = (Base‘𝐸)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ 0 = (0g‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ 𝑍 = (0g‘𝑃)    &   ⊢ (𝜑 → ((𝑂‘𝐺)‘𝐴) = 0 )    &   ⊢ (𝜑 → 𝐺 ∈ (Irred‘𝑃))    &   ⊢ (𝜑 → 𝐺 ∈ (Monic1p‘(𝐸 ↾s 𝐹)))    ⇒   ⊢ (𝜑 → 𝐺 = (𝑀‘𝐴))
Theorem	algextdeglem1 33697	Lemma for algextdeg 33705. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐾 = (𝐸 ↾s 𝐹)    &   ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))    &   ⊢ 𝐷 = (deg1‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    ⇒   ⊢ (𝜑 → (𝐿 ↾s 𝐹) = 𝐾)
Theorem	algextdeglem2 33698*	Lemma for algextdeg 33705. Both the ring of polynomials 𝑃 and the field 𝐿 generated by 𝐾 and the algebraic element 𝐴 can be considered as modules over the elements of 𝐹. Then, the evaluation map 𝐺, mapping polynomials to their evaluation at 𝐴, is a module homomorphism between those modules. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐾 = (𝐸 ↾s 𝐹)    &   ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))    &   ⊢ 𝐷 = (deg1‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    &   ⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘𝐾)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴))    &   ⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~QG 𝑍))    &   ⊢ 𝑍 = (◡𝐺 “ {(0g‘𝐿)})    &   ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍))    &   ⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝑃 LMHom ((subringAlg ‘𝐿)‘𝐹)))
Theorem	algextdeglem3 33699*	Lemma for algextdeg 33705. The quotient 𝑃 / 𝑍 of the vector space 𝑃 of polynomials by the subspace 𝑍 of polynomials annihilating 𝐴 is itself a vector space. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐾 = (𝐸 ↾s 𝐹)    &   ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))    &   ⊢ 𝐷 = (deg1‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    &   ⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘𝐾)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴))    &   ⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~QG 𝑍))    &   ⊢ 𝑍 = (◡𝐺 “ {(0g‘𝐿)})    &   ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍))    &   ⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝))    ⇒   ⊢ (𝜑 → 𝑄 ∈ LVec)
Theorem	algextdeglem4 33700*	Lemma for algextdeg 33705. By lmhmqusker 33378, the surjective module homomorphism 𝐺 described in algextdeglem2 33698 induces an isomorphism with the quotient space. Therefore, the dimension of that quotient space 𝑃 / 𝑍 is the degree of the algebraic field extension. (Contributed by Thierry Arnoux, 2-Apr-2025.)
⊢ 𝐾 = (𝐸 ↾s 𝐹)    &   ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))    &   ⊢ 𝐷 = (deg1‘𝐸)    &   ⊢ 𝑀 = (𝐸 minPoly 𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ Field)    &   ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))    &   ⊢ 𝑂 = (𝐸 evalSub1 𝐹)    &   ⊢ 𝑃 = (Poly1‘𝐾)    &   ⊢ 𝑈 = (Base‘𝑃)    &   ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴))    &   ⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~QG 𝑍))    &   ⊢ 𝑍 = (◡𝐺 “ {(0g‘𝐿)})    &   ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍))    &   ⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝))    ⇒   ⊢ (𝜑 → (dim‘𝑄) = (𝐿[:]𝐾))