Home | Metamath
Proof Explorer Theorem List (p. 354 of 464) | < 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-29181) |
Hilbert Space Explorer
(29182-30704) |
Users' Mathboxes
(30705-46395) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | chalf 35301 | Syntax for the temporary one-half. |
class 1/2 | ||
Definition | df-bj-onehalf 35302 |
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 7230) $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 35303 | An element of the circle at infinity is not a complex number. (Contributed by BJ, 4-Feb-2023.) |
⊢ ¬ (+∞eiτ‘𝐴) ∈ ℂ | ||
Syntax | cinftyexpi 35304 | Syntax for the function +∞ei parameterizing ℂ∞. |
class +∞ei | ||
Definition | df-bj-inftyexpi 35305 | Definition of the auxiliary function +∞ei parameterizing the circle at infinity ℂ∞ in ℂ̅. We use coupling with ℂ to simplify the proof of bj-ccinftydisj 35311. 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 35297 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 35306 | 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 35307 | Injectivity of the parameterization +∞ei. Remark: a more conceptual proof would use bj-inftyexpiinv 35306 and the fact that a function with a retraction is injective. (Contributed by BJ, 22-Jun-2019.) |
⊢ ((𝐴 ∈ (-π(,]π) ∧ 𝐵 ∈ (-π(,]π)) → (𝐴 = 𝐵 ↔ (+∞ei‘𝐴) = (+∞ei‘𝐵))) | ||
Theorem | bj-inftyexpidisj 35308 | 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 35309 | Syntax for the circle at infinity ℂ∞. |
class ℂ∞ | ||
Definition | df-bj-ccinfty 35310 | 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 35311 | The circle at infinity is disjoint from the set of complex numbers. (Contributed by BJ, 22-Jun-2019.) |
⊢ (ℂ ∩ ℂ∞) = ∅ | ||
Theorem | bj-elccinfty 35312 | A lemma for infinite extended complex numbers. (Contributed by BJ, 27-Jun-2019.) |
⊢ (𝐴 ∈ (-π(,]π) → (+∞ei‘𝐴) ∈ ℂ∞) | ||
Syntax | cccbar 35313 | Syntax for the set of extended complex numbers ℂ̅. |
class ℂ̅ | ||
Definition | df-bj-ccbar 35314 | Definition of the set of extended complex numbers ℂ̅. (Contributed by BJ, 22-Jun-2019.) |
⊢ ℂ̅ = (ℂ ∪ ℂ∞) | ||
Theorem | bj-ccssccbar 35315 | Complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.) |
⊢ ℂ ⊆ ℂ̅ | ||
Theorem | bj-ccinftyssccbar 35316 | Infinite extended complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.) |
⊢ ℂ∞ ⊆ ℂ̅ | ||
Syntax | cpinfty 35317 | Syntax for "plus infinity". |
class +∞ | ||
Definition | df-bj-pinfty 35318 | Definition of "plus infinity". (Contributed by BJ, 27-Jun-2019.) |
⊢ +∞ = (+∞ei‘0) | ||
Theorem | bj-pinftyccb 35319 | The class +∞ is an extended complex number. (Contributed by BJ, 27-Jun-2019.) |
⊢ +∞ ∈ ℂ̅ | ||
Theorem | bj-pinftynrr 35320 | The extended complex number +∞ is not a complex number. (Contributed by BJ, 27-Jun-2019.) |
⊢ ¬ +∞ ∈ ℂ | ||
Syntax | cminfty 35321 | Syntax for "minus infinity". |
class -∞ | ||
Definition | df-bj-minfty 35322 | Definition of "minus infinity". (Contributed by BJ, 27-Jun-2019.) |
⊢ -∞ = (+∞ei‘π) | ||
Theorem | bj-minftyccb 35323 | The class -∞ is an extended complex number. (Contributed by BJ, 27-Jun-2019.) |
⊢ -∞ ∈ ℂ̅ | ||
Theorem | bj-minftynrr 35324 | The extended complex number -∞ is not a complex number. (Contributed by BJ, 27-Jun-2019.) |
⊢ ¬ -∞ ∈ ℂ | ||
Theorem | bj-pinftynminfty 35325 | The extended complex numbers +∞ and -∞ are different. (Contributed by BJ, 27-Jun-2019.) |
⊢ +∞ ≠ -∞ | ||
Syntax | crrbar 35326 | Syntax for the set of extended real numbers. |
class ℝ̅ | ||
Definition | df-bj-rrbar 35327 | Definition of the set of extended real numbers. This aims to replace df-xr 10944. (Contributed by BJ, 29-Jun-2019.) |
⊢ ℝ̅ = (ℝ ∪ {-∞, +∞}) | ||
Syntax | cinfty 35328 | Syntax for ∞. |
class ∞ | ||
Definition | df-bj-infty 35329 | 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 35330 | Syntax for ℂ̂. |
class ℂ̂ | ||
Definition | df-bj-cchat 35331 | Define the complex projective line, or Riemann sphere. (Contributed by BJ, 27-Jun-2019.) |
⊢ ℂ̂ = (ℂ ∪ {∞}) | ||
Syntax | crrhat 35332 | Syntax for ℝ̂. |
class ℝ̂ | ||
Definition | df-bj-rrhat 35333 | Define the real projective line. (Contributed by BJ, 27-Jun-2019.) |
⊢ ℝ̂ = (ℝ ∪ {∞}) | ||
Theorem | bj-rrhatsscchat 35334 | 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 35335 | Syntax for the addition on extended complex numbers. |
class +ℂ̅ | ||
Definition | df-bj-addc 35336 | 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 35337 | Syntax for negation on the set of extended complex numbers and the complex projective line (Riemann sphere). |
class -ℂ̅ | ||
Definition | df-bj-oppc 35338* | 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 10945 without the intermediate step of df-lt 10815. | ||
Syntax | cltxr 35339 | Syntax for the standard (strict) order on the extended reals. |
class <ℝ̅ | ||
Definition | df-bj-lt 35340* | 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 35344. | ||
Syntax | carg 35341 | Syntax for the argument of a nonzero extended complex number. |
class Arg | ||
Definition | df-bj-arg 35342 | 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 35297), and therefore should not be relied upon. (New usage is discouraged.) |
⊢ Arg = (𝑥 ∈ (ℂ̅ ∖ {0}) ↦ if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π, (((1st ‘𝑥) / (2 · π)) − π)))) | ||
Syntax | cmulc 35343 | Syntax for the multiplication of extended complex numbers. |
class ·ℂ̅ | ||
Definition | df-bj-mulc 35344 |
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 35346).
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 35345 | Syntax for the inverse of nonzero extended complex numbers. |
class -1ℂ̅ | ||
Definition | df-bj-invc 35346* | 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 35344, 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 35347 | Syntax for the canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}). |
class iω↪ℕ | ||
Definition | df-bj-iomnn 35348* |
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 35295 but we did not use the present definition there since we wanted to have defined +∞ first. See bj-iomnnom 35357 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 35349 | 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 35350 | 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 35351 | 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 35352 | 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 35353 | 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 35354 | The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 7037. (Contributed by NM, 23-Sep-2007.) Put in deduction form. (Revised by BJ, 18-Mar-2023.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐺 = ((𝐹 ↾ (𝐶 ∖ {𝐴})) ∪ {〈𝐴, 𝐵〉})) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐺‘𝐴) = 𝐵) | ||
Theorem | bj-fvmptunsn1 35355* | 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 35356* | 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 35357 | The canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}) maps ω to +∞. (Contributed by BJ, 18-Feb-2023.) |
⊢ (iω↪ℕ‘ω) = +∞ | ||
Syntax | cnnbar 35358 | Syntax for the extended natural numbers. |
class ℕ̅ | ||
Definition | df-bj-nnbar 35359 | Definition of the extended natural numbers. (Contributed by BJ, 28-Jul-2023.) |
⊢ ℕ̅ = (ℕ0 ∪ {+∞}) | ||
Syntax | czzbar 35360 | Syntax for the extended integers. |
class ℤ̅ | ||
Definition | df-bj-zzbar 35361 | Definition of the extended integers. (Contributed by BJ, 28-Jul-2023.) |
⊢ ℤ̅ = (ℤ ∪ {-∞, +∞}) | ||
Syntax | czzhat 35362 | Syntax for the one-point-compactified integers. |
class ℤ̂ | ||
Definition | df-bj-zzhat 35363 | Definition of the one-point-compactified. (Contributed by BJ, 28-Jul-2023.) |
⊢ ℤ̂ = (ℤ ∪ {∞}) | ||
Syntax | cdivc 35364 | Syntax for the divisibility relation. |
class ∥ℂ | ||
Definition | df-bj-divc 35365* |
Definition of the divisibility relation (compare df-dvds 15892).
Since 0 is absorbing, ⊢ (𝐴 ∈ (ℂ̅ ∪ ℂ̂) → (𝐴 ∥ℂ 0)) and ⊢ ((0 ∥ℂ 𝐴) ↔ 𝐴 = 0). (Contributed by BJ, 28-Jul-2023.) |
⊢ ∥ℂ = {〈𝑥, 𝑦〉 ∣ (〈𝑥, 𝑦〉 ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)} | ||
See ccmn 19301 and subsequents. The first few statements of this subsection can be put very early after ccmn 19301. Proposal: in the main part, make separate subsections of commutative monoids and abelian groups. Relabel cabl 19302 to "cabl" or, preferably, other labels containing "abl" to "abel", for consistency. | ||
Theorem | bj-smgrpssmgm 35366 | Semigroups are magmas. (Contributed by BJ, 12-Apr-2024.) (Proof modification is discouraged.) |
⊢ Smgrp ⊆ Mgm | ||
Theorem | bj-smgrpssmgmel 35367 | Semigroups are magmas (elemental version). (Contributed by BJ, 12-Apr-2024.) (Proof modification is discouraged.) |
⊢ (𝐺 ∈ Smgrp → 𝐺 ∈ Mgm) | ||
Theorem | bj-mndsssmgrp 35368 | Monoids are semigroups. (Contributed by BJ, 11-Apr-2024.) (Proof modification is discouraged.) |
⊢ Mnd ⊆ Smgrp | ||
Theorem | bj-mndsssmgrpel 35369 | Monoids are semigroups (elemental version). (Contributed by BJ, 11-Apr-2024.) (Proof modification is discouraged.) |
⊢ (𝐺 ∈ Mnd → 𝐺 ∈ Smgrp) | ||
Theorem | bj-cmnssmnd 35370 | Commutative monoids are monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ CMnd ⊆ Mnd | ||
Theorem | bj-cmnssmndel 35371 | Commutative monoids are monoids (elemental version). This is a more direct proof of cmnmnd 19317, which relies on iscmn 19309. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ CMnd → 𝐴 ∈ Mnd) | ||
Theorem | bj-grpssmnd 35372 | Groups are monoids. (Contributed by BJ, 5-Jan-2024.) (Proof modification is discouraged.) |
⊢ Grp ⊆ Mnd | ||
Theorem | bj-grpssmndel 35373 | Groups are monoids (elemental version). Shorter proof of grpmnd 18499. (Contributed by BJ, 5-Jan-2024.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ Grp → 𝐴 ∈ Mnd) | ||
Theorem | bj-ablssgrp 35374 | Abelian groups are groups. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ Abel ⊆ Grp | ||
Theorem | bj-ablssgrpel 35375 | Abelian groups are groups (elemental version). This is a shorter proof of ablgrp 19306. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ Abel → 𝐴 ∈ Grp) | ||
Theorem | bj-ablsscmn 35376 | Abelian groups are commutative monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ Abel ⊆ CMnd | ||
Theorem | bj-ablsscmnel 35377 | Abelian groups are commutative monoids (elemental version). This is a shorter proof of ablcmn 19308. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ Abel → 𝐴 ∈ CMnd) | ||
Theorem | bj-modssabl 35378 | (The additive groups of) modules are abelian groups. (The elemental version is lmodabl 20085; see also lmodgrp 20045 and lmodcmn 20086.) (Contributed by BJ, 9-Jun-2019.) |
⊢ LMod ⊆ Abel | ||
Theorem | bj-vecssmod 35379 | Vector spaces are modules. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ LVec ⊆ LMod | ||
Theorem | bj-vecssmodel 35380 | Vector spaces are modules (elemental version). This is a shorter proof of lveclmod 20283. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod) | ||
UPDATE: a similar summation is already defined as df-gsum 17070 (although it mixes finite and infinite sums, which makes it harder to understand). | ||
Syntax | cfinsum 35381 | Syntax for the class "finite summation in monoids". |
class FinSum | ||
Definition | df-bj-finsum 35382* | 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 35383* | 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 35384 | Variant of fvimacnv 6912 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 44499. (Contributed by BJ, 7-Jan-2024.) |
⊢ ((Fun 𝐹 ∧ ¬ ∅ ∈ 𝐵) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵))) | ||
Theorem | bj-isvec 35385 | The predicate "is a vector space". (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝜑 → 𝐾 = (Scalar‘𝑉)) ⇒ ⊢ (𝜑 → (𝑉 ∈ LVec ↔ (𝑉 ∈ LMod ∧ 𝐾 ∈ DivRing))) | ||
Theorem | bj-fldssdrng 35386 | Fields are division rings. (Contributed by BJ, 6-Jan-2024.) |
⊢ Field ⊆ DivRing | ||
Theorem | bj-flddrng 35387 | Fields are division rings (elemental version). (Contributed by BJ, 9-Nov-2024.) |
⊢ (𝐹 ∈ Field → 𝐹 ∈ DivRing) | ||
Theorem | bj-rrdrg 35388 | The field of real numbers is a division ring. (Contributed by BJ, 6-Jan-2024.) |
⊢ ℝfld ∈ DivRing | ||
Theorem | bj-isclm 35389 | The predicate "is a subcomplex module". (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝜑 → 𝐹 = (Scalar‘𝑊)) & ⊢ (𝜑 → 𝐾 = (Base‘𝐹)) ⇒ ⊢ (𝜑 → (𝑊 ∈ ℂMod ↔ (𝑊 ∈ LMod ∧ 𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 ∈ (SubRing‘ℂfld)))) | ||
Syntax | crrvec 35390 | Syntax for the class of real vector spaces. |
class ℝ-Vec | ||
Definition | df-bj-rvec 35391 | Definition of the class of real vector spaces. The previous definition, ⊢ ℝ-Vec = {𝑥 ∈ LMod ∣ (Scalar‘𝑥) = ℝfld}, can be recovered using bj-isrvec 35392. 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 35398. (Contributed by BJ, 9-Jun-2019.) |
⊢ ℝ-Vec = (LMod ∩ (◡Scalar “ {ℝfld})) | ||
Theorem | bj-isrvec 35392 | The predicate "is a real vector space". Using df-sca 16904 instead of scaid 16951 would shorten the proof by two syntactic steps, but it is preferable not to rely on the precise definition df-sca 16904. (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LMod ∧ (Scalar‘𝑉) = ℝfld)) | ||
Theorem | bj-rvecmod 35393 | Real vector spaces are modules (elemental version). (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ LMod) | ||
Theorem | bj-rvecssmod 35394 | Real vector spaces are modules. (Contributed by BJ, 6-Jan-2024.) |
⊢ ℝ-Vec ⊆ LMod | ||
Theorem | bj-rvecrr 35395 | 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 35396 | The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝜑 → (Scalar‘𝑉) = 𝐾) ⇒ ⊢ (𝜑 → (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LMod ∧ 𝐾 = ℝfld))) | ||
Theorem | bj-rvecvec 35397 | Real vector spaces are vector spaces (elemental version). (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ LVec) | ||
Theorem | bj-isrvec2 35398 | The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝜑 → (Scalar‘𝑉) = 𝐾) ⇒ ⊢ (𝜑 → (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LVec ∧ 𝐾 = ℝfld))) | ||
Theorem | bj-rvecssvec 35399 | Real vector spaces are vector spaces. (Contributed by BJ, 6-Jan-2024.) |
⊢ ℝ-Vec ⊆ LVec | ||
Theorem | bj-rveccmod 35400 | Real vector spaces are subcomplex modules (elemental version). (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ ℂMod) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |