Home | Metamath
Proof Explorer Theorem List (p. 346 of 450) | < 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-28698) |
Hilbert Space Explorer
(28699-30221) |
Users' Mathboxes
(30222-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cccbar 34501 | Syntax for the set of extended complex numbers ℂ̅. |
class ℂ̅ | ||
Definition | df-bj-ccbar 34502 | Definition of the set of extended complex numbers ℂ̅. (Contributed by BJ, 22-Jun-2019.) |
⊢ ℂ̅ = (ℂ ∪ ℂ∞) | ||
Theorem | bj-ccssccbar 34503 | Complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.) |
⊢ ℂ ⊆ ℂ̅ | ||
Theorem | bj-ccinftyssccbar 34504 | Infinite extended complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.) |
⊢ ℂ∞ ⊆ ℂ̅ | ||
Syntax | cpinfty 34505 | Syntax for "plus infinity". |
class +∞ | ||
Definition | df-bj-pinfty 34506 | Definition of "plus infinity". (Contributed by BJ, 27-Jun-2019.) |
⊢ +∞ = (+∞ei‘0) | ||
Theorem | bj-pinftyccb 34507 | The class +∞ is an extended complex number. (Contributed by BJ, 27-Jun-2019.) |
⊢ +∞ ∈ ℂ̅ | ||
Theorem | bj-pinftynrr 34508 | The extended complex number +∞ is not a complex number. (Contributed by BJ, 27-Jun-2019.) |
⊢ ¬ +∞ ∈ ℂ | ||
Syntax | cminfty 34509 | Syntax for "minus infinity". |
class -∞ | ||
Definition | df-bj-minfty 34510 | Definition of "minus infinity". (Contributed by BJ, 27-Jun-2019.) |
⊢ -∞ = (+∞ei‘π) | ||
Theorem | bj-minftyccb 34511 | The class -∞ is an extended complex number. (Contributed by BJ, 27-Jun-2019.) |
⊢ -∞ ∈ ℂ̅ | ||
Theorem | bj-minftynrr 34512 | The extended complex number -∞ is not a complex number. (Contributed by BJ, 27-Jun-2019.) |
⊢ ¬ -∞ ∈ ℂ | ||
Theorem | bj-pinftynminfty 34513 | The extended complex numbers +∞ and -∞ are different. (Contributed by BJ, 27-Jun-2019.) |
⊢ +∞ ≠ -∞ | ||
Syntax | crrbar 34514 | Syntax for the set of extended real numbers. |
class ℝ̅ | ||
Definition | df-bj-rrbar 34515 | Definition of the set of extended real numbers. This aims to replace df-xr 10682. (Contributed by BJ, 29-Jun-2019.) |
⊢ ℝ̅ = (ℝ ∪ {-∞, +∞}) | ||
Syntax | cinfty 34516 | Syntax for ∞. |
class ∞ | ||
Definition | df-bj-infty 34517 | 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 34518 | Syntax for ℂ̂. |
class ℂ̂ | ||
Definition | df-bj-cchat 34519 | Define the complex projective line, or Riemann sphere. (Contributed by BJ, 27-Jun-2019.) |
⊢ ℂ̂ = (ℂ ∪ {∞}) | ||
Syntax | crrhat 34520 | Syntax for ℝ̂. |
class ℝ̂ | ||
Definition | df-bj-rrhat 34521 | Define the real projective line. (Contributed by BJ, 27-Jun-2019.) |
⊢ ℝ̂ = (ℝ ∪ {∞}) | ||
Theorem | bj-rrhatsscchat 34522 | 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 34523 | Syntax for the addition on extended complex numbers. |
class +ℂ̅ | ||
Definition | df-bj-addc 34524 | 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 34525 | Syntax for negation on the set of extended complex numbers and the complex projective line (Riemann sphere). |
class -ℂ̅ | ||
Definition | df-bj-oppc 34526* | 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 10683 without the intermediate step of df-lt 10553. | ||
Syntax | cltxr 34527 | Syntax for the standard (strict) order on the extended reals. |
class <ℝ̅ | ||
Definition | df-bj-lt 34528* | 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 contrieved 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 34532. | ||
Syntax | carg 34529 | Syntax for the argument of a nonzero extended complex number. |
class Arg | ||
Definition | df-bj-arg 34530 | 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 34485), and therefore should not be relied upon. (New usage is discouraged.) |
⊢ Arg = (𝑥 ∈ (ℂ̅ ∖ {0}) ↦ if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π, (((1st ‘𝑥) / (2 · π)) − π)))) | ||
Syntax | cmulc 34531 | Syntax for the multiplication of extended complex numbers. |
class ·ℂ̅ | ||
Definition | df-bj-mulc 34532 |
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 34534).
Note that this definition uses · and Arg and /. Indeed, it would be contrieved 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 34533 | Syntax for the inverse of nonzero extended complex numbers. |
class -1ℂ̅ | ||
Definition | df-bj-invc 34534* | 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 34532, 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 34535 | Syntax for the canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}). |
class iω↪ℕ | ||
Definition | df-bj-iomnn 34536* |
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 34483 but we did not use the present definition there since we wanted to have defined +∞ first. See bj-iomnnom 34545 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 34537 | 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 34538 | 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 34539 | 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 34540 | 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 34541 | 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 34542 | The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 6948. (Contributed by NM, 23-Sep-2007.) Put in deduction form. (Revised by BJ, 18-Mar-2023.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐺 = ((𝐹 ↾ (𝐶 ∖ {𝐴})) ∪ {〈𝐴, 𝐵〉})) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐺‘𝐴) = 𝐵) | ||
Theorem | bj-fvmptunsn1 34543* | 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 34544* | 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 34545 | The canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}) maps ω to +∞. (Contributed by BJ, 18-Feb-2023.) |
⊢ (iω↪ℕ‘ω) = +∞ | ||
Syntax | cnnbar 34546 | Syntax for the extended natural numbers. |
class ℕ̅ | ||
Definition | df-bj-nnbar 34547 | Definition of the extended natural numbers. (Contributed by BJ, 28-Jul-2023.) |
⊢ ℕ̅ = (ℕ0 ∪ {+∞}) | ||
Syntax | czzbar 34548 | Syntax for the extended integers. |
class ℤ̅ | ||
Definition | df-bj-zzbar 34549 | Definition of the extended integers. (Contributed by BJ, 28-Jul-2023.) |
⊢ ℤ̅ = (ℤ ∪ {-∞, +∞}) | ||
Syntax | czzhat 34550 | Syntax for the one-point-compactified integers. |
class ℤ̂ | ||
Definition | df-bj-zzhat 34551 | Definition of the one-point-compactified. (Contributed by BJ, 28-Jul-2023.) |
⊢ ℤ̂ = (ℤ ∪ {∞}) | ||
Syntax | cdivc 34552 | Syntax for the divisibility relation. |
class ∥ℂ | ||
Definition | df-bj-divc 34553* |
Definition of the divisibility relation (compare df-dvds 15611).
Since 0 is absorbing, ⊢ (𝐴 ∈ (ℂ̅ ∪ ℂ̂) → (𝐴 ∥ℂ 0)) and ⊢ ((0 ∥ℂ 𝐴) ↔ 𝐴 = 0). (Contributed by BJ, 28-Jul-2023.) |
⊢ ∥ℂ = {〈𝑥, 𝑦〉 ∣ (〈𝑥, 𝑦〉 ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)} | ||
See ccmn 18909 and subsequents. The first few statements of this subsection can be put very early after ccmn 18909. Proposal: in the main part, make separate subsections of commutative monoids and abelian groups. Relabel cabl 18910 to "cabl" or, preferably, other labels containing "abl" to "abel", for consistency. | ||
Theorem | bj-smgrpssmgm 34554 | Semigroups are magmas. (Contributed by BJ, 12-Apr-2024.) (Proof modification is discouraged.) |
⊢ Smgrp ⊆ Mgm | ||
Theorem | bj-smgrpssmgmel 34555 | Semigroups are magmas (elemental version). (Contributed by BJ, 12-Apr-2024.) (Proof modification is discouraged.) |
⊢ (𝐺 ∈ Smgrp → 𝐺 ∈ Mgm) | ||
Theorem | bj-mndsssmgrp 34556 | Monoids are semigroups. (Contributed by BJ, 11-Apr-2024.) (Proof modification is discouraged.) |
⊢ Mnd ⊆ Smgrp | ||
Theorem | bj-mndsssmgrpel 34557 | Monoids are semigroups (elemental version). (Contributed by BJ, 11-Apr-2024.) (Proof modification is discouraged.) |
⊢ (𝐺 ∈ Mnd → 𝐺 ∈ Smgrp) | ||
Theorem | bj-cmnssmnd 34558 | Commutative monoids are monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ CMnd ⊆ Mnd | ||
Theorem | bj-cmnssmndel 34559 | Commutative monoids are monoids (elemental version). This is a more direct proof of cmnmnd 18925, which relies on iscmn 18917. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ CMnd → 𝐴 ∈ Mnd) | ||
Theorem | bj-grpssmnd 34560 | Groups are monoids. (Contributed by BJ, 5-Jan-2024.) (Proof modification is discouraged.) |
⊢ Grp ⊆ Mnd | ||
Theorem | bj-grpssmndel 34561 | Groups are monoids (elemental version). Shorter proof of grpmnd 18113. (Contributed by BJ, 5-Jan-2024.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ Grp → 𝐴 ∈ Mnd) | ||
Theorem | bj-ablssgrp 34562 | Abelian groups are groups. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ Abel ⊆ Grp | ||
Theorem | bj-ablssgrpel 34563 | Abelian groups are groups (elemental version). This is a shorter proof of ablgrp 18914. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ Abel → 𝐴 ∈ Grp) | ||
Theorem | bj-ablsscmn 34564 | Abelian groups are commutative monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ Abel ⊆ CMnd | ||
Theorem | bj-ablsscmnel 34565 | Abelian groups are commutative monoids (elemental version). This is a shorter proof of ablcmn 18916. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ Abel → 𝐴 ∈ CMnd) | ||
Theorem | bj-modssabl 34566 | (The additive groups of) modules are abelian groups. (The elemental version is lmodabl 19684; see also lmodgrp 19644 and lmodcmn 19685.) (Contributed by BJ, 9-Jun-2019.) |
⊢ LMod ⊆ Abel | ||
Theorem | bj-vecssmod 34567 | Vector spaces are modules. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ LVec ⊆ LMod | ||
Theorem | bj-vecssmodel 34568 | Vector spaces are modules (elemental version). This is a shorter proof of lveclmod 19881. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod) | ||
UPDATE: a similar summation is already defined as df-gsum 16719 (although it mixes finite and infinite sums, which makes it harder to understand). | ||
Syntax | cfinsum 34569 | Syntax for the class "finite summation in monoids". |
class FinSum | ||
Definition | df-bj-finsum 34570* | 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 34571* | 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 34572 | Variant of fvimacnv 6826 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 43326. (Contributed by BJ, 7-Jan-2024.) |
⊢ ((Fun 𝐹 ∧ ¬ ∅ ∈ 𝐵) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵))) | ||
Theorem | bj-isvec 34573 | The predicate "is a vector space". (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝜑 → 𝐾 = (Scalar‘𝑉)) ⇒ ⊢ (𝜑 → (𝑉 ∈ LVec ↔ (𝑉 ∈ LMod ∧ 𝐾 ∈ DivRing))) | ||
Theorem | bj-flddrng 34574 | Fields are division rings. (Contributed by BJ, 6-Jan-2024.) |
⊢ Field ⊆ DivRing | ||
Theorem | bj-rrdrg 34575 | The field of real numbers is a division ring. (Contributed by BJ, 6-Jan-2024.) |
⊢ ℝfld ∈ DivRing | ||
Theorem | bj-isclm 34576 | The predicate "is a subcomplex module". (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝜑 → 𝐹 = (Scalar‘𝑊)) & ⊢ (𝜑 → 𝐾 = (Base‘𝐹)) ⇒ ⊢ (𝜑 → (𝑊 ∈ ℂMod ↔ (𝑊 ∈ LMod ∧ 𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 ∈ (SubRing‘ℂfld)))) | ||
Syntax | crrvec 34577 | Syntax for the class of real vector spaces. |
class ℝ-Vec | ||
Definition | df-bj-rvec 34578 | Definition of the class of real vector spaces. The previous definition, ⊢ ℝ-Vec = {𝑥 ∈ LMod ∣ (Scalar‘𝑥) = ℝfld}, can be recovered using bj-isrvec 34579. 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 34585. (Contributed by BJ, 9-Jun-2019.) |
⊢ ℝ-Vec = (LMod ∩ (◡Scalar “ {ℝfld})) | ||
Theorem | bj-isrvec 34579 | The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LMod ∧ (Scalar‘𝑉) = ℝfld)) | ||
Theorem | bj-rvecmod 34580 | Real vector spaces are modules (elemental version). (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ LMod) | ||
Theorem | bj-rvecssmod 34581 | Real vector spaces are modules. (Contributed by BJ, 6-Jan-2024.) |
⊢ ℝ-Vec ⊆ LMod | ||
Theorem | bj-rvecrr 34582 | 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 34583 | The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝜑 → (Scalar‘𝑉) = 𝐾) ⇒ ⊢ (𝜑 → (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LMod ∧ 𝐾 = ℝfld))) | ||
Theorem | bj-rvecvec 34584 | Real vector spaces are vector spaces (elemental version). (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ LVec) | ||
Theorem | bj-isrvec2 34585 | The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝜑 → (Scalar‘𝑉) = 𝐾) ⇒ ⊢ (𝜑 → (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LVec ∧ 𝐾 = ℝfld))) | ||
Theorem | bj-rvecssvec 34586 | Real vector spaces are vector spaces. (Contributed by BJ, 6-Jan-2024.) |
⊢ ℝ-Vec ⊆ LVec | ||
Theorem | bj-rveccmod 34587 | Real vector spaces are subcomplex modules (elemental version). (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ ℂMod) | ||
Theorem | bj-rvecsscmod 34588 | Real vector spaces are subcomplex modules. (Contributed by BJ, 6-Jan-2024.) |
⊢ ℝ-Vec ⊆ ℂMod | ||
Theorem | bj-rvecsscvec 34589 | Real vector spaces are subcomplex vector spaces. (Contributed by BJ, 6-Jan-2024.) |
⊢ ℝ-Vec ⊆ ℂVec | ||
Theorem | bj-rveccvec 34590 | Real vector spaces are subcomplex vector spaces (elemental version). (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ ℂVec) | ||
Theorem | bj-rvecssabl 34591 | (The additive groups of) real vector spaces are commutative groups. (Contributed by BJ, 9-Jun-2019.) |
⊢ ℝ-Vec ⊆ Abel | ||
Theorem | bj-rvecabl 34592 | (The additive groups of) real vector spaces are commutative groups (elemental version). (Contributed by BJ, 9-Jun-2019.) |
⊢ (𝐴 ∈ ℝ-Vec → 𝐴 ∈ Abel) | ||
Some lemmas to ease algebraic manipulations. | ||
Theorem | bj-subcom 34593 | A consequence of commutativity of multiplication. (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) − (𝐵 · 𝐴)) = 0) | ||
Theorem | bj-lineqi 34594 | 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 are proved by bj-bary1 34597 (which computes them). It would be nice to prove the two-dimensional case (is it easier to use ad hoc computations, or Cramer formulas?), in order to do some planar geometry. | ||
Theorem | bj-bary1lem 34595 | Lemma for bj-bary1 34597: expression for a barycenter of two points in one dimension (complex line). (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 = ((((𝐵 − 𝑋) / (𝐵 − 𝐴)) · 𝐴) + (((𝑋 − 𝐴) / (𝐵 − 𝐴)) · 𝐵))) | ||
Theorem | bj-bary1lem1 34596 | Lemma for bj-bary1: computation of one of the two barycentric coordinates of a barycenter of two points in one dimension (complex line). (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝑆 ∈ ℂ) & ⊢ (𝜑 → 𝑇 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝑋 = ((𝑆 · 𝐴) + (𝑇 · 𝐵)) ∧ (𝑆 + 𝑇) = 1) → 𝑇 = ((𝑋 − 𝐴) / (𝐵 − 𝐴)))) | ||
Theorem | bj-bary1 34597 | Barycentric coordinates in one dimension (complex line). In the statement, 𝑋 is the barycenter of the two points 𝐴, 𝐵 with respective normalized coefficients 𝑆, 𝑇. (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝑆 ∈ ℂ) & ⊢ (𝜑 → 𝑇 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝑋 = ((𝑆 · 𝐴) + (𝑇 · 𝐵)) ∧ (𝑆 + 𝑇) = 1) ↔ (𝑆 = ((𝐵 − 𝑋) / (𝐵 − 𝐴)) ∧ 𝑇 = ((𝑋 − 𝐴) / (𝐵 − 𝐴))))) | ||
Syntax | cend 34598 | Token for the monoid of endomorphisms. |
class End | ||
Definition | df-bj-end 34599* | The monoid of endomorphisms on an object of a category. (Contributed by BJ, 4-Apr-2024.) |
⊢ End = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐) ↦ {〈(Base‘ndx), (𝑥(Hom ‘𝑐)𝑥)〉, 〈(+g‘ndx), (〈𝑥, 𝑥〉(comp‘𝑐)𝑥)〉})) | ||
Theorem | bj-endval 34600 | Value of the monoid of endomorphisms on an object of a category. (Contributed by BJ, 5-Apr-2024.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) ⇒ ⊢ (𝜑 → ((End ‘𝐶)‘𝑋) = {〈(Base‘ndx), (𝑋(Hom ‘𝐶)𝑋)〉, 〈(+g‘ndx), (〈𝑋, 𝑋〉(comp‘𝐶)𝑋)〉}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |