![]() |
Metamath
Proof Explorer Theorem List (p. 363 of 480) | < 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-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | crrbar 36201 | Syntax for the set of extended real numbers. |
class ℝ̅ | ||
Definition | df-bj-rrbar 36202 | Definition of the set of extended real numbers. This aims to replace df-xr 11254. (Contributed by BJ, 29-Jun-2019.) |
⊢ ℝ̅ = (ℝ ∪ {-∞, +∞}) | ||
Syntax | cinfty 36203 | Syntax for ∞. |
class ∞ | ||
Definition | df-bj-infty 36204 | 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 36205 | Syntax for ℂ̂. |
class ℂ̂ | ||
Definition | df-bj-cchat 36206 | Define the complex projective line, or Riemann sphere. (Contributed by BJ, 27-Jun-2019.) |
⊢ ℂ̂ = (ℂ ∪ {∞}) | ||
Syntax | crrhat 36207 | Syntax for ℝ̂. |
class ℝ̂ | ||
Definition | df-bj-rrhat 36208 | Define the real projective line. (Contributed by BJ, 27-Jun-2019.) |
⊢ ℝ̂ = (ℝ ∪ {∞}) | ||
Theorem | bj-rrhatsscchat 36209 | 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 36210 | Syntax for the addition on extended complex numbers. |
class +ℂ̅ | ||
Definition | df-bj-addc 36211 | 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 36212 | Syntax for negation on the set of extended complex numbers and the complex projective line (Riemann sphere). |
class -ℂ̅ | ||
Definition | df-bj-oppc 36213* | 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 11255 without the intermediate step of df-lt 11125. | ||
Syntax | cltxr 36214 | Syntax for the standard (strict) order on the extended reals. |
class <ℝ̅ | ||
Definition | df-bj-lt 36215* | 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 36219. | ||
Syntax | carg 36216 | Syntax for the argument of a nonzero extended complex number. |
class Arg | ||
Definition | df-bj-arg 36217 | 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 36172), and therefore should not be relied upon. (New usage is discouraged.) |
⊢ Arg = (𝑥 ∈ (ℂ̅ ∖ {0}) ↦ if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π, (((1st ‘𝑥) / (2 · π)) − π)))) | ||
Syntax | cmulc 36218 | Syntax for the multiplication of extended complex numbers. |
class ·ℂ̅ | ||
Definition | df-bj-mulc 36219 |
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 36221).
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 36220 | Syntax for the inverse of nonzero extended complex numbers. |
class -1ℂ̅ | ||
Definition | df-bj-invc 36221* | 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 36219, 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 36222 | Syntax for the canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}). |
class iω↪ℕ | ||
Definition | df-bj-iomnn 36223* |
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 36170 but we did not use the present definition there since we wanted to have defined +∞ first. See bj-iomnnom 36232 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 36224 | 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 36225 | 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 36226 | 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 36227 | 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 36228 | 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 36229 | The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 7183. (Contributed by NM, 23-Sep-2007.) Put in deduction form. (Revised by BJ, 18-Mar-2023.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐺 = ((𝐹 ↾ (𝐶 ∖ {𝐴})) ∪ {⟨𝐴, 𝐵⟩})) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐺‘𝐴) = 𝐵) | ||
Theorem | bj-fvmptunsn1 36230* | 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 36231* | 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 36232 | The canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}) maps ω to +∞. (Contributed by BJ, 18-Feb-2023.) |
⊢ (iω↪ℕ‘ω) = +∞ | ||
Syntax | cnnbar 36233 | Syntax for the extended natural numbers. |
class ℕ̅ | ||
Definition | df-bj-nnbar 36234 | Definition of the extended natural numbers. (Contributed by BJ, 28-Jul-2023.) |
⊢ ℕ̅ = (ℕ0 ∪ {+∞}) | ||
Syntax | czzbar 36235 | Syntax for the extended integers. |
class ℤ̅ | ||
Definition | df-bj-zzbar 36236 | Definition of the extended integers. (Contributed by BJ, 28-Jul-2023.) |
⊢ ℤ̅ = (ℤ ∪ {-∞, +∞}) | ||
Syntax | czzhat 36237 | Syntax for the one-point-compactified integers. |
class ℤ̂ | ||
Definition | df-bj-zzhat 36238 | Definition of the one-point-compactified. (Contributed by BJ, 28-Jul-2023.) |
⊢ ℤ̂ = (ℤ ∪ {∞}) | ||
Syntax | cdivc 36239 | Syntax for the divisibility relation. |
class ∥ℂ | ||
Definition | df-bj-divc 36240* |
Definition of the divisibility relation (compare df-dvds 16200).
Since 0 is absorbing, ⊢ (𝐴 ∈ (ℂ̅ ∪ ℂ̂) → (𝐴 ∥ℂ 0)) and ⊢ ((0 ∥ℂ 𝐴) ↔ 𝐴 = 0). (Contributed by BJ, 28-Jul-2023.) |
⊢ ∥ℂ = {⟨𝑥, 𝑦⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)} | ||
See ccmn 19650 and subsequents. The first few statements of this subsection can be put very early after ccmn 19650. Proposal: in the main part, make separate subsections of commutative monoids and abelian groups. Relabel cabl 19651 to "cabl" or, preferably, other labels containing "abl" to "abel", for consistency. | ||
Theorem | bj-smgrpssmgm 36241 | Semigroups are magmas. (Contributed by BJ, 12-Apr-2024.) (Proof modification is discouraged.) |
⊢ Smgrp ⊆ Mgm | ||
Theorem | bj-smgrpssmgmel 36242 | Semigroups are magmas (elemental version). (Contributed by BJ, 12-Apr-2024.) (Proof modification is discouraged.) |
⊢ (𝐺 ∈ Smgrp → 𝐺 ∈ Mgm) | ||
Theorem | bj-mndsssmgrp 36243 | Monoids are semigroups. (Contributed by BJ, 11-Apr-2024.) (Proof modification is discouraged.) |
⊢ Mnd ⊆ Smgrp | ||
Theorem | bj-mndsssmgrpel 36244 | Monoids are semigroups (elemental version). (Contributed by BJ, 11-Apr-2024.) (Proof modification is discouraged.) |
⊢ (𝐺 ∈ Mnd → 𝐺 ∈ Smgrp) | ||
Theorem | bj-cmnssmnd 36245 | Commutative monoids are monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ CMnd ⊆ Mnd | ||
Theorem | bj-cmnssmndel 36246 | Commutative monoids are monoids (elemental version). This is a more direct proof of cmnmnd 19667, which relies on iscmn 19659. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ CMnd → 𝐴 ∈ Mnd) | ||
Theorem | bj-grpssmnd 36247 | Groups are monoids. (Contributed by BJ, 5-Jan-2024.) (Proof modification is discouraged.) |
⊢ Grp ⊆ Mnd | ||
Theorem | bj-grpssmndel 36248 | Groups are monoids (elemental version). Shorter proof of grpmnd 18828. (Contributed by BJ, 5-Jan-2024.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ Grp → 𝐴 ∈ Mnd) | ||
Theorem | bj-ablssgrp 36249 | Abelian groups are groups. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ Abel ⊆ Grp | ||
Theorem | bj-ablssgrpel 36250 | Abelian groups are groups (elemental version). This is a shorter proof of ablgrp 19655. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ Abel → 𝐴 ∈ Grp) | ||
Theorem | bj-ablsscmn 36251 | Abelian groups are commutative monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ Abel ⊆ CMnd | ||
Theorem | bj-ablsscmnel 36252 | Abelian groups are commutative monoids (elemental version). This is a shorter proof of ablcmn 19657. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ Abel → 𝐴 ∈ CMnd) | ||
Theorem | bj-modssabl 36253 | (The additive groups of) modules are abelian groups. (The elemental version is lmodabl 20524; see also lmodgrp 20482 and lmodcmn 20525.) (Contributed by BJ, 9-Jun-2019.) |
⊢ LMod ⊆ Abel | ||
Theorem | bj-vecssmod 36254 | Vector spaces are modules. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ LVec ⊆ LMod | ||
Theorem | bj-vecssmodel 36255 | Vector spaces are modules (elemental version). This is a shorter proof of lveclmod 20722. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod) | ||
UPDATE: a similar summation is already defined as df-gsum 17390 (although it mixes finite and infinite sums, which makes it harder to understand). | ||
Syntax | cfinsum 36256 | Syntax for the class "finite summation in monoids". |
class FinSum | ||
Definition | df-bj-finsum 36257* | 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 36258* | 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 36259 | Variant of fvimacnv 7054 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 45913. (Contributed by BJ, 7-Jan-2024.) |
⊢ ((Fun 𝐹 ∧ ¬ ∅ ∈ 𝐵) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵))) | ||
Theorem | bj-isvec 36260 | The predicate "is a vector space". (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝜑 → 𝐾 = (Scalar‘𝑉)) ⇒ ⊢ (𝜑 → (𝑉 ∈ LVec ↔ (𝑉 ∈ LMod ∧ 𝐾 ∈ DivRing))) | ||
Theorem | bj-fldssdrng 36261 | Fields are division rings. (Contributed by BJ, 6-Jan-2024.) |
⊢ Field ⊆ DivRing | ||
Theorem | bj-flddrng 36262 | Fields are division rings (elemental version). (Contributed by BJ, 9-Nov-2024.) |
⊢ (𝐹 ∈ Field → 𝐹 ∈ DivRing) | ||
Theorem | bj-rrdrg 36263 | The field of real numbers is a division ring. (Contributed by BJ, 6-Jan-2024.) |
⊢ ℝfld ∈ DivRing | ||
Theorem | bj-isclm 36264 | The predicate "is a subcomplex module". (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝜑 → 𝐹 = (Scalar‘𝑊)) & ⊢ (𝜑 → 𝐾 = (Base‘𝐹)) ⇒ ⊢ (𝜑 → (𝑊 ∈ ℂMod ↔ (𝑊 ∈ LMod ∧ 𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 ∈ (SubRing‘ℂfld)))) | ||
Syntax | crrvec 36265 | Syntax for the class of real vector spaces. |
class ℝ-Vec | ||
Definition | df-bj-rvec 36266 | Definition of the class of real vector spaces. The previous definition, ⊢ ℝ-Vec = {𝑥 ∈ LMod ∣ (Scalar‘𝑥) = ℝfld}, can be recovered using bj-isrvec 36267. 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 36273. (Contributed by BJ, 9-Jun-2019.) |
⊢ ℝ-Vec = (LMod ∩ (◡Scalar “ {ℝfld})) | ||
Theorem | bj-isrvec 36267 | The predicate "is a real vector space". Using df-sca 17215 instead of scaid 17262 would shorten the proof by two syntactic steps, but it is preferable not to rely on the precise definition df-sca 17215. (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LMod ∧ (Scalar‘𝑉) = ℝfld)) | ||
Theorem | bj-rvecmod 36268 | Real vector spaces are modules (elemental version). (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ LMod) | ||
Theorem | bj-rvecssmod 36269 | Real vector spaces are modules. (Contributed by BJ, 6-Jan-2024.) |
⊢ ℝ-Vec ⊆ LMod | ||
Theorem | bj-rvecrr 36270 | 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 36271 | The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝜑 → (Scalar‘𝑉) = 𝐾) ⇒ ⊢ (𝜑 → (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LMod ∧ 𝐾 = ℝfld))) | ||
Theorem | bj-rvecvec 36272 | Real vector spaces are vector spaces (elemental version). (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ LVec) | ||
Theorem | bj-isrvec2 36273 | The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝜑 → (Scalar‘𝑉) = 𝐾) ⇒ ⊢ (𝜑 → (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LVec ∧ 𝐾 = ℝfld))) | ||
Theorem | bj-rvecssvec 36274 | Real vector spaces are vector spaces. (Contributed by BJ, 6-Jan-2024.) |
⊢ ℝ-Vec ⊆ LVec | ||
Theorem | bj-rveccmod 36275 | Real vector spaces are subcomplex modules (elemental version). (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ ℂMod) | ||
Theorem | bj-rvecsscmod 36276 | Real vector spaces are subcomplex modules. (Contributed by BJ, 6-Jan-2024.) |
⊢ ℝ-Vec ⊆ ℂMod | ||
Theorem | bj-rvecsscvec 36277 | Real vector spaces are subcomplex vector spaces. (Contributed by BJ, 6-Jan-2024.) |
⊢ ℝ-Vec ⊆ ℂVec | ||
Theorem | bj-rveccvec 36278 | Real vector spaces are subcomplex vector spaces (elemental version). (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ ℂVec) | ||
Theorem | bj-rvecssabl 36279 | (The additive groups of) real vector spaces are commutative groups. (Contributed by BJ, 9-Jun-2019.) |
⊢ ℝ-Vec ⊆ Abel | ||
Theorem | bj-rvecabl 36280 | (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 36281 | A consequence of commutativity of multiplication. (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) − (𝐵 · 𝐴)) = 0) | ||
Theorem | bj-lineqi 36282 | 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 36285 (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 36283 | Lemma for bj-bary1 36285: expression for a barycenter of two points in one dimension (complex line). (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 = ((((𝐵 − 𝑋) / (𝐵 − 𝐴)) · 𝐴) + (((𝑋 − 𝐴) / (𝐵 − 𝐴)) · 𝐵))) | ||
Theorem | bj-bary1lem1 36284 | 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 36285 | 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 36286 | Token for the monoid of endomorphisms. |
class End | ||
Definition | df-bj-end 36287* | 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 36288 | 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 36289 | 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 36290 | 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 36291 | 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) | ||
Theorem | taupilem3 36292 | Lemma for tau-related theorems. (Contributed by Jim Kingdon, 16-Feb-2019.) |
⊢ (𝐴 ∈ (ℝ+ ∩ (◡cos “ {1})) ↔ (𝐴 ∈ ℝ+ ∧ (cos‘𝐴) = 1)) | ||
Theorem | taupilemrplb 36293* | A set of positive reals has (in the reals) a lower bound. (Contributed by Jim Kingdon, 19-Feb-2019.) |
⊢ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (ℝ+ ∩ 𝐴)𝑥 ≤ 𝑦 | ||
Theorem | taupilem1 36294 | Lemma for taupi 36296. A positive real whose cosine is one is at least 2 · π. (Contributed by Jim Kingdon, 19-Feb-2019.) |
⊢ ((𝐴 ∈ ℝ+ ∧ (cos‘𝐴) = 1) → (2 · π) ≤ 𝐴) | ||
Theorem | taupilem2 36295 | Lemma for taupi 36296. The smallest positive real whose cosine is one is at most 2 · π. (Contributed by Jim Kingdon, 19-Feb-2019.) (Revised by AV, 1-Oct-2020.) |
⊢ τ ≤ (2 · π) | ||
Theorem | taupi 36296 | Relationship between τ and π. This can be seen as connecting the ratio of a circle's circumference to its radius and the ratio of a circle's circumference to its diameter. (Contributed by Jim Kingdon, 19-Feb-2019.) (Revised by AV, 1-Oct-2020.) |
⊢ τ = (2 · π) | ||
Theorem | dfgcd3 36297* | Alternate definition of the gcd operator. (Contributed by Jim Kingdon, 31-Dec-2021.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (℩𝑑 ∈ ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)))) | ||
Theorem | irrdifflemf 36298 | Lemma for irrdiff 36299. The forward direction. (Contributed by Jim Kingdon, 20-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → ¬ 𝐴 ∈ ℚ) & ⊢ (𝜑 → 𝑄 ∈ ℚ) & ⊢ (𝜑 → 𝑅 ∈ ℚ) & ⊢ (𝜑 → 𝑄 ≠ 𝑅) ⇒ ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) ≠ (abs‘(𝐴 − 𝑅))) | ||
Theorem | irrdiff 36299* | The irrationals are exactly those reals that are a different distance from every rational. (Contributed by Jim Kingdon, 19-May-2024.) |
⊢ (𝐴 ∈ ℝ → (¬ 𝐴 ∈ ℚ ↔ ∀𝑞 ∈ ℚ ∀𝑟 ∈ ℚ (𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟))))) | ||
Theorem | iccioo01 36300 | The closed unit interval is equinumerous to the open unit interval. Based on a Mastodon post by Michael Kinyon. (Contributed by Jim Kingdon, 4-Jun-2024.) |
⊢ (0[,]1) ≈ (0(,)1) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |