P. 373 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37201-37300   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	crrbar 37201	Syntax for the set of extended real numbers.
class ℝ̅
Definition	df-bj-rrbar 37202	Definition of the set of extended real numbers. This aims to replace df-xr 11172. (Contributed by BJ, 29-Jun-2019.)
⊢ ℝ̅ = (ℝ ∪ {-∞, +∞})
Syntax	cinfty 37203	Syntax for ∞.
class ∞
Definition	df-bj-infty 37204	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 37205	Syntax for ℂ̂.
class ℂ̂
Definition	df-bj-cchat 37206	Define the complex projective line, or Riemann sphere. (Contributed by BJ, 27-Jun-2019.)
⊢ ℂ̂ = (ℂ ∪ {∞})
Syntax	crrhat 37207	Syntax for ℝ̂.
class ℝ̂
Definition	df-bj-rrhat 37208	Define the real projective line. (Contributed by BJ, 27-Jun-2019.)
⊢ ℝ̂ = (ℝ ∪ {∞})
Theorem	bj-rrhatsscchat 37209	The real projective line is included in the complex projective line. (Contributed by BJ, 27-Jun-2019.)
⊢ ℝ̂ ⊆ ℂ̂
21.19.6.6  Addition and opposite 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 37210	Syntax for the addition on extended complex numbers.
class +ℂ̅
Definition	df-bj-addc 37211	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 37212	Syntax for negation on the set of extended complex numbers and the complex projective line (Riemann sphere).
class -ℂ̅
Definition	df-bj-oppc 37213*	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⟩)))))
21.19.6.7  Order relation on the extended reals In this section, we redefine df-ltxr 11173 without the intermediate step of df-lt 11041.
Syntax	cltxr 37214	Syntax for the standard (strict) order on the extended reals.
class <ℝ̅
Definition	df-bj-lt 37215*	Define the standard (strict) order on the extended reals. (Contributed by BJ, 4-Feb-2023.)
⊢ <ℝ̅ = ({𝑥 ∈ (ℝ̅ × ℝ̅) ∣ ∃𝑦∃𝑧(((1st ‘𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd ‘𝑥) = ⟨𝑧, 0R⟩) ∧ 𝑦 <R 𝑧)} ∪ ((({-∞} × ℝ) ∪ (ℝ × {+∞})) ∪ ({-∞} × {+∞})))
21.19.6.8  Argument, multiplication and inverse 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 37219.
Syntax	carg 37216	Syntax for the argument of a nonzero extended complex number.
class Arg
Definition	df-bj-arg 37217	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 37172), and therefore should not be relied upon. (New usage is discouraged.)
⊢ Arg = (𝑥 ∈ (ℂ̅ ∖ {0}) ↦ if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π, (((1st ‘𝑥) / (2 · π)) − π))))
Syntax	cmulc 37218	Syntax for the multiplication of extended complex numbers.
class ·ℂ̅
Definition	df-bj-mulc 37219	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 37221). 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 37220	Syntax for the inverse of nonzero extended complex numbers.
class -1ℂ̅
Definition	df-bj-invc 37221*	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 37219, 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)))
21.19.6.9  The canonical bijection from the finite ordinals
Syntax	ciomnn 37222	Syntax for the canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}).
class iω↪ℕ
Definition	df-bj-iomnn 37223*	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 37170 but we did not use the present definition there since we wanted to have defined +∞ first. See bj-iomnnom 37232 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 37224	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 37225	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 37226	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 37227	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 37228	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 37229	The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 7123. (Contributed by NM, 23-Sep-2007.) Put in deduction form. (Revised by BJ, 18-Mar-2023.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐺 = ((𝐹 ↾ (𝐶 ∖ {𝐴})) ∪ {⟨𝐴, 𝐵⟩}))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐺‘𝐴) = 𝐵)
Theorem	bj-fvmptunsn1 37230*	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 37231*	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 37232	The canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}) maps ω to +∞. (Contributed by BJ, 18-Feb-2023.)
⊢ (iω↪ℕ‘ω) = +∞
21.19.6.10  Divisibility
Syntax	cnnbar 37233	Syntax for the extended natural numbers.
class ℕ̅
Definition	df-bj-nnbar 37234	Definition of the extended natural numbers. (Contributed by BJ, 28-Jul-2023.)
⊢ ℕ̅ = (ℕ0 ∪ {+∞})
Syntax	czzbar 37235	Syntax for the extended integers.
class ℤ̅
Definition	df-bj-zzbar 37236	Definition of the extended integers. (Contributed by BJ, 28-Jul-2023.)
⊢ ℤ̅ = (ℤ ∪ {-∞, +∞})
Syntax	czzhat 37237	Syntax for the one-point-compactified integers.
class ℤ̂
Definition	df-bj-zzhat 37238	Definition of the one-point-compactified. (Contributed by BJ, 28-Jul-2023.)
⊢ ℤ̂ = (ℤ ∪ {∞})
Syntax	cdivc 37239	Syntax for the divisibility relation.
class ∥ℂ
Definition	df-bj-divc 37240*	Definition of the divisibility relation (compare df-dvds 16182). Since 0 is absorbing, ⊢ (𝐴 ∈ (ℂ̅ ∪ ℂ̂) → (𝐴 ∥ℂ 0)) and ⊢ ((0 ∥ℂ 𝐴) ↔ 𝐴 = 0). (Contributed by BJ, 28-Jul-2023.)
⊢ ∥ℂ = {⟨𝑥, 𝑦⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)}
21.19.7  Monoids See ccmn 19677 and subsequents. The first few statements of this subsection can be put very early after ccmn 19677. Proposal: in the main part, make separate subsections of commutative monoids and abelian groups. Relabel cabl 19678 to "cabl" or, preferably, other labels containing "abl" to "abel", for consistency.
Theorem	bj-smgrpssmgm 37241	Semigroups are magmas. (Contributed by BJ, 12-Apr-2024.) (Proof modification is discouraged.)
⊢ Smgrp ⊆ Mgm
Theorem	bj-smgrpssmgmel 37242	Semigroups are magmas (elemental version). (Contributed by BJ, 12-Apr-2024.) (Proof modification is discouraged.)
⊢ (𝐺 ∈ Smgrp → 𝐺 ∈ Mgm)
Theorem	bj-mndsssmgrp 37243	Monoids are semigroups. (Contributed by BJ, 11-Apr-2024.) (Proof modification is discouraged.)
⊢ Mnd ⊆ Smgrp
Theorem	bj-mndsssmgrpel 37244	Monoids are semigroups (elemental version). (Contributed by BJ, 11-Apr-2024.) (Proof modification is discouraged.)
⊢ (𝐺 ∈ Mnd → 𝐺 ∈ Smgrp)
Theorem	bj-cmnssmnd 37245	Commutative monoids are monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ CMnd ⊆ Mnd
Theorem	bj-cmnssmndel 37246	Commutative monoids are monoids (elemental version). This is a more direct proof of cmnmnd 19694, which relies on iscmn 19686. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ CMnd → 𝐴 ∈ Mnd)
Theorem	bj-grpssmnd 37247	Groups are monoids. (Contributed by BJ, 5-Jan-2024.) (Proof modification is discouraged.)
⊢ Grp ⊆ Mnd
Theorem	bj-grpssmndel 37248	Groups are monoids (elemental version). Shorter proof of grpmnd 18837. (Contributed by BJ, 5-Jan-2024.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ Grp → 𝐴 ∈ Mnd)
Theorem	bj-ablssgrp 37249	Abelian groups are groups. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ Abel ⊆ Grp
Theorem	bj-ablssgrpel 37250	Abelian groups are groups (elemental version). This is a shorter proof of ablgrp 19682. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ Abel → 𝐴 ∈ Grp)
Theorem	bj-ablsscmn 37251	Abelian groups are commutative monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ Abel ⊆ CMnd
Theorem	bj-ablsscmnel 37252	Abelian groups are commutative monoids (elemental version). This is a shorter proof of ablcmn 19684. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ Abel → 𝐴 ∈ CMnd)
Theorem	bj-modssabl 37253	(The additive groups of) modules are abelian groups. (The elemental version is lmodabl 20830; see also lmodgrp 20788 and lmodcmn 20831.) (Contributed by BJ, 9-Jun-2019.)
⊢ LMod ⊆ Abel
Theorem	bj-vecssmod 37254	Vector spaces are modules. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ LVec ⊆ LMod
Theorem	bj-vecssmodel 37255	Vector spaces are modules (elemental version). This is a shorter proof of lveclmod 21028. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod)
21.19.7.1  Finite sums in monoids UPDATE: a similar summation is already defined as df-gsum 17364 (although it mixes finite and infinite sums, which makes it harder to understand).
Syntax	cfinsum 37256	Syntax for the class "finite summation in monoids".
class FinSum
Definition	df-bj-finsum 37257*	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 37258*	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‘𝐴), (𝑛 ∈ ℕ ↦ (𝐵‘(𝑓‘𝑛))))‘(♯‘𝐼)))))
21.19.8  Affine, Euclidean, and Cartesian geometry 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.
21.19.8.1  Real vector spaces In this section, we introduce real vector spaces.
Theorem	bj-fvimacnv0 37259	Variant of fvimacnv 6991 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 47105. (Contributed by BJ, 7-Jan-2024.)
⊢ ((Fun 𝐹 ∧ ¬ ∅ ∈ 𝐵) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵)))
Theorem	bj-isvec 37260	The predicate "is a vector space". (Contributed by BJ, 6-Jan-2024.)
⊢ (𝜑 → 𝐾 = (Scalar‘𝑉))    ⇒   ⊢ (𝜑 → (𝑉 ∈ LVec ↔ (𝑉 ∈ LMod ∧ 𝐾 ∈ DivRing)))
Theorem	bj-fldssdrng 37261	Fields are division rings. (Contributed by BJ, 6-Jan-2024.)
⊢ Field ⊆ DivRing
Theorem	bj-flddrng 37262	Fields are division rings (elemental version). (Contributed by BJ, 9-Nov-2024.)
⊢ (𝐹 ∈ Field → 𝐹 ∈ DivRing)
Theorem	bj-rrdrg 37263	The field of real numbers is a division ring. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝfld ∈ DivRing
Theorem	bj-isclm 37264	The predicate "is a subcomplex module". (Contributed by BJ, 6-Jan-2024.)
⊢ (𝜑 → 𝐹 = (Scalar‘𝑊))    &   ⊢ (𝜑 → 𝐾 = (Base‘𝐹))    ⇒   ⊢ (𝜑 → (𝑊 ∈ ℂMod ↔ (𝑊 ∈ LMod ∧ 𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 ∈ (SubRing‘ℂfld))))
Syntax	crrvec 37265	Syntax for the class of real vector spaces.
class ℝ-Vec
Definition	df-bj-rvec 37266	Definition of the class of real vector spaces. The previous definition, ⊢ ℝ-Vec = {𝑥 ∈ LMod ∣ (Scalar‘𝑥) = ℝfld}, can be recovered using bj-isrvec 37267. 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 37273. (Contributed by BJ, 9-Jun-2019.)
⊢ ℝ-Vec = (LMod ∩ (◡Scalar “ {ℝfld}))
Theorem	bj-isrvec 37267	The predicate "is a real vector space". Using df-sca 17195 instead of scaid 17237 would shorten the proof by two syntactic steps, but it is preferable not to rely on the precise definition df-sca 17195. (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LMod ∧ (Scalar‘𝑉) = ℝfld))
Theorem	bj-rvecmod 37268	Real vector spaces are modules (elemental version). (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ LMod)
Theorem	bj-rvecssmod 37269	Real vector spaces are modules. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝ-Vec ⊆ LMod
Theorem	bj-rvecrr 37270	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 37271	The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024.)
⊢ (𝜑 → (Scalar‘𝑉) = 𝐾)    ⇒   ⊢ (𝜑 → (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LMod ∧ 𝐾 = ℝfld)))
Theorem	bj-rvecvec 37272	Real vector spaces are vector spaces (elemental version). (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ LVec)
Theorem	bj-isrvec2 37273	The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024.)
⊢ (𝜑 → (Scalar‘𝑉) = 𝐾)    ⇒   ⊢ (𝜑 → (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LVec ∧ 𝐾 = ℝfld)))
Theorem	bj-rvecssvec 37274	Real vector spaces are vector spaces. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝ-Vec ⊆ LVec
Theorem	bj-rveccmod 37275	Real vector spaces are subcomplex modules (elemental version). (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ ℂMod)
Theorem	bj-rvecsscmod 37276	Real vector spaces are subcomplex modules. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝ-Vec ⊆ ℂMod
Theorem	bj-rvecsscvec 37277	Real vector spaces are subcomplex vector spaces. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝ-Vec ⊆ ℂVec
Theorem	bj-rveccvec 37278	Real vector spaces are subcomplex vector spaces (elemental version). (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ ℂVec)
Theorem	bj-rvecssabl 37279	(The additive groups of) real vector spaces are commutative groups. (Contributed by BJ, 9-Jun-2019.)
⊢ ℝ-Vec ⊆ Abel
Theorem	bj-rvecabl 37280	(The additive groups of) real vector spaces are commutative groups (elemental version). (Contributed by BJ, 9-Jun-2019.)
⊢ (𝐴 ∈ ℝ-Vec → 𝐴 ∈ Abel)
21.19.8.2  Complex numbers (supplements) Some lemmas to ease algebraic manipulations.
Theorem	bj-subcom 37281	A consequence of commutativity of multiplication. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) − (𝐵 · 𝐴)) = 0)
Theorem	bj-lineqi 37282	Solution of a (scalar) linear equation. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑌 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → ((𝐴 · 𝑋) + 𝐵) = 𝑌)    ⇒   ⊢ (𝜑 → 𝑋 = ((𝑌 − 𝐵) / 𝐴))
21.19.8.3  Barycentric coordinates 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 37285 (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 37283	Lemma for bj-bary1 37285: expression for a barycenter of two points in one dimension (complex line). (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = ((((𝐵 − 𝑋) / (𝐵 − 𝐴)) · 𝐴) + (((𝑋 − 𝐴) / (𝐵 − 𝐴)) · 𝐵)))
Theorem	bj-bary1lem1 37284	Lemma for bj-bary1 37285: 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 37285	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) ↔ (𝑆 = ((𝐵 − 𝑋) / (𝐵 − 𝐴)) ∧ 𝑇 = ((𝑋 − 𝐴) / (𝐵 − 𝐴)))))
21.19.9  Monoid of endomorphisms
Syntax	cend 37286	Token for the monoid of endomorphisms.
class End
Definition	df-bj-end 37287*	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 37288	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 37289	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 37290	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 37291	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)
21.20  Mathbox for Jim Kingdon
21.20.1  Circle constant
Theorem	taupilem3 37292	Lemma for tau-related theorems. (Contributed by Jim Kingdon, 16-Feb-2019.)
⊢ (𝐴 ∈ (ℝ+ ∩ (◡cos “ {1})) ↔ (𝐴 ∈ ℝ+ ∧ (cos‘𝐴) = 1))
Theorem	taupilemrplb 37293*	A set of positive reals has (in the reals) a lower bound. (Contributed by Jim Kingdon, 19-Feb-2019.)
⊢ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (ℝ+ ∩ 𝐴)𝑥 ≤ 𝑦
Theorem	taupilem1 37294	Lemma for taupi 37296. A positive real whose cosine is one is at least 2 · π. (Contributed by Jim Kingdon, 19-Feb-2019.)
⊢ ((𝐴 ∈ ℝ+ ∧ (cos‘𝐴) = 1) → (2 · π) ≤ 𝐴)
Theorem	taupilem2 37295	Lemma for taupi 37296. 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 37296	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 · π)
21.20.2  Number theory
Theorem	dfgcd3 37297*	Alternate definition of the gcd operator. (Contributed by Jim Kingdon, 31-Dec-2021.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (℩𝑑 ∈ ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))))
21.20.3  Real numbers
Theorem	irrdifflemf 37298	Lemma for irrdiff 37299. The forward direction. (Contributed by Jim Kingdon, 20-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ ℚ)    &   ⊢ (𝜑 → 𝑄 ∈ ℚ)    &   ⊢ (𝜑 → 𝑅 ∈ ℚ)    &   ⊢ (𝜑 → 𝑄 ≠ 𝑅)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) ≠ (abs‘(𝐴 − 𝑅)))
Theorem	irrdiff 37299*	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 37300	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)