Home | Metamath
Proof Explorer Theorem List (p. 345 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bj-minftynrr 34401 | The extended complex number -∞ is not a complex number. (Contributed by BJ, 27-Jun-2019.) |
⊢ ¬ -∞ ∈ ℂ | ||
Theorem | bj-pinftynminfty 34402 | The extended complex numbers +∞ and -∞ are different. (Contributed by BJ, 27-Jun-2019.) |
⊢ +∞ ≠ -∞ | ||
Syntax | crrbar 34403 | Syntax for the set of extended real numbers. |
class ℝ̅ | ||
Definition | df-bj-rrbar 34404 | Definition of the set of extended real numbers. This aims to replace df-xr 10668. (Contributed by BJ, 29-Jun-2019.) |
⊢ ℝ̅ = (ℝ ∪ {-∞, +∞}) | ||
Syntax | cinfty 34405 | Syntax for ∞. |
class ∞ | ||
Definition | df-bj-infty 34406 | 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 34407 | Syntax for ℂ̂. |
class ℂ̂ | ||
Definition | df-bj-cchat 34408 | Define the complex projective line, or Riemann sphere. (Contributed by BJ, 27-Jun-2019.) |
⊢ ℂ̂ = (ℂ ∪ {∞}) | ||
Syntax | crrhat 34409 | Syntax for ℝ̂. |
class ℝ̂ | ||
Definition | df-bj-rrhat 34410 | Define the real projective line. (Contributed by BJ, 27-Jun-2019.) |
⊢ ℝ̂ = (ℝ ∪ {∞}) | ||
Theorem | bj-rrhatsscchat 34411 | 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 34412 | Syntax for the addition on extended complex numbers. |
class +ℂ̅ | ||
Definition | df-bj-addc 34413 | 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 34414 | Syntax for negation on the set of extended complex numbers and the complex projective line (Riemann sphere). |
class -ℂ̅ | ||
Definition | df-bj-oppc 34415* | 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 10669 without the intermediate step of df-lt 10539. | ||
Syntax | cltxr 34416 | Syntax for the standard (strict) order on the extended reals. |
class <ℝ̅ | ||
Definition | df-bj-lt 34417* | 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 34421. | ||
Syntax | carg 34418 | Syntax for the argument of a nonzero extended complex number. |
class Arg | ||
Definition | df-bj-arg 34419 | 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 34374), and therefore should not be relied upon. (New usage is discouraged.) |
⊢ Arg = (𝑥 ∈ (ℂ̅ ∖ {0}) ↦ if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π, (((1st ‘𝑥) / (2 · π)) − π)))) | ||
Syntax | cmulc 34420 | Syntax for the multiplication of extended complex numbers. |
class ·ℂ̅ | ||
Definition | df-bj-mulc 34421 |
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 34423).
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 34422 | Syntax for the inverse of nonzero extended complex numbers. |
class -1ℂ̅ | ||
Definition | df-bj-invc 34423* | 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 34421, 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 34424 | Syntax for the canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}). |
class iω↪ℕ | ||
Definition | df-bj-iomnn 34425* |
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 34372 but we did not use the present definition there since we wanted to have defined +∞ first. See bj-iomnnom 34434 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 34426 | 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 34427 | 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 34428 | 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 34429 | 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 34430 | 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 34431 | The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 6938. (Contributed by NM, 23-Sep-2007.) Put in deduction form. (Revised by BJ, 18-Mar-2023.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐺 = ((𝐹 ↾ (𝐶 ∖ {𝐴})) ∪ {〈𝐴, 𝐵〉})) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐺‘𝐴) = 𝐵) | ||
Theorem | bj-fvmptunsn1 34432* | 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 34433* | 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 34434 | The canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}) maps ω to +∞. (Contributed by BJ, 18-Feb-2023.) |
⊢ (iω↪ℕ‘ω) = +∞ | ||
Syntax | cnnbar 34435 | Syntax for the extended natural numbers. |
class ℕ̅ | ||
Definition | df-bj-nnbar 34436 | Definition of the extended natural numbers. (Contributed by BJ, 28-Jul-2023.) |
⊢ ℕ̅ = (ℕ0 ∪ {+∞}) | ||
Syntax | czzbar 34437 | Syntax for the extended integers. |
class ℤ̅ | ||
Definition | df-bj-zzbar 34438 | Definition of the extended integers. (Contributed by BJ, 28-Jul-2023.) |
⊢ ℤ̅ = (ℤ ∪ {-∞, +∞}) | ||
Syntax | czzhat 34439 | Syntax for the one-point-compactified integers. |
class ℤ̂ | ||
Definition | df-bj-zzhat 34440 | Definition of the one-point-compactified. (Contributed by BJ, 28-Jul-2023.) |
⊢ ℤ̂ = (ℤ ∪ {∞}) | ||
Syntax | cdivc 34441 | Syntax for the divisibility relation. |
class ∥ℂ | ||
Definition | df-bj-divc 34442* |
Definition of the divisibility relation (compare df-dvds 15598).
Since 0 is absorbing, ⊢ (𝐴 ∈ (ℂ̅ ∪ ℂ̂) → (𝐴 ∥ℂ 0)) and ⊢ ((0 ∥ℂ 𝐴) ↔ 𝐴 = 0). (Contributed by BJ, 28-Jul-2023.) |
⊢ ∥ℂ = {〈𝑥, 𝑦〉 ∣ (〈𝑥, 𝑦〉 ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)} | ||
See ccmn 18837 and subsequents. The first few statements of this subsection can be put very early after ccmn 18837. Proposal: in the main part, make separate subsections of commutative monoids and abelian groups. Relabel cabl 18838 to "cabl" or, preferably, other labels containing "abl" to "abel", for consistency. | ||
Theorem | bj-cmnssmnd 34443 | Commutative monoids are monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ CMnd ⊆ Mnd | ||
Theorem | bj-cmnssmndel 34444 | Commutative monoids are monoids (elemental version). This is a more direct proof of cmnmnd 18853, which relies on iscmn 18845. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ CMnd → 𝐴 ∈ Mnd) | ||
Theorem | bj-grpssmnd 34445 | Groups are monoids. (Contributed by BJ, 5-Jan-2024.) (Proof modification is discouraged.) |
⊢ Grp ⊆ Mnd | ||
Theorem | bj-grpssmndel 34446 | Groups are monoids (elemental version). Shorter proof of grpmnd 18050. (Contributed by BJ, 5-Jan-2024.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ Grp → 𝐴 ∈ Mnd) | ||
Theorem | bj-ablssgrp 34447 | Abelian groups are groups. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ Abel ⊆ Grp | ||
Theorem | bj-ablssgrpel 34448 | Abelian groups are groups (elemental version). This is a shorter proof of ablgrp 18842. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ Abel → 𝐴 ∈ Grp) | ||
Theorem | bj-ablsscmn 34449 | Abelian groups are commutative monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ Abel ⊆ CMnd | ||
Theorem | bj-ablsscmnel 34450 | Abelian groups are commutative monoids (elemental version). This is a shorter proof of ablcmn 18844. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ Abel → 𝐴 ∈ CMnd) | ||
Theorem | bj-modssabl 34451 | (The additive groups of) modules are abelian groups. (The elemental version is lmodabl 19612; see also lmodgrp 19572 and lmodcmn 19613.) (Contributed by BJ, 9-Jun-2019.) |
⊢ LMod ⊆ Abel | ||
Theorem | bj-vecssmod 34452 | Vector spaces are modules. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ LVec ⊆ LMod | ||
Theorem | bj-vecssmodel 34453 | Vector spaces are modules (elemental version). This is a shorter proof of lveclmod 19809. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod) | ||
UPDATE: a similar summation is already defined as df-gsum 16706 (although it mixes finite and infinite sums, which makes it harder to understand). | ||
Syntax | cfinsum 34454 | Syntax for the class "finite summation in monoids". |
class FinSum | ||
Definition | df-bj-finsum 34455* | 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 34456* | 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 34457 | Variant of fvimacnv 6816 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 43200. (Contributed by BJ, 7-Jan-2024.) |
⊢ ((Fun 𝐹 ∧ ¬ ∅ ∈ 𝐵) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵))) | ||
Theorem | bj-isvec 34458 | The predicate "is a vector space". (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝜑 → 𝐾 = (Scalar‘𝑉)) ⇒ ⊢ (𝜑 → (𝑉 ∈ LVec ↔ (𝑉 ∈ LMod ∧ 𝐾 ∈ DivRing))) | ||
Theorem | bj-flddrng 34459 | Fields are division rings. (Contributed by BJ, 6-Jan-2024.) |
⊢ Field ⊆ DivRing | ||
Theorem | bj-rrdrg 34460 | The field of real numbers is a division ring. (Contributed by BJ, 6-Jan-2024.) |
⊢ ℝfld ∈ DivRing | ||
Theorem | bj-isclm 34461 | The predicate "is a subcomplex module". (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝜑 → 𝐹 = (Scalar‘𝑊)) & ⊢ (𝜑 → 𝐾 = (Base‘𝐹)) ⇒ ⊢ (𝜑 → (𝑊 ∈ ℂMod ↔ (𝑊 ∈ LMod ∧ 𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 ∈ (SubRing‘ℂfld)))) | ||
Syntax | crrvec 34462 | Syntax for the class of real vector spaces. |
class ℝ-Vec | ||
Definition | df-bj-rvec 34463 | Definition of the class of real vector spaces. The previous definition, ⊢ ℝ-Vec = {𝑥 ∈ LMod ∣ (Scalar‘𝑥) = ℝfld}, can be recovered using bj-isrvec 34464. 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 34470. (Contributed by BJ, 9-Jun-2019.) |
⊢ ℝ-Vec = (LMod ∩ (◡Scalar “ {ℝfld})) | ||
Theorem | bj-isrvec 34464 | The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LMod ∧ (Scalar‘𝑉) = ℝfld)) | ||
Theorem | bj-rvecmod 34465 | Real vector spaces are modules (elemental version). (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ LMod) | ||
Theorem | bj-rvecssmod 34466 | Real vector spaces are modules. (Contributed by BJ, 6-Jan-2024.) |
⊢ ℝ-Vec ⊆ LMod | ||
Theorem | bj-rvecrr 34467 | 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 34468 | The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝜑 → (Scalar‘𝑉) = 𝐾) ⇒ ⊢ (𝜑 → (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LMod ∧ 𝐾 = ℝfld))) | ||
Theorem | bj-rvecvec 34469 | Real vector spaces are vector spaces (elemental version). (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ LVec) | ||
Theorem | bj-isrvec2 34470 | The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝜑 → (Scalar‘𝑉) = 𝐾) ⇒ ⊢ (𝜑 → (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LVec ∧ 𝐾 = ℝfld))) | ||
Theorem | bj-rvecssvec 34471 | Real vector spaces are vector spaces. (Contributed by BJ, 6-Jan-2024.) |
⊢ ℝ-Vec ⊆ LVec | ||
Theorem | bj-rveccmod 34472 | Real vector spaces are subcomplex modules (elemental version). (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ ℂMod) | ||
Theorem | bj-rvecsscmod 34473 | Real vector spaces are subcomplex modules. (Contributed by BJ, 6-Jan-2024.) |
⊢ ℝ-Vec ⊆ ℂMod | ||
Theorem | bj-rvecsscvec 34474 | Real vector spaces are subcomplex vector spaces. (Contributed by BJ, 6-Jan-2024.) |
⊢ ℝ-Vec ⊆ ℂVec | ||
Theorem | bj-rveccvec 34475 | Real vector spaces are subcomplex vector spaces (elemental version). (Contributed by BJ, 6-Jan-2024.) |
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ ℂVec) | ||
Theorem | bj-rvecssabl 34476 | (The additive groups of) real vector spaces are commutative groups. (Contributed by BJ, 9-Jun-2019.) |
⊢ ℝ-Vec ⊆ Abel | ||
Theorem | bj-rvecabl 34477 | (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 34478 | A consequence of commutativity of multiplication. (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) − (𝐵 · 𝐴)) = 0) | ||
Theorem | bj-lineqi 34479 | 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 34482 (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 34480 | Lemma for bj-bary1 34482: expression for a barycenter of two points in one dimension (complex line). (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝑋 = ((((𝐵 − 𝑋) / (𝐵 − 𝐴)) · 𝐴) + (((𝑋 − 𝐴) / (𝐵 − 𝐴)) · 𝐵))) | ||
Theorem | bj-bary1lem1 34481 | 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 34482 | 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) ↔ (𝑆 = ((𝐵 − 𝑋) / (𝐵 − 𝐴)) ∧ 𝑇 = ((𝑋 − 𝐴) / (𝐵 − 𝐴))))) | ||
Theorem | taupilem3 34483 | Lemma for tau-related theorems. (Contributed by Jim Kingdon, 16-Feb-2019.) |
⊢ (𝐴 ∈ (ℝ+ ∩ (◡cos “ {1})) ↔ (𝐴 ∈ ℝ+ ∧ (cos‘𝐴) = 1)) | ||
Theorem | taupilemrplb 34484* | A set of positive reals has (in the reals) a lower bound. (Contributed by Jim Kingdon, 19-Feb-2019.) |
⊢ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (ℝ+ ∩ 𝐴)𝑥 ≤ 𝑦 | ||
Theorem | taupilem1 34485 | Lemma for taupi 34487. A positive real whose cosine is one is at least 2 · π. (Contributed by Jim Kingdon, 19-Feb-2019.) |
⊢ ((𝐴 ∈ ℝ+ ∧ (cos‘𝐴) = 1) → (2 · π) ≤ 𝐴) | ||
Theorem | taupilem2 34486 | Lemma for taupi 34487. 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 34487 | 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 34488* | Alternate definition of the gcd operator. (Contributed by Jim Kingdon, 31-Dec-2021.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (℩𝑑 ∈ ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)))) | ||
Theorem | csbdif 34489 | Distribution of class substitution over difference of two classes. (Contributed by ML, 14-Jul-2020.) |
⊢ ⦋𝐴 / 𝑥⦌(𝐵 ∖ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∖ ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | csbpredg 34490 | Move class substitution in and out of the predecessor class of a relationship. (Contributed by ML, 25-Oct-2020.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌Pred(𝑅, 𝐷, 𝑋) = Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, ⦋𝐴 / 𝑥⦌𝑋)) | ||
Theorem | csbwrecsg 34491 | Move class substitution in and out of the well-founded recursive function generator. (Contributed by ML, 25-Oct-2020.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌wrecs(𝑅, 𝐷, 𝐹) = wrecs(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, ⦋𝐴 / 𝑥⦌𝐹)) | ||
Theorem | csbrecsg 34492 | Move class substitution in and out of recs. (Contributed by ML, 25-Oct-2020.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌recs(𝐹) = recs(⦋𝐴 / 𝑥⦌𝐹)) | ||
Theorem | csbrdgg 34493 | Move class substitution in and out of the recursive function generator. (Contributed by ML, 25-Oct-2020.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌rec(𝐹, 𝐼) = rec(⦋𝐴 / 𝑥⦌𝐹, ⦋𝐴 / 𝑥⦌𝐼)) | ||
Theorem | csboprabg 34494* | Move class substitution in and out of class abstractions of nested ordered pairs. (Contributed by ML, 25-Oct-2020.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{〈〈𝑦, 𝑧〉, 𝑑〉 ∣ 𝜑} = {〈〈𝑦, 𝑧〉, 𝑑〉 ∣ [𝐴 / 𝑥]𝜑}) | ||
Theorem | csbmpo123 34495* | Move class substitution in and out of maps-to notation for operations. (Contributed by ML, 25-Oct-2020.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑦 ∈ 𝑌, 𝑧 ∈ 𝑍 ↦ 𝐷) = (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌, 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑍 ↦ ⦋𝐴 / 𝑥⦌𝐷)) | ||
Theorem | con1bii2 34496 | A contraposition inference. (Contributed by ML, 18-Oct-2020.) |
⊢ (¬ 𝜑 ↔ 𝜓) ⇒ ⊢ (𝜑 ↔ ¬ 𝜓) | ||
Theorem | con2bii2 34497 | A contraposition inference. (Contributed by ML, 18-Oct-2020.) |
⊢ (𝜑 ↔ ¬ 𝜓) ⇒ ⊢ (¬ 𝜑 ↔ 𝜓) | ||
Theorem | vtoclefex 34498* | Implicit substitution of a class for a setvar variable. (Contributed by ML, 17-Oct-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝑥 = 𝐴 → 𝜑) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜑) | ||
Theorem | rnmptsn 34499* | The range of a function mapping to singletons. (Contributed by ML, 15-Jul-2020.) |
⊢ ran (𝑥 ∈ 𝐴 ↦ {𝑥}) = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}} | ||
Theorem | f1omptsnlem 34500* | This is the core of the proof of f1omptsn 34501, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 15-Jul-2020.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ {𝑥}) & ⊢ 𝑅 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}} ⇒ ⊢ 𝐹:𝐴–1-1-onto→𝑅 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |