Home | Metamath
Proof Explorer Theorem List (p. 324 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 | ||
We define the operations on the extended real and complex numbers and on the real and complex projective lines simultaneously, thus "overloading" the operations. | ||
Syntax | caddcc 32301 | Syntax for the addition of extended complex numbers. |
class +ℂ̅ | ||
Definition | df-bj-addc 32302 | Define the additions on the extended complex numbers (on the subset of (ℂ̅ × ℂ̅) where it makes sense) and on the complex projective line (Riemann sphere). (Contributed by BJ, 22-Jun-2019.) |
⊢ +ℂ̅ = (𝑥 ∈ (((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂ × ℂ̂) ∪ (Diag‘ℂ∞))) ↦ if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if((1st ‘𝑥) ∈ ℂ, if((2nd ‘𝑥) ∈ ℂ, ((1st ‘𝑥) + (2nd ‘𝑥)), (2nd ‘𝑥)), (1st ‘𝑥)))) | ||
Syntax | coppcc 32303 | Syntax for the opposite of extended complex numbers. |
class -ℂ̅ | ||
Definition | df-bj-oppc 32304 | Define the negation (operation givin the opposite) the set of extended complex numbers and the complex projective line (Riemann sphere). One could use the prcpal function in the infinite case, but we want to use only basic functions at this point. (Contributed by BJ, 22-Jun-2019.) |
⊢ -ℂ̅ = (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, -𝑥, (inftyexpi ‘if(0 < (1st ‘𝑥), ((1st ‘𝑥) − π), ((1st ‘𝑥) + π)))))) | ||
Since one needs arguments in order to define multiplication in ℂ̅, it seems harder to put this at the very beginning of the introduction of complex numbers. | ||
Syntax | cprcpal 32305 | Syntax for the function prcpal. |
class prcpal | ||
Definition | df-bj-prcpal 32306 | Define the function prcpal. (Contributed by BJ, 22-Jun-2019.) |
⊢ prcpal = (𝑥 ∈ ℝ ↦ ((𝑥 mod (2 · π)) − if((𝑥 mod (2 · π)) ≤ π, 0, (2 · π)))) | ||
Syntax | carg 32307 | Syntax for the argument of a nonzero extended complex number. |
class Arg | ||
Definition | df-bj-arg 32308 | Define the argument of a nonzero extended complex number. By convention, it has values in (-π, π]. Another convention chooses [0, 2π) but the present one simplifies formulas giving the argument as an arctangent. (Contributed by BJ, 22-Jun-2019.) |
⊢ Arg = (𝑥 ∈ (ℂ̅ ∖ {0}) ↦ if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), (1st ‘𝑥))) | ||
Syntax | cmulc 32309 | Syntax for the multiplication of extended complex numbers. |
class ·ℂ̅ | ||
Definition | df-bj-mulc 32310 | Define the multiplication of extended complex numbers and of the complex projective line (Riemann sphere). In our convention, a product with 0 is 0, even when the other factor is infinite. An alternate convention leaves products of 0 with an infinite number undefined since the multiplication is not continuous at these points. Note that our convention entails (0 / 0) = 0. (Contributed by BJ, 22-Jun-2019.) |
⊢ ·ℂ̅ = (𝑥 ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ↦ if(((1st ‘𝑥) = 0 ∨ (2nd ‘𝑥) = 0), 0, if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if(𝑥 ∈ (ℂ × ℂ), ((1st ‘𝑥) · (2nd ‘𝑥)), (inftyexpi ‘(prcpal‘((Arg‘(1st ‘𝑥)) + (Arg‘(2nd ‘𝑥))))))))) | ||
Syntax | cinvc 32311 | Syntax for the inverse of nonzero extended complex numbers. |
class -1ℂ̅ | ||
Definition | df-bj-invc 32312 | Define inversion, which maps a nonzero extended complex number or element of the complex projective line (Riemann sphere) to its inverse. Beware of the overloading: the equality (-1ℂ̅‘0) = ∞ is to be understood in the complex projective line, but 0 as an extended complex number does not have an inverse, which we can state as (-1ℂ̅‘0) ∉ ℂ̅. (Contributed by BJ, 22-Jun-2019.) |
⊢ -1ℂ̅ = (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = 0, ∞, if(𝑥 ∈ ℂ, (1 / 𝑥), 0))) | ||
See ccmn 18016 and subsequents. The first few statements of this subsection can be put very early after ccmn 18016. Proposal: in the main part, make separate subsections of commutative monoids and abelian groups. Relabel cabl 18017 to "cabl" or, preferably, other labels containing "abl" to "abel", for consistency. | ||
Theorem | bj-cmnssmnd 32313 | Commutative monoids are monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ CMnd ⊆ Mnd | ||
Theorem | bj-cmnssmndel 32314 | Commutative monoids are monoids (elemental version). This is a more direct proof of cmnmnd 18031, which relies on iscmn 18023. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ CMnd → 𝐴 ∈ Mnd) | ||
Theorem | bj-ablssgrp 32315 | Abelian groups are groups. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ Abel ⊆ Grp | ||
Theorem | bj-ablssgrpel 32316 | Abelian groups are groups (elemental version). This is a shorter proof of ablgrp 18021. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ Abel → 𝐴 ∈ Grp) | ||
Theorem | bj-ablsscmn 32317 | Abelian groups are commutative monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ Abel ⊆ CMnd | ||
Theorem | bj-ablsscmnel 32318 | Abelian groups are commutative monoids (elemental version). This is a shorter proof of ablcmn 18022. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ Abel → 𝐴 ∈ CMnd) | ||
Theorem | bj-modssabl 32319 | (The additive groups of) modules are abelian groups. (The elemental version is lmodabl 18733; see also lmodgrp 18693 and lmodcmn 18734.) (Contributed by BJ, 9-Jun-2019.) |
⊢ LMod ⊆ Abel | ||
Theorem | bj-vecssmod 32320 | Vector spaces are modules. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ LVec ⊆ LMod | ||
Theorem | bj-vecssmodel 32321 | Vector spaces are modules (elemental version). This is a shorter proof of lveclmod 18927. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod) | ||
UPDATE: a similar summation is already defined as df-gsum 15926 (although it mixes finite and infinite sums, which makes it harder to understand). | ||
Syntax | cfinsum 32322 | Syntax for the class "finite summation in monoids". |
class FinSum | ||
Definition | df-bj-finsum 32323* | Finite summation in commutative monoids. This finite summation function can be extended to pairs 〈𝑦, 𝑧〉 where 𝑦 is a left-unital magma and 𝑧 is defined on a totally ordered set (choosing left-associative composition), or dropping unitality and requiring nonempty families, or on any monoids for families of permutable elements, etc. We use the term "summation", even though the definition stands for any unital, commutative and associative composition law. (Contributed by BJ, 9-Jun-2019.) |
⊢ FinSum = (𝑥 ∈ {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ CMnd ∧ ∃𝑡 ∈ Fin 𝑧:𝑡⟶(Base‘𝑦))} ↦ (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→dom (2nd ‘𝑥) ∧ 𝑠 = (seq1((+g‘(1st ‘𝑥)), (𝑛 ∈ ℕ ↦ ((2nd ‘𝑥)‘(𝑓‘𝑛))))‘𝑚)))) | ||
Theorem | bj-finsumval0 32324* | Value of a finite sum. (Contributed by BJ, 9-Jun-2019.) (Proof shortened by AV, 5-May-2021.) |
⊢ (𝜑 → 𝐴 ∈ CMnd) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐵:𝐼⟶(Base‘𝐴)) ⇒ ⊢ (𝜑 → (𝐴 FinSum 𝐵) = (℩𝑠∃𝑚 ∈ ℕ0 ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐼 ∧ 𝑠 = (seq1((+g‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(#‘𝐼))))) | ||
A few basic theorems to start affine, Euclidean, and Cartesian geometry. | ||
A few basic definitions and theorems about convex hulls in real vector spaces. TODO: prove inclusion in the class of subcomplex vector spaces. | ||
Syntax | crrvec 32325 | Syntax for the class of real vector spaces. |
class ℝ-Vec | ||
Definition | df-bj-rrvec 32326 | Definition of the class of real vector spaces. (Contributed by BJ, 9-Jun-2019.) |
⊢ ℝ-Vec = {𝑥 ∈ LVec ∣ (Scalar‘𝑥) = ℝfld} | ||
Theorem | bj-rrvecssvec 32327 | Real vector spaces are vector spaces. (Contributed by BJ, 9-Jun-2019.) |
⊢ ℝ-Vec ⊆ LVec | ||
Theorem | bj-rrvecssvecel 32328 | Real vector spaces are vector spaces (elemental version). (Contributed by BJ, 9-Jun-2019.) |
⊢ (𝐴 ∈ ℝ-Vec → 𝐴 ∈ LVec) | ||
Theorem | bj-rrvecsscmn 32329 | (The additive groups of) real vector spaces are commutative monoids. (Contributed by BJ, 9-Jun-2019.) |
⊢ ℝ-Vec ⊆ CMnd | ||
Theorem | bj-rrvecsscmnel 32330 | (The additive groups of) real vector spaces are commutative monoids (elemental version). (Contributed by BJ, 9-Jun-2019.) |
⊢ (𝐴 ∈ ℝ-Vec → 𝐴 ∈ CMnd) | ||
Some lemmas to ease algebraic manipulations. | ||
Theorem | bj-subcom 32331 | A consequence of commutativity of multiplication. (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) − (𝐵 · 𝐴)) = 0) | ||
Theorem | bj-ldiv 32332 | Left-division. (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) = 𝐶 ↔ 𝐴 = (𝐶 / 𝐵))) | ||
Theorem | bj-rdiv 32333 | Right-division. (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) = 𝐶 ↔ 𝐵 = (𝐶 / 𝐴))) | ||
Theorem | bj-mdiv 32334 | A division law. (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 = (𝐶 / 𝐵) ↔ 𝐵 = (𝐶 / 𝐴))) | ||
Theorem | bj-lineq 32335 | Solution of a (scalar) linear equation. (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑌 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (((𝐴 · 𝑋) + 𝐵) = 𝑌 ↔ 𝑋 = ((𝑌 − 𝐵) / 𝐴))) | ||
Theorem | bj-lineqi 32336 | Solution of a (scalar) linear equation. (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑌 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → ((𝐴 · 𝑋) + 𝐵) = 𝑌) ⇒ ⊢ (𝜑 → 𝑋 = ((𝑌 − 𝐵) / 𝐴)) | ||
Lemmas about barycentric coordinates. For the moment, this is limited to the one-dimensional case (complex line), where existence and uniqueness of barycentric coordinates is proved by bj-bary1 32339 (which computes them). | ||
Theorem | bj-bary1lem 32337 | A lemma for barycentric coordinates in one dimension. (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 = ((((𝐵 − 𝑋) / (𝐵 − 𝐴)) · 𝐴) + (((𝑋 − 𝐴) / (𝐵 − 𝐴)) · 𝐵))) | ||
Theorem | bj-bary1lem1 32338 | Existence and uniqueness (and actual computation) of barycentric coordinates in dimension 1 (complex line). (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝑆 ∈ ℂ) & ⊢ (𝜑 → 𝑇 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝑋 = ((𝑆 · 𝐴) + (𝑇 · 𝐵)) ∧ (𝑆 + 𝑇) = 1) → 𝑇 = ((𝑋 − 𝐴) / (𝐵 − 𝐴)))) | ||
Theorem | bj-bary1 32339 | Barycentric coordinates in one dimension. (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝑆 ∈ ℂ) & ⊢ (𝜑 → 𝑇 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝑋 = ((𝑆 · 𝐴) + (𝑇 · 𝐵)) ∧ (𝑆 + 𝑇) = 1) ↔ (𝑆 = ((𝐵 − 𝑋) / (𝐵 − 𝐴)) ∧ 𝑇 = ((𝑋 − 𝐴) / (𝐵 − 𝐴))))) | ||
Syntax | ctau 32340 | Extend class notation to include tau = 6.283185.... |
class τ | ||
Definition | df-tau 32341 | Define tau = 6.283185..., which is the smallest positive real number whose cosine is one. Various notations have been used or proposed for this number including τ, a three-legged variant of π, or 2π. Note the difference between this constant τ and the variable 𝜏 which is a variable representing a propositional logic formula. Only the latter is italic, and the colors are different. (Contributed by Jim Kingdon, 9-Apr-2018.) (Revised by AV, 1-Oct-2020.) |
⊢ τ = inf((ℝ+ ∩ (◡cos “ {1})), ℝ, < ) | ||
Theorem | taupilem3 32342 | Lemma for tau-related theorems . (Contributed by Jim Kingdon, 16-Feb-2019.) |
⊢ (𝐴 ∈ (ℝ+ ∩ (◡cos “ {1})) ↔ (𝐴 ∈ ℝ+ ∧ (cos‘𝐴) = 1)) | ||
Theorem | taupilemrplb 32343* | A set of positive reals has (in the reals) a lower bound. (Contributed by Jim Kingdon, 19-Feb-2019.) |
⊢ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (ℝ+ ∩ 𝐴)𝑥 ≤ 𝑦 | ||
Theorem | taupilem1 32344 | Lemma for taupi 32346. A positive real whose cosine is one is at least 2 · π. (Contributed by Jim Kingdon, 19-Feb-2019.) |
⊢ ((𝐴 ∈ ℝ+ ∧ (cos‘𝐴) = 1) → (2 · π) ≤ 𝐴) | ||
Theorem | taupilem2 32345 | Lemma for taupi 32346. The smallest positive real whose cosine is one is at most 2 · π. (Contributed by Jim Kingdon, 19-Feb-2019.) (Revised by AV, 1-Oct-2020.) |
⊢ τ ≤ (2 · π) | ||
Theorem | taupi 32346 | Relationship between τ and π. This can be seen as connecting the ratio of a circle's circumference to its radius and the ratio of a circle's circumference to its diameter. (Contributed by Jim Kingdon, 19-Feb-2019.) (Revised by AV, 1-Oct-2020.) |
⊢ τ = (2 · π) | ||
Theorem | csbdif 32347 | Distribution of class substitution over difference of two classes. (Contributed by ML, 14-Jul-2020.) |
⊢ ⦋𝐴 / 𝑥⦌(𝐵 ∖ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∖ ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | csbpredg 32348 | Move class substitution in and out of the predecessor class of a relationship. (Contributed by ML, 25-Oct-2020.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌Pred(𝑅, 𝐷, 𝑋) = Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, ⦋𝐴 / 𝑥⦌𝑋)) | ||
Theorem | csbwrecsg 32349 | Move class substitution in and out of the well-founded recursive function generator . (Contributed by ML, 25-Oct-2020.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌wrecs(𝑅, 𝐷, 𝐹) = wrecs(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, ⦋𝐴 / 𝑥⦌𝐹)) | ||
Theorem | csbrecsg 32350 | Move class substitution in and out of recs. (Contributed by ML, 25-Oct-2020.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌recs(𝐹) = recs(⦋𝐴 / 𝑥⦌𝐹)) | ||
Theorem | csbrdgg 32351 | Move class substitution in and out of the recursive function generator. (Contributed by ML, 25-Oct-2020.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌rec(𝐹, 𝐼) = rec(⦋𝐴 / 𝑥⦌𝐹, ⦋𝐴 / 𝑥⦌𝐼)) | ||
Theorem | csboprabg 32352* | Move class substitution in and out of class abstractions of nested ordered pairs. (Contributed by ML, 25-Oct-2020.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{〈〈𝑦, 𝑧〉, 𝑑〉 ∣ 𝜑} = {〈〈𝑦, 𝑧〉, 𝑑〉 ∣ [𝐴 / 𝑥]𝜑}) | ||
Theorem | csbmpt22g 32353* | Move class substitution in and out of maps-to notation for operations. (Contributed by ML, 25-Oct-2020.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑦 ∈ 𝑌, 𝑧 ∈ 𝑍 ↦ 𝐷) = (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌, 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑍 ↦ ⦋𝐴 / 𝑥⦌𝐷)) | ||
Theorem | mpnanrd 32354 | Eliminate the right side of a negated conjunction in an implication. (Contributed by ML, 17-Oct-2020.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜒) | ||
Theorem | con1bii2 32355 | A contraposition inference. (Contributed by ML, 18-Oct-2020.) |
⊢ (¬ 𝜑 ↔ 𝜓) ⇒ ⊢ (𝜑 ↔ ¬ 𝜓) | ||
Theorem | con2bii2 32356 | A contraposition inference. (Contributed by ML, 18-Oct-2020.) |
⊢ (𝜑 ↔ ¬ 𝜓) ⇒ ⊢ (¬ 𝜑 ↔ 𝜓) | ||
Theorem | vtoclefex 32357* | Implicit substitution of a class for a setvar variable. (Contributed by ML, 17-Oct-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝑥 = 𝐴 → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜑) | ||
Theorem | rnmptsn 32358* | The range of a function mapping to singletons. (Contributed by ML, 15-Jul-2020.) |
⊢ ran (𝑥 ∈ 𝐴 ↦ {𝑥}) = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}} | ||
Theorem | f1omptsnlem 32359* | This is the core of the proof of f1omptsn 32360, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 15-Jul-2020.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ {𝑥}) & ⊢ 𝑅 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}} ⇒ ⊢ 𝐹:𝐴–1-1-onto→𝑅 | ||
Theorem | f1omptsn 32360* | A function mapping to singletons is bijective onto a set of singletons. (Contributed by ML, 16-Jul-2020.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ {𝑥}) & ⊢ 𝑅 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}} ⇒ ⊢ 𝐹:𝐴–1-1-onto→𝑅 | ||
Theorem | mptsnunlem 32361* | This is the core of the proof of mptsnun 32362, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 16-Jul-2020.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ {𝑥}) & ⊢ 𝑅 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}} ⇒ ⊢ (𝐵 ⊆ 𝐴 → 𝐵 = ∪ (𝐹 “ 𝐵)) | ||
Theorem | mptsnun 32362* | A class 𝐵 is equal to the union of the class of all singletons of elements of 𝐵. (Contributed by ML, 16-Jul-2020.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ {𝑥}) & ⊢ 𝑅 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}} ⇒ ⊢ (𝐵 ⊆ 𝐴 → 𝐵 = ∪ (𝐹 “ 𝐵)) | ||
Theorem | dissneqlem 32363* | This is the core of the proof of dissneq 32364, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 16-Jul-2020.) |
⊢ 𝐶 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}} ⇒ ⊢ ((𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ (TopOn‘𝐴)) → 𝐵 = 𝒫 𝐴) | ||
Theorem | dissneq 32364* | Any topology that contains every single-point set is the discrete topology. (Contributed by ML, 16-Jul-2020.) |
⊢ 𝐶 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}} ⇒ ⊢ ((𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ (TopOn‘𝐴)) → 𝐵 = 𝒫 𝐴) | ||
Theorem | exlimim 32365* | Closed form of exlimimd 32366. (Contributed by ML, 17-Jul-2020.) |
⊢ ((∃𝑥𝜑 ∧ ∀𝑥(𝜑 → 𝜓)) → 𝜓) | ||
Theorem | exlimimd 32366* | Existential elimination rule of natural deduction. (Contributed by ML, 17-Jul-2020.) |
⊢ (𝜑 → ∃𝑥𝜓) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | exlimimdd 32367 | Existential elimination rule of natural deduction. (Contributed by ML, 17-Jul-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝜑 → ∃𝑥𝜓) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | exellim 32368* | Closed form of exellimddv 32369. See also exlimim 32365 for a more general theorem. (Contributed by ML, 17-Jul-2020.) |
⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) → 𝜑) | ||
Theorem | exellimddv 32369* | Eliminate an antecedent when the antecedent is elementhood, deduction version. See exellim 32368 for the closed form, which requires the use of a universal quantifier. (Contributed by ML, 17-Jul-2020.) |
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | topdifinfindis 32370* | Part of Exercise 3 of [Munkres] p. 83. The topology of all subsets 𝑥 of 𝐴 such that the complement of 𝑥 in 𝐴 is infinite, or 𝑥 is the empty set, or 𝑥 is all of 𝐴, is the trivial topology when 𝐴 is finite. (Contributed by ML, 14-Jul-2020.) |
⊢ 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))} ⇒ ⊢ (𝐴 ∈ Fin → 𝑇 = {∅, 𝐴}) | ||
Theorem | topdifinffinlem 32371* | This is the core of the proof of topdifinffin 32372, but to avoid the distinct variables on the definition, we need to split this proof into two. (Contributed by ML, 17-Jul-2020.) |
⊢ 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))} ⇒ ⊢ (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ Fin) | ||
Theorem | topdifinffin 32372* | Part of Exercise 3 of [Munkres] p. 83. The topology of all subsets 𝑥 of 𝐴 such that the complement of 𝑥 in 𝐴 is infinite, or 𝑥 is the empty set, or 𝑥 is all of 𝐴, is a topology only if 𝐴 is finite. (Contributed by ML, 17-Jul-2020.) |
⊢ 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))} ⇒ ⊢ (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ Fin) | ||
Theorem | topdifinf 32373* | Part of Exercise 3 of [Munkres] p. 83. The topology of all subsets 𝑥 of 𝐴 such that the complement of 𝑥 in 𝐴 is infinite, or 𝑥 is the empty set, or 𝑥 is all of 𝐴, is a topology if and only if 𝐴 is finite, in which case it is the trivial topology. (Contributed by ML, 17-Jul-2020.) |
⊢ 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))} ⇒ ⊢ ((𝑇 ∈ (TopOn‘𝐴) ↔ 𝐴 ∈ Fin) ∧ (𝑇 ∈ (TopOn‘𝐴) → 𝑇 = {∅, 𝐴})) | ||
Theorem | topdifinfeq 32374* | Two different ways of defining the collection from Exercise 3 of [Munkres] p. 83. (Contributed by ML, 18-Jul-2020.) |
⊢ {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ ((𝐴 ∖ 𝑥) = ∅ ∨ (𝐴 ∖ 𝑥) = 𝐴))} = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))} | ||
Theorem | icorempt2 32375* | Closed-below, open-above intervals of reals. (Contributed by ML, 26-Jul-2020.) |
⊢ 𝐹 = ([,) ↾ (ℝ × ℝ)) ⇒ ⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) | ||
Theorem | icoreresf 32376 | Closed-below, open-above intervals of reals map to subsets of reals. (Contributed by ML, 25-Jul-2020.) |
⊢ ([,) ↾ (ℝ × ℝ)):(ℝ × ℝ)⟶𝒫 ℝ | ||
Theorem | icoreval 32377* | Value of the closed-below, open-above interval function on reals. (Contributed by ML, 26-Jul-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,)𝐵) = {𝑧 ∈ ℝ ∣ (𝐴 ≤ 𝑧 ∧ 𝑧 < 𝐵)}) | ||
Theorem | icoreelrnab 32378* | Elementhood in the set of closed-below, open-above intervals of reals. (Contributed by ML, 27-Jul-2020.) |
⊢ 𝐼 = ([,) “ (ℝ × ℝ)) ⇒ ⊢ (𝑋 ∈ 𝐼 ↔ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 𝑋 = {𝑧 ∈ ℝ ∣ (𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏)}) | ||
Theorem | isbasisrelowllem1 32379* | Lemma for isbasisrelowl 32382. (Contributed by ML, 27-Jul-2020.) |
⊢ 𝐼 = ([,) “ (ℝ × ℝ)) ⇒ ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = {𝑧 ∈ ℝ ∣ (𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏)}) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = {𝑧 ∈ ℝ ∣ (𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑)})) ∧ (𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑)) → (𝑥 ∩ 𝑦) ∈ 𝐼) | ||
Theorem | isbasisrelowllem2 32380* | Lemma for isbasisrelowl 32382. (Contributed by ML, 27-Jul-2020.) |
⊢ 𝐼 = ([,) “ (ℝ × ℝ)) ⇒ ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = {𝑧 ∈ ℝ ∣ (𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏)}) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = {𝑧 ∈ ℝ ∣ (𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑)})) ∧ (𝑎 ≤ 𝑐 ∧ 𝑑 ≤ 𝑏)) → (𝑥 ∩ 𝑦) ∈ 𝐼) | ||
Theorem | icoreclin 32381* | The set of closed-below, open-above intervals of reals is closed under finite intersection. (Contributed by ML, 27-Jul-2020.) |
⊢ 𝐼 = ([,) “ (ℝ × ℝ)) ⇒ ⊢ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) → (𝑥 ∩ 𝑦) ∈ 𝐼) | ||
Theorem | isbasisrelowl 32382 | The set of all closed-below, open-above intervals of reals form a basis. (Contributed by ML, 27-Jul-2020.) |
⊢ 𝐼 = ([,) “ (ℝ × ℝ)) ⇒ ⊢ 𝐼 ∈ TopBases | ||
Theorem | icoreunrn 32383 | The union of all closed-below, open-above intervals of reals is the set of reals. (Contributed by ML, 27-Jul-2020.) |
⊢ 𝐼 = ([,) “ (ℝ × ℝ)) ⇒ ⊢ ℝ = ∪ 𝐼 | ||
Theorem | istoprelowl 32384 | The set of all closed-below, open-above intervals of reals generate a topology on the reals. (Contributed by ML, 27-Jul-2020.) |
⊢ 𝐼 = ([,) “ (ℝ × ℝ)) ⇒ ⊢ (topGen‘𝐼) ∈ (TopOn‘ℝ) | ||
Theorem | icoreelrn 32385* | A class abstraction which is an element of the set of closed-below, open-above intervals of reals. (Contributed by ML, 1-Aug-2020.) |
⊢ 𝐼 = ([,) “ (ℝ × ℝ)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → {𝑧 ∈ ℝ ∣ (𝐴 ≤ 𝑧 ∧ 𝑧 < 𝐵)} ∈ 𝐼) | ||
Theorem | iooelexlt 32386* | An element of an open interval is not its smallest element. (Contributed by ML, 2-Aug-2020.) |
⊢ (𝑋 ∈ (𝐴(,)𝐵) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋) | ||
Theorem | relowlssretop 32387 | The lower limit topology on the reals is finer than the standard topology. (Contributed by ML, 1-Aug-2020.) |
⊢ 𝐼 = ([,) “ (ℝ × ℝ)) ⇒ ⊢ (topGen‘ran (,)) ⊆ (topGen‘𝐼) | ||
Theorem | relowlpssretop 32388 | The lower limit topology on the reals is strictly finer than the standard topology. (Contributed by ML, 2-Aug-2020.) |
⊢ 𝐼 = ([,) “ (ℝ × ℝ)) ⇒ ⊢ (topGen‘ran (,)) ⊊ (topGen‘𝐼) | ||
Theorem | sucneqond 32389 | Inequality of an ordinal set with its successor. Does not use the axiom of regularity. (Contributed by ML, 18-Oct-2020.) |
⊢ (𝜑 → 𝑋 = suc 𝑌) & ⊢ (𝜑 → 𝑌 ∈ On) ⇒ ⊢ (𝜑 → 𝑋 ≠ 𝑌) | ||
Theorem | sucneqoni 32390 | Inequality of an ordinal set with its successor. Does not use the axiom of regularity. (Contributed by ML, 18-Oct-2020.) |
⊢ 𝑋 = suc 𝑌 & ⊢ 𝑌 ∈ On ⇒ ⊢ 𝑋 ≠ 𝑌 | ||
Theorem | onsucuni3 32391 | If an ordinal number has a predecessor, then it is successor of that predecessor. (Contributed by ML, 17-Oct-2020.) |
⊢ ((𝐵 ∈ On ∧ 𝐵 ≠ ∅ ∧ ¬ Lim 𝐵) → 𝐵 = suc ∪ 𝐵) | ||
Theorem | 1oequni2o 32392 | The ordinal number 1𝑜 is the predecessor of the ordinal number 2𝑜. (Contributed by ML, 19-Oct-2020.) |
⊢ 1𝑜 = ∪ 2𝑜 | ||
Theorem | rdgsucuni 32393 | If an ordinal number has a predecessor, the value of the recursive definition generator at that number in terms of its predecessor. (Contributed by ML, 17-Oct-2020.) |
⊢ ((𝐵 ∈ On ∧ 𝐵 ≠ ∅ ∧ ¬ Lim 𝐵) → (rec(𝐹, 𝐼)‘𝐵) = (𝐹‘(rec(𝐹, 𝐼)‘∪ 𝐵))) | ||
Theorem | rdgeqoa 32394 | If a recursive function with an initial value 𝐴 at step 𝑁 is equal to itself with an initial value 𝐵 at step 𝑀, then every finite number of successor steps will also be equal. (Contributed by ML, 21-Oct-2020.) |
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑋 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +𝑜 𝑋)) = (rec(𝐹, 𝐵)‘(𝑀 +𝑜 𝑋)))) | ||
Theorem | elxp8 32395 | Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp7 7092. (Contributed by ML, 19-Oct-2020.) |
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ((1st ‘𝐴) ∈ 𝐵 ∧ 𝐴 ∈ (V × 𝐶))) | ||
Syntax | cfinxp 32396 | Extend the definition of a class to include Cartesian exponentiation. |
class (𝑈↑↑𝑁) | ||
Definition | df-finxp 32397* |
Define Cartesian exponentiation on a class.
Note that this definition is limited to finite exponents, since it is defined using nested ordered pairs. If tuples of infinite length are needed, or if they might be needed in the future, use df-ixp 7795 or df-map 7746 instead. The main advantage of this definition is that it integrates better with functions and relations. For example if 𝑅 is a subset of (𝐴↑↑2𝑜), then df-br 4584 can be used on it, and df-fv 5812 can also be used, and so on. It's also worth keeping in mind that ((𝑈↑↑𝑀) × (𝑈↑↑𝑁)) is generally not equal to (𝑈↑↑(𝑀 +𝑜 𝑁)). This definition is technical. Use finxp1o 32405 and finxpsuc 32411 for a more standard recursive experience. (Contributed by ML, 16-Oct-2020.) |
⊢ (𝑈↑↑𝑁) = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈𝑁, 𝑦〉)‘𝑁))} | ||
Theorem | dffinxpf 32398* | This theorem is the same as the definition df-finxp 32397, except that the large function is replaced by a class variable for brevity. (Contributed by ML, 24-Oct-2020.) |
⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) ⇒ ⊢ (𝑈↑↑𝑁) = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec(𝐹, 〈𝑁, 𝑦〉)‘𝑁))} | ||
Theorem | finxpeq1 32399 | Equality theorem for Cartesian exponentiation. (Contributed by ML, 19-Oct-2020.) |
⊢ (𝑈 = 𝑉 → (𝑈↑↑𝑁) = (𝑉↑↑𝑁)) | ||
Theorem | finxpeq2 32400 | Equality theorem for Cartesian exponentiation. (Contributed by ML, 19-Oct-2020.) |
⊢ (𝑀 = 𝑁 → (𝑈↑↑𝑀) = (𝑈↑↑𝑁)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |