| Metamath
Proof Explorer Theorem List (p. 373 of 494) | < 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: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Syntax | cccinftyN 37201 | Syntax for the circle at infinity ℂ∞N. |
| class ℂ∞N | ||
| Definition | df-bj-ccinftyN 37202 | Definition of the circle at infinity ℂ∞N. (Contributed by BJ, 22-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.) |
| ⊢ ℂ∞N = ran +∞eiτ | ||
| Theorem | bj-inftyexpitaufo 37203 | The function +∞eiτ written as a surjection with domain and range. (Contributed by BJ, 4-Feb-2023.) |
| ⊢ +∞eiτ:ℝ–onto→ℂ∞N | ||
| Syntax | chalf 37204 | Syntax for the temporary one-half. |
| class 1/2 | ||
| Definition | df-bj-onehalf 37205 |
Define the temporary real "one-half". Once the machinery is
developed,
the real number "one-half" is commonly denoted by (1 / 2).
(Contributed by BJ, 4-Feb-2023.) (New usage is discouraged.)
TODO: $p |- 1/2 e. R. $= ? $. (riotacl 7405) $p |- -. 0R = 1/2 $= ? $. (since -. ( 0R +R 0R ) = 1R ) $p |- 0R <R 1/2 $= ? $. $p |- 1/2 <R 1R $= ? $. $p |- ( {R ` 0R ) = 0R $= ? $. $p |- ( {R ` 1/2 ) = 1/2 $= ? $. df-minfty $a |- minfty = ( inftyexpitau ` <. 1/2 , 0R >. ) $. |
| ⊢ 1/2 = (℩𝑥 ∈ R (𝑥 +R 𝑥) = 1R) | ||
| Theorem | bj-inftyexpitaudisj 37206 | An element of the circle at infinity is not a complex number. (Contributed by BJ, 4-Feb-2023.) |
| ⊢ ¬ (+∞eiτ‘𝐴) ∈ ℂ | ||
| Syntax | cinftyexpi 37207 | Syntax for the function +∞ei parameterizing ℂ∞. |
| class +∞ei | ||
| Definition | df-bj-inftyexpi 37208 | Definition of the auxiliary function +∞ei parameterizing the circle at infinity ℂ∞ in ℂ̅. We use coupling with ℂ to simplify the proof of bj-ccinftydisj 37214. It could seem more natural to define +∞ei on all of ℝ, but we want to use only basic functions in the definition of ℂ̅. TODO: transition to df-bj-inftyexpitau 37200 instead. (Contributed by BJ, 22-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.) |
| ⊢ +∞ei = (𝑥 ∈ (-π(,]π) ↦ 〈𝑥, ℂ〉) | ||
| Theorem | bj-inftyexpiinv 37209 | Utility theorem for the inverse of +∞ei. (Contributed by BJ, 22-Jun-2019.) This utility theorem is irrelevant and should generally not be used. (New usage is discouraged.) |
| ⊢ (𝐴 ∈ (-π(,]π) → (1st ‘(+∞ei‘𝐴)) = 𝐴) | ||
| Theorem | bj-inftyexpiinj 37210 | Injectivity of the parameterization +∞ei. Remark: a more conceptual proof would use bj-inftyexpiinv 37209 and the fact that a function with a retraction is injective. (Contributed by BJ, 22-Jun-2019.) |
| ⊢ ((𝐴 ∈ (-π(,]π) ∧ 𝐵 ∈ (-π(,]π)) → (𝐴 = 𝐵 ↔ (+∞ei‘𝐴) = (+∞ei‘𝐵))) | ||
| Theorem | bj-inftyexpidisj 37211 | An element of the circle at infinity is not a complex number. (Contributed by BJ, 22-Jun-2019.) This utility theorem is irrelevant and should generally not be used. (New usage is discouraged.) |
| ⊢ ¬ (+∞ei‘𝐴) ∈ ℂ | ||
| Syntax | cccinfty 37212 | Syntax for the circle at infinity ℂ∞. |
| class ℂ∞ | ||
| Definition | df-bj-ccinfty 37213 | Definition of the circle at infinity ℂ∞. (Contributed by BJ, 22-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.) |
| ⊢ ℂ∞ = ran +∞ei | ||
| Theorem | bj-ccinftydisj 37214 | The circle at infinity is disjoint from the set of complex numbers. (Contributed by BJ, 22-Jun-2019.) |
| ⊢ (ℂ ∩ ℂ∞) = ∅ | ||
| Theorem | bj-elccinfty 37215 | A lemma for infinite extended complex numbers. (Contributed by BJ, 27-Jun-2019.) |
| ⊢ (𝐴 ∈ (-π(,]π) → (+∞ei‘𝐴) ∈ ℂ∞) | ||
| Syntax | cccbar 37216 | Syntax for the set of extended complex numbers ℂ̅. |
| class ℂ̅ | ||
| Definition | df-bj-ccbar 37217 | Definition of the set of extended complex numbers ℂ̅. (Contributed by BJ, 22-Jun-2019.) |
| ⊢ ℂ̅ = (ℂ ∪ ℂ∞) | ||
| Theorem | bj-ccssccbar 37218 | Complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.) |
| ⊢ ℂ ⊆ ℂ̅ | ||
| Theorem | bj-ccinftyssccbar 37219 | Infinite extended complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.) |
| ⊢ ℂ∞ ⊆ ℂ̅ | ||
| Syntax | cpinfty 37220 | Syntax for "plus infinity". |
| class +∞ | ||
| Definition | df-bj-pinfty 37221 | Definition of "plus infinity". (Contributed by BJ, 27-Jun-2019.) |
| ⊢ +∞ = (+∞ei‘0) | ||
| Theorem | bj-pinftyccb 37222 | The class +∞ is an extended complex number. (Contributed by BJ, 27-Jun-2019.) |
| ⊢ +∞ ∈ ℂ̅ | ||
| Theorem | bj-pinftynrr 37223 | The extended complex number +∞ is not a complex number. (Contributed by BJ, 27-Jun-2019.) |
| ⊢ ¬ +∞ ∈ ℂ | ||
| Syntax | cminfty 37224 | Syntax for "minus infinity". |
| class -∞ | ||
| Definition | df-bj-minfty 37225 | Definition of "minus infinity". (Contributed by BJ, 27-Jun-2019.) |
| ⊢ -∞ = (+∞ei‘π) | ||
| Theorem | bj-minftyccb 37226 | The class -∞ is an extended complex number. (Contributed by BJ, 27-Jun-2019.) |
| ⊢ -∞ ∈ ℂ̅ | ||
| Theorem | bj-minftynrr 37227 | The extended complex number -∞ is not a complex number. (Contributed by BJ, 27-Jun-2019.) |
| ⊢ ¬ -∞ ∈ ℂ | ||
| Theorem | bj-pinftynminfty 37228 | The extended complex numbers +∞ and -∞ are different. (Contributed by BJ, 27-Jun-2019.) |
| ⊢ +∞ ≠ -∞ | ||
| Syntax | crrbar 37229 | Syntax for the set of extended real numbers. |
| class ℝ̅ | ||
| Definition | df-bj-rrbar 37230 | Definition of the set of extended real numbers. This aims to replace df-xr 11299. (Contributed by BJ, 29-Jun-2019.) |
| ⊢ ℝ̅ = (ℝ ∪ {-∞, +∞}) | ||
| Syntax | cinfty 37231 | Syntax for ∞. |
| class ∞ | ||
| Definition | df-bj-infty 37232 | Definition of ∞, the point at infinity of the real or complex projective line. (Contributed by BJ, 27-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.) |
| ⊢ ∞ = 𝒫 ∪ ℂ | ||
| Syntax | ccchat 37233 | Syntax for ℂ̂. |
| class ℂ̂ | ||
| Definition | df-bj-cchat 37234 | Define the complex projective line, or Riemann sphere. (Contributed by BJ, 27-Jun-2019.) |
| ⊢ ℂ̂ = (ℂ ∪ {∞}) | ||
| Syntax | crrhat 37235 | Syntax for ℝ̂. |
| class ℝ̂ | ||
| Definition | df-bj-rrhat 37236 | Define the real projective line. (Contributed by BJ, 27-Jun-2019.) |
| ⊢ ℝ̂ = (ℝ ∪ {∞}) | ||
| Theorem | bj-rrhatsscchat 37237 | The real projective line is included in the complex projective line. (Contributed by BJ, 27-Jun-2019.) |
| ⊢ ℝ̂ ⊆ ℂ̂ | ||
We define the operations of addition and opposite on the extended complex numbers and on the complex projective line (Riemann sphere) simultaneously, thus "overloading" the operations. | ||
| Syntax | caddcc 37238 | Syntax for the addition on extended complex numbers. |
| class +ℂ̅ | ||
| Definition | df-bj-addc 37239 | Define the additions on the extended complex numbers (on the subset of (ℂ̅ × ℂ̅) where it makes sense) and on the complex projective line (Riemann sphere). We use the plural in "additions" since these are two different operations, even though +ℂ̅ is overloaded. (Contributed by BJ, 22-Jun-2019.) |
| ⊢ +ℂ̅ = (𝑥 ∈ (((ℂ × ℂ̅) ∪ (ℂ̅ × ℂ)) ∪ ((ℂ̂ × ℂ̂) ∪ ( I ↾ ℂ∞))) ↦ if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if((1st ‘𝑥) ∈ ℂ, if((2nd ‘𝑥) ∈ ℂ, 〈((1st ‘(1st ‘𝑥)) +R (1st ‘(2nd ‘𝑥))), ((2nd ‘(1st ‘𝑥)) +R (2nd ‘(2nd ‘𝑥)))〉, (2nd ‘𝑥)), (1st ‘𝑥)))) | ||
| Syntax | coppcc 37240 | Syntax for negation on the set of extended complex numbers and the complex projective line (Riemann sphere). |
| class -ℂ̅ | ||
| Definition | df-bj-oppc 37241* | Define the negation (operation giving the opposite) on the set of extended complex numbers and the complex projective line (Riemann sphere). (Contributed by BJ, 22-Jun-2019.) |
| ⊢ -ℂ̅ = (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = ∞, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 +ℂ̅ 𝑦) = 0), (+∞eiτ‘(𝑥 +ℂ̅ 〈1/2, 0R〉))))) | ||
In this section, we redefine df-ltxr 11300 without the intermediate step of df-lt 11168. | ||
| Syntax | cltxr 37242 | Syntax for the standard (strict) order on the extended reals. |
| class <ℝ̅ | ||
| Definition | df-bj-lt 37243* | Define the standard (strict) order on the extended reals. (Contributed by BJ, 4-Feb-2023.) |
| ⊢ <ℝ̅ = ({𝑥 ∈ (ℝ̅ × ℝ̅) ∣ ∃𝑦∃𝑧(((1st ‘𝑥) = 〈𝑦, 0R〉 ∧ (2nd ‘𝑥) = 〈𝑧, 0R〉) ∧ 𝑦 <R 𝑧)} ∪ ((({-∞} × ℝ) ∪ (ℝ × {+∞})) ∪ ({-∞} × {+∞}))) | ||
Since one needs arguments in order to define multiplication in ℂ̅, and one needs complex multiplication in order to define arguments, it would be contrived to construct a whole theory for a temporary multiplication (and temporary powers, then temporary logarithm, and finally temporary argument) before redefining the extended complex multiplication. Therefore, we adopt a two-step process, see df-bj-mulc 37247. | ||
| Syntax | carg 37244 | Syntax for the argument of a nonzero extended complex number. |
| class Arg | ||
| Definition | df-bj-arg 37245 | Define the argument of a nonzero extended complex number. By convention, it has values in (-π, π]. Another convention chooses values in [0, 2π) but the present convention simplifies formulas giving the argument as an arctangent. (Contributed by BJ, 22-Jun-2019.) The "else" case of the second conditional operator, corresponding to infinite extended complex numbers other than -∞, gives a definition depending on the specific definition chosen for these numbers (df-bj-inftyexpitau 37200), and therefore should not be relied upon. (New usage is discouraged.) |
| ⊢ Arg = (𝑥 ∈ (ℂ̅ ∖ {0}) ↦ if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π, (((1st ‘𝑥) / (2 · π)) − π)))) | ||
| Syntax | cmulc 37246 | Syntax for the multiplication of extended complex numbers. |
| class ·ℂ̅ | ||
| Definition | df-bj-mulc 37247 |
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 (given df-bj-invc 37249).
Note that this definition uses · and Arg and /. Indeed, it would be contrived to bypass ordinary complex multiplication, and the present two-step definition looks like a good compromise. (Contributed by BJ, 22-Jun-2019.) |
| ⊢ ·ℂ̅ = (𝑥 ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ↦ if(((1st ‘𝑥) = 0 ∨ (2nd ‘𝑥) = 0), 0, if(((1st ‘𝑥) = ∞ ∨ (2nd ‘𝑥) = ∞), ∞, if(𝑥 ∈ (ℂ × ℂ), ((1st ‘𝑥) · (2nd ‘𝑥)), (+∞eiτ‘(((Arg‘(1st ‘𝑥)) +ℂ̅ (Arg‘(2nd ‘𝑥))) / τ)))))) | ||
| Syntax | cinvc 37248 | Syntax for the inverse of nonzero extended complex numbers. |
| class -1ℂ̅ | ||
| Definition | df-bj-invc 37249* | 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) ∉ ℂ̅. Note that this definition relies on df-bj-mulc 37247, which does not bypass ordinary complex multiplication, but defines extended complex multiplication on top of it. Therefore, we could have used directly / instead of (℩... ·ℂ̅ ...). (Contributed by BJ, 22-Jun-2019.) |
| ⊢ -1ℂ̅ = (𝑥 ∈ (ℂ̅ ∪ ℂ̂) ↦ if(𝑥 = 0, ∞, if(𝑥 ∈ ℂ, (℩𝑦 ∈ ℂ (𝑥 ·ℂ̅ 𝑦) = 1), 0))) | ||
| Syntax | ciomnn 37250 | Syntax for the canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}). |
| class iω↪ℕ | ||
| Definition | df-bj-iomnn 37251* |
Definition of the canonical bijection from (ω ∪
{ω}) onto
(ℕ0 ∪ {+∞}).
To understand this definition, recall that set.mm constructs reals as couples whose first component is a prereal and second component is the zero prereal (in order that one have ℝ ⊆ ℂ), that prereals are equivalence classes of couples of positive reals, the latter are Dedekind cuts of positive rationals, which are equivalence classes of positive ordinals. In partiular, we take the successor ordinal at the beginning and subtract 1 at the end since the intermediate systems contain only (strictly) positive numbers. Note the similarity with df-bj-fractemp 37198 but we did not use the present definition there since we wanted to have defined +∞ first. See bj-iomnnom 37260 for its value at +∞. TODO: Prove ⊢ (iω↪ℕ‘∅) = 0. Define ⊢ ℕ0 = (iω↪ℕ “ ω) and ⊢ ℕ = (ℕ0 ∖ {0}). Prove ⊢ iω↪ℕ:(ω ∪ {ω})–1-1-onto→(ℕ0 ∪ {+∞}) and ⊢ (iω↪ℕ ↾ ω):ω–1-1-onto→ℕ0. Prove that these bijections are respectively an isomorphism of ordered "extended rigs" and of ordered rigs. Prove ⊢ (iω↪ℕ ↾ ω) = rec((𝑥 ∈ ℝ ↦ (𝑥 + 1)), 0). (Contributed by BJ, 18-Feb-2023.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.) |
| ⊢ iω↪ℕ = ((𝑛 ∈ ω ↦ 〈[〈{𝑟 ∈ Q ∣ 𝑟 <Q 〈suc 𝑛, 1o〉}, 1P〉] ~R , 0R〉) ∪ {〈ω, +∞〉}) | ||
| Theorem | bj-imafv 37252 | If the direct image of a singleton under any of two functions is the same, then the values of these functions at the corresponding point agree. (Contributed by BJ, 18-Mar-2023.) |
| ⊢ ((𝐹 “ {𝐴}) = (𝐺 “ {𝐴}) → (𝐹‘𝐴) = (𝐺‘𝐴)) | ||
| Theorem | bj-funun 37253 | Value of a function expressed as a union of two functions at a point not in the domain of one of them. (Contributed by BJ, 18-Mar-2023.) |
| ⊢ (𝜑 → 𝐹 = (𝐺 ∪ 𝐻)) & ⊢ (𝜑 → ¬ 𝐴 ∈ dom 𝐻) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴)) | ||
| Theorem | bj-fununsn1 37254 | Value of a function expressed as a union of a function and a singleton on a couple (with disjoint domain) at a point not equal to the first component of that couple. (Contributed by BJ, 18-Mar-2023.) (Proof modification is discouraged.) |
| ⊢ (𝜑 → 𝐹 = (𝐺 ∪ {〈𝐵, 𝐶〉})) & ⊢ (𝜑 → ¬ 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴)) | ||
| Theorem | bj-fununsn2 37255 | Value of a function expressed as a union of a function and a singleton on a couple (with disjoint domain) at the first component of that couple. (Contributed by BJ, 18-Mar-2023.) (Proof modification is discouraged.) |
| ⊢ (𝜑 → 𝐹 = (𝐺 ∪ {〈𝐵, 𝐶〉})) & ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐺) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐹‘𝐵) = 𝐶) | ||
| Theorem | bj-fvsnun1 37256 | The value of a function with one of its ordered pairs replaced, at arguments other than the replaced one. (Contributed by NM, 23-Sep-2007.) Put in deduction form and remove two sethood hypotheses. (Revised by BJ, 18-Mar-2023.) |
| ⊢ (𝜑 → 𝐺 = ((𝐹 ↾ (𝐶 ∖ {𝐴})) ∪ {〈𝐴, 𝐵〉})) & ⊢ (𝜑 → 𝐷 ∈ (𝐶 ∖ {𝐴})) ⇒ ⊢ (𝜑 → (𝐺‘𝐷) = (𝐹‘𝐷)) | ||
| Theorem | bj-fvsnun2 37257 | The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 7203. (Contributed by NM, 23-Sep-2007.) Put in deduction form. (Revised by BJ, 18-Mar-2023.) (Proof modification is discouraged.) |
| ⊢ (𝜑 → 𝐺 = ((𝐹 ↾ (𝐶 ∖ {𝐴})) ∪ {〈𝐴, 𝐵〉})) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐺‘𝐴) = 𝐵) | ||
| Theorem | bj-fvmptunsn1 37258* | Value of a function expressed as a union of a mapsto expression and a singleton on a couple (with disjoint domain) at the first component of that couple. (Contributed by BJ, 18-Mar-2023.) (Proof modification is discouraged.) |
| ⊢ (𝜑 → 𝐹 = ((𝑥 ∈ 𝐴 ↦ 𝐵) ∪ {〈𝐶, 𝐷〉})) & ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐹‘𝐶) = 𝐷) | ||
| Theorem | bj-fvmptunsn2 37259* | Value of a function expressed as a union of a mapsto expression and a singleton on a couple (with disjoint domain) at a point in the domain of the mapsto construction. (Contributed by BJ, 18-Mar-2023.) (Proof modification is discouraged.) |
| ⊢ (𝜑 → 𝐹 = ((𝑥 ∈ 𝐴 ↦ 𝐵) ∪ {〈𝐶, 𝐷〉})) & ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐸 ∈ 𝐴) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝐸) → 𝐵 = 𝐺) ⇒ ⊢ (𝜑 → (𝐹‘𝐸) = 𝐺) | ||
| Theorem | bj-iomnnom 37260 | The canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}) maps ω to +∞. (Contributed by BJ, 18-Feb-2023.) |
| ⊢ (iω↪ℕ‘ω) = +∞ | ||
| Syntax | cnnbar 37261 | Syntax for the extended natural numbers. |
| class ℕ̅ | ||
| Definition | df-bj-nnbar 37262 | Definition of the extended natural numbers. (Contributed by BJ, 28-Jul-2023.) |
| ⊢ ℕ̅ = (ℕ0 ∪ {+∞}) | ||
| Syntax | czzbar 37263 | Syntax for the extended integers. |
| class ℤ̅ | ||
| Definition | df-bj-zzbar 37264 | Definition of the extended integers. (Contributed by BJ, 28-Jul-2023.) |
| ⊢ ℤ̅ = (ℤ ∪ {-∞, +∞}) | ||
| Syntax | czzhat 37265 | Syntax for the one-point-compactified integers. |
| class ℤ̂ | ||
| Definition | df-bj-zzhat 37266 | Definition of the one-point-compactified. (Contributed by BJ, 28-Jul-2023.) |
| ⊢ ℤ̂ = (ℤ ∪ {∞}) | ||
| Syntax | cdivc 37267 | Syntax for the divisibility relation. |
| class ∥ℂ | ||
| Definition | df-bj-divc 37268* |
Definition of the divisibility relation (compare df-dvds 16291).
Since 0 is absorbing, ⊢ (𝐴 ∈ (ℂ̅ ∪ ℂ̂) → (𝐴 ∥ℂ 0)) and ⊢ ((0 ∥ℂ 𝐴) ↔ 𝐴 = 0). (Contributed by BJ, 28-Jul-2023.) |
| ⊢ ∥ℂ = {〈𝑥, 𝑦〉 ∣ (〈𝑥, 𝑦〉 ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)} | ||
See ccmn 19798 and subsequents. The first few statements of this subsection can be put very early after ccmn 19798. Proposal: in the main part, make separate subsections of commutative monoids and abelian groups. Relabel cabl 19799 to "cabl" or, preferably, other labels containing "abl" to "abel", for consistency. | ||
| Theorem | bj-smgrpssmgm 37269 | Semigroups are magmas. (Contributed by BJ, 12-Apr-2024.) (Proof modification is discouraged.) |
| ⊢ Smgrp ⊆ Mgm | ||
| Theorem | bj-smgrpssmgmel 37270 | Semigroups are magmas (elemental version). (Contributed by BJ, 12-Apr-2024.) (Proof modification is discouraged.) |
| ⊢ (𝐺 ∈ Smgrp → 𝐺 ∈ Mgm) | ||
| Theorem | bj-mndsssmgrp 37271 | Monoids are semigroups. (Contributed by BJ, 11-Apr-2024.) (Proof modification is discouraged.) |
| ⊢ Mnd ⊆ Smgrp | ||
| Theorem | bj-mndsssmgrpel 37272 | Monoids are semigroups (elemental version). (Contributed by BJ, 11-Apr-2024.) (Proof modification is discouraged.) |
| ⊢ (𝐺 ∈ Mnd → 𝐺 ∈ Smgrp) | ||
| Theorem | bj-cmnssmnd 37273 | Commutative monoids are monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
| ⊢ CMnd ⊆ Mnd | ||
| Theorem | bj-cmnssmndel 37274 | Commutative monoids are monoids (elemental version). This is a more direct proof of cmnmnd 19815, which relies on iscmn 19807. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
| ⊢ (𝐴 ∈ CMnd → 𝐴 ∈ Mnd) | ||
| Theorem | bj-grpssmnd 37275 | Groups are monoids. (Contributed by BJ, 5-Jan-2024.) (Proof modification is discouraged.) |
| ⊢ Grp ⊆ Mnd | ||
| Theorem | bj-grpssmndel 37276 | Groups are monoids (elemental version). Shorter proof of grpmnd 18958. (Contributed by BJ, 5-Jan-2024.) (Proof modification is discouraged.) |
| ⊢ (𝐴 ∈ Grp → 𝐴 ∈ Mnd) | ||
| Theorem | bj-ablssgrp 37277 | Abelian groups are groups. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
| ⊢ Abel ⊆ Grp | ||
| Theorem | bj-ablssgrpel 37278 | Abelian groups are groups (elemental version). This is a shorter proof of ablgrp 19803. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
| ⊢ (𝐴 ∈ Abel → 𝐴 ∈ Grp) | ||
| Theorem | bj-ablsscmn 37279 | Abelian groups are commutative monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
| ⊢ Abel ⊆ CMnd | ||
| Theorem | bj-ablsscmnel 37280 | Abelian groups are commutative monoids (elemental version). This is a shorter proof of ablcmn 19805. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
| ⊢ (𝐴 ∈ Abel → 𝐴 ∈ CMnd) | ||
| Theorem | bj-modssabl 37281 | (The additive groups of) modules are abelian groups. (The elemental version is lmodabl 20907; see also lmodgrp 20865 and lmodcmn 20908.) (Contributed by BJ, 9-Jun-2019.) |
| ⊢ LMod ⊆ Abel | ||
| Theorem | bj-vecssmod 37282 | Vector spaces are modules. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
| ⊢ LVec ⊆ LMod | ||
| Theorem | bj-vecssmodel 37283 | Vector spaces are modules (elemental version). This is a shorter proof of lveclmod 21105. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
| ⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod) | ||
UPDATE: a similar summation is already defined as df-gsum 17487 (although it mixes finite and infinite sums, which makes it harder to understand). | ||
| Syntax | cfinsum 37284 | Syntax for the class "finite summation in monoids". |
| class FinSum | ||
| Definition | df-bj-finsum 37285* | 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 37286* | 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. The first step is to define real vector spaces, then barycentric coordinates and convex hulls. | ||
In this section, we introduce real vector spaces. | ||
| Theorem | bj-fvimacnv0 37287 | Variant of fvimacnv 7073 where membership of 𝐴 in the domain is not needed provided the containing class 𝐵 does not contain the empty set. Note that this antecedent would not be needed with Definition df-afv 47132. (Contributed by BJ, 7-Jan-2024.) |
| ⊢ ((Fun 𝐹 ∧ ¬ ∅ ∈ 𝐵) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵))) | ||
| Theorem | bj-isvec 37288 | The predicate "is a vector space". (Contributed by BJ, 6-Jan-2024.) |
| ⊢ (𝜑 → 𝐾 = (Scalar‘𝑉)) ⇒ ⊢ (𝜑 → (𝑉 ∈ LVec ↔ (𝑉 ∈ LMod ∧ 𝐾 ∈ DivRing))) | ||
| Theorem | bj-fldssdrng 37289 | Fields are division rings. (Contributed by BJ, 6-Jan-2024.) |
| ⊢ Field ⊆ DivRing | ||
| Theorem | bj-flddrng 37290 | Fields are division rings (elemental version). (Contributed by BJ, 9-Nov-2024.) |
| ⊢ (𝐹 ∈ Field → 𝐹 ∈ DivRing) | ||
| Theorem | bj-rrdrg 37291 | The field of real numbers is a division ring. (Contributed by BJ, 6-Jan-2024.) |
| ⊢ ℝfld ∈ DivRing | ||
| Theorem | bj-isclm 37292 | The predicate "is a subcomplex module". (Contributed by BJ, 6-Jan-2024.) |
| ⊢ (𝜑 → 𝐹 = (Scalar‘𝑊)) & ⊢ (𝜑 → 𝐾 = (Base‘𝐹)) ⇒ ⊢ (𝜑 → (𝑊 ∈ ℂMod ↔ (𝑊 ∈ LMod ∧ 𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 ∈ (SubRing‘ℂfld)))) | ||
| Syntax | crrvec 37293 | Syntax for the class of real vector spaces. |
| class ℝ-Vec | ||
| Definition | df-bj-rvec 37294 | Definition of the class of real vector spaces. The previous definition, ⊢ ℝ-Vec = {𝑥 ∈ LMod ∣ (Scalar‘𝑥) = ℝfld}, can be recovered using bj-isrvec 37295. The present one is preferred since it does not use any dummy variable. That ℝ-Vec could be defined with LVec in place of LMod is a consequence of bj-isrvec2 37301. (Contributed by BJ, 9-Jun-2019.) |
| ⊢ ℝ-Vec = (LMod ∩ (◡Scalar “ {ℝfld})) | ||
| Theorem | bj-isrvec 37295 | The predicate "is a real vector space". Using df-sca 17313 instead of scaid 17359 would shorten the proof by two syntactic steps, but it is preferable not to rely on the precise definition df-sca 17313. (Contributed by BJ, 6-Jan-2024.) |
| ⊢ (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LMod ∧ (Scalar‘𝑉) = ℝfld)) | ||
| Theorem | bj-rvecmod 37296 | Real vector spaces are modules (elemental version). (Contributed by BJ, 6-Jan-2024.) |
| ⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ LMod) | ||
| Theorem | bj-rvecssmod 37297 | Real vector spaces are modules. (Contributed by BJ, 6-Jan-2024.) |
| ⊢ ℝ-Vec ⊆ LMod | ||
| Theorem | bj-rvecrr 37298 | The field of scalars of a real vector space is the field of real numbers. (Contributed by BJ, 6-Jan-2024.) |
| ⊢ (𝑉 ∈ ℝ-Vec → (Scalar‘𝑉) = ℝfld) | ||
| Theorem | bj-isrvecd 37299 | The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024.) |
| ⊢ (𝜑 → (Scalar‘𝑉) = 𝐾) ⇒ ⊢ (𝜑 → (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LMod ∧ 𝐾 = ℝfld))) | ||
| Theorem | bj-rvecvec 37300 | Real vector spaces are vector spaces (elemental version). (Contributed by BJ, 6-Jan-2024.) |
| ⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ LVec) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |