P. 379 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37801-37900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-eldiag 37801	Characterization of the elements of the diagonal of a Cartesian square. Subsumed by bj-elid6 37795. (Contributed by BJ, 22-Jun-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ (Id‘𝐴) ↔ (𝐵 ∈ (𝐴 × 𝐴) ∧ (1st ‘𝐵) = (2nd ‘𝐵))))
Theorem	bj-eldiag2 37802	Characterization of the elements of the diagonal of a Cartesian square. Subsumed by bj-elid7 37796. (Contributed by BJ, 22-Jun-2019.)
⊢ (𝐴 ∈ 𝑉 → (⟨𝐵, 𝐶⟩ ∈ (Id‘𝐴) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 = 𝐶)))
21.19.6.4  Direct image and inverse image Definitions of the functionalized direct image and inverse image. The functionalized direct (resp. inverse) image is the morphism component of the covariant (resp. contravariant) powerset endofunctor of the category of sets and relations (and, up to restriction, of its subcategory of sets and functions). Its object component is the powerset operation 𝒫 defined in df-pw 4565.
Syntax	cimdir 37803	Syntax for the functionalized direct image.
class 𝒫*
Definition	df-imdir 37804*	Definition of the functionalized direct image, which maps a binary relation between two given sets to its associated direct image relation. (Contributed by BJ, 16-Dec-2023.)
⊢ 𝒫* = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏) ∧ (𝑟 “ 𝑥) = 𝑦)}))
Theorem	bj-imdirvallem 37805*	Lemma for bj-imdirval 37806 and bj-iminvval 37818. (Contributed by BJ, 23-May-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ 𝐶 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏) ∧ 𝜓)}))    ⇒   ⊢ (𝜑 → (𝐴𝐶𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ 𝜓)}))
Theorem	bj-imdirval 37806*	Value of the functionalized direct image. (Contributed by BJ, 16-Dec-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴𝒫*𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ (𝑟 “ 𝑥) = 𝑦)}))
Theorem	bj-imdirval2lem 37807*	Lemma for bj-imdirval2 37808 and bj-iminvval2 37819. (Contributed by BJ, 23-May-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ 𝜓)} ∈ V)
Theorem	bj-imdirval2 37808*	Value of the functionalized direct image. (Contributed by BJ, 16-Dec-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ⊆ (𝐴 × 𝐵))    ⇒   ⊢ (𝜑 → ((𝐴𝒫*𝐵)‘𝑅) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ (𝑅 “ 𝑥) = 𝑦)})
Theorem	bj-imdirval3 37809	Value of the functionalized direct image. (Contributed by BJ, 16-Dec-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ⊆ (𝐴 × 𝐵))    ⇒   ⊢ (𝜑 → (𝑋((𝐴𝒫*𝐵)‘𝑅)𝑌 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐵) ∧ (𝑅 “ 𝑋) = 𝑌)))
Theorem	bj-imdiridlem 37810*	Lemma for bj-imdirid 37811 and bj-iminvid 37820. (Contributed by BJ, 26-May-2024.)
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) → (𝜑 ↔ 𝑥 = 𝑦))    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐴) ∧ 𝜑)} = ( I ↾ 𝒫 𝐴)
Theorem	bj-imdirid 37811	Functorial property of the direct image: the direct image by the identity on a set is the identity on the powerset. (Contributed by BJ, 24-Dec-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝐴𝒫*𝐴)‘( I ↾ 𝐴)) = ( I ↾ 𝒫 𝐴))
Theorem	bj-opelopabid 37812*	Membership in an ordered-pair class abstraction. One can remove the DV condition on 𝑥, 𝑦 by using opabid 5511 in place of opabidw 5510. (Contributed by BJ, 22-May-2024.)
⊢ (𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦 ↔ 𝜑)
Theorem	bj-opabco 37813*	Composition of ordered-pair class abstractions. (Contributed by BJ, 22-May-2024.)
⊢ ({⟨𝑦, 𝑧⟩ ∣ 𝜓} ∘ {⟨𝑥, 𝑦⟩ ∣ 𝜑}) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝜑 ∧ 𝜓)}
Theorem	bj-xpcossxp 37814	The composition of two Cartesian products is included in the expected Cartesian product. There is equality if (𝐵 ∩ 𝐶) ≠ ∅, see xpcogend 15013. (Contributed by BJ, 22-May-2024.)
⊢ ((𝐶 × 𝐷) ∘ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐷)
Theorem	bj-imdirco 37815	Functorial property of the direct image: the direct image by a composition is the composition of the direct images. (Contributed by BJ, 23-May-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ⊆ (𝐴 × 𝐵))    &   ⊢ (𝜑 → 𝑆 ⊆ (𝐵 × 𝐶))    ⇒   ⊢ (𝜑 → ((𝐴𝒫*𝐶)‘(𝑆 ∘ 𝑅)) = (((𝐵𝒫*𝐶)‘𝑆) ∘ ((𝐴𝒫*𝐵)‘𝑅)))
Syntax	ciminv 37816	Syntax for the functionalized inverse image.
class 𝒫*
Definition	df-iminv 37817*	Definition of the functionalized inverse image, which maps a binary relation between two given sets to its associated inverse image relation. (Contributed by BJ, 23-Dec-2023.)
⊢ 𝒫* = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝑎 ∧ 𝑦 ⊆ 𝑏) ∧ 𝑥 = (◡𝑟 “ 𝑦))}))
Theorem	bj-iminvval 37818*	Value of the functionalized inverse image. (Contributed by BJ, 23-May-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴𝒫*𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ 𝑥 = (◡𝑟 “ 𝑦))}))
Theorem	bj-iminvval2 37819*	Value of the functionalized inverse image. (Contributed by BJ, 23-May-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ⊆ (𝐴 × 𝐵))    ⇒   ⊢ (𝜑 → ((𝐴𝒫*𝐵)‘𝑅) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵) ∧ 𝑥 = (◡𝑅 “ 𝑦))})
Theorem	bj-iminvid 37820	Functorial property of the inverse image: the inverse image by the identity on a set is the identity on the powerset. (Contributed by BJ, 26-May-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝐴𝒫*𝐴)‘( I ↾ 𝐴)) = ( I ↾ 𝒫 𝐴))
21.19.6.5  Extended numbers and projective lines as sets We parameterize the set of infinite extended complex numbers ℂ∞ (df-bj-ccinfty 37837) using the real numbers ℝ (df-r 11111) via the function +∞eiτ. Since at that point, we have only defined the set of real numbers but no operations on it, we define a temporary "fractional part" function, which is more convenient to define on the temporary reals R (df-nr 11042) since we can use operations on the latter. We also define the temporary real "one-half" in order to define minus infinity (df-bj-minfty 37849) and then we can define the sets of extended real numbers and of extended complex numbers, and the projective real and complex lines, as well as addition and negation on these, and also the order relation on the extended reals (which bypasses the intermediate definition of a temporary order on the real numbers and then a superseding one on the extended real numbers).
Syntax	cfractemp 37821	Syntax for the fractional part of a temporary real.
class {R
Definition	df-bj-fractemp 37822*	Temporary definition: fractional part of a temporary real. To understand this definition, recall the canonical injection ω⟶R, 𝑛 ↦ [{𝑥 ∈ Q ∣ 𝑥 <Q ⟨suc 𝑛, 1o⟩}, 1P] ~R where we successively take the successor of 𝑛 to land in positive integers, then take the couple with 1o as second component to land in positive rationals, then take the Dedekind cut that positive rational forms, and finally take the equivalence class of the couple with 1P as second component. Adding one at the beginning and subtracting it at the end is necessary since the constructions used in set.mm use the positive integers, positive rationals, and positive reals as intermediate number systems. (Contributed by BJ, 22-Jan-2023.) The precise definition is irrelevant and should generally not be used. One could even inline it. The definitive fractional part of an extended or projective complex number will be defined later. (New usage is discouraged.)
⊢ {R = (𝑥 ∈ R ↦ (℩𝑦 ∈ R ((𝑦 = 0R ∨ (0R <R 𝑦 ∧ 𝑦 <R 1R)) ∧ ∃𝑛 ∈ ω ([⟨{𝑧 ∈ Q ∣ 𝑧 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R +R 𝑦) = 𝑥)))
Syntax	cinftyexpitau 37823	Syntax for the function +∞eiτ parameterizing ℂ∞.
class +∞eiτ
Definition	df-bj-inftyexpitau 37824	Definition of the auxiliary function +∞eiτ parameterizing the circle at infinity ℂ∞ in ℂ̅. We use coupling with {R} to simplify the proof of bj-inftyexpitaudisj 37830. (Contributed by BJ, 22-Jan-2023.) The precise definition is irrelevant and should generally not be used. TODO: prove only the necessary lemmas to prove ⊢ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((+∞eiτ‘𝐴) = (+∞eiτ‘𝐵) ↔ (𝐴 − 𝐵) ∈ ℤ)). (New usage is discouraged.)
⊢ +∞eiτ = (𝑥 ∈ ℝ ↦ ⟨({R‘(1st ‘𝑥)), {R}⟩)
Syntax	cccinftyN 37825	Syntax for the circle at infinity ℂ∞N.
class ℂ∞N
Definition	df-bj-ccinftyN 37826	Definition of the circle at infinity ℂ∞N. (Contributed by BJ, 22-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.)
⊢ ℂ∞N = ran +∞eiτ
Theorem	bj-inftyexpitaufo 37827	The function +∞eiτ written as a surjection with domain and range. (Contributed by BJ, 4-Feb-2023.)
⊢ +∞eiτ:ℝ–onto→ℂ∞N
Syntax	chalf 37828	Syntax for the temporary one-half.
class 1/2
Definition	df-bj-onehalf 37829	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 7386) $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/2 = (℩𝑥 ∈ R (𝑥 +R 𝑥) = 1R)
Theorem	bj-inftyexpitaudisj 37830	An element of the circle at infinity is not a complex number. (Contributed by BJ, 4-Feb-2023.)
⊢ ¬ (+∞eiτ‘𝐴) ∈ ℂ
Syntax	cinftyexpi 37831	Syntax for the function +∞ei parameterizing ℂ∞.
class +∞ei
Definition	df-bj-inftyexpi 37832	Definition of the auxiliary function +∞ei parameterizing the circle at infinity ℂ∞ in ℂ̅. We use coupling with ℂ to simplify the proof of bj-ccinftydisj 37838. 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 37824 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 37833	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 37834	Injectivity of the parameterization +∞ei. Remark: a more conceptual proof would use bj-inftyexpiinv 37833 and the fact that a function with a retraction is injective. (Contributed by BJ, 22-Jun-2019.)
⊢ ((𝐴 ∈ (-π(,]π) ∧ 𝐵 ∈ (-π(,]π)) → (𝐴 = 𝐵 ↔ (+∞ei‘𝐴) = (+∞ei‘𝐵)))
Theorem	bj-inftyexpidisj 37835	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 37836	Syntax for the circle at infinity ℂ∞.
class ℂ∞
Definition	df-bj-ccinfty 37837	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 37838	The circle at infinity is disjoint from the set of complex numbers. (Contributed by BJ, 22-Jun-2019.)
⊢ (ℂ ∩ ℂ∞) = ∅
Theorem	bj-elccinfty 37839	A lemma for infinite extended complex numbers. (Contributed by BJ, 27-Jun-2019.)
⊢ (𝐴 ∈ (-π(,]π) → (+∞ei‘𝐴) ∈ ℂ∞)
Syntax	cccbar 37840	Syntax for the set of extended complex numbers ℂ̅.
class ℂ̅
Definition	df-bj-ccbar 37841	Definition of the set of extended complex numbers ℂ̅. (Contributed by BJ, 22-Jun-2019.)
⊢ ℂ̅ = (ℂ ∪ ℂ∞)
Theorem	bj-ccssccbar 37842	Complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.)
⊢ ℂ ⊆ ℂ̅
Theorem	bj-ccinftyssccbar 37843	Infinite extended complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.)
⊢ ℂ∞ ⊆ ℂ̅
Syntax	cpinfty 37844	Syntax for "plus infinity".
class +∞
Definition	df-bj-pinfty 37845	Definition of "plus infinity". (Contributed by BJ, 27-Jun-2019.)
⊢ +∞ = (+∞ei‘0)
Theorem	bj-pinftyccb 37846	The class +∞ is an extended complex number. (Contributed by BJ, 27-Jun-2019.)
⊢ +∞ ∈ ℂ̅
Theorem	bj-pinftynrr 37847	The extended complex number +∞ is not a complex number. (Contributed by BJ, 27-Jun-2019.)
⊢ ¬ +∞ ∈ ℂ
Syntax	cminfty 37848	Syntax for "minus infinity".
class -∞
Definition	df-bj-minfty 37849	Definition of "minus infinity". (Contributed by BJ, 27-Jun-2019.)
⊢ -∞ = (+∞ei‘π)
Theorem	bj-minftyccb 37850	The class -∞ is an extended complex number. (Contributed by BJ, 27-Jun-2019.)
⊢ -∞ ∈ ℂ̅
Theorem	bj-minftynrr 37851	The extended complex number -∞ is not a complex number. (Contributed by BJ, 27-Jun-2019.)
⊢ ¬ -∞ ∈ ℂ
Theorem	bj-pinftynminfty 37852	The extended complex numbers +∞ and -∞ are different. (Contributed by BJ, 27-Jun-2019.)
⊢ +∞ ≠ -∞
Syntax	crrbar 37853	Syntax for the set of extended real numbers.
class ℝ̅
Definition	df-bj-rrbar 37854	Definition of the set of extended real numbers. This aims to replace df-xr 11248. (Contributed by BJ, 29-Jun-2019.)
⊢ ℝ̅ = (ℝ ∪ {-∞, +∞})
Syntax	cinfty 37855	Syntax for ∞.
class ∞
Definition	df-bj-infty 37856	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 37857	Syntax for ℂ̂.
class ℂ̂
Definition	df-bj-cchat 37858	Define the complex projective line, or Riemann sphere. (Contributed by BJ, 27-Jun-2019.)
⊢ ℂ̂ = (ℂ ∪ {∞})
Syntax	crrhat 37859	Syntax for ℝ̂.
class ℝ̂
Definition	df-bj-rrhat 37860	Define the real projective line. (Contributed by BJ, 27-Jun-2019.)
⊢ ℝ̂ = (ℝ ∪ {∞})
Theorem	bj-rrhatsscchat 37861	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 37862	Syntax for the addition on extended complex numbers.
class +ℂ̅
Definition	df-bj-addc 37863	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 37864	Syntax for negation on the set of extended complex numbers and the complex projective line (Riemann sphere).
class -ℂ̅
Definition	df-bj-oppc 37865*	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 11249 without the intermediate step of df-lt 11114.
Syntax	cltxr 37866	Syntax for the standard (strict) order on the extended reals.
class <ℝ̅
Definition	df-bj-lt 37867*	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 37871.
Syntax	carg 37868	Syntax for the argument of a nonzero extended complex number.
class Arg
Definition	df-bj-arg 37869	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 37824), and therefore should not be relied upon. (New usage is discouraged.)
⊢ Arg = (𝑥 ∈ (ℂ̅ ∖ {0}) ↦ if(𝑥 ∈ ℂ, (ℑ‘(log‘𝑥)), if(𝑥<ℝ̅0, π, (((1st ‘𝑥) / (2 · π)) − π))))
Syntax	cmulc 37870	Syntax for the multiplication of extended complex numbers.
class ·ℂ̅
Definition	df-bj-mulc 37871	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 37873). 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 37872	Syntax for the inverse of nonzero extended complex numbers.
class -1ℂ̅
Definition	df-bj-invc 37873*	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 37871, 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 37874	Syntax for the canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}).
class iω↪ℕ
Definition	df-bj-iomnn 37875*	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 37822 but we did not use the present definition there since we wanted to have defined +∞ first. See bj-iomnnom 37884 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 37876	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 37877	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 37878	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 37879	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 37880	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 37881	The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 7183. (Contributed by NM, 23-Sep-2007.) Put in deduction form. (Revised by BJ, 18-Mar-2023.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐺 = ((𝐹 ↾ (𝐶 ∖ {𝐴})) ∪ {⟨𝐴, 𝐵⟩}))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐺‘𝐴) = 𝐵)
Theorem	bj-fvmptunsn1 37882*	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 37883*	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 37884	The canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}) maps ω to +∞. (Contributed by BJ, 18-Feb-2023.)
⊢ (iω↪ℕ‘ω) = +∞
21.19.6.10  Divisibility
Syntax	cnnbar 37885	Syntax for the extended natural numbers.
class ℕ̅
Definition	df-bj-nnbar 37886	Definition of the extended natural numbers. (Contributed by BJ, 28-Jul-2023.)
⊢ ℕ̅ = (ℕ0 ∪ {+∞})
Syntax	czzbar 37887	Syntax for the extended integers.
class ℤ̅
Definition	df-bj-zzbar 37888	Definition of the extended integers. (Contributed by BJ, 28-Jul-2023.)
⊢ ℤ̅ = (ℤ ∪ {-∞, +∞})
Syntax	czzhat 37889	Syntax for the one-point-compactified integers.
class ℤ̂
Definition	df-bj-zzhat 37890	Definition of the one-point-compactified. (Contributed by BJ, 28-Jul-2023.)
⊢ ℤ̂ = (ℤ ∪ {∞})
Syntax	cdivc 37891	Syntax for the divisibility relation.
class ∥ℂ
Definition	df-bj-divc 37892*	Definition of the divisibility relation (compare df-dvds 16312). Since 0 is absorbing, ⊢ (𝐴 ∈ (ℂ̅ ∪ ℂ̂) → (𝐴 ∥ℂ 0)) and ⊢ ((0 ∥ℂ 𝐴) ↔ 𝐴 = 0). (Contributed by BJ, 28-Jul-2023.)
⊢ ∥ℂ = {⟨𝑥, 𝑦⟩ ∣ (⟨𝑥, 𝑦⟩ ∈ ((ℂ̅ × ℂ̅) ∪ (ℂ̂ × ℂ̂)) ∧ ∃𝑛 ∈ (ℤ̅ ∪ ℤ̂)(𝑛 ·ℂ̅ 𝑥) = 𝑦)}
21.19.7  Monoids See ccmn 19851 and subsequents. The first few statements of this subsection can be put very early after ccmn 19851. Proposal: in the main part, make separate subsections of commutative monoids and abelian groups. Relabel cabl 19852 to "cabl" or, preferably, other labels containing "abl" to "abel", for consistency.
Theorem	bj-smgrpssmgm 37893	Semigroups are magmas. (Contributed by BJ, 12-Apr-2024.) (Proof modification is discouraged.)
⊢ Smgrp ⊆ Mgm
Theorem	bj-smgrpssmgmel 37894	Semigroups are magmas (elemental version). (Contributed by BJ, 12-Apr-2024.) (Proof modification is discouraged.)
⊢ (𝐺 ∈ Smgrp → 𝐺 ∈ Mgm)
Theorem	bj-mndsssmgrp 37895	Monoids are semigroups. (Contributed by BJ, 11-Apr-2024.) (Proof modification is discouraged.)
⊢ Mnd ⊆ Smgrp
Theorem	bj-mndsssmgrpel 37896	Monoids are semigroups (elemental version). (Contributed by BJ, 11-Apr-2024.) (Proof modification is discouraged.)
⊢ (𝐺 ∈ Mnd → 𝐺 ∈ Smgrp)
Theorem	bj-cmnssmnd 37897	Commutative monoids are monoids. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ CMnd ⊆ Mnd
Theorem	bj-cmnssmndel 37898	Commutative monoids are monoids (elemental version). This is a more direct proof of cmnmnd 19868, which relies on iscmn 19860. (Contributed by BJ, 9-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ CMnd → 𝐴 ∈ Mnd)
Theorem	bj-grpssmnd 37899	Groups are monoids. (Contributed by BJ, 5-Jan-2024.) (Proof modification is discouraged.)
⊢ Grp ⊆ Mnd
Theorem	bj-grpssmndel 37900	Groups are monoids (elemental version). Shorter proof of grpmnd 19008. (Contributed by BJ, 5-Jan-2024.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ Grp → 𝐴 ∈ Mnd)