P. 377 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37601-37700   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	crrhat 37601	Syntax for ℝ̂.
class ℝ̂
Definition	df-bj-rrhat 37602	Define the real projective line. (Contributed by BJ, 27-Jun-2019.)
⊢ ℝ̂ = (ℝ ∪ {∞})
Theorem	bj-rrhatsscchat 37603	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 37604	Syntax for the addition on extended complex numbers.
class +ℂ̅
Definition	df-bj-addc 37605	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 37606	Syntax for negation on the set of extended complex numbers and the complex projective line (Riemann sphere).
class -ℂ̅
Definition	df-bj-oppc 37607*	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 11182 without the intermediate step of df-lt 11049.
Syntax	cltxr 37608	Syntax for the standard (strict) order on the extended reals.
class <ℝ̅
Definition	df-bj-lt 37609*	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 37613.
Syntax	carg 37610	Syntax for the argument of a nonzero extended complex number.
class Arg
Definition	df-bj-arg 37611	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 37566), and therefore should not be relied upon. (New usage is discouraged.)
⊢ Arg = (𝑥 ∈ (ℂ̅ ∖ {0}) ↦ if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π, (((1st ‘𝑥) / (2 · π)) − π))))
Syntax	cmulc 37612	Syntax for the multiplication of extended complex numbers.
class ·ℂ̅
Definition	df-bj-mulc 37613	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 37615). 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 37614	Syntax for the inverse of nonzero extended complex numbers.
class -1ℂ̅
Definition	df-bj-invc 37615*	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 37613, 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 37616	Syntax for the canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}).
class iω↪ℕ
Definition	df-bj-iomnn 37617*	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 37564 but we did not use the present definition there since we wanted to have defined +∞ first. See bj-iomnnom 37626 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 37618	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 37619	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 37620	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 37621	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 37622	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 37623	The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 7134. (Contributed by NM, 23-Sep-2007.) Put in deduction form. (Revised by BJ, 18-Mar-2023.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐺 = ((𝐹 ↾ (𝐶 ∖ {𝐴})) ∪ {⟨𝐴, 𝐵⟩}))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐺‘𝐴) = 𝐵)
Theorem	bj-fvmptunsn1 37624*	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 37625*	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 37626	The canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}) maps ω to +∞. (Contributed by BJ, 18-Feb-2023.)
⊢ (iω↪ℕ‘ω) = +∞
21.19.6.10  Divisibility
Syntax	cnnbar 37627	Syntax for the extended natural numbers.
class ℕ̅
Definition	df-bj-nnbar 37628	Definition of the extended natural numbers. (Contributed by BJ, 28-Jul-2023.)
⊢ ℕ̅ = (ℕ0 ∪ {+∞})
Syntax	czzbar 37629	Syntax for the extended integers.
class ℤ̅
Definition	df-bj-zzbar 37630	Definition of the extended integers. (Contributed by BJ, 28-Jul-2023.)
⊢ ℤ̅ = (ℤ ∪ {-∞, +∞})
Syntax	czzhat 37631	Syntax for the one-point-compactified integers.
class ℤ̂
Definition	df-bj-zzhat 37632	Definition of the one-point-compactified. (Contributed by BJ, 28-Jul-2023.)
⊢ ℤ̂ = (ℤ ∪ {∞})
Syntax	cdivc 37633	Syntax for the divisibility relation.
class ∥ℂ
Definition	df-bj-divc 37634*	Definition of the divisibility relation (compare df-dvds 16220). Since 0 is absorbing, ⊢ (𝐴 ∈ (ℂ̅ ∪ ℂ̂) → (𝐴 ∥ℂ 0)) and ⊢ ((0 ∥ℂ 𝐴) ↔ 𝐴 = 0). (Contributed by BJ, 28-Jul-2023.)
⊢ ∥ℂ = {⟨𝑥, 𝑦⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)}
21.19.7  Monoids See ccmn 19753 and subsequents. The first few statements of this subsection can be put very early after ccmn 19753. Proposal: in the main part, make separate subsections of commutative monoids and abelian groups. Relabel cabl 19754 to "cabl" or, preferably, other labels containing "abl" to "abel", for consistency.
Theorem	bj-smgrpssmgm 37635	Semigroups are magmas. (Contributed by BJ, 12-Apr-2024.) (Proof modification is discouraged.)
⊢ Smgrp ⊆ Mgm
Theorem	bj-smgrpssmgmel 37636	Semigroups are magmas (elemental version). (Contributed by BJ, 12-Apr-2024.) (Proof modification is discouraged.)
⊢ (𝐺 ∈ Smgrp → 𝐺 ∈ Mgm)
Theorem	bj-mndsssmgrp 37637	Monoids are semigroups. (Contributed by BJ, 11-Apr-2024.) (Proof modification is discouraged.)
⊢ Mnd ⊆ Smgrp
Theorem	bj-mndsssmgrpel 37638	Monoids are semigroups (elemental version). (Contributed by BJ, 11-Apr-2024.) (Proof modification is discouraged.)
⊢ (𝐺 ∈ Mnd → 𝐺 ∈ Smgrp)
Theorem	bj-cmnssmnd 37639	Commutative monoids are monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ CMnd ⊆ Mnd
Theorem	bj-cmnssmndel 37640	Commutative monoids are monoids (elemental version). This is a more direct proof of cmnmnd 19770, which relies on iscmn 19762. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ CMnd → 𝐴 ∈ Mnd)
Theorem	bj-grpssmnd 37641	Groups are monoids. (Contributed by BJ, 5-Jan-2024.) (Proof modification is discouraged.)
⊢ Grp ⊆ Mnd
Theorem	bj-grpssmndel 37642	Groups are monoids (elemental version). Shorter proof of grpmnd 18914. (Contributed by BJ, 5-Jan-2024.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ Grp → 𝐴 ∈ Mnd)
Theorem	bj-ablssgrp 37643	Abelian groups are groups. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ Abel ⊆ Grp
Theorem	bj-ablssgrpel 37644	Abelian groups are groups (elemental version). This is a shorter proof of ablgrp 19758. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ Abel → 𝐴 ∈ Grp)
Theorem	bj-ablsscmn 37645	Abelian groups are commutative monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ Abel ⊆ CMnd
Theorem	bj-ablsscmnel 37646	Abelian groups are commutative monoids (elemental version). This is a shorter proof of ablcmn 19760. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ Abel → 𝐴 ∈ CMnd)
Theorem	bj-modssabl 37647	(The additive groups of) modules are abelian groups. (The elemental version is lmodabl 20906; see also lmodgrp 20864 and lmodcmn 20907.) (Contributed by BJ, 9-Jun-2019.)
⊢ LMod ⊆ Abel
Theorem	bj-vecssmod 37648	Vector spaces are modules. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ LVec ⊆ LMod
Theorem	bj-vecssmodel 37649	Vector spaces are modules (elemental version). This is a shorter proof of lveclmod 21103. (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 17403 (although it mixes finite and infinite sums, which makes it harder to understand).
Syntax	cfinsum 37650	Syntax for the class "finite summation in monoids".
class FinSum
Definition	df-bj-finsum 37651*	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 37652*	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 37653	Variant of fvimacnv 7001 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 47590. (Contributed by BJ, 7-Jan-2024.)
⊢ ((Fun 𝐹 ∧ ¬ ∅ ∈ 𝐵) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵)))
Theorem	bj-isvec 37654	The predicate "is a vector space". (Contributed by BJ, 6-Jan-2024.)
⊢ (𝜑 → 𝐾 = (Scalar‘𝑉))    ⇒   ⊢ (𝜑 → (𝑉 ∈ LVec ↔ (𝑉 ∈ LMod ∧ 𝐾 ∈ DivRing)))
Theorem	bj-fldssdrng 37655	Fields are division rings. (Contributed by BJ, 6-Jan-2024.)
⊢ Field ⊆ DivRing
Theorem	bj-flddrng 37656	Fields are division rings (elemental version). (Contributed by BJ, 9-Nov-2024.)
⊢ (𝐹 ∈ Field → 𝐹 ∈ DivRing)
Theorem	bj-rrdrg 37657	The field of real numbers is a division ring. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝfld ∈ DivRing
Theorem	bj-isclm 37658	The predicate "is a subcomplex module". (Contributed by BJ, 6-Jan-2024.)
⊢ (𝜑 → 𝐹 = (Scalar‘𝑊))    &   ⊢ (𝜑 → 𝐾 = (Base‘𝐹))    ⇒   ⊢ (𝜑 → (𝑊 ∈ ℂMod ↔ (𝑊 ∈ LMod ∧ 𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 ∈ (SubRing‘ℂfld))))
Syntax	crrvec 37659	Syntax for the class of real vector spaces.
class ℝ-Vec
Definition	df-bj-rvec 37660	Definition of the class of real vector spaces. The previous definition, ⊢ ℝ-Vec = {𝑥 ∈ LMod ∣ (Scalar‘𝑥) = ℝfld}, can be recovered using bj-isrvec 37661. 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 37667. (Contributed by BJ, 9-Jun-2019.)
⊢ ℝ-Vec = (LMod ∩ (◡Scalar “ {ℝfld}))
Theorem	bj-isrvec 37661	The predicate "is a real vector space". Using df-sca 17234 instead of scaid 17276 shortens the proof by two syntactic steps, but it is preferable not to rely on the precise definition df-sca 17234. (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LMod ∧ (Scalar‘𝑉) = ℝfld))
Theorem	bj-rvecmod 37662	Real vector spaces are modules (elemental version). (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ LMod)
Theorem	bj-rvecssmod 37663	Real vector spaces are modules. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝ-Vec ⊆ LMod
Theorem	bj-rvecrr 37664	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 37665	The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024.)
⊢ (𝜑 → (Scalar‘𝑉) = 𝐾)    ⇒   ⊢ (𝜑 → (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LMod ∧ 𝐾 = ℝfld)))
Theorem	bj-rvecvec 37666	Real vector spaces are vector spaces (elemental version). (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ LVec)
Theorem	bj-isrvec2 37667	The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024.)
⊢ (𝜑 → (Scalar‘𝑉) = 𝐾)    ⇒   ⊢ (𝜑 → (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LVec ∧ 𝐾 = ℝfld)))
Theorem	bj-rvecssvec 37668	Real vector spaces are vector spaces. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝ-Vec ⊆ LVec
Theorem	bj-rveccmod 37669	Real vector spaces are subcomplex modules (elemental version). (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ ℂMod)
Theorem	bj-rvecsscmod 37670	Real vector spaces are subcomplex modules. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝ-Vec ⊆ ℂMod
Theorem	bj-rvecsscvec 37671	Real vector spaces are subcomplex vector spaces. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝ-Vec ⊆ ℂVec
Theorem	bj-rveccvec 37672	Real vector spaces are subcomplex vector spaces (elemental version). (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ ℂVec)
Theorem	bj-rvecssabl 37673	(The additive groups of) real vector spaces are commutative groups. (Contributed by BJ, 9-Jun-2019.)
⊢ ℝ-Vec ⊆ Abel
Theorem	bj-rvecabl 37674	(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 37675	A consequence of commutativity of multiplication. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) − (𝐵 · 𝐴)) = 0)
Theorem	bj-lineqi 37676	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 37679 (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 37677	Lemma for bj-bary1 37679: expression for a barycenter of two points in one dimension (complex line). (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = ((((𝐵 − 𝑋) / (𝐵 − 𝐴)) · 𝐴) + (((𝑋 − 𝐴) / (𝐵 − 𝐴)) · 𝐵)))
Theorem	bj-bary1lem1 37678	Lemma for bj-bary1 37679: 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 37679	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 37680	Token for the monoid of endomorphisms.
class End
Definition	df-bj-end 37681*	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 37682	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 37683	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 37684	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 37685	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 37686	Lemma for tau-related theorems. (Contributed by Jim Kingdon, 16-Feb-2019.)
⊢ (𝐴 ∈ (ℝ+ ∩ (◡cos “ {1})) ↔ (𝐴 ∈ ℝ+ ∧ (cos‘𝐴) = 1))
Theorem	taupilemrplb 37687*	A set of positive reals has (in the reals) a lower bound. (Contributed by Jim Kingdon, 19-Feb-2019.)
⊢ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (ℝ+ ∩ 𝐴)𝑥 ≤ 𝑦
Theorem	taupilem1 37688	Lemma for taupi 37690. A positive real whose cosine is one is at least 2 · π. (Contributed by Jim Kingdon, 19-Feb-2019.)
⊢ ((𝐴 ∈ ℝ+ ∧ (cos‘𝐴) = 1) → (2 · π) ≤ 𝐴)
Theorem	taupilem2 37689	Lemma for taupi 37690. 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 37690	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 37691*	Alternate definition of the gcd operator. (Contributed by Jim Kingdon, 31-Dec-2021.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (℩𝑑 ∈ ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))))
21.20.3  Real numbers
Theorem	irrdifflemf 37692	Lemma for irrdiff 37693. The forward direction. (Contributed by Jim Kingdon, 20-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ ℚ)    &   ⊢ (𝜑 → 𝑄 ∈ ℚ)    &   ⊢ (𝜑 → 𝑅 ∈ ℚ)    &   ⊢ (𝜑 → 𝑄 ≠ 𝑅)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) ≠ (abs‘(𝐴 − 𝑅)))
Theorem	irrdiff 37693*	The irrationals are exactly those reals that are a different distance from every rational. (Contributed by Jim Kingdon, 19-May-2024.)
⊢ (𝐴 ∈ ℝ → (¬ 𝐴 ∈ ℚ ↔ ∀𝑞 ∈ ℚ ∀𝑟 ∈ ℚ (𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) ≠ (abs‘(𝐴 − 𝑟)))))
Theorem	qdiff 37694*	The rationals are exactly those reals for which there exist two distinct rationals that are the same distance from the original number. Similar to irrdiff 37693 but here proved with a proof which would also work in constructive mathematics. From an online post by Ingo Blechschmidt. For a proof using irrdiff 37693, see qdiffALT 37695. (Contributed by Jim Kingdon, 24-Apr-2026.)
⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℚ ↔ ∃𝑞 ∈ ℚ ∃𝑟 ∈ ℚ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))))
Theorem	qdiffALT 37695*	Alternate proof of qdiff 37694. This is a proof from irrdiff 37693 using excluded middle in a variety of places. (Contributed by Jim Kingdon, 27-Apr-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℚ ↔ ∃𝑞 ∈ ℚ ∃𝑟 ∈ ℚ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))))
Theorem	iccioo01 37696	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)
21.21  Mathbox for ML
21.21.1  Miscellaneous
Theorem	csbrecsg 37697	Move class substitution in and out of recs. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌recs(𝐹) = recs(⦋𝐴 / 𝑥⦌𝐹))
Theorem	csbrdgg 37698	Move class substitution in and out of the recursive function generator. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌rec(𝐹, 𝐼) = rec(⦋𝐴 / 𝑥⦌𝐹, ⦋𝐴 / 𝑥⦌𝐼))
Theorem	csboprabg 37699*	Move class substitution in and out of class abstractions of nested ordered pairs. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∣ 𝜑} = {⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∣ [𝐴 / 𝑥]𝜑})
Theorem	csbmpo123 37700*	Move class substitution in and out of maps-to notation for operations. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑦 ∈ 𝑌, 𝑧 ∈ 𝑍 ↦ 𝐷) = (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌, 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑍 ↦ ⦋𝐴 / 𝑥⦌𝐷))