![]() |
Metamath
Proof Explorer Theorem List (p. 373 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cpinfty 37201 | Syntax for "plus infinity". |
class +∞ | ||
Definition | df-bj-pinfty 37202 | Definition of "plus infinity". (Contributed by BJ, 27-Jun-2019.) |
⊢ +∞ = (+∞ei‘0) | ||
Theorem | bj-pinftyccb 37203 | The class +∞ is an extended complex number. (Contributed by BJ, 27-Jun-2019.) |
⊢ +∞ ∈ ℂ̅ | ||
Theorem | bj-pinftynrr 37204 | The extended complex number +∞ is not a complex number. (Contributed by BJ, 27-Jun-2019.) |
⊢ ¬ +∞ ∈ ℂ | ||
Syntax | cminfty 37205 | Syntax for "minus infinity". |
class -∞ | ||
Definition | df-bj-minfty 37206 | Definition of "minus infinity". (Contributed by BJ, 27-Jun-2019.) |
⊢ -∞ = (+∞ei‘π) | ||
Theorem | bj-minftyccb 37207 | The class -∞ is an extended complex number. (Contributed by BJ, 27-Jun-2019.) |
⊢ -∞ ∈ ℂ̅ | ||
Theorem | bj-minftynrr 37208 | The extended complex number -∞ is not a complex number. (Contributed by BJ, 27-Jun-2019.) |
⊢ ¬ -∞ ∈ ℂ | ||
Theorem | bj-pinftynminfty 37209 | The extended complex numbers +∞ and -∞ are different. (Contributed by BJ, 27-Jun-2019.) |
⊢ +∞ ≠ -∞ | ||
Syntax | crrbar 37210 | Syntax for the set of extended real numbers. |
class ℝ̅ | ||
Definition | df-bj-rrbar 37211 | Definition of the set of extended real numbers. This aims to replace df-xr 11296. (Contributed by BJ, 29-Jun-2019.) |
⊢ ℝ̅ = (ℝ ∪ {-∞, +∞}) | ||
Syntax | cinfty 37212 | Syntax for ∞. |
class ∞ | ||
Definition | df-bj-infty 37213 | 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 37214 | Syntax for ℂ̂. |
class ℂ̂ | ||
Definition | df-bj-cchat 37215 | Define the complex projective line, or Riemann sphere. (Contributed by BJ, 27-Jun-2019.) |
⊢ ℂ̂ = (ℂ ∪ {∞}) | ||
Syntax | crrhat 37216 | Syntax for ℝ̂. |
class ℝ̂ | ||
Definition | df-bj-rrhat 37217 | Define the real projective line. (Contributed by BJ, 27-Jun-2019.) |
⊢ ℝ̂ = (ℝ ∪ {∞}) | ||
Theorem | bj-rrhatsscchat 37218 | 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 37219 | Syntax for the addition on extended complex numbers. |
class +ℂ̅ | ||
Definition | df-bj-addc 37220 | 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 37221 | Syntax for negation on the set of extended complex numbers and the complex projective line (Riemann sphere). |
class -ℂ̅ | ||
Definition | df-bj-oppc 37222* | 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 11297 without the intermediate step of df-lt 11165. | ||
Syntax | cltxr 37223 | Syntax for the standard (strict) order on the extended reals. |
class <ℝ̅ | ||
Definition | df-bj-lt 37224* | 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 37228. | ||
Syntax | carg 37225 | Syntax for the argument of a nonzero extended complex number. |
class Arg | ||
Definition | df-bj-arg 37226 | 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 37181), and therefore should not be relied upon. (New usage is discouraged.) |
⊢ Arg = (𝑥 ∈ (ℂ̅ ∖ {0}) ↦ if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π, (((1st ‘𝑥) / (2 · π)) − π)))) | ||
Syntax | cmulc 37227 | Syntax for the multiplication of extended complex numbers. |
class ·ℂ̅ | ||
Definition | df-bj-mulc 37228 |
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 37230).
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 37229 | Syntax for the inverse of nonzero extended complex numbers. |
class -1ℂ̅ | ||
Definition | df-bj-invc 37230* | 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 37228, 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 37231 | Syntax for the canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}). |
class iω↪ℕ | ||
Definition | df-bj-iomnn 37232* |
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 37179 but we did not use the present definition there since we wanted to have defined +∞ first. See bj-iomnnom 37241 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 37233 | 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 37234 | 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 37235 | 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 37236 | 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 37237 | 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 37238 | The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 7202. (Contributed by NM, 23-Sep-2007.) Put in deduction form. (Revised by BJ, 18-Mar-2023.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐺 = ((𝐹 ↾ (𝐶 ∖ {𝐴})) ∪ {〈𝐴, 𝐵〉})) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐺‘𝐴) = 𝐵) | ||
Theorem | bj-fvmptunsn1 37239* | 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 37240* | 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 37241 | The canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}) maps ω to +∞. (Contributed by BJ, 18-Feb-2023.) |
⊢ (iω↪ℕ‘ω) = +∞ | ||
Syntax | cnnbar 37242 | Syntax for the extended natural numbers. |
class ℕ̅ | ||
Definition | df-bj-nnbar 37243 | Definition of the extended natural numbers. (Contributed by BJ, 28-Jul-2023.) |
⊢ ℕ̅ = (ℕ0 ∪ {+∞}) | ||
Syntax | czzbar 37244 | Syntax for the extended integers. |
class ℤ̅ | ||
Definition | df-bj-zzbar 37245 | Definition of the extended integers. (Contributed by BJ, 28-Jul-2023.) |
⊢ ℤ̅ = (ℤ ∪ {-∞, +∞}) | ||
Syntax | czzhat 37246 | Syntax for the one-point-compactified integers. |
class ℤ̂ | ||
Definition | df-bj-zzhat 37247 | Definition of the one-point-compactified. (Contributed by BJ, 28-Jul-2023.) |
⊢ ℤ̂ = (ℤ ∪ {∞}) | ||
Syntax | cdivc 37248 | Syntax for the divisibility relation. |
class ∥ℂ | ||
Definition | df-bj-divc 37249* |
Definition of the divisibility relation (compare df-dvds 16287).
Since 0 is absorbing, ⊢ (𝐴 ∈ (ℂ̅ ∪ ℂ̂) → (𝐴 ∥ℂ 0)) and ⊢ ((0 ∥ℂ 𝐴) ↔ 𝐴 = 0). (Contributed by BJ, 28-Jul-2023.) |
⊢ ∥ℂ = {〈𝑥, 𝑦〉 ∣ (〈𝑥, 𝑦〉 ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)} | ||
See ccmn 19812 and subsequents. The first few statements of this subsection can be put very early after ccmn 19812. Proposal: in the main part, make separate subsections of commutative monoids and abelian groups. Relabel cabl 19813 to "cabl" or, preferably, other labels containing "abl" to "abel", for consistency. | ||
Theorem | bj-smgrpssmgm 37250 | Semigroups are magmas. (Contributed by BJ, 12-Apr-2024.) (Proof modification is discouraged.) |
⊢ Smgrp ⊆ Mgm | ||
Theorem | bj-smgrpssmgmel 37251 | Semigroups are magmas (elemental version). (Contributed by BJ, 12-Apr-2024.) (Proof modification is discouraged.) |
⊢ (𝐺 ∈ Smgrp → 𝐺 ∈ Mgm) | ||
Theorem | bj-mndsssmgrp 37252 | Monoids are semigroups. (Contributed by BJ, 11-Apr-2024.) (Proof modification is discouraged.) |
⊢ Mnd ⊆ Smgrp | ||
Theorem | bj-mndsssmgrpel 37253 | Monoids are semigroups (elemental version). (Contributed by BJ, 11-Apr-2024.) (Proof modification is discouraged.) |
⊢ (𝐺 ∈ Mnd → 𝐺 ∈ Smgrp) | ||
Theorem | bj-cmnssmnd 37254 | Commutative monoids are monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ CMnd ⊆ Mnd | ||
Theorem | bj-cmnssmndel 37255 | Commutative monoids are monoids (elemental version). This is a more direct proof of cmnmnd 19829, which relies on iscmn 19821. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ CMnd → 𝐴 ∈ Mnd) | ||
Theorem | bj-grpssmnd 37256 | Groups are monoids. (Contributed by BJ, 5-Jan-2024.) (Proof modification is discouraged.) |
⊢ Grp ⊆ Mnd | ||
Theorem | bj-grpssmndel 37257 | Groups are monoids (elemental version). Shorter proof of grpmnd 18970. (Contributed by BJ, 5-Jan-2024.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ Grp → 𝐴 ∈ Mnd) | ||
Theorem | bj-ablssgrp 37258 | Abelian groups are groups. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ Abel ⊆ Grp | ||
Theorem | bj-ablssgrpel 37259 | Abelian groups are groups (elemental version). This is a shorter proof of ablgrp 19817. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ Abel → 𝐴 ∈ Grp) | ||
Theorem | bj-ablsscmn 37260 | Abelian groups are commutative monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ Abel ⊆ CMnd | ||
Theorem | bj-ablsscmnel 37261 | Abelian groups are commutative monoids (elemental version). This is a shorter proof of ablcmn 19819. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ Abel → 𝐴 ∈ CMnd) | ||
Theorem | bj-modssabl 37262 | (The additive groups of) modules are abelian groups. (The elemental version is lmodabl 20923; see also lmodgrp 20881 and lmodcmn 20924.) (Contributed by BJ, 9-Jun-2019.) |
⊢ LMod ⊆ Abel | ||
Theorem | bj-vecssmod 37263 | Vector spaces are modules. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ LVec ⊆ LMod | ||
Theorem | bj-vecssmodel 37264 | Vector spaces are modules (elemental version). This is a shorter proof of lveclmod 21122. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod) | ||
UPDATE: a similar summation is already defined as df-gsum 17488 (although it mixes finite and infinite sums, which makes it harder to understand). | ||
Syntax | cfinsum 37265 | Syntax for the class "finite summation in monoids". |
class FinSum | ||
Definition | df-bj-finsum 37266* | 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 37267* | 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 37268 | Variant of fvimacnv 7072 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 47069. (Contributed by BJ, 7-Jan-2024.) |
⊢ ((Fun 𝐹 ∧ ¬ ∅ ∈ 𝐵) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵))) | ||
Theorem | bj-isvec 37269 | The predicate "is a vector space". (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝜑 → 𝐾 = (Scalar‘𝑉)) ⇒ ⊢ (𝜑 → (𝑉 ∈ LVec ↔ (𝑉 ∈ LMod ∧ 𝐾 ∈ DivRing))) | ||
Theorem | bj-fldssdrng 37270 | Fields are division rings. (Contributed by BJ, 6-Jan-2024.) |
⊢ Field ⊆ DivRing | ||
Theorem | bj-flddrng 37271 | Fields are division rings (elemental version). (Contributed by BJ, 9-Nov-2024.) |
⊢ (𝐹 ∈ Field → 𝐹 ∈ DivRing) | ||
Theorem | bj-rrdrg 37272 | The field of real numbers is a division ring. (Contributed by BJ, 6-Jan-2024.) |
⊢ ℝfld ∈ DivRing | ||
Theorem | bj-isclm 37273 | The predicate "is a subcomplex module". (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝜑 → 𝐹 = (Scalar‘𝑊)) & ⊢ (𝜑 → 𝐾 = (Base‘𝐹)) ⇒ ⊢ (𝜑 → (𝑊 ∈ ℂMod ↔ (𝑊 ∈ LMod ∧ 𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 ∈ (SubRing‘ℂfld)))) | ||
Syntax | crrvec 37274 | Syntax for the class of real vector spaces. |
class ℝ-Vec | ||
Definition | df-bj-rvec 37275 | Definition of the class of real vector spaces. The previous definition, ⊢ ℝ-Vec = {𝑥 ∈ LMod ∣ (Scalar‘𝑥) = ℝfld}, can be recovered using bj-isrvec 37276. 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 37282. (Contributed by BJ, 9-Jun-2019.) |
⊢ ℝ-Vec = (LMod ∩ (◡Scalar “ {ℝfld})) | ||
Theorem | bj-isrvec 37276 | The predicate "is a real vector space". Using df-sca 17313 instead of scaid 17360 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 37277 | Real vector spaces are modules (elemental version). (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ LMod) | ||
Theorem | bj-rvecssmod 37278 | Real vector spaces are modules. (Contributed by BJ, 6-Jan-2024.) |
⊢ ℝ-Vec ⊆ LMod | ||
Theorem | bj-rvecrr 37279 | 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 37280 | The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝜑 → (Scalar‘𝑉) = 𝐾) ⇒ ⊢ (𝜑 → (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LMod ∧ 𝐾 = ℝfld))) | ||
Theorem | bj-rvecvec 37281 | Real vector spaces are vector spaces (elemental version). (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ LVec) | ||
Theorem | bj-isrvec2 37282 | The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝜑 → (Scalar‘𝑉) = 𝐾) ⇒ ⊢ (𝜑 → (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LVec ∧ 𝐾 = ℝfld))) | ||
Theorem | bj-rvecssvec 37283 | Real vector spaces are vector spaces. (Contributed by BJ, 6-Jan-2024.) |
⊢ ℝ-Vec ⊆ LVec | ||
Theorem | bj-rveccmod 37284 | Real vector spaces are subcomplex modules (elemental version). (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ ℂMod) | ||
Theorem | bj-rvecsscmod 37285 | Real vector spaces are subcomplex modules. (Contributed by BJ, 6-Jan-2024.) |
⊢ ℝ-Vec ⊆ ℂMod | ||
Theorem | bj-rvecsscvec 37286 | Real vector spaces are subcomplex vector spaces. (Contributed by BJ, 6-Jan-2024.) |
⊢ ℝ-Vec ⊆ ℂVec | ||
Theorem | bj-rveccvec 37287 | Real vector spaces are subcomplex vector spaces (elemental version). (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ ℂVec) | ||
Theorem | bj-rvecssabl 37288 | (The additive groups of) real vector spaces are commutative groups. (Contributed by BJ, 9-Jun-2019.) |
⊢ ℝ-Vec ⊆ Abel | ||
Theorem | bj-rvecabl 37289 | (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 37290 | A consequence of commutativity of multiplication. (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) − (𝐵 · 𝐴)) = 0) | ||
Theorem | bj-lineqi 37291 | 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 37294 (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 37292 | Lemma for bj-bary1 37294: expression for a barycenter of two points in one dimension (complex line). (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 = ((((𝐵 − 𝑋) / (𝐵 − 𝐴)) · 𝐴) + (((𝑋 − 𝐴) / (𝐵 − 𝐴)) · 𝐵))) | ||
Theorem | bj-bary1lem1 37293 | Lemma for bj-bary1 37294: 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 37294 | 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 37295 | Token for the monoid of endomorphisms. |
class End | ||
Definition | df-bj-end 37296* | 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 37297 | Value of the monoid of endomorphisms on an object of a category. (Contributed by BJ, 5-Apr-2024.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) ⇒ ⊢ (𝜑 → ((End ‘𝐶)‘𝑋) = {〈(Base‘ndx), (𝑋(Hom ‘𝐶)𝑋)〉, 〈(+g‘ndx), (〈𝑋, 𝑋〉(comp‘𝐶)𝑋)〉}) | ||
Theorem | bj-endbase 37298 | Base set of the monoid of endomorphisms on an object of a category. (Contributed by BJ, 5-Apr-2024.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) ⇒ ⊢ (𝜑 → (Base‘((End ‘𝐶)‘𝑋)) = (𝑋(Hom ‘𝐶)𝑋)) | ||
Theorem | bj-endcomp 37299 | Composition law of the monoid of endomorphisms on an object of a category. (Contributed by BJ, 5-Apr-2024.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) ⇒ ⊢ (𝜑 → (+g‘((End ‘𝐶)‘𝑋)) = (〈𝑋, 𝑋〉(comp‘𝐶)𝑋)) | ||
Theorem | bj-endmnd 37300 | The monoid of endomorphisms on an object of a category is a monoid. (Contributed by BJ, 5-Apr-2024.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐶 ∈ Cat) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐶)) ⇒ ⊢ (𝜑 → ((End ‘𝐶)‘𝑋) ∈ Mnd) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |