P. 383 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38201-38300   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-bj-onehalf 38201	Define the temporary real "one-half". Once the machinery is developed, the real number "one-half" is commonly denoted by (1 / 2). (Contributed by BJ, 4-Feb-2023.) (New usage is discouraged.) TODO: $p |- 1/2 e. R. $= ? $. (riotacl 7394) $p |- -. 0R = 1/2 $= ? $. (since -. ( 0R +R 0R ) = 1R ) $p |- 0R <R 1/2 $= ? $. $p |- 1/2 <R 1R $= ? $. $p |- ( {R ` 0R ) = 0R $= ? $. $p |- ( {R ` 1/2 ) = 1/2 $= ? $. df-minfty $a |- minfty = ( inftyexpitau ` <. 1/2 , 0R >. ) $.
⊢ 1/2R = (℩𝑥 ∈ R (𝑥 +R 𝑥) = 1R)
Theorem	bj-inftyexpitaudisj 38202	An element of the circle at infinity is not a complex number. (Contributed by BJ, 4-Feb-2023.)
⊢ ¬ (+∞eiτ‘𝐴) ∈ ℂ
Syntax	cinftyexpi 38203	Syntax for the function +∞ei parameterizing ℂ∞.
class +∞ei
Definition	df-bj-inftyexpi 38204	Definition of the auxiliary function +∞ei parameterizing the circle at infinity ℂ∞ in ℂ̅. We use coupling with ℂ to simplify the proof of bj-ccinftydisj 38210. It could seem more natural to define +∞ei on all of ℝ, but we want to use only basic functions in the definition of ℂ̅. TODO: transition to df-bj-inftyexpitau 38196 instead. (Contributed by BJ, 22-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.)
⊢ +∞ei = (𝑥 ∈ ( -π(,]π) ↦ ⟨𝑥, ℂ⟩)
Theorem	bj-inftyexpiinv 38205	Utility theorem for the inverse of +∞ei. (Contributed by BJ, 22-Jun-2019.) This utility theorem is irrelevant and should generally not be used. (New usage is discouraged.)
⊢ (𝐴 ∈ ( -π(,]π) → (1st ‘(+∞ei‘𝐴)) = 𝐴)
Theorem	bj-inftyexpiinj 38206	Injectivity of the parameterization +∞ei. Remark: a more conceptual proof would use bj-inftyexpiinv 38205 and the fact that a function with a retraction is injective. (Contributed by BJ, 22-Jun-2019.)
⊢ ((𝐴 ∈ ( -π(,]π) ∧ 𝐵 ∈ ( -π(,]π)) → (𝐴 = 𝐵 ↔ (+∞ei‘𝐴) = (+∞ei‘𝐵)))
Theorem	bj-inftyexpidisj 38207	An element of the circle at infinity is not a complex number. (Contributed by BJ, 22-Jun-2019.) This utility theorem is irrelevant and should generally not be used. (New usage is discouraged.)
⊢ ¬ (+∞ei‘𝐴) ∈ ℂ
Syntax	cccinfty 38208	Syntax for the circle at infinity ℂ∞.
class ℂ∞
Definition	df-bj-ccinfty 38209	Definition of the circle at infinity ℂ∞. (Contributed by BJ, 22-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.)
⊢ ℂ∞ = ran +∞ei
Theorem	bj-ccinftydisj 38210	The circle at infinity is disjoint from the set of complex numbers. (Contributed by BJ, 22-Jun-2019.)
⊢ (ℂ ∩ ℂ∞) = ∅
Theorem	bj-elccinfty 38211	A lemma for infinite extended complex numbers. (Contributed by BJ, 27-Jun-2019.)
⊢ (𝐴 ∈ ( -π(,]π) → (+∞ei‘𝐴) ∈ ℂ∞)
Syntax	cccbar 38212	Syntax for the set of extended complex numbers ℂ̅.
class ℂ̅
Definition	df-bj-ccbar 38213	Definition of the set of extended complex numbers ℂ̅. (Contributed by BJ, 22-Jun-2019.)
⊢ ℂ̅ = (ℂ ∪ ℂ∞)
Theorem	bj-ccssccbar 38214	Complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.)
⊢ ℂ ⊆ ℂ̅
Theorem	bj-ccinftyssccbar 38215	Infinite extended complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.)
⊢ ℂ∞ ⊆ ℂ̅
Syntax	cpinfty 38216	Syntax for "plus infinity".
class +∞
Definition	df-bj-pinfty 38217	Definition of "plus infinity". (Contributed by BJ, 27-Jun-2019.)
⊢ +∞ = (+∞ei‘0)
Theorem	bj-pinftyccb 38218	The class +∞ is an extended complex number. (Contributed by BJ, 27-Jun-2019.)
⊢ +∞ ∈ ℂ̅
Theorem	bj-pinftynrr 38219	The extended complex number +∞ is not a complex number. (Contributed by BJ, 27-Jun-2019.)
⊢ ¬ +∞ ∈ ℂ
Syntax	cminfty 38220	Syntax for "minus infinity".
class -∞
Definition	df-bj-minfty 38221	Definition of "minus infinity". (Contributed by BJ, 27-Jun-2019.)
⊢ -∞ = (+∞ei‘π)
Theorem	bj-minftyccb 38222	The class -∞ is an extended complex number. (Contributed by BJ, 27-Jun-2019.)
⊢ -∞ ∈ ℂ̅
Theorem	bj-minftynrr 38223	The extended complex number -∞ is not a complex number. (Contributed by BJ, 27-Jun-2019.)
⊢ ¬ -∞ ∈ ℂ
Theorem	bj-pinftynminfty 38224	The extended complex numbers +∞ and -∞ are different. (Contributed by BJ, 27-Jun-2019.)
⊢ +∞ ≠ -∞
Syntax	crrbar 38225	Syntax for the set of extended real numbers.
class ℝ̅
Definition	df-bj-rrbar 38226	Definition of the set of extended real numbers. This aims to replace df-xr 11348. (Contributed by BJ, 29-Jun-2019.)
⊢ ℝ̅ = (ℝ ∪ {-∞, +∞})
Syntax	cinfty 38227	Syntax for ∞.
class ∞
Definition	df-bj-infty 38228	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 38229	Syntax for ℂ̂.
class ℂ̂
Definition	df-bj-cchat 38230	Define the complex projective line, or Riemann sphere. (Contributed by BJ, 27-Jun-2019.)
⊢ ℂ̂ = (ℂ ∪ {∞})
Syntax	crrhat 38231	Syntax for ℝ̂.
class ℝ̂
Definition	df-bj-rrhat 38232	Define the real projective line. (Contributed by BJ, 27-Jun-2019.)
⊢ ℝ̂ = (ℝ ∪ {∞})
Theorem	bj-rrhatsscchat 38233	The real projective line is included in the complex projective line. (Contributed by BJ, 27-Jun-2019.)
⊢ ℝ̂ ⊆ ℂ̂
21.20.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 38234	Syntax for the addition on extended complex numbers.
class +ℂ̅
Definition	df-bj-addc 38235	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 38236	Syntax for negation on the set of extended complex numbers and the complex projective line (Riemann sphere).
class -ℂ̅
Definition	df-bj-oppc 38237*	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/2R, 0R⟩)))))
21.20.6.7  Order relation on the extended reals In this section, we redefine df-ltxr 11349 without the intermediate step of df-lt 11214.
Syntax	cltxr 38238	Syntax for the standard (strict) order on the extended reals.
class <ℝ̅
Definition	df-bj-lt 38239*	Define the standard (strict) order on the extended reals. (Contributed by BJ, 4-Feb-2023.)
⊢ <ℝ̅ = ({𝑥 ∈ (ℝ̅ × ℝ̅) ∣ ∃𝑦∃𝑧(((1st ‘𝑥) = ⟨𝑦, 0R⟩ ∧ (2nd ‘𝑥) = ⟨𝑧, 0R⟩) ∧ 𝑦 <R 𝑧)} ∪ ((({-∞} × ℝ) ∪ (ℝ × {+∞})) ∪ ({-∞} × {+∞})))
21.20.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 38243.
Syntax	carg 38240	Syntax for the argument of a nonzero extended complex number.
class Arg
Definition	df-bj-arg 38241	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 38196), and therefore should not be relied upon. (New usage is discouraged.)
⊢ Arg = (𝑥 ∈ (ℂ̅ ∖ {0}) ↦ if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π, (((1st ‘𝑥) / (2 · π)) − π))))
Syntax	cmulc 38242	Syntax for the multiplication of extended complex numbers.
class ·ℂ̅
Definition	df-bj-mulc 38243	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. This convention entails (0 / 0) = 0 (given df-bj-invc 38245). 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 38244	Syntax for the inverse of nonzero extended complex numbers.
class ·-1
Definition	df-bj-invc 38245*	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) ∉ ℂ̅. This definition relies on df-bj-mulc 38243, 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.20.6.9  The canonical bijection from the finite ordinals
Syntax	ciomnn 38246	Syntax for the canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}).
class iω↪ℕ
Definition	df-bj-iomnn 38247*	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 38194 but we did not use the present definition there since we wanted to have defined +∞ first. See bj-iomnnom 38256 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 38248	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 38249	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 38250	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 38251	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 38252	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 38253	The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 7188. (Contributed by NM, 23-Sep-2007.) Put in deduction form. (Revised by BJ, 18-Mar-2023.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐺 = ((𝐹 ↾ (𝐶 ∖ {𝐴})) ∪ {⟨𝐴, 𝐵⟩}))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐺‘𝐴) = 𝐵)
Theorem	bj-fvmptunsn1 38254*	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 38255*	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 38256	The canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}) maps ω to +∞. (Contributed by BJ, 18-Feb-2023.)
⊢ (iω↪ℕ‘ω) = +∞
21.20.6.10  Divisibility
Syntax	cnnbar 38257	Syntax for the extended natural numbers.
class ℕ̅
Definition	df-bj-nnbar 38258	Definition of the extended natural numbers. (Contributed by BJ, 28-Jul-2023.)
⊢ ℕ̅ = (ℕ0 ∪ {+∞})
Syntax	czzbar 38259	Syntax for the extended integers.
class ℤ̅
Definition	df-bj-zzbar 38260	Definition of the extended integers. (Contributed by BJ, 28-Jul-2023.)
⊢ ℤ̅ = (ℤ ∪ {-∞, +∞})
Syntax	czzhat 38261	Syntax for the one-point-compactified integers.
class ℤ̂
Definition	df-bj-zzhat 38262	Definition of the one-point-compactified. (Contributed by BJ, 28-Jul-2023.)
⊢ ℤ̂ = (ℤ ∪ {∞})
Syntax	cdivc 38263	Syntax for the divisibility relation.
class ∥ℂ
Definition	df-bj-divc 38264*	Definition of the divisibility relation (compare df-dvds 16424). Since 0 is absorbing, ⊢ (𝐴 ∈ (ℂ̅ ∪ ℂ̂) → (𝐴 ∥ℂ 0)) and ⊢ ((0 ∥ℂ 𝐴) ↔ 𝐴 = 0). (Contributed by BJ, 28-Jul-2023.)
⊢ ∥ℂ = {⟨𝑥, 𝑦⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)}
21.20.7  Monoids See ccmn 19995 and subsequents. The first few statements of this subsection can be put very early after ccmn 19995. Proposal: in the main part, make separate subsections of commutative monoids and abelian groups. Relabel cabl 19996 to "cabl" or, preferably, other labels containing "abl" to "abel", for consistency.
Theorem	bj-smgrpssmgm 38265	Semigroups are magmas. (Contributed by BJ, 12-Apr-2024.) (Proof modification is discouraged.)
⊢ Smgrp ⊆ Mgm
Theorem	bj-smgrpssmgmel 38266	Semigroups are magmas (elemental version). (Contributed by BJ, 12-Apr-2024.) (Proof modification is discouraged.)
⊢ (𝐺 ∈ Smgrp → 𝐺 ∈ Mgm)
Theorem	bj-mndsssmgrp 38267	Monoids are semigroups. (Contributed by BJ, 11-Apr-2024.) (Proof modification is discouraged.)
⊢ Mnd ⊆ Smgrp
Theorem	bj-mndsssmgrpel 38268	Monoids are semigroups (elemental version). (Contributed by BJ, 11-Apr-2024.) (Proof modification is discouraged.)
⊢ (𝐺 ∈ Mnd → 𝐺 ∈ Smgrp)
Theorem	bj-cmnssmnd 38269	Commutative monoids are monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ CMnd ⊆ Mnd
Theorem	bj-cmnssmndel 38270	Commutative monoids are monoids (elemental version). This is a more direct proof of cmnmnd 20012, which relies on iscmn 20004. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ CMnd → 𝐴 ∈ Mnd)
Theorem	bj-grpssmnd 38271	Groups are monoids. (Contributed by BJ, 5-Jan-2024.) (Proof modification is discouraged.)
⊢ Grp ⊆ Mnd
Theorem	bj-grpssmndel 38272	Groups are monoids (elemental version). Shorter proof of grpmnd 19152. (Contributed by BJ, 5-Jan-2024.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ Grp → 𝐴 ∈ Mnd)
Theorem	bj-ablssgrp 38273	Abelian groups are groups. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ Abel ⊆ Grp
Theorem	bj-ablssgrpel 38274	Abelian groups are groups (elemental version). This is a shorter proof of ablgrp 20000. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ Abel → 𝐴 ∈ Grp)
Theorem	bj-ablsscmn 38275	Abelian groups are commutative monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ Abel ⊆ CMnd
Theorem	bj-ablsscmnel 38276	Abelian groups are commutative monoids (elemental version). This is a shorter proof of ablcmn 20002. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ Abel → 𝐴 ∈ CMnd)
Theorem	bj-modssabl 38277	(The additive groups of) modules are abelian groups. (The elemental version is lmodabl 21185; see also lmodgrp 21143 and lmodcmn 21186.) (Contributed by BJ, 9-Jun-2019.)
⊢ LMod ⊆ Abel
Theorem	bj-vecssmod 38278	Vector spaces are modules. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ LVec ⊆ LMod
Theorem	bj-vecssmodel 38279	Vector spaces are modules (elemental version). This is a shorter proof of lveclmod 21382. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ LVec → 𝐴 ∈ LMod)
21.20.7.1  Finite sums in monoids UPDATE: a similar summation is already defined as df-gsum 17614 (although it mixes finite and infinite sums, which makes it harder to understand).
Syntax	cfinsum 38280	Syntax for the class "finite summation in monoids".
class FinSum
Definition	df-bj-finsum 38281*	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 38282*	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.20.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.20.8.1  Real vector spaces In this section, we introduce real vector spaces.
Theorem	bj-fvimacnv0 38283	Variant of fvimacnv 7052 where membership of 𝐴 in the domain is not needed provided the containing class 𝐵 does not contain the empty set. This antecedent would not be needed with Definition df-afv 48266. (Contributed by BJ, 7-Jan-2024.)
⊢ ((Fun 𝐹 ∧ ¬ ∅ ∈ 𝐵) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵)))
Theorem	bj-isvec 38284	The predicate "is a vector space". (Contributed by BJ, 6-Jan-2024.)
⊢ (𝜑 → 𝐾 = (Scalar‘𝑉))    ⇒   ⊢ (𝜑 → (𝑉 ∈ LVec ↔ (𝑉 ∈ LMod ∧ 𝐾 ∈ DivRing)))
Theorem	bj-fldssdrng 38285	Fields are division rings. (Contributed by BJ, 6-Jan-2024.)
⊢ Field ⊆ DivRing
Theorem	bj-flddrng 38286	Fields are division rings (elemental version). (Contributed by BJ, 9-Nov-2024.)
⊢ (𝐹 ∈ Field → 𝐹 ∈ DivRing)
Theorem	bj-rrdrg 38287	The field of real numbers is a division ring. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝfld ∈ DivRing
Theorem	bj-isclm 38288	The predicate "is a subcomplex module". (Contributed by BJ, 6-Jan-2024.)
⊢ (𝜑 → 𝐹 = (Scalar‘𝑊))    &   ⊢ (𝜑 → 𝐾 = (Base‘𝐹))    ⇒   ⊢ (𝜑 → (𝑊 ∈ ℂMod ↔ (𝑊 ∈ LMod ∧ 𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 ∈ (SubRing‘ℂfld))))
Syntax	crrvec 38289	Syntax for the class of real vector spaces.
class ℝ-Vec
Definition	df-bj-rvec 38290	Definition of the class of real vector spaces. The previous definition, ⊢ ℝ-Vec = {𝑥 ∈ LMod ∣ (Scalar‘𝑥) = ℝfld}, can be recovered using bj-isrvec 38291. 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 38297. (Contributed by BJ, 9-Jun-2019.)
⊢ ℝ-Vec = (LMod ∩ (◡Scalar “ {ℝfld}))
Theorem	bj-isrvec 38291	The predicate "is a real vector space". Using df-sca 17445 instead of scaid 17487 shortens the proof by two syntactic steps, but it is preferable not to rely on the precise definition df-sca 17445. (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LMod ∧ (Scalar‘𝑉) = ℝfld))
Theorem	bj-rvecmod 38292	Real vector spaces are modules (elemental version). (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ LMod)
Theorem	bj-rvecssmod 38293	Real vector spaces are modules. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝ-Vec ⊆ LMod
Theorem	bj-rvecrr 38294	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 38295	The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024.)
⊢ (𝜑 → (Scalar‘𝑉) = 𝐾)    ⇒   ⊢ (𝜑 → (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LMod ∧ 𝐾 = ℝfld)))
Theorem	bj-rvecvec 38296	Real vector spaces are vector spaces (elemental version). (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ LVec)
Theorem	bj-isrvec2 38297	The predicate "is a real vector space". (Contributed by BJ, 6-Jan-2024.)
⊢ (𝜑 → (Scalar‘𝑉) = 𝐾)    ⇒   ⊢ (𝜑 → (𝑉 ∈ ℝ-Vec ↔ (𝑉 ∈ LVec ∧ 𝐾 = ℝfld)))
Theorem	bj-rvecssvec 38298	Real vector spaces are vector spaces. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝ-Vec ⊆ LVec
Theorem	bj-rveccmod 38299	Real vector spaces are subcomplex modules (elemental version). (Contributed by BJ, 6-Jan-2024.)
⊢ (𝑉 ∈ ℝ-Vec → 𝑉 ∈ ℂMod)
Theorem	bj-rvecsscmod 38300	Real vector spaces are subcomplex modules. (Contributed by BJ, 6-Jan-2024.)
⊢ ℝ-Vec ⊆ ℂMod