P. 311 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31001-31100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dimval 31001	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 31002	The dimension of a vector space 𝐹 is the cardinality of one of its bases. This version of dimval 31001 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 31003	Closure of the vector space dimension. (Contributed by Thierry Arnoux, 18-May-2023.)
⊢ (𝑉 ∈ LVec → (dim‘𝑉) ∈ ℕ0*)
Theorem	lvecdim0i 31004	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 31005	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 31006	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 31007*	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	rgmoddim 31008	The left vector space induced by a ring over itself has dimension 1. (Contributed by Thierry Arnoux, 5-Aug-2023.)
⊢ 𝑉 = (ringLMod‘𝐹)    ⇒   ⊢ (𝐹 ∈ Field → (dim‘𝑉) = 1)
Theorem	frlmdim 31009	Dimension of a free left module. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝐹 = (𝑅 freeLMod 𝐼)    ⇒   ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉) → (dim‘𝐹) = (♯‘𝐼))
Theorem	tnglvec 31010	Augmenting a structure with a norm conserves left vector spaces. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 ∈ LVec ↔ 𝑇 ∈ LVec))
Theorem	tngdim 31011	Dimension of a left vector space augmented with a norm. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁)    ⇒   ⊢ ((𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉) → (dim‘𝐺) = (dim‘𝑇))
Theorem	rrxdim 31012	Dimension of the generalized Euclidean space. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝐻 = (ℝ^‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → (dim‘𝐻) = (♯‘𝐼))
Theorem	matdim 31013	Dimension of the space of square matrices. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝐴 = (𝐼 Mat 𝑅)    &   ⊢ 𝑁 = (♯‘𝐼)    ⇒   ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → (dim‘𝐴) = (𝑁 · 𝑁))
Theorem	lbslsat 31014	A nonzero vector 𝑋 is a basis of a line spanned by the singleton 𝑋. Spans of nonzero singletons are sometimes called "atoms", see df-lsatoms 36127 and for example lsatlspsn 36144. (Contributed by Thierry Arnoux, 20-May-2023.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ 𝑌 = (𝑊 ↾s (𝑁‘{𝑋}))    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → {𝑋} ∈ (LBasis‘𝑌))
Theorem	lsatdim 31015	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 31016	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 31017	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 31018	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 31019	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	lindsunlem 31020	Lemma for lindsun 31021. (Contributed by Thierry Arnoux, 9-May-2023.)
⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝑈 ∈ (LIndS‘𝑊))    &   ⊢ (𝜑 → 𝑉 ∈ (LIndS‘𝑊))    &   ⊢ (𝜑 → ((𝑁‘𝑈) ∩ (𝑁‘𝑉)) = { 0 })    &   ⊢ 𝑂 = (0g‘(Scalar‘𝑊))    &   ⊢ 𝐹 = (Base‘(Scalar‘𝑊))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐾 ∈ (𝐹 ∖ {𝑂}))    &   ⊢ (𝜑 → (𝐾( ·𝑠 ‘𝑊)𝐶) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝐶})))    ⇒   ⊢ (𝜑 → ⊥)
Theorem	lindsun 31021	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 31022	The linear spans of two disjunct independent sets only have a trivial intersection. This can be seen as the opposite direction of lindsun 31021. (Contributed by Thierry Arnoux, 17-May-2023.)
⊢ 𝐽 = (LBasis‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ∧ 𝑉 ⊆ 𝐵) → ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉)) = { 0 })
Theorem	dimkerim 31023	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 31024	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 31025*	Lemma for fedgmul 31027 (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 31026*	Lemma for fedgmul 31027 (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 31027	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‘𝐶)))
20.3.10  Field Extensions
Syntax	cfldext 31028	Syntax for the field extension relation.
class /FldExt
Syntax	cfinext 31029	Syntax for the finite field extension relation.
class /FinExt
Syntax	calgext 31030	Syntax for the algebraic field extension relation.
class /AlgExt
Syntax	cextdg 31031	Syntax for the field extension degree operation.
class [:]
Definition	df-fldext 31032*	Definition of the field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ /FldExt = {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒 ↾s (Base‘𝑓)) ∧ (Base‘𝑓) ∈ (SubRing‘𝑒)))}
Definition	df-extdg 31033*	Definition of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ [:] = (𝑒 ∈ V, 𝑓 ∈ (/FldExt “ {𝑒}) ↦ (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓))))
Definition	df-finext 31034*	Definition of the finite field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ /FinExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)}
Definition	df-algext 31035*	Definition of the algebraic extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ /AlgExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ ∀𝑥 ∈ (Base‘𝑒)∃𝑝 ∈ (Poly1‘𝑓)(((eval1‘𝑓)‘𝑝)‘𝑥) = (0g‘𝑒))}
Theorem	relfldext 31036	The field extension is a relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ Rel /FldExt
Theorem	brfldext 31037	The field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ Field) → (𝐸/FldExt𝐹 ↔ (𝐹 = (𝐸 ↾s (Base‘𝐹)) ∧ (Base‘𝐹) ∈ (SubRing‘𝐸))))
Theorem	ccfldextrr 31038	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 31039	A field extension is only defined if the extension is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → 𝐸 ∈ Field)
Theorem	fldextfld2 31040	A field extension is only defined if the subfield is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → 𝐹 ∈ Field)
Theorem	fldextsubrg 31041	Field extension implies a subring relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ 𝑈 = (Base‘𝐹)    ⇒   ⊢ (𝐸/FldExt𝐹 → 𝑈 ∈ (SubRing‘𝐸))
Theorem	fldextress 31042	Field extension implies a structure restriction relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → 𝐹 = (𝐸 ↾s (Base‘𝐹)))
Theorem	brfinext 31043	The finite field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → (𝐸/FinExt𝐹 ↔ (𝐸[:]𝐹) ∈ ℕ0))
Theorem	extdgval 31044	Value of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) = (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
Theorem	fldextsralvec 31045	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 31046	Closure of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) ∈ ℕ0*)
Theorem	extdggt0 31047	Degrees of field extension are greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023.)
⊢ (𝐸/FldExt𝐹 → 0 < (𝐸[:]𝐹))
Theorem	fldexttr 31048	Field extension is a transitive relation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
⊢ ((𝐸/FldExt𝐹 ∧ 𝐹/FldExt𝐾) → 𝐸/FldExt𝐾)
Theorem	fldextid 31049	The field extension relation is reflexive. (Contributed by Thierry Arnoux, 30-Jul-2023.)
⊢ (𝐹 ∈ Field → 𝐹/FldExt𝐹)
Theorem	extdgid 31050	A trivial field extension has degree one. (Contributed by Thierry Arnoux, 4-Aug-2023.)
⊢ (𝐸 ∈ Field → (𝐸[:]𝐸) = 1)
Theorem	extdgmul 31051	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 31052	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 31053	If the degree of the extension 𝐸/FldExt𝐹 is 1, then 𝐸 and 𝐹 are identical. (Contributed by Thierry Arnoux, 6-Aug-2023.)
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → 𝐸 = 𝐹)
Theorem	extdg1b 31054	The degree of the extension 𝐸/FldExt𝐹 is 1 iff 𝐸 and 𝐹 are the same structure. (Contributed by Thierry Arnoux, 6-Aug-2023.)
⊢ (𝐸/FldExt𝐹 → ((𝐸[:]𝐹) = 1 ↔ 𝐸 = 𝐹))
Theorem	fldextchr 31055	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	ccfldsrarelvec 31056	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 31057	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
20.3.11  Matrices
20.3.11.1  Submatrices
Syntax	csmat 31058	Syntax for a function generating submatrices.
class subMat1
Definition	df-smat 31059*	Define a function generating submatrices of an integer-indexed matrix. The function maps an index in ((1...𝑀) × (1...𝑁)) into a new index in ((1...(𝑀 − 1)) × (1...(𝑁 − 1))). A submatrix is obtained by deleting a row and a column of the original matrix. Because this function re-indexes the matrix, the resulting submatrix still has the same index set for rows and columns, and its determinent is defined, unlike the current df-subma 21186. (Contributed by Thierry Arnoux, 18-Aug-2020.)
⊢ subMat1 = (𝑚 ∈ V ↦ (𝑘 ∈ ℕ, 𝑙 ∈ ℕ ↦ (𝑚 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩))))
Theorem	smatfval 31060*	Value of the submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ ((𝐾 ∈ ℕ ∧ 𝐿 ∈ ℕ ∧ 𝑀 ∈ 𝑉) → (𝐾(subMat1‘𝑀)𝐿) = (𝑀 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩)))
Theorem	smatrcl 31061	Closure of the rectangular submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))))    ⇒   ⊢ (𝜑 → 𝑆 ∈ (𝐵 ↑m ((1...(𝑀 − 1)) × (1...(𝑁 − 1)))))
Theorem	smatlem 31062	Lemma for the next theorems. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))))    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐽 ∈ ℕ)    &   ⊢ (𝜑 → if(𝐼 < 𝐾, 𝐼, (𝐼 + 1)) = 𝑋)    &   ⊢ (𝜑 → if(𝐽 < 𝐿, 𝐽, (𝐽 + 1)) = 𝑌)    ⇒   ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝑋𝐴𝑌))
Theorem	smattl 31063	Entries of a submatrix, top left. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))))    &   ⊢ (𝜑 → 𝐼 ∈ (1..^𝐾))    &   ⊢ (𝜑 → 𝐽 ∈ (1..^𝐿))    ⇒   ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝐼𝐴𝐽))
Theorem	smattr 31064	Entries of a submatrix, top right. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))))    &   ⊢ (𝜑 → 𝐼 ∈ (𝐾...𝑀))    &   ⊢ (𝜑 → 𝐽 ∈ (1..^𝐿))    ⇒   ⊢ (𝜑 → (𝐼𝑆𝐽) = ((𝐼 + 1)𝐴𝐽))
Theorem	smatbl 31065	Entries of a submatrix, bottom left. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))))    &   ⊢ (𝜑 → 𝐼 ∈ (1..^𝐾))    &   ⊢ (𝜑 → 𝐽 ∈ (𝐿...𝑁))    ⇒   ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝐼𝐴(𝐽 + 1)))
Theorem	smatbr 31066	Entries of a submatrix, bottom right. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑀))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁))))    &   ⊢ (𝜑 → 𝐼 ∈ (𝐾...𝑀))    &   ⊢ (𝜑 → 𝐽 ∈ (𝐿...𝑁))    ⇒   ⊢ (𝜑 → (𝐼𝑆𝐽) = ((𝐼 + 1)𝐴(𝐽 + 1)))
Theorem	smatcl 31067	Closure of the square submatrix: if 𝑀 is a square matrix of dimension 𝑁 with indices in (1...𝑁), then a submatrix of 𝑀 is of dimension (𝑁 − 1). (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝐴 = ((1...𝑁) Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐶 = (Base‘((1...(𝑁 − 1)) Mat 𝑅))    &   ⊢ 𝑆 = (𝐾(subMat1‘𝑀)𝐿)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑆 ∈ 𝐶)
Theorem	matmpo 31068*	Write a square matrix as a mapping operation. (Contributed by Thierry Arnoux, 16-Aug-2020.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ (𝑀 ∈ 𝐵 → 𝑀 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖𝑀𝑗)))
Theorem	1smat1 31069	The submatrix of the identity matrix obtained by removing the ith row and the ith column is an identity matrix. Cf. 1marepvsma1 21192. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 1 = (1r‘((1...𝑁) Mat 𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ (1...𝑁))    ⇒   ⊢ (𝜑 → (𝐼(subMat1‘ 1 )𝐼) = (1r‘((1...(𝑁 − 1)) Mat 𝑅)))
Theorem	submat1n 31070	One case where the submatrix with integer indices, subMat1, and the general submatrix subMat, agree. (Contributed by Thierry Arnoux, 22-Aug-2020.)
⊢ 𝐴 = ((1...𝑁) Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) → (𝑁(subMat1‘𝑀)𝑁) = (𝑁(((1...𝑁) subMat 𝑅)‘𝑀)𝑁))
Theorem	submatres 31071	Special case where the submatrix is a restriction of the initial matrix, and no renumbering occurs. (Contributed by Thierry Arnoux, 26-Aug-2020.)
⊢ 𝐴 = ((1...𝑁) Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) → (𝑁(subMat1‘𝑀)𝑁) = (𝑀 ↾ ((1...(𝑁 − 1)) × (1...(𝑁 − 1)))))
Theorem	submateqlem1 31072	Lemma for submateq 31074. (Contributed by Thierry Arnoux, 25-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1)))    &   ⊢ (𝜑 → 𝐾 ≤ 𝑀)    ⇒   ⊢ (𝜑 → (𝑀 ∈ (𝐾...𝑁) ∧ (𝑀 + 1) ∈ ((1...𝑁) ∖ {𝐾})))
Theorem	submateqlem2 31073	Lemma for submateq 31074. (Contributed by Thierry Arnoux, 26-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1)))    &   ⊢ (𝜑 → 𝑀 < 𝐾)    ⇒   ⊢ (𝜑 → (𝑀 ∈ (1..^𝐾) ∧ 𝑀 ∈ ((1...𝑁) ∖ {𝐾})))
Theorem	submateq 31074*	Sufficient condition for two submatrices to be equal. (Contributed by Thierry Arnoux, 25-Aug-2020.)
⊢ 𝐴 = ((1...𝑁) Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐽 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐸 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝐽})) → (𝑖𝐸𝑗) = (𝑖𝐹𝑗))    ⇒   ⊢ (𝜑 → (𝐼(subMat1‘𝐸)𝐽) = (𝐼(subMat1‘𝐹)𝐽))
Theorem	submatminr1 31075	If we take a submatrix by removing the row 𝐼 and column 𝐽, then the result is the same on the matrix with row 𝐼 and column 𝐽 modified by the minMatR1 operator. (Contributed by Thierry Arnoux, 25-Aug-2020.)
⊢ 𝐴 = ((1...𝑁) Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐽 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    &   ⊢ 𝐸 = (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)    ⇒   ⊢ (𝜑 → (𝐼(subMat1‘𝑀)𝐽) = (𝐼(subMat1‘𝐸)𝐽))
20.3.11.2  Matrix literals
Syntax	clmat 31076	Extend class notation with the literal matrix conversion function.
class litMat
Definition	df-lmat 31077*	Define a function converting words of words into matrices. (Contributed by Thierry Arnoux, 28-Aug-2020.)
⊢ litMat = (𝑚 ∈ V ↦ (𝑖 ∈ (1...(♯‘𝑚)), 𝑗 ∈ (1...(♯‘(𝑚‘0))) ↦ ((𝑚‘(𝑖 − 1))‘(𝑗 − 1))))
Theorem	lmatval 31078*	Value of the literal matrix conversion function. (Contributed by Thierry Arnoux, 28-Aug-2020.)
⊢ (𝑀 ∈ 𝑉 → (litMat‘𝑀) = (𝑖 ∈ (1...(♯‘𝑀)), 𝑗 ∈ (1...(♯‘(𝑀‘0))) ↦ ((𝑀‘(𝑖 − 1))‘(𝑗 − 1))))
Theorem	lmatfval 31079*	Entries of a literal matrix. (Contributed by Thierry Arnoux, 28-Aug-2020.)
⊢ 𝑀 = (litMat‘𝑊)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑊 ∈ Word Word 𝑉)    &   ⊢ (𝜑 → (♯‘𝑊) = 𝑁)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (♯‘(𝑊‘𝑖)) = 𝑁)    &   ⊢ (𝜑 → 𝐼 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐽 ∈ (1...𝑁))    ⇒   ⊢ (𝜑 → (𝐼𝑀𝐽) = ((𝑊‘(𝐼 − 1))‘(𝐽 − 1)))
Theorem	lmatfvlem 31080*	Useful lemma to extract literal matrix entries. Suggested by Mario Carneiro. (Contributed by Thierry Arnoux, 3-Sep-2020.)
⊢ 𝑀 = (litMat‘𝑊)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑊 ∈ Word Word 𝑉)    &   ⊢ (𝜑 → (♯‘𝑊) = 𝑁)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (♯‘(𝑊‘𝑖)) = 𝑁)    &   ⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝐿 ∈ ℕ0    &   ⊢ 𝐼 ≤ 𝑁    &   ⊢ 𝐽 ≤ 𝑁    &   ⊢ (𝐾 + 1) = 𝐼    &   ⊢ (𝐿 + 1) = 𝐽    &   ⊢ (𝑊‘𝐾) = 𝑋    &   ⊢ (𝜑 → (𝑋‘𝐿) = 𝑌)    ⇒   ⊢ (𝜑 → (𝐼𝑀𝐽) = 𝑌)
Theorem	lmatcl 31081*	Closure of the literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.)
⊢ 𝑀 = (litMat‘𝑊)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑊 ∈ Word Word 𝑉)    &   ⊢ (𝜑 → (♯‘𝑊) = 𝑁)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (♯‘(𝑊‘𝑖)) = 𝑁)    &   ⊢ 𝑉 = (Base‘𝑅)    &   ⊢ 𝑂 = ((1...𝑁) Mat 𝑅)    &   ⊢ 𝑃 = (Base‘𝑂)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝑀 ∈ 𝑃)
Theorem	lmat22lem 31082*	Lemma for lmat22e11 31083 and co. (Contributed by Thierry Arnoux, 28-Aug-2020.)
⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^2)) → (♯‘(⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩‘𝑖)) = 2)
Theorem	lmat22e11 31083	Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 28-Aug-2020.)
⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (1𝑀1) = 𝐴)
Theorem	lmat22e12 31084	Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.)
⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (1𝑀2) = 𝐵)
Theorem	lmat22e21 31085	Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.)
⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (2𝑀1) = 𝐶)
Theorem	lmat22e22 31086	Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.)
⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (2𝑀2) = 𝐷)
Theorem	lmat22det 31087	The determinant of a literal 2x2 complex matrix. (Contributed by Thierry Arnoux, 1-Sep-2020.)
⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ · = (.r‘𝑅)    &   ⊢ − = (-g‘𝑅)    &   ⊢ 𝑉 = (Base‘𝑅)    &   ⊢ 𝐽 = ((1...2) maDet 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → (𝐽‘𝑀) = ((𝐴 · 𝐷) − (𝐶 · 𝐵)))
20.3.11.3  Laplace expansion of determinants
Theorem	mdetpmtr1 31088*	The determinant of a matrix with permuted rows is the determinant of the original matrix multiplied by the sign of the permutation. (Contributed by Thierry Arnoux, 22-Aug-2020.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐺 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ 𝑍 = (ℤRHom‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀𝑗))    ⇒   ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝐷‘𝐸)))
Theorem	mdetpmtr2 31089*	The determinant of a matrix with permuted columns is the determinant of the original matrix multiplied by the sign of the permutation. (Contributed by Thierry Arnoux, 22-Aug-2020.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐺 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ 𝑍 = (ℤRHom‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖𝑀(𝑃‘𝑗)))    ⇒   ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝐷‘𝐸)))
Theorem	mdetpmtr12 31090*	The determinant of a matrix with permuted rows and columns is the determinant of the original matrix multiplied by the product of the signs of the permutations. (Contributed by Thierry Arnoux, 22-Aug-2020.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐺 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ 𝑍 = (ℤRHom‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀(𝑄‘𝑗)))    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑃 ∈ 𝐺)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐺)    ⇒   ⊢ (𝜑 → (𝐷‘𝑀) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐷‘𝐸)))
Theorem	mdetlap1 31091*	A Laplace expansion of the determinant of a matrix, using the adjunct (cofactor) matrix. (Contributed by Thierry Arnoux, 16-Aug-2020.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐾 = (𝑁 maAdju 𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁) → (𝐷‘𝑀) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝐼𝑀𝑗) · (𝑗(𝐾‘𝑀)𝐼)))))
Theorem	madjusmdetlem1 31092*	Lemma for madjusmdet 31096. (Contributed by Thierry Arnoux, 22-Aug-2020.)
⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐴 = ((1...𝑁) Mat 𝑅)    &   ⊢ 𝐷 = ((1...𝑁) maDet 𝑅)    &   ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑍 = (ℤRHom‘𝑅)    &   ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐼 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐽 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    &   ⊢ 𝐺 = (Base‘(SymGrp‘(1...𝑁)))    &   ⊢ 𝑆 = (pmSgn‘(1...𝑁))    &   ⊢ 𝑈 = (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)    &   ⊢ 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)𝑈(𝑄‘𝑗)))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐺)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐺)    &   ⊢ (𝜑 → (𝑃‘𝑁) = 𝐼)    &   ⊢ (𝜑 → (𝑄‘𝑁) = 𝐽)    &   ⊢ (𝜑 → (𝐼(subMat1‘𝑈)𝐽) = (𝑁(subMat1‘𝑊)𝑁))    ⇒   ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))
Theorem	madjusmdetlem2 31093*	Lemma for madjusmdet 31096. (Contributed by Thierry Arnoux, 26-Aug-2020.)
⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐴 = ((1...𝑁) Mat 𝑅)    &   ⊢ 𝐷 = ((1...𝑁) maDet 𝑅)    &   ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑍 = (ℤRHom‘𝑅)    &   ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐼 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐽 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    &   ⊢ 𝑃 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖)))    &   ⊢ 𝑆 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝑁, if(𝑖 ≤ 𝑁, (𝑖 − 1), 𝑖)))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)) = ((𝑃 ∘ ◡𝑆)‘𝑋))
Theorem	madjusmdetlem3 31094*	Lemma for madjusmdet 31096. (Contributed by Thierry Arnoux, 27-Aug-2020.)
⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐴 = ((1...𝑁) Mat 𝑅)    &   ⊢ 𝐷 = ((1...𝑁) maDet 𝑅)    &   ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑍 = (ℤRHom‘𝑅)    &   ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐼 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐽 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    &   ⊢ 𝑃 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖)))    &   ⊢ 𝑆 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝑁, if(𝑖 ≤ 𝑁, (𝑖 − 1), 𝑖)))    &   ⊢ 𝑄 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝐽, if(𝑗 ≤ 𝐽, (𝑗 − 1), 𝑗)))    &   ⊢ 𝑇 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝑁, if(𝑗 ≤ 𝑁, (𝑗 − 1), 𝑗)))    &   ⊢ 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ (((𝑃 ∘ ◡𝑆)‘𝑖)𝑈((𝑄 ∘ ◡𝑇)‘𝑗)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼(subMat1‘𝑈)𝐽) = (𝑁(subMat1‘𝑊)𝑁))
Theorem	madjusmdetlem4 31095*	Lemma for madjusmdet 31096. (Contributed by Thierry Arnoux, 22-Aug-2020.)
⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐴 = ((1...𝑁) Mat 𝑅)    &   ⊢ 𝐷 = ((1...𝑁) maDet 𝑅)    &   ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑍 = (ℤRHom‘𝑅)    &   ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐼 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐽 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    &   ⊢ 𝑃 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖)))    &   ⊢ 𝑆 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝑁, if(𝑖 ≤ 𝑁, (𝑖 − 1), 𝑖)))    &   ⊢ 𝑄 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝐽, if(𝑗 ≤ 𝐽, (𝑗 − 1), 𝑗)))    &   ⊢ 𝑇 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝑁, if(𝑗 ≤ 𝑁, (𝑗 − 1), 𝑗)))    ⇒   ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘(-1↑(𝐼 + 𝐽))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))
Theorem	madjusmdet 31096	Express the cofactor of the matrix, i.e. the entries of its adjunct matrix, using determinant of submatrices. (Contributed by Thierry Arnoux, 23-Aug-2020.)
⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐴 = ((1...𝑁) Mat 𝑅)    &   ⊢ 𝐷 = ((1...𝑁) maDet 𝑅)    &   ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑍 = (ℤRHom‘𝑅)    &   ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐼 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐽 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘(-1↑(𝐼 + 𝐽))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))
Theorem	mdetlap 31097*	Laplace expansion of the determinant of a square matrix. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐴 = ((1...𝑁) Mat 𝑅)    &   ⊢ 𝐷 = ((1...𝑁) maDet 𝑅)    &   ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑍 = (ℤRHom‘𝑅)    &   ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐼 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐽 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐷‘𝑀) = (𝑅 Σg (𝑗 ∈ (1...𝑁) ↦ ((𝑍‘(-1↑(𝐼 + 𝑗))) · ((𝐼𝑀𝑗) · (𝐸‘(𝐼(subMat1‘𝑀)𝑗)))))))
20.3.12  Topology
20.3.12.1  Open maps
Theorem	txomap 31098*	Given two open maps 𝐹 and 𝐺, 𝐻 mapping pairs of sets, is also an open map for the product topology. (Contributed by Thierry Arnoux, 29-Dec-2019.)
⊢ (𝜑 → 𝐹:𝑋⟶𝑍)    &   ⊢ (𝜑 → 𝐺:𝑌⟶𝑇)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍))    &   ⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑇))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ 𝐿)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 “ 𝑦) ∈ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐽 ×t 𝐾))    &   ⊢ 𝐻 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩)    ⇒   ⊢ (𝜑 → (𝐻 “ 𝐴) ∈ (𝐿 ×t 𝑀))
20.3.12.2  Topology of the unit circle
Theorem	qtopt1 31099*	If every equivalence class is closed, then the quotient space is T1 . (Contributed by Thierry Arnoux, 5-Jan-2020.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐽 ∈ Fre)    &   ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (◡𝐹 “ {𝑥}) ∈ (Clsd‘𝐽))    ⇒   ⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ Fre)
Theorem	qtophaus 31100*	If an open map's graph in the product space (𝐽 ×t 𝐽) is closed, then its quotient topology is Hausdorff. (Contributed by Thierry Arnoux, 4-Jan-2020.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ ∼ = (◡𝐹 ∘ 𝐹)    &   ⊢ 𝐻 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)    &   ⊢ (𝜑 → 𝐽 ∈ Haus)    &   ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹))    &   ⊢ (𝜑 → ∼ ∈ (Clsd‘(𝐽 ×t 𝐽)))    ⇒   ⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ Haus)