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
Definition	df-bj-rrhat 37201	Define the real projective line. (Contributed by BJ, 27-Jun-2019.)
⊢ ℝ̂ = (ℝ ∪ {∞})
Theorem	bj-rrhatsscchat 37202	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 37203	Syntax for the addition on extended complex numbers.
class +ℂ̅
Definition	df-bj-addc 37204	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 37205	Syntax for negation on the set of extended complex numbers and the complex projective line (Riemann sphere).
class -ℂ̅
Definition	df-bj-oppc 37206*	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 11329 without the intermediate step of df-lt 11197.
Syntax	cltxr 37207	Syntax for the standard (strict) order on the extended reals.
class <ℝ̅
Definition	df-bj-lt 37208*	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 37212.
Syntax	carg 37209	Syntax for the argument of a nonzero extended complex number.
class Arg
Definition	df-bj-arg 37210	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 37165), and therefore should not be relied upon. (New usage is discouraged.)
⊢ Arg = (𝑥 ∈ (ℂ̅ ∖ {0}) ↦ if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π, (((1st ‘𝑥) / (2 · π)) − π))))
Syntax	cmulc 37211	Syntax for the multiplication of extended complex numbers.
class ·ℂ̅
Definition	df-bj-mulc 37212	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 37214). 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 37213	Syntax for the inverse of nonzero extended complex numbers.
class -1ℂ̅
Definition	df-bj-invc 37214*	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 37212, 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 37215	Syntax for the canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}).
class iω↪ℕ
Definition	df-bj-iomnn 37216*	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 37163 but we did not use the present definition there since we wanted to have defined +∞ first. See bj-iomnnom 37225 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 37217	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 37218	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 37219	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 37220	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 37221	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 37222	The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 7217. (Contributed by NM, 23-Sep-2007.) Put in deduction form. (Revised by BJ, 18-Mar-2023.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐺 = ((𝐹 ↾ (𝐶 ∖ {𝐴})) ∪ {⟨𝐴, 𝐵⟩}))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐺‘𝐴) = 𝐵)
Theorem	bj-fvmptunsn1 37223*	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 37224*	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 37225	The canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}) maps ω to +∞. (Contributed by BJ, 18-Feb-2023.)
⊢ (iω↪ℕ‘ω) = +∞
21.19.6.10  Divisibility
Syntax	cnnbar 37226	Syntax for the extended natural numbers.
class ℕ̅
Definition	df-bj-nnbar 37227	Definition of the extended natural numbers. (Contributed by BJ, 28-Jul-2023.)
⊢ ℕ̅ = (ℕ0 ∪ {+∞})
Syntax	czzbar 37228	Syntax for the extended integers.
class ℤ̅
Definition	df-bj-zzbar 37229	Definition of the extended integers. (Contributed by BJ, 28-Jul-2023.)
⊢ ℤ̅ = (ℤ ∪ {-∞, +∞})
Syntax	czzhat 37230	Syntax for the one-point-compactified integers.
class ℤ̂
Definition	df-bj-zzhat 37231	Definition of the one-point-compactified. (Contributed by BJ, 28-Jul-2023.)
⊢ ℤ̂ = (ℤ ∪ {∞})
Syntax	cdivc 37232	Syntax for the divisibility relation.
class ∥ℂ
Definition	df-bj-divc 37233*	Definition of the divisibility relation (compare df-dvds 16303). Since 0 is absorbing, ⊢ (𝐴 ∈ (ℂ̅ ∪ ℂ̂) → (𝐴 ∥ℂ 0)) and ⊢ ((0 ∥ℂ 𝐴) ↔ 𝐴 = 0). (Contributed by BJ, 28-Jul-2023.)
⊢ ∥ℂ = {⟨𝑥, 𝑦⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)}
21.19.7  Monoids See ccmn 19822 and subsequents. The first few statements of this subsection can be put very early after ccmn 19822. Proposal: in the main part, make separate subsections of commutative monoids and abelian groups. Relabel cabl 19823 to "cabl" or, preferably, other labels containing "abl" to "abel", for consistency.
Theorem	bj-smgrpssmgm 37234	Semigroups are magmas. (Contributed by BJ, 12-Apr-2024.) (Proof modification is discouraged.)
⊢ Smgrp ⊆ Mgm
Theorem	bj-smgrpssmgmel 37235	Semigroups are magmas (elemental version). (Contributed by BJ, 12-Apr-2024.) (Proof modification is discouraged.)
⊢ (𝐺 ∈ Smgrp → 𝐺 ∈ Mgm)
Theorem	bj-mndsssmgrp 37236	Monoids are semigroups. (Contributed by BJ, 11-Apr-2024.) (Proof modification is discouraged.)
⊢ Mnd ⊆ Smgrp
Theorem	bj-mndsssmgrpel 37237	Monoids are semigroups (elemental version). (Contributed by BJ, 11-Apr-2024.) (Proof modification is discouraged.)
⊢ (𝐺 ∈ Mnd → 𝐺 ∈ Smgrp)
Theorem	bj-cmnssmnd 37238	Commutative monoids are monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ CMnd ⊆ Mnd
Theorem	bj-cmnssmndel 37239	Commutative monoids are monoids (elemental version). This is a more direct proof of cmnmnd 19839, which relies on iscmn 19831. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ CMnd → 𝐴 ∈ Mnd)
Theorem	bj-grpssmnd 37240	Groups are monoids. (Contributed by BJ, 5-Jan-2024.) (Proof modification is discouraged.)
⊢ Grp ⊆ Mnd
Theorem	bj-grpssmndel 37241	Groups are monoids (elemental version). Shorter proof of grpmnd 18980. (Contributed by BJ, 5-Jan-2024.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ Grp → 𝐴 ∈ Mnd)
Theorem	bj-ablssgrp 37242	Abelian groups are groups. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ Abel ⊆ Grp
Theorem	bj-ablssgrpel 37243	Abelian groups are groups (elemental version). This is a shorter proof of ablgrp 19827. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ Abel → 𝐴 ∈ Grp)
Theorem	bj-ablsscmn 37244	Abelian groups are commutative monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ Abel ⊆ CMnd
Theorem	bj-ablsscmnel 37245	Abelian groups are commutative monoids (elemental version). This is a shorter proof of ablcmn 19829. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ Abel → 𝐴 ∈ CMnd)
Theorem	bj-modssabl 37246	(The additive groups of) modules are abelian groups. (The elemental version is lmodabl 20929; see also lmodgrp 20887 and lmodcmn 20930.) (Contributed by BJ, 9-Jun-2019.)
⊢ LMod ⊆ Abel
Theorem	bj-vecssmod 37247	Vector spaces are modules. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ LVec ⊆ LMod
Theorem	bj-vecssmodel 37248	Vector spaces are modules (elemental version). This is a shorter proof of lveclmod 21128. (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 17502 (although it mixes finite and infinite sums, which makes it harder to understand).
Syntax	cfinsum 37249	Syntax for the class "finite summation in monoids".
class FinSum
Definition	df-bj-finsum 37250*	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 37251*	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 37252	Variant of fvimacnv 7086 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 47035. (Contributed by BJ, 7-Jan-2024.)
⊢ ((Fun 𝐹 ∧ ¬ ∅ ∈ 𝐵) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵)))
Theorem	bj-isvec 37253	The predicate "is a vector space". (Contributed by BJ, 6-Jan-2024.)
⊢ (𝜑 → 𝐾 = (Scalar‘𝑉))    ⇒   ⊢ (𝜑 → (𝑉 ∈ LVec ↔ (𝑉 ∈ LMod ∧ 𝐾 ∈ DivRing)))
Theorem	bj-fldssdrng 37254	Fields are division rings. (Contributed by BJ, 6-Jan-2024.)
⊢ Field ⊆ DivRing
Theorem	bj-flddrng 37255	Fields are division rings (elemental version). (Contributed by BJ, 9-Nov-2024.)
⊢ (𝐹 ∈ Field → 𝐹 ∈ DivRing)
Theorem	bj-rrdrg 37256	The field of real numbers is a division ring. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝfld ∈ DivRing
Theorem	bj-isclm 37257	The predicate "is a subcomplex module". (Contributed by BJ, 6-Jan-2024.)
⊢ (𝜑 → 𝐹 = (Scalar‘𝑊))    &   ⊢ (𝜑 → 𝐾 = (Base‘𝐹))    ⇒   ⊢ (𝜑 → (𝑊 ∈ ℂMod ↔ (𝑊 ∈ LMod ∧ 𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 ∈ (SubRing‘ℂfld))))
Syntax	crrvec 37258	Syntax for the class of real vector spaces.
class ℝ-Vec
Definition	df-bj-rvec 37259	Definition of the class of real vector spaces. The previous definition, ⊢ ℝ-Vec = {𝑥 ∈ LMod ∣ (Scalar‘𝑥) = ℝfld}, can be recovered using bj-isrvec 37260. 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 37266. (Contributed by BJ, 9-Jun-2019.)
⊢ ℝ-Vec = (LMod ∩ (◡Scalar “ {ℝfld}))
Theorem	bj-isrvec 37260	The predicate "is a real vector space". Using df-sca 17327 instead of scaid 17374 would shorten the proof by two syntactic steps, but it is preferable not to rely on the precise definition df-sca 17327. (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LMod ∧ (Scalar‘𝑉) = ℝfld))
Theorem	bj-rvecmod 37261	Real vector spaces are modules (elemental version). (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ LMod)
Theorem	bj-rvecssmod 37262	Real vector spaces are modules. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝ-Vec ⊆ LMod
Theorem	bj-rvecrr 37263	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 37264	The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024.)
⊢ (𝜑 → (Scalar‘𝑉) = 𝐾)    ⇒   ⊢ (𝜑 → (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LMod ∧ 𝐾 = ℝfld)))
Theorem	bj-rvecvec 37265	Real vector spaces are vector spaces (elemental version). (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ LVec)
Theorem	bj-isrvec2 37266	The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024.)
⊢ (𝜑 → (Scalar‘𝑉) = 𝐾)    ⇒   ⊢ (𝜑 → (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LVec ∧ 𝐾 = ℝfld)))
Theorem	bj-rvecssvec 37267	Real vector spaces are vector spaces. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝ-Vec ⊆ LVec
Theorem	bj-rveccmod 37268	Real vector spaces are subcomplex modules (elemental version). (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ ℂMod)
Theorem	bj-rvecsscmod 37269	Real vector spaces are subcomplex modules. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝ-Vec ⊆ ℂMod
Theorem	bj-rvecsscvec 37270	Real vector spaces are subcomplex vector spaces. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝ-Vec ⊆ ℂVec
Theorem	bj-rveccvec 37271	Real vector spaces are subcomplex vector spaces (elemental version). (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ ℂVec)
Theorem	bj-rvecssabl 37272	(The additive groups of) real vector spaces are commutative groups. (Contributed by BJ, 9-Jun-2019.)
⊢ ℝ-Vec ⊆ Abel
Theorem	bj-rvecabl 37273	(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 37274	A consequence of commutativity of multiplication. (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) − (𝐵 · 𝐴)) = 0)
Theorem	bj-lineqi 37275	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 37278 (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 37276	Lemma for bj-bary1 37278: expression for a barycenter of two points in one dimension (complex line). (Contributed by BJ, 6-Jun-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → 𝑋 = ((((𝐵 − 𝑋) / (𝐵 − 𝐴)) · 𝐴) + (((𝑋 − 𝐴) / (𝐵 − 𝐴)) · 𝐵)))
Theorem	bj-bary1lem1 37277	Lemma for bj-bary1 37278: 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 37278	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 37279	Token for the monoid of endomorphisms.
class End
Definition	df-bj-end 37280*	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 37281	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 37282	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 37283	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 37284	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.0.1  Circle constant
Theorem	taupilem3 37285	Lemma for tau-related theorems. (Contributed by Jim Kingdon, 16-Feb-2019.)
⊢ (𝐴 ∈ (ℝ+ ∩ (◡cos “ {1})) ↔ (𝐴 ∈ ℝ+ ∧ (cos‘𝐴) = 1))
Theorem	taupilemrplb 37286*	A set of positive reals has (in the reals) a lower bound. (Contributed by Jim Kingdon, 19-Feb-2019.)
⊢ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (ℝ+ ∩ 𝐴)𝑥 ≤ 𝑦
Theorem	taupilem1 37287	Lemma for taupi 37289. A positive real whose cosine is one is at least 2 · π. (Contributed by Jim Kingdon, 19-Feb-2019.)
⊢ ((𝐴 ∈ ℝ+ ∧ (cos‘𝐴) = 1) → (2 · π) ≤ 𝐴)
Theorem	taupilem2 37288	Lemma for taupi 37289. 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 37289	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.0.2  Number theory
Theorem	dfgcd3 37290*	Alternate definition of the gcd operator. (Contributed by Jim Kingdon, 31-Dec-2021.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (℩𝑑 ∈ ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))))
21.20.0.3  Real numbers
Theorem	irrdifflemf 37291	Lemma for irrdiff 37292. The forward direction. (Contributed by Jim Kingdon, 20-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ ℚ)    &   ⊢ (𝜑 → 𝑄 ∈ ℚ)    &   ⊢ (𝜑 → 𝑅 ∈ ℚ)    &   ⊢ (𝜑 → 𝑄 ≠ 𝑅)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) ≠ (abs‘(𝐴 − 𝑅)))
Theorem	irrdiff 37292*	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 37293	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 37294	Move class substitution in and out of recs. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌recs(𝐹) = recs(⦋𝐴 / 𝑥⦌𝐹))
Theorem	csbrdgg 37295	Move class substitution in and out of the recursive function generator. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌rec(𝐹, 𝐼) = rec(⦋𝐴 / 𝑥⦌𝐹, ⦋𝐴 / 𝑥⦌𝐼))
Theorem	csboprabg 37296*	Move class substitution in and out of class abstractions of nested ordered pairs. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∣ 𝜑} = {⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∣ [𝐴 / 𝑥]𝜑})
Theorem	csbmpo123 37297*	Move class substitution in and out of maps-to notation for operations. (Contributed by ML, 25-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑦 ∈ 𝑌, 𝑧 ∈ 𝑍 ↦ 𝐷) = (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌, 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑍 ↦ ⦋𝐴 / 𝑥⦌𝐷))
Theorem	con1bii2 37298	A contraposition inference. (Contributed by ML, 18-Oct-2020.)
⊢ (¬ 𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜑 ↔ ¬ 𝜓)
Theorem	con2bii2 37299	A contraposition inference. (Contributed by ML, 18-Oct-2020.)
⊢ (𝜑 ↔ ¬ 𝜓)    ⇒   ⊢ (¬ 𝜑 ↔ 𝜓)
Theorem	vtoclefex 37300*	Implicit substitution of a class for a setvar variable. (Contributed by ML, 17-Oct-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝐴 → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜑)