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	smatcl 33801	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 33802*	Write a square matrix as a mapping operation. (Contributed by Thierry Arnoux, 16-Aug-2020.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ (𝑀 ∈ 𝐵 → 𝑀 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖𝑀𝑗)))
Theorem	1smat1 33803	The submatrix of the identity matrix obtained by removing the ith row and the ith column is an identity matrix. Cf. 1marepvsma1 22589. (Contributed by Thierry Arnoux, 19-Aug-2020.)
⊢ 1 = (1r‘((1...𝑁) Mat 𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐼 ∈ (1...𝑁))    ⇒   ⊢ (𝜑 → (𝐼(subMat1‘ 1 )𝐼) = (1r‘((1...(𝑁 − 1)) Mat 𝑅)))
Theorem	submat1n 33804	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 33805	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 33806	Lemma for submateq 33808. (Contributed by Thierry Arnoux, 25-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1)))    &   ⊢ (𝜑 → 𝐾 ≤ 𝑀)    ⇒   ⊢ (𝜑 → (𝑀 ∈ (𝐾...𝑁) ∧ (𝑀 + 1) ∈ ((1...𝑁) ∖ {𝐾})))
Theorem	submateqlem2 33807	Lemma for submateq 33808. (Contributed by Thierry Arnoux, 26-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1)))    &   ⊢ (𝜑 → 𝑀 < 𝐾)    ⇒   ⊢ (𝜑 → (𝑀 ∈ (1..^𝐾) ∧ 𝑀 ∈ ((1...𝑁) ∖ {𝐾})))
Theorem	submateq 33808*	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 33809	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‘𝐸)𝐽))
21.3.13.2  Matrix literals
Syntax	clmat 33810	Extend class notation with the literal matrix conversion function.
class litMat
Definition	df-lmat 33811*	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 33812*	Value of the literal matrix conversion function. (Contributed by Thierry Arnoux, 28-Aug-2020.)
⊢ (𝑀 ∈ 𝑉 → (litMat‘𝑀) = (𝑖 ∈ (1...(♯‘𝑀)), 𝑗 ∈ (1...(♯‘(𝑀‘0))) ↦ ((𝑀‘(𝑖 − 1))‘(𝑗 − 1))))
Theorem	lmatfval 33813*	Entries of a literal matrix. (Contributed by Thierry Arnoux, 28-Aug-2020.)
⊢ 𝑀 = (litMat‘𝑊)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑊 ∈ Word Word 𝑉)    &   ⊢ (𝜑 → (♯‘𝑊) = 𝑁)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (♯‘(𝑊‘𝑖)) = 𝑁)    &   ⊢ (𝜑 → 𝐼 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐽 ∈ (1...𝑁))    ⇒   ⊢ (𝜑 → (𝐼𝑀𝐽) = ((𝑊‘(𝐼 − 1))‘(𝐽 − 1)))
Theorem	lmatfvlem 33814*	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 33815*	Closure of the literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.)
⊢ 𝑀 = (litMat‘𝑊)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑊 ∈ Word Word 𝑉)    &   ⊢ (𝜑 → (♯‘𝑊) = 𝑁)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (♯‘(𝑊‘𝑖)) = 𝑁)    &   ⊢ 𝑉 = (Base‘𝑅)    &   ⊢ 𝑂 = ((1...𝑁) Mat 𝑅)    &   ⊢ 𝑃 = (Base‘𝑂)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝑀 ∈ 𝑃)
Theorem	lmat22lem 33816*	Lemma for lmat22e11 33817 and co. (Contributed by Thierry Arnoux, 28-Aug-2020.)
⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^2)) → (♯‘(⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩‘𝑖)) = 2)
Theorem	lmat22e11 33817	Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 28-Aug-2020.)
⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (1𝑀1) = 𝐴)
Theorem	lmat22e12 33818	Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.)
⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (1𝑀2) = 𝐵)
Theorem	lmat22e21 33819	Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.)
⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (2𝑀1) = 𝐶)
Theorem	lmat22e22 33820	Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.)
⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (2𝑀2) = 𝐷)
Theorem	lmat22det 33821	The determinant of a literal 2x2 complex matrix. (Contributed by Thierry Arnoux, 1-Sep-2020.)
⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ · = (.r‘𝑅)    &   ⊢ − = (-g‘𝑅)    &   ⊢ 𝑉 = (Base‘𝑅)    &   ⊢ 𝐽 = ((1...2) maDet 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    ⇒   ⊢ (𝜑 → (𝐽‘𝑀) = ((𝐴 · 𝐷) − (𝐶 · 𝐵)))
21.3.13.3  Laplace expansion of determinants
Theorem	mdetpmtr1 33822*	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 33823*	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 33824*	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 33825*	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 33826*	Lemma for madjusmdet 33830. (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 33827*	Lemma for madjusmdet 33830. (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 33828*	Lemma for madjusmdet 33830. (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 33829*	Lemma for madjusmdet 33830. (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 33830	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 33831*	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‘𝑀)𝑗)))))))
21.3.14  Topology
Theorem	ist0cld 33832*	The predicate "is a T0 space", using closed sets. (Contributed by Thierry Arnoux, 16-Aug-2020.)
⊢ (𝜑 → 𝐵 = ∪ 𝐽)    &   ⊢ (𝜑 → 𝐷 = (Clsd‘𝐽))    ⇒   ⊢ (𝜑 → (𝐽 ∈ Kol2 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∀𝑑 ∈ 𝐷 (𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑) → 𝑥 = 𝑦))))
21.3.14.1  Open maps
Theorem	txomap 33833*	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 𝑀))
21.3.14.2  Topology of the unit circle
Theorem	qtopt1 33834*	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 33835*	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)
Theorem	circtopn 33836*	The topology of the unit circle is generated by open intervals of the polar coordinate. (Contributed by Thierry Arnoux, 4-Jan-2020.)
⊢ 𝐼 = (0[,](2 · π))    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (exp‘(i · 𝑥)))    &   ⊢ 𝐶 = (◡abs “ {1})    ⇒   ⊢ (𝐽 qTop 𝐹) = (TopOpen‘(𝐹 “s ℝfld))
Theorem	circcn 33837*	The function gluing the real line into the unit circle is continuous. (Contributed by Thierry Arnoux, 5-Jan-2020.)
⊢ 𝐼 = (0[,](2 · π))    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (exp‘(i · 𝑥)))    &   ⊢ 𝐶 = (◡abs “ {1})    ⇒   ⊢ 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹))
21.3.14.3  Refinements
Theorem	reff 33838*	For any cover refinement, there exists a function associating with each set in the refinement a set in the original cover containing it. This is sometimes used as a definition of refinement. Note that this definition uses the axiom of choice through ac6sg 10528. (Contributed by Thierry Arnoux, 12-Jan-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴Ref𝐵 ↔ (∪ 𝐵 ⊆ ∪ 𝐴 ∧ ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑣 ∈ 𝐴 𝑣 ⊆ (𝑓‘𝑣)))))
Theorem	locfinreflem 33839*	A locally finite refinement of an open cover induces a locally finite open cover with the original index set. This is fact 2 of http://at.yorku.ca/p/a/c/a/02.pdf, it is expressed by exposing a function 𝑓 from the original cover 𝑈, which is taken as the index set. The solution is constructed by building unions, so the same method can be used to prove a similar theorem about closed covers. (Contributed by Thierry Arnoux, 29-Jan-2020.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝑈)    &   ⊢ (𝜑 → 𝑉 ⊆ 𝐽)    &   ⊢ (𝜑 → 𝑉Ref𝑈)    &   ⊢ (𝜑 → 𝑉 ∈ (LocFin‘𝐽))    ⇒   ⊢ (𝜑 → ∃𝑓((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))))
Theorem	locfinref 33840*	A locally finite refinement of an open cover induces a locally finite open cover with the original index set. This is fact 2 of http://at.yorku.ca/p/a/c/a/02.pdf, it is expressed by exposing a function 𝑓 from the original cover 𝑈, which is taken as the index set. (Contributed by Thierry Arnoux, 31-Jan-2020.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝑈)    &   ⊢ (𝜑 → 𝑉 ⊆ 𝐽)    &   ⊢ (𝜑 → 𝑉Ref𝑈)    &   ⊢ (𝜑 → 𝑉 ∈ (LocFin‘𝐽))    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:𝑈⟶𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))
21.3.14.4  Open cover refinement property
Syntax	ccref 33841	The "every open cover has an 𝐴 refinement" predicate.
class CovHasRef𝐴
Definition	df-cref 33842*	Define a statement "every open cover has an 𝐴 refinement" , where 𝐴 is a property for refinements like "finite", "countable", "point finite" or "locally finite". (Contributed by Thierry Arnoux, 7-Jan-2020.)
⊢ CovHasRef𝐴 = {𝑗 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑗(∪ 𝑗 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑗 ∩ 𝐴)𝑧Ref𝑦)}
Theorem	iscref 33843*	The property that every open cover has an 𝐴 refinement for the topological space 𝐽. (Contributed by Thierry Arnoux, 7-Jan-2020.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ CovHasRef𝐴 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ 𝐴)𝑧Ref𝑦)))
Theorem	crefeq 33844	Equality theorem for the "every open cover has an A refinement" predicate. (Contributed by Thierry Arnoux, 7-Jan-2020.)
⊢ (𝐴 = 𝐵 → CovHasRef𝐴 = CovHasRef𝐵)
Theorem	creftop 33845	A space where every open cover has an 𝐴 refinement is a topological space. (Contributed by Thierry Arnoux, 7-Jan-2020.)
⊢ (𝐽 ∈ CovHasRef𝐴 → 𝐽 ∈ Top)
Theorem	crefi 33846*	The property that every open cover has an 𝐴 refinement for the topological space 𝐽. (Contributed by Thierry Arnoux, 7-Jan-2020.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ CovHasRef𝐴 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶) → ∃𝑧 ∈ (𝒫 𝐽 ∩ 𝐴)𝑧Ref𝐶)
Theorem	crefdf 33847*	A formulation of crefi 33846 easier to use for definitions. (Contributed by Thierry Arnoux, 7-Jan-2020.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐵 = CovHasRef𝐴    &   ⊢ (𝑧 ∈ 𝐴 → 𝜑)    ⇒   ⊢ ((𝐽 ∈ 𝐵 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶) → ∃𝑧 ∈ 𝒫 𝐽(𝜑 ∧ 𝑧Ref𝐶))
Theorem	crefss 33848	The "every open cover has an 𝐴 refinement" predicate respects inclusion. (Contributed by Thierry Arnoux, 7-Jan-2020.)
⊢ (𝐴 ⊆ 𝐵 → CovHasRef𝐴 ⊆ CovHasRef𝐵)
Theorem	cmpcref 33849	Equivalent definition of compact space in terms of open cover refinements. Compact spaces are topologies with finite open cover refinements. (Contributed by Thierry Arnoux, 7-Jan-2020.)
⊢ Comp = CovHasRefFin
Theorem	cmpfiref 33850*	Every open cover of a Compact space has a finite refinement. (Contributed by Thierry Arnoux, 1-Feb-2020.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Comp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈) → ∃𝑣 ∈ 𝒫 𝐽(𝑣 ∈ Fin ∧ 𝑣Ref𝑈))
21.3.14.5  Lindelöf spaces
Syntax	cldlf 33851	Extend class notation with the class of all Lindelöf spaces.
class Ldlf
Definition	df-ldlf 33852	Definition of a Lindelöf space. A Lindelöf space is a topological space in which every open cover has a countable subcover. Definition 1 of [BourbakiTop2] p. 195. (Contributed by Thierry Arnoux, 30-Jan-2020.)
⊢ Ldlf = CovHasRef{𝑥 ∣ 𝑥 ≼ ω}
Theorem	ldlfcntref 33853*	Every open cover of a Lindelöf space has a countable refinement. (Contributed by Thierry Arnoux, 1-Feb-2020.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Ldlf ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈) → ∃𝑣 ∈ 𝒫 𝐽(𝑣 ≼ ω ∧ 𝑣Ref𝑈))
21.3.14.6  Paracompact spaces
Syntax	cpcmp 33854	Extend class notation with the class of all paracompact topologies.
class Paracomp
Definition	df-pcmp 33855	Definition of a paracompact topology. A topology is said to be paracompact iff every open cover has an open refinement that is locally finite. The definition 6 of [BourbakiTop1] p. I.69. also requires the topology to be Hausdorff, but this is dropped here. (Contributed by Thierry Arnoux, 7-Jan-2020.)
⊢ Paracomp = {𝑗 ∣ 𝑗 ∈ CovHasRef(LocFin‘𝑗)}
Theorem	ispcmp 33856	The predicate "is a paracompact topology". (Contributed by Thierry Arnoux, 7-Jan-2020.)
⊢ (𝐽 ∈ Paracomp ↔ 𝐽 ∈ CovHasRef(LocFin‘𝐽))
Theorem	cmppcmp 33857	Every compact space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020.)
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Paracomp)
Theorem	dispcmp 33858	Every discrete space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020.)
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Paracomp)
Theorem	pcmplfin 33859*	Given a paracompact topology 𝐽 and an open cover 𝑈, there exists an open refinement 𝑣 that is locally finite. (Contributed by Thierry Arnoux, 31-Jan-2020.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈) → ∃𝑣 ∈ 𝒫 𝐽(𝑣 ∈ (LocFin‘𝐽) ∧ 𝑣Ref𝑈))
Theorem	pcmplfinf 33860*	Given a paracompact topology 𝐽 and an open cover 𝑈, there exists an open refinement ran 𝑓 that is locally finite, using the same index as the original cover 𝑈. (Contributed by Thierry Arnoux, 31-Jan-2020.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈) → ∃𝑓(𝑓:𝑈⟶𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))
21.3.14.7  Spectrum of a ring The prime ideals of a ring 𝑅 can be endowed with the Zariski topology. This is done by defining a function 𝑉 which maps ideals of 𝑅 to closed sets (see for example zarcls0 33867 for the definition of 𝑉). The closed sets of the topology are in the range of 𝑉 (see zartopon 33876). The correspondence with the open sets is made in zarcls 33873. As proved in zart0 33878, the Zariski topology is T0 , but generally not T1 .
Syntax	crspec 33861	Extend class notation with the spectrum of a ring.
class Spec
Definition	df-rspec 33862	Define the spectrum of a ring. (Contributed by Thierry Arnoux, 21-Jan-2024.)
⊢ Spec = (𝑟 ∈ Ring ↦ ((IDLsrg‘𝑟) ↾s (PrmIdeal‘𝑟)))
Theorem	rspecval 33863	Value of the spectrum of the ring 𝑅. Notation 1.1.1 of [EGA] p. 80. (Contributed by Thierry Arnoux, 2-Jun-2024.)
⊢ (𝑅 ∈ Ring → (Spec‘𝑅) = ((IDLsrg‘𝑅) ↾s (PrmIdeal‘𝑅)))
Theorem	rspecbas 33864	The prime ideals form the base of the spectrum of a ring. (Contributed by Thierry Arnoux, 2-Jun-2024.)
⊢ 𝑆 = (Spec‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (PrmIdeal‘𝑅) = (Base‘𝑆))
Theorem	rspectset 33865*	Topology component of the spectrum of a ring. (Contributed by Thierry Arnoux, 2-Jun-2024.)
⊢ 𝑆 = (Spec‘𝑅)    &   ⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝐽 = ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})    ⇒   ⊢ (𝑅 ∈ Ring → 𝐽 = (TopSet‘𝑆))
Theorem	rspectopn 33866*	The topology component of the spectrum of a ring. (Contributed by Thierry Arnoux, 4-Jun-2024.)
⊢ 𝑆 = (Spec‘𝑅)    &   ⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝑃 = (PrmIdeal‘𝑅)    &   ⊢ 𝐽 = ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗})    ⇒   ⊢ (𝑅 ∈ Ring → 𝐽 = (TopOpen‘𝑆))
Theorem	zarcls0 33867*	The closure of the identity ideal in the Zariski topology. Proposition 1.1.2(i) of [EGA] p. 80. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})    &   ⊢ 𝑃 = (PrmIdeal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝑉‘{ 0 }) = 𝑃)
Theorem	zarcls1 33868*	The unit ideal 𝐵 is the only ideal whose closure in the Zariski topology is the empty set. Stronger form of the Proposition 1.1.2(i) of [EGA] p. 80. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → ((𝑉‘𝐼) = ∅ ↔ 𝐼 = 𝐵))
Theorem	zarclsun 33869*	The union of two closed sets of the Zariski topology is closed. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ ran 𝑉 ∧ 𝑌 ∈ ran 𝑉) → (𝑋 ∪ 𝑌) ∈ ran 𝑉)
Theorem	zarclsiin 33870*	In a Zariski topology, the intersection of the closures of a family of ideals is the closure of the span of their union. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})    &   ⊢ 𝐾 = (RSpan‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙) = (𝑉‘(𝐾‘∪ 𝑇)))
Theorem	zarclsint 33871*	The intersection of a family of closed sets is closed in the Zariski topology. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ∧ 𝑆 ≠ ∅) → ∩ 𝑆 ∈ ran 𝑉)
Theorem	zarclssn 33872*	The closed points of Zariski topology are the maximal ideals. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})    &   ⊢ 𝐵 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ({𝑀} = (𝑉‘𝑀) ↔ 𝑀 ∈ (MaxIdeal‘𝑅)))
Theorem	zarcls 33873*	The open sets of the Zariski topology are the complements of the closed sets. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑆 = (Spec‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑆)    &   ⊢ 𝑃 = (PrmIdeal‘𝑅)    &   ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗})    ⇒   ⊢ (𝑅 ∈ Ring → 𝐽 = {𝑠 ∈ 𝒫 𝑃 ∣ (𝑃 ∖ 𝑠) ∈ ran 𝑉})
Theorem	zartopn 33874*	The Zariski topology is a topology, and its closed sets are images by 𝑉 of the ideals of 𝑅. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑆 = (Spec‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑆)    &   ⊢ 𝑃 = (PrmIdeal‘𝑅)    &   ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗})    ⇒   ⊢ (𝑅 ∈ CRing → (𝐽 ∈ (TopOn‘𝑃) ∧ ran 𝑉 = (Clsd‘𝐽)))
Theorem	zartop 33875	The Zariski topology is a topology. Proposition 1.1.2 of [EGA] p. 80. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑆 = (Spec‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑆)    ⇒   ⊢ (𝑅 ∈ CRing → 𝐽 ∈ Top)
Theorem	zartopon 33876	The points of the Zariski topology are the prime ideals. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑆 = (Spec‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑆)    &   ⊢ 𝑃 = (PrmIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝐽 ∈ (TopOn‘𝑃))
Theorem	zar0ring 33877	The Zariski Topology of the trivial ring. (Contributed by Thierry Arnoux, 1-Jul-2024.)
⊢ 𝑆 = (Spec‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (♯‘𝐵) = 1) → 𝐽 = {∅})
Theorem	zart0 33878	The Zariski topology is T0 . Corollary 1.1.8 of [EGA] p. 81. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑆 = (Spec‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑆)    ⇒   ⊢ (𝑅 ∈ CRing → 𝐽 ∈ Kol2)
Theorem	zarmxt1 33879	The Zariski topology restricted to maximal ideals is T1 . (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑆 = (Spec‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑆)    &   ⊢ 𝑀 = (MaxIdeal‘𝑅)    &   ⊢ 𝑇 = (𝐽 ↾t 𝑀)    ⇒   ⊢ (𝑅 ∈ CRing → 𝑇 ∈ Fre)
Theorem	zarcmplem 33880*	Lemma for zarcmp 33881. (Contributed by Thierry Arnoux, 2-Jul-2024.)
⊢ 𝑆 = (Spec‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑆)    &   ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})    ⇒   ⊢ (𝑅 ∈ CRing → 𝐽 ∈ Comp)
Theorem	zarcmp 33881	The Zariski topology is compact. Proposition 1.1.10(ii) of [EGA], p. 82. (Contributed by Thierry Arnoux, 2-Jul-2024.)
⊢ 𝑆 = (Spec‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑆)    ⇒   ⊢ (𝑅 ∈ CRing → 𝐽 ∈ Comp)
Theorem	rspectps 33882	The spectrum of a ring 𝑅 is a topological space. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑆 = (Spec‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝑆 ∈ TopSp)
Theorem	rhmpreimacnlem 33883*	Lemma for rhmpreimacn 33884. (Contributed by Thierry Arnoux, 7-Jul-2024.)
⊢ 𝑇 = (Spec‘𝑅)    &   ⊢ 𝑈 = (Spec‘𝑆)    &   ⊢ 𝐴 = (PrmIdeal‘𝑅)    &   ⊢ 𝐵 = (PrmIdeal‘𝑆)    &   ⊢ 𝐽 = (TopOpen‘𝑇)    &   ⊢ 𝐾 = (TopOpen‘𝑈)    &   ⊢ 𝐺 = (𝑖 ∈ 𝐵 ↦ (◡𝐹 “ 𝑖))    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → ran 𝐹 = (Base‘𝑆))    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))    &   ⊢ 𝑉 = (𝑗 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑗 ⊆ 𝑘})    &   ⊢ 𝑊 = (𝑗 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑗 ⊆ 𝑘})    ⇒   ⊢ (𝜑 → (𝑊‘(𝐹 “ 𝐼)) = (◡𝐺 “ (𝑉‘𝐼)))
Theorem	rhmpreimacn 33884*	The function mapping a prime ideal to its preimage by a surjective ring homomorphism is continuous, when considering the Zariski topology. Corollary 1.2.3 of [EGA], p. 83. Notice that the direction of the continuous map 𝐺 is reverse: the original ring homomorphism 𝐹 goes from 𝑅 to 𝑆, but the continuous map 𝐺 goes from 𝐵 to 𝐴. This mapping is also called "induced map on prime spectra" or "pullback on primes". (Contributed by Thierry Arnoux, 8-Jul-2024.)
⊢ 𝑇 = (Spec‘𝑅)    &   ⊢ 𝑈 = (Spec‘𝑆)    &   ⊢ 𝐴 = (PrmIdeal‘𝑅)    &   ⊢ 𝐵 = (PrmIdeal‘𝑆)    &   ⊢ 𝐽 = (TopOpen‘𝑇)    &   ⊢ 𝐾 = (TopOpen‘𝑈)    &   ⊢ 𝐺 = (𝑖 ∈ 𝐵 ↦ (◡𝐹 “ 𝑖))    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → ran 𝐹 = (Base‘𝑆))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽))
21.3.14.8  Pseudometrics
Syntax	cmetid 33885	Extend class notation with the class of metric identifications.
class ~Met
Syntax	cpstm 33886	Extend class notation with the metric induced by a pseudometric.
class pstoMet
Definition	df-metid 33887*	Define the metric identification relation for a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ ~Met = (𝑑 ∈ ∪ ran PsMet ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)})
Definition	df-pstm 33888*	Define the metric induced by a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ pstoMet = (𝑑 ∈ ∪ ran PsMet ↦ (𝑎 ∈ (dom dom 𝑑 / (~Met‘𝑑)), 𝑏 ∈ (dom dom 𝑑 / (~Met‘𝑑)) ↦ ∪ {𝑧 ∣ ∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑧 = (𝑥𝑑𝑦)}))
Theorem	metidval 33889*	Value of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑥𝐷𝑦) = 0)})
Theorem	metidss 33890	As a relation, the metric identification is a subset of a Cartesian product. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) ⊆ (𝑋 × 𝑋))
Theorem	metidv 33891	𝐴 and 𝐵 identify by the metric 𝐷 if their distance is zero. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴(~Met‘𝐷)𝐵 ↔ (𝐴𝐷𝐵) = 0))
Theorem	metideq 33892	Basic property of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐴𝐷𝐸) = (𝐵𝐷𝐹))
Theorem	metider 33893	The metric identification is an equivalence relation. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) Er 𝑋)
Theorem	pstmval 33894*	Value of the metric induced by a pseudometric 𝐷. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ ∼ = (~Met‘𝐷)    ⇒   ⊢ (𝐷 ∈ (PsMet‘𝑋) → (pstoMet‘𝐷) = (𝑎 ∈ (𝑋 / ∼ ), 𝑏 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧 ∣ ∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑧 = (𝑥𝐷𝑦)}))
Theorem	pstmfval 33895	Function value of the metric induced by a pseudometric 𝐷 (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ ∼ = (~Met‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ([𝐴] ∼ (pstoMet‘𝐷)[𝐵] ∼ ) = (𝐴𝐷𝐵))
Theorem	pstmxmet 33896	The metric induced by a pseudometric is a full-fledged metric on the equivalence classes of the metric identification. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ ∼ = (~Met‘𝐷)    ⇒   ⊢ (𝐷 ∈ (PsMet‘𝑋) → (pstoMet‘𝐷) ∈ (∞Met‘(𝑋 / ∼ )))
21.3.14.9  Continuity - misc additions
Theorem	hauseqcn 33897	In a Hausdorff topology, two continuous functions which agree on a dense set agree everywhere. (Contributed by Thierry Arnoux, 28-Dec-2017.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐾 ∈ Haus)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → (𝐹 ↾ 𝐴) = (𝐺 ↾ 𝐴))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝑋)    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
21.3.14.10  Topology of the closed unit interval
Theorem	elunitge0 33898	An element of the closed unit interval is positive. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 20-Dec-2016.)
⊢ (𝐴 ∈ (0[,]1) → 0 ≤ 𝐴)
Theorem	unitssxrge0 33899	The closed unit interval is a subset of the set of the extended nonnegative reals. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 12-Dec-2016.)
⊢ (0[,]1) ⊆ (0[,]+∞)
Theorem	unitdivcld 33900	Necessary conditions for a quotient to be in the closed unit interval. (somewhat too strong, it would be sufficient that A and B are in RR+) (Contributed by Thierry Arnoux, 20-Dec-2016.)
⊢ ((𝐴 ∈ (0[,]1) ∧ 𝐵 ∈ (0[,]1) ∧ 𝐵 ≠ 0) → (𝐴 ≤ 𝐵 ↔ (𝐴 / 𝐵) ∈ (0[,]1)))