Home | Metamath
Proof Explorer Theorem List (p. 293 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | submateqlem1 29201 | Lemma for submateq 29203. (Contributed by Thierry Arnoux, 25-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1))) & ⊢ (𝜑 → 𝐾 ≤ 𝑀) ⇒ ⊢ (𝜑 → (𝑀 ∈ (𝐾...𝑁) ∧ (𝑀 + 1) ∈ ((1...𝑁) ∖ {𝐾}))) | ||
Theorem | submateqlem2 29202 | Lemma for submateq 29203. (Contributed by Thierry Arnoux, 26-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1))) & ⊢ (𝜑 → 𝑀 < 𝐾) ⇒ ⊢ (𝜑 → (𝑀 ∈ (1..^𝐾) ∧ 𝑀 ∈ ((1...𝑁) ∖ {𝐾}))) | ||
Theorem | submateq 29203* | 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 29204 | 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‘𝐸)𝐽)) | ||
Syntax | clmat 29205 | Extend class notation with the literal matrix conversion function. |
class litMat | ||
Definition | df-lmat 29206* | 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 29207* | Value of the literal matrix conversion function. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
⊢ (𝑀 ∈ 𝑉 → (litMat‘𝑀) = (𝑖 ∈ (1...(#‘𝑀)), 𝑗 ∈ (1...(#‘(𝑀‘0))) ↦ ((𝑀‘(𝑖 − 1))‘(𝑗 − 1)))) | ||
Theorem | lmatfval 29208* | Entries of a literal matrix. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
⊢ 𝑀 = (litMat‘𝑊) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑊 ∈ Word Word 𝑉) & ⊢ (𝜑 → (#‘𝑊) = 𝑁) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (#‘(𝑊‘𝑖)) = 𝑁) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) ⇒ ⊢ (𝜑 → (𝐼𝑀𝐽) = ((𝑊‘(𝐼 − 1))‘(𝐽 − 1))) | ||
Theorem | lmatfvlem 29209* | 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 29210* | Closure of the literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
⊢ 𝑀 = (litMat‘𝑊) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑊 ∈ Word Word 𝑉) & ⊢ (𝜑 → (#‘𝑊) = 𝑁) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (#‘(𝑊‘𝑖)) = 𝑁) & ⊢ 𝑉 = (Base‘𝑅) & ⊢ 𝑂 = ((1...𝑁) Mat 𝑅) & ⊢ 𝑃 = (Base‘𝑂) & ⊢ (𝜑 → 𝑅 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝑀 ∈ 𝑃) | ||
Theorem | lmat22lem 29211* | Lemma for lmat22e11 29212 and co. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
⊢ 𝑀 = (litMat‘〈“〈“𝐴𝐵”〉〈“𝐶𝐷”〉”〉) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^2)) → (#‘(〈“〈“𝐴𝐵”〉〈“𝐶𝐷”〉”〉‘𝑖)) = 2) | ||
Theorem | lmat22e11 29212 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
⊢ 𝑀 = (litMat‘〈“〈“𝐴𝐵”〉〈“𝐶𝐷”〉”〉) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (1𝑀1) = 𝐴) | ||
Theorem | lmat22e12 29213 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
⊢ 𝑀 = (litMat‘〈“〈“𝐴𝐵”〉〈“𝐶𝐷”〉”〉) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (1𝑀2) = 𝐵) | ||
Theorem | lmat22e21 29214 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
⊢ 𝑀 = (litMat‘〈“〈“𝐴𝐵”〉〈“𝐶𝐷”〉”〉) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (2𝑀1) = 𝐶) | ||
Theorem | lmat22e22 29215 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
⊢ 𝑀 = (litMat‘〈“〈“𝐴𝐵”〉〈“𝐶𝐷”〉”〉) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (2𝑀2) = 𝐷) | ||
Theorem | lmat22det 29216 | The determinant of a literal 2x2 complex matrix. (Contributed by Thierry Arnoux, 1-Sep-2020.) |
⊢ 𝑀 = (litMat‘〈“〈“𝐴𝐵”〉〈“𝐶𝐷”〉”〉) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ · = (.r‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ 𝑉 = (Base‘𝑅) & ⊢ 𝐽 = ((1...2) maDet 𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (𝐽‘𝑀) = ((𝐴 · 𝐷) − (𝐶 · 𝐵))) | ||
Theorem | mdetpmtr1 29217* | 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 29218* | 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 29219* | 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 29220* | 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 29221* | Lemma for madjusmdet 29225. (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 29222* | Lemma for madjusmdet 29225. (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 29223* | Lemma for madjusmdet 29225. (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 29224* | Lemma for madjusmdet 29225. (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 29225 | Express the cofactor of the matrix, i.e. the entries of its adjunct matrix, using determinant of submatrixes. (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 29226* | 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‘𝑀)𝑗))))))) | ||
Theorem | fvproj 29227* | Value of a function on pairs, given two projections 𝐹 and 𝐺. (Contributed by Thierry Arnoux, 30-Dec-2019.) |
⊢ 𝐻 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐻‘〈𝑋, 𝑌〉) = 〈(𝐹‘𝑋), (𝐺‘𝑌)〉) | ||
Theorem | fimaproj 29228* | Image of a cartesian product for a function on pairs, given two projections 𝐹 and 𝐺. (Contributed by Thierry Arnoux, 30-Dec-2019.) |
⊢ 𝐻 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝑋 ⊆ 𝐴) & ⊢ (𝜑 → 𝑌 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐻 “ (𝑋 × 𝑌)) = ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) | ||
Theorem | txomap 29229* | 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 𝑀)) | ||
Theorem | qtopt1 29230* | 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 29231* | 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 29232* | 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 29233* | 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 𝐹)) | ||
Theorem | reff 29234* | 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 defintion of refinement. Note that this definition uses the axiom of choice through ac6sg 9193. (Contributed by Thierry Arnoux, 12-Jan-2020.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴Ref𝐵 ↔ (∪ 𝐵 ⊆ ∪ 𝐴 ∧ ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑣 ∈ 𝐴 𝑣 ⊆ (𝑓‘𝑣))))) | ||
Theorem | locfinreflem 29235* | 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 29236* | 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‘𝐽))) | ||
Syntax | ccref 29237 | The "every open cover has an 𝐴 refinement" predicate. |
class CovHasRef𝐴 | ||
Definition | df-cref 29238* | 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 29239* | 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 29240 | Equality theorem for the "every open cover has an A refinement" predicate. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
⊢ (𝐴 = 𝐵 → CovHasRef𝐴 = CovHasRef𝐵) | ||
Theorem | creftop 29241 | A space where every open cover has an 𝐴 refinement is a topological space. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
⊢ (𝐽 ∈ CovHasRef𝐴 → 𝐽 ∈ Top) | ||
Theorem | crefi 29242* | The property that every open cover has an 𝐴 refinement for the topological space 𝐽. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ CovHasRef𝐴 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶) → ∃𝑧 ∈ (𝒫 𝐽 ∩ 𝐴)𝑧Ref𝐶) | ||
Theorem | crefdf 29243* | A formulation of crefi 29242 easier to use for definitions. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐵 = CovHasRef𝐴 & ⊢ (𝑧 ∈ 𝐴 → 𝜑) ⇒ ⊢ ((𝐽 ∈ 𝐵 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶) → ∃𝑧 ∈ 𝒫 𝐽(𝜑 ∧ 𝑧Ref𝐶)) | ||
Theorem | crefss 29244 | The "every open cover has an 𝐴 refinement" predicate respects inclusion. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
⊢ (𝐴 ⊆ 𝐵 → CovHasRef𝐴 ⊆ CovHasRef𝐵) | ||
Theorem | cmpcref 29245 | 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 29246* | Every open cover of a Compact space has a finite refinement. (Contributed by Thierry Arnoux, 1-Feb-2020.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Comp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈) → ∃𝑣 ∈ 𝒫 𝐽(𝑣 ∈ Fin ∧ 𝑣Ref𝑈)) | ||
Syntax | cldlf 29247 | Extend class notation with the class of all Lindelöf spaces. |
class Ldlf | ||
Definition | df-ldlf 29248 | 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 29249* | Every open cover of a Lindelöf space has a countable refinement. (Contributed by Thierry Arnoux, 1-Feb-2020.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Ldlf ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈) → ∃𝑣 ∈ 𝒫 𝐽(𝑣 ≼ ω ∧ 𝑣Ref𝑈)) | ||
Syntax | cpcmp 29250 | Extend class notation with the class of all paracompact topologies. |
class Paracomp | ||
Definition | df-pcmp 29251 | 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 29252 | The predicate "is a paracompact topology". (Contributed by Thierry Arnoux, 7-Jan-2020.) |
⊢ (𝐽 ∈ Paracomp ↔ 𝐽 ∈ CovHasRef(LocFin‘𝐽)) | ||
Theorem | cmppcmp 29253 | Every compact space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Paracomp) | ||
Theorem | dispcmp 29254 | Every discrete space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Paracomp) | ||
Theorem | pcmplfin 29255* | 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 29256* | 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‘𝐽))) | ||
Syntax | cmetid 29257 | Extend class notation with the class of metric identifications. |
class ~Met | ||
Syntax | cpstm 29258 | Extend class notation with the metric induced by a pseudometric. |
class pstoMet | ||
Definition | df-metid 29259* | 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 29260* | 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 29261* | Value of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑥𝐷𝑦) = 0)}) | ||
Theorem | metidss 29262 | As a relation, the metric identification is a subset of a Cartesian product. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) ⊆ (𝑋 × 𝑋)) | ||
Theorem | metidv 29263 | 𝐴 and 𝐵 identify by the metric 𝐷 if their distance is zero. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴(~Met‘𝐷)𝐵 ↔ (𝐴𝐷𝐵) = 0)) | ||
Theorem | metideq 29264 | Basic property of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐴𝐷𝐸) = (𝐵𝐷𝐹)) | ||
Theorem | metider 29265 | The metric identification is an equivalence relation. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) Er 𝑋) | ||
Theorem | pstmval 29266* | Value of the metric induced by a pseudometric 𝐷. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ ∼ = (~Met‘𝐷) ⇒ ⊢ (𝐷 ∈ (PsMet‘𝑋) → (pstoMet‘𝐷) = (𝑎 ∈ (𝑋 / ∼ ), 𝑏 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧 ∣ ∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑧 = (𝑥𝐷𝑦)})) | ||
Theorem | pstmfval 29267 | Function value of the metric induced by a pseudometric 𝐷 (Contributed by Thierry Arnoux, 11-Feb-2018.) |
⊢ ∼ = (~Met‘𝐷) ⇒ ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ([𝐴] ∼ (pstoMet‘𝐷)[𝐵] ∼ ) = (𝐴𝐷𝐵)) | ||
Theorem | pstmxmet 29268 | 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‘(𝑋 / ∼ ))) | ||
Theorem | hauseqcn 29269 | 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‘𝐽)‘𝐴) = 𝑋) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
Theorem | unitsscn 29270 | The closed unit is a subset of the set of the complex numbers Useful lemma for manipulating probabilities within the closed unit. (Contributed by Thierry Arnoux, 12-Dec-2016.) |
⊢ (0[,]1) ⊆ ℂ | ||
Theorem | elunitrn 29271 | The closed unit is a subset of the set of the real numbers Useful lemma for manipulating probabilities within the closed unit. (Contributed by Thierry Arnoux, 21-Dec-2016.) |
⊢ (𝐴 ∈ (0[,]1) → 𝐴 ∈ ℝ) | ||
Theorem | elunitcn 29272 | The closed unit is a subset of the set of the complext numbers Useful lemma for manipulating probabilities within the closed unit. (Contributed by Thierry Arnoux, 21-Dec-2016.) |
⊢ (𝐴 ∈ (0[,]1) → 𝐴 ∈ ℂ) | ||
Theorem | elunitge0 29273 | An element of the closed unit is positive Useful lemma for manipulating probabilities within the closed unit. (Contributed by Thierry Arnoux, 20-Dec-2016.) |
⊢ (𝐴 ∈ (0[,]1) → 0 ≤ 𝐴) | ||
Theorem | unitssxrge0 29274 | The closed unit is a subset of the set of the extended nonnegative reals. Useful lemma for manipulating probabilities within the closed unit. (Contributed by Thierry Arnoux, 12-Dec-2016.) |
⊢ (0[,]1) ⊆ (0[,]+∞) | ||
Theorem | unitdivcld 29275 | Necessary conditions for a quotient to be in the closed unit. (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))) | ||
Theorem | iistmd 29276 | The closed unit forms a topological monoid. (Contributed by Thierry Arnoux, 25-Mar-2017.) |
⊢ 𝐼 = ((mulGrp‘ℂfld) ↾s (0[,]1)) ⇒ ⊢ 𝐼 ∈ TopMnd | ||
Theorem | unicls 29277 | The union of the closed set is the underlying set of the topology. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
⊢ 𝐽 ∈ Top & ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ∪ (Clsd‘𝐽) = 𝑋 | ||
Theorem | tpr2tp 29278 | The usual topology on (ℝ × ℝ) is the product topology of the usual topology on ℝ. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) ⇒ ⊢ (𝐽 ×t 𝐽) ∈ (TopOn‘(ℝ × ℝ)) | ||
Theorem | tpr2uni 29279 | The usual topology on (ℝ × ℝ) is the product topology of the usual topology on ℝ. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) ⇒ ⊢ ∪ (𝐽 ×t 𝐽) = (ℝ × ℝ) | ||
Theorem | xpinpreima 29280 | Rewrite the cartesian product of two sets as the intersection of their preimage by 1st and 2nd, the projections on the first and second elements. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
⊢ (𝐴 × 𝐵) = ((◡(1st ↾ (V × V)) “ 𝐴) ∩ (◡(2nd ↾ (V × V)) “ 𝐵)) | ||
Theorem | xpinpreima2 29281 | Rewrite the cartesian product of two sets as the intersection of their preimage by 1st and 2nd, the projections on the first and second elements. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
⊢ ((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) → (𝐴 × 𝐵) = ((◡(1st ↾ (𝐸 × 𝐹)) “ 𝐴) ∩ (◡(2nd ↾ (𝐸 × 𝐹)) “ 𝐵))) | ||
Theorem | sqsscirc1 29282 | The complex square of side 𝐷 is a subset of the complex circle of radius 𝐷. (Contributed by Thierry Arnoux, 25-Sep-2017.) |
⊢ ((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ+) → ((𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2)) → (√‘((𝑋↑2) + (𝑌↑2))) < 𝐷)) | ||
Theorem | sqsscirc2 29283 | The complex square of side 𝐷 is a subset of the complex disc of radius 𝐷. (Contributed by Thierry Arnoux, 25-Sep-2017.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝐷 ∈ ℝ+) → (((abs‘(ℜ‘(𝐵 − 𝐴))) < (𝐷 / 2) ∧ (abs‘(ℑ‘(𝐵 − 𝐴))) < (𝐷 / 2)) → (abs‘(𝐵 − 𝐴)) < 𝐷)) | ||
Theorem | cnre2csqlem 29284* | Lemma for cnre2csqima 29285. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
⊢ (𝐺 ↾ (ℝ × ℝ)) = (𝐻 ∘ 𝐹) & ⊢ 𝐹 Fn (ℝ × ℝ) & ⊢ 𝐺 Fn V & ⊢ (𝑥 ∈ (ℝ × ℝ) → (𝐺‘𝑥) ∈ ℝ) & ⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → (𝐻‘(𝑥 − 𝑦)) = ((𝐻‘𝑥) − (𝐻‘𝑦))) ⇒ ⊢ ((𝑋 ∈ (ℝ × ℝ) ∧ 𝑌 ∈ (ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ (◡(𝐺 ↾ (ℝ × ℝ)) “ (((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷))) → (abs‘(𝐻‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷)) | ||
Theorem | cnre2csqima 29285* | Image of a centered square by the canonical bijection from (ℝ × ℝ) to ℂ. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) ⇒ ⊢ ((𝑋 ∈ (ℝ × ℝ) ∧ 𝑌 ∈ (ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ ((((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷)) × (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷))) → ((abs‘(ℜ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷 ∧ (abs‘(ℑ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷))) | ||
Theorem | tpr2rico 29286* | For any point of an open set of the usual topology on (ℝ × ℝ) there is an open square which contains that point and is entirely in the open set. This is square is actually a ball by the (𝑙↑+∞) norm 𝑋. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐺 = (𝑢 ∈ ℝ, 𝑣 ∈ ℝ ↦ (𝑢 + (i · 𝑣))) & ⊢ 𝐵 = ran (𝑥 ∈ ran (,), 𝑦 ∈ ran (,) ↦ (𝑥 × 𝑦)) ⇒ ⊢ ((𝐴 ∈ (𝐽 ×t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑟 ∈ 𝐵 (𝑋 ∈ 𝑟 ∧ 𝑟 ⊆ 𝐴)) | ||
Theorem | cnvordtrestixx 29287* | The restriction of the 'greater than' order to an interval gives the same topology as the subspace topology. (Contributed by Thierry Arnoux, 1-Apr-2017.) |
⊢ 𝐴 ⊆ ℝ* & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥[,]𝑦) ⊆ 𝐴) ⇒ ⊢ ((ordTop‘ ≤ ) ↾t 𝐴) = (ordTop‘(◡ ≤ ∩ (𝐴 × 𝐴))) | ||
Theorem | prsdm 29288 | Domain of the relation of a preset. (Contributed by Thierry Arnoux, 11-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ (𝐾 ∈ Preset → dom ≤ = 𝐵) | ||
Theorem | prsrn 29289 | Range of the relation of a preset. (Contributed by Thierry Arnoux, 11-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ (𝐾 ∈ Preset → ran ≤ = 𝐵) | ||
Theorem | prsss 29290 | Relation of a subpreset. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → ( ≤ ∩ (𝐴 × 𝐴)) = ((le‘𝐾) ∩ (𝐴 × 𝐴))) | ||
Theorem | prsssdm 29291 | Domain of a subpreset relation. (Contributed by Thierry Arnoux, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → dom ( ≤ ∩ (𝐴 × 𝐴)) = 𝐴) | ||
Theorem | ordtprsval 29292* | Value of the order topology for a preset. (Contributed by Thierry Arnoux, 11-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ 𝐸 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) & ⊢ 𝐹 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ⇒ ⊢ (𝐾 ∈ Preset → (ordTop‘ ≤ ) = (topGen‘(fi‘({𝐵} ∪ (𝐸 ∪ 𝐹))))) | ||
Theorem | ordtprsuni 29293* | Value of the order topology. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ 𝐸 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) & ⊢ 𝐹 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ⇒ ⊢ (𝐾 ∈ Preset → 𝐵 = ∪ ({𝐵} ∪ (𝐸 ∪ 𝐹))) | ||
Theorem | ordtcnvNEW 29294 | The order dual generates the same topology as the original order. (Contributed by Mario Carneiro, 3-Sep-2015.) (Revised by Thierry Arnoux, 13-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ (𝐾 ∈ Preset → (ordTop‘◡ ≤ ) = (ordTop‘ ≤ )) | ||
Theorem | ordtrestNEW 29295 | The subspace topology of an order topology is in general finer than the topology generated by the restricted order, but we do have inclusion in one direction. (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ⊆ ((ordTop‘ ≤ ) ↾t 𝐴)) | ||
Theorem | ordtrest2NEWlem 29296* | Lemma for ordtrest2NEW 29297. (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} ⊆ 𝐴) ⇒ ⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) | ||
Theorem | ordtrest2NEW 29297* | An interval-closed set 𝐴 in a total order has the same subspace topology as the restricted order topology. (An interval-closed set is the same thing as an open or half-open or closed interval in ℝ, but in other sets like ℚ there are interval-closed sets like (π, +∞) ∩ ℚ that are not intervals.) (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} ⊆ 𝐴) ⇒ ⊢ (𝜑 → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) = ((ordTop‘ ≤ ) ↾t 𝐴)) | ||
Theorem | ordtconlem1 29298* | Connectedness in the order topology of a toset. This is the "easy" direction of ordtcon 29299. See also reconnlem1 22437. (Contributed by Thierry Arnoux, 14-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ 𝐽 = (ordTop‘ ≤ ) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → ((𝐽 ↾t 𝐴) ∈ Con → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))) | ||
Theorem | ordtcon 29299 | Connectedness in the order topology of a complete uniform totally ordered space. (Contributed by Thierry Arnoux, 15-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ 𝐽 = (ordTop‘ ≤ ) ⇒ ⊢ ⊤ | ||
Theorem | mndpluscn 29300* | A mapping that is both a homeomorphism and a monoid homomorphism preserves the "continuousness" of the operation. (Contributed by Thierry Arnoux, 25-Mar-2017.) |
⊢ 𝐹 ∈ (𝐽Homeo𝐾) & ⊢ + :(𝐵 × 𝐵)⟶𝐵 & ⊢ ∗ :(𝐶 × 𝐶)⟶𝐶 & ⊢ 𝐽 ∈ (TopOn‘𝐵) & ⊢ 𝐾 ∈ (TopOn‘𝐶) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ∗ (𝐹‘𝑦))) & ⊢ + ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ⇒ ⊢ ∗ ∈ ((𝐾 ×t 𝐾) Cn 𝐾) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |