P. 375 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37401-37500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cnpwstotbnd 37401	A subset of 𝐴↑𝐼, where 𝐴 ⊆ ℂ, is totally bounded iff it is bounded. (Contributed by Mario Carneiro, 14-Sep-2015.)
⊢ 𝑌 = ((ℂfld ↾s 𝐴) ↑s 𝐼)    &   ⊢ 𝐷 = ((dist‘𝑌) ↾ (𝑋 × 𝑋))    ⇒   ⊢ ((𝐴 ⊆ ℂ ∧ 𝐼 ∈ Fin) → (𝐷 ∈ (TotBnd‘𝑋) ↔ 𝐷 ∈ (Bnd‘𝑋)))
21.22.8  Isometries
Syntax	cismty 37402	Extend class notation with the class of metric space isometries.
class Ismty
Definition	df-ismty 37403*	Define a function which takes two metric spaces and returns the set of isometries between the spaces. An isometry is a bijection which preserves distance. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ Ismty = (𝑚 ∈ ∪ ran ∞Met, 𝑛 ∈ ∪ ran ∞Met ↦ {𝑓 ∣ (𝑓:dom dom 𝑚–1-1-onto→dom dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚∀𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦)))})
Theorem	ismtyval 37404*	The set of isometries between two metric spaces. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝑀 Ismty 𝑁) = {𝑓 ∣ (𝑓:𝑋–1-1-onto→𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) = ((𝑓‘𝑥)𝑁(𝑓‘𝑦)))})
Theorem	isismty 37405*	The condition "is an isometry". (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝐹 ∈ (𝑀 Ismty 𝑁) ↔ (𝐹:𝑋–1-1-onto→𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) = ((𝐹‘𝑥)𝑁(𝐹‘𝑦)))))
Theorem	ismtycnv 37406	The inverse of an isometry is an isometry. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝐹 ∈ (𝑀 Ismty 𝑁) → ◡𝐹 ∈ (𝑁 Ismty 𝑀)))
Theorem	ismtyima 37407	The image of a ball under an isometry is another ball. (Contributed by Jeff Madsen, 31-Jan-2014.)
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌) ∧ 𝐹 ∈ (𝑀 Ismty 𝑁)) ∧ (𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*)) → (𝐹 “ (𝑃(ball‘𝑀)𝑅)) = ((𝐹‘𝑃)(ball‘𝑁)𝑅))
Theorem	ismtyhmeolem 37408	Lemma for ismtyhmeo 37409. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.)
⊢ 𝐽 = (MetOpen‘𝑀)    &   ⊢ 𝐾 = (MetOpen‘𝑁)    &   ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌))    &   ⊢ (𝜑 → 𝐹 ∈ (𝑀 Ismty 𝑁))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))
Theorem	ismtyhmeo 37409	An isometry is a homeomorphism on the induced topology. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.)
⊢ 𝐽 = (MetOpen‘𝑀)    &   ⊢ 𝐾 = (MetOpen‘𝑁)    ⇒   ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝑀 Ismty 𝑁) ⊆ (𝐽Homeo𝐾))
Theorem	ismtybndlem 37410	Lemma for ismtybnd 37411. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 19-Jan-2014.)
⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝐹 ∈ (𝑀 Ismty 𝑁)) → (𝑀 ∈ (Bnd‘𝑋) → 𝑁 ∈ (Bnd‘𝑌)))
Theorem	ismtybnd 37411	Isometries preserve boundedness. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 19-Jan-2014.)
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌) ∧ 𝐹 ∈ (𝑀 Ismty 𝑁)) → (𝑀 ∈ (Bnd‘𝑋) ↔ 𝑁 ∈ (Bnd‘𝑌)))
Theorem	ismtyres 37412	A restriction of an isometry is an isometry. The condition 𝐴 ⊆ 𝑋 is not necessary but makes the proof easier. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.)
⊢ 𝐵 = (𝐹 “ 𝐴)    &   ⊢ 𝑆 = (𝑀 ↾ (𝐴 × 𝐴))    &   ⊢ 𝑇 = (𝑁 ↾ (𝐵 × 𝐵))    ⇒   ⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ (𝑀 Ismty 𝑁) ∧ 𝐴 ⊆ 𝑋)) → (𝐹 ↾ 𝐴) ∈ (𝑆 Ismty 𝑇))
21.22.9  Heine-Borel Theorem
Theorem	heibor1lem 37413	Lemma for heibor1 37414. A compact metric space is complete. This proof works by considering the collection cls(𝐹 “ (ℤ≥‘𝑛)) for each 𝑛 ∈ ℕ, which has the finite intersection property because any finite intersection of upper integer sets is another upper integer set, so any finite intersection of the image closures will contain (𝐹 “ (ℤ≥‘𝑚)) for some 𝑚. Thus, by compactness, the intersection contains a point 𝑦, which must then be the convergent point of 𝐹. (Contributed by Jeff Madsen, 17-Jan-2014.) (Revised by Mario Carneiro, 5-Jun-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷))    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑋)    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽))
Theorem	heibor1 37414	One half of heibor 37425, that does not require any Choice. A compact metric space is complete and totally bounded. We prove completeness in cmpcmet 25291 and total boundedness here, which follows trivially from the fact that the set of all 𝑟-balls is an open cover of 𝑋, so finitely many cover 𝑋. (Contributed by Jeff Madsen, 16-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐽 ∈ Comp) → (𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)))
Theorem	heiborlem1 37415*	Lemma for heibor 37425. We work with a fixed open cover 𝑈 throughout. The set 𝐾 is the set of all subsets of 𝑋 that admit no finite subcover of 𝑈. (We wish to prove that 𝐾 is empty.) If a set 𝐶 has no finite subcover, then any finite cover of 𝐶 must contain a set that also has no finite subcover. (Contributed by Jeff Madsen, 23-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐴 ∈ Fin ∧ 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐶 ∈ 𝐾) → ∃𝑥 ∈ 𝐴 𝐵 ∈ 𝐾)
Theorem	heiborlem2 37416*	Lemma for heibor 37425. Substitutions for the set 𝐺. (Contributed by Jeff Madsen, 23-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}    &   ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴𝐺𝐶 ↔ (𝐶 ∈ ℕ0 ∧ 𝐴 ∈ (𝐹‘𝐶) ∧ (𝐴𝐵𝐶) ∈ 𝐾))
Theorem	heiborlem3 37417*	Lemma for heibor 37425. Using countable choice ax-cc 10460, we have fixed in advance a collection of finite 2↑-𝑛 nets (𝐹‘𝑛) for 𝑋 (note that an 𝑟-net is a set of points in 𝑋 whose 𝑟 -balls cover 𝑋). The set 𝐺 is the subset of these points whose corresponding balls have no finite subcover (i.e. in the set 𝐾). If the theorem was false, then 𝑋 would be in 𝐾, and so some ball at each level would also be in 𝐾. But we can say more than this; given a ball (𝑦𝐵𝑛) on level 𝑛, since level 𝑛 + 1 covers the space and thus also (𝑦𝐵𝑛), using heiborlem1 37415 there is a ball on the next level whose intersection with (𝑦𝐵𝑛) also has no finite subcover. Now since the set 𝐺 is a countable union of finite sets, it is countable (which needs ax-cc 10460 via iunctb 10599), and so we can apply ax-cc 10460 to 𝐺 directly to get a function from 𝐺 to itself, which points from each ball in 𝐾 to a ball on the next level in 𝐾, and such that the intersection between these balls is also in 𝐾. (Contributed by Jeff Madsen, 18-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}    &   ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}    &   ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))    ⇒   ⊢ (𝜑 → ∃𝑔∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))
Theorem	heiborlem4 37418*	Lemma for heibor 37425. Using the function 𝑇 constructed in heiborlem3 37417, construct an infinite path in 𝐺. (Contributed by Jeff Madsen, 23-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}    &   ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}    &   ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))    &   ⊢ (𝜑 → 𝐶𝐺0)    &   ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ0) → (𝑆‘𝐴)𝐺𝐴)
Theorem	heiborlem5 37419*	Lemma for heibor 37425. The function 𝑀 is a set of point-and-radius pairs suitable for application to caubl 25280. (Contributed by Jeff Madsen, 23-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}    &   ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}    &   ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))    &   ⊢ (𝜑 → 𝐶𝐺0)    &   ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))    &   ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩)    ⇒   ⊢ (𝜑 → 𝑀:ℕ⟶(𝑋 × ℝ+))
Theorem	heiborlem6 37420*	Lemma for heibor 37425. Since the sequence of balls connected by the function 𝑇 ensures that each ball nontrivially intersects with the next (since the empty set has a finite subcover, the intersection of any two successive balls in the sequence is nonempty), and each ball is half the size of the previous one, the distance between the centers is at most 3 / 2 times the size of the larger, and so if we expand each ball by a factor of 3 we get a nested sequence of balls. (Contributed by Jeff Madsen, 23-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}    &   ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}    &   ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))    &   ⊢ (𝜑 → 𝐶𝐺0)    &   ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))    &   ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩)    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ ℕ ((ball‘𝐷)‘(𝑀‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝑀‘𝑘)))
Theorem	heiborlem7 37421*	Lemma for heibor 37425. Since the sizes of the balls decrease exponentially, the sequence converges to zero. (Contributed by Jeff Madsen, 23-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}    &   ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}    &   ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))    &   ⊢ (𝜑 → 𝐶𝐺0)    &   ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))    &   ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩)    ⇒   ⊢ ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℕ (2nd ‘(𝑀‘𝑘)) < 𝑟
Theorem	heiborlem8 37422*	Lemma for heibor 37425. The previous lemmas establish that the sequence 𝑀 is Cauchy, so using completeness we now consider the convergent point 𝑌. By assumption, 𝑈 is an open cover, so 𝑌 is an element of some 𝑍 ∈ 𝑈, and some ball centered at 𝑌 is contained in 𝑍. But the sequence contains arbitrarily small balls close to 𝑌, so some element ball(𝑀‘𝑛) of the sequence is contained in 𝑍. And finally we arrive at a contradiction, because {𝑍} is a finite subcover of 𝑈 that covers ball(𝑀‘𝑛), yet ball(𝑀‘𝑛) ∈ 𝐾. For convenience, we write this contradiction as 𝜑 → 𝜓 where 𝜑 is all the accumulated hypotheses and 𝜓 is anything at all. (Contributed by Jeff Madsen, 22-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}    &   ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}    &   ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))    &   ⊢ (𝜑 → 𝐶𝐺0)    &   ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))    &   ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ 𝑌 ∈ V    &   ⊢ (𝜑 → 𝑌 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑈)    &   ⊢ (𝜑 → (1st ∘ 𝑀)(⇝𝑡‘𝐽)𝑌)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	heiborlem9 37423*	Lemma for heibor 37425. Discharge the hypotheses of heiborlem8 37422 by applying caubl 25280 to get a convergent point and adding the open cover assumption. (Contributed by Jeff Madsen, 20-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}    &   ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}    &   ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ((𝑇‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑇‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))    &   ⊢ (𝜑 → 𝐶𝐺0)    &   ⊢ 𝑆 = seq0(𝑇, (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐶, (𝑚 − 1))))    &   ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ ⟨(𝑆‘𝑛), (3 / (2↑𝑛))⟩)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → ∪ 𝑈 = 𝑋)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	heiborlem10 37424*	Lemma for heibor 37425. The last remaining piece of the proof is to find an element 𝐶 such that 𝐶𝐺0, i.e. 𝐶 is an element of (𝐹‘0) that has no finite subcover, which is true by heiborlem1 37415, since (𝐹‘0) is a finite cover of 𝑋, which has no finite subcover. Thus, the rest of the proof follows to a contradiction, and thus there must be a finite subcover of 𝑈 that covers 𝑋, i.e. 𝑋 is compact. (Contributed by Jeff Madsen, 22-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}    &   ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}    &   ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))    ⇒   ⊢ ((𝜑 ∧ (𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈)) → ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)∪ 𝐽 = ∪ 𝑣)
Theorem	heibor 37425	Generalized Heine-Borel Theorem. A metric space is compact iff it is complete and totally bounded. See heibor1 37414 and heiborlem1 37415 for a description of the proof. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐽 ∈ Comp) ↔ (𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)))
21.22.10  Banach Fixed Point Theorem
Theorem	bfplem1 37426*	Lemma for bfp 37428. The sequence 𝐺, which simply starts from any point in the space and iterates 𝐹, satisfies the property that the distance from 𝐺(𝑛) to 𝐺(𝑛 + 1) decreases by at least 𝐾 after each step. Thus, the total distance from any 𝐺(𝑖) to 𝐺(𝑗) is bounded by a geometric series, and the sequence is Cauchy. Therefore, it converges to a point ((⇝𝑡‘𝐽)‘𝐺) since the space is complete. (Contributed by Jeff Madsen, 17-Jun-2014.)
⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    &   ⊢ (𝜑 → 𝐾 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐾 < 1)    &   ⊢ (𝜑 → 𝐹:𝑋⟶𝑋)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦)))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐺 = seq1((𝐹 ∘ 1st ), (ℕ × {𝐴}))    ⇒   ⊢ (𝜑 → 𝐺(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝐺))
Theorem	bfplem2 37427*	Lemma for bfp 37428. Using the point found in bfplem1 37426, we show that this convergent point is a fixed point of 𝐹. Since for any positive 𝑥, the sequence 𝐺 is in 𝐵(𝑥 / 2, 𝑃) for all 𝑘 ∈ (ℤ≥‘𝑗) (where 𝑃 = ((⇝𝑡‘𝐽)‘𝐺)), we have 𝐷(𝐺(𝑗 + 1), 𝐹(𝑃)) ≤ 𝐷(𝐺(𝑗), 𝑃) < 𝑥 / 2 and 𝐷(𝐺(𝑗 + 1), 𝑃) < 𝑥 / 2, so 𝐹(𝑃) is in every neighborhood of 𝑃 and 𝑃 is a fixed point of 𝐹. (Contributed by Jeff Madsen, 5-Jun-2014.)
⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    &   ⊢ (𝜑 → 𝐾 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐾 < 1)    &   ⊢ (𝜑 → 𝐹:𝑋⟶𝑋)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦)))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐺 = seq1((𝐹 ∘ 1st ), (ℕ × {𝐴}))    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑧)
Theorem	bfp 37428*	Banach fixed point theorem, also known as contraction mapping theorem. A contraction on a complete metric space has a unique fixed point. We show existence in the lemmas, and uniqueness here - if 𝐹 has two fixed points, then the distance between them is less than 𝐾 times itself, a contradiction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.)
⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    &   ⊢ (𝜑 → 𝐾 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐾 < 1)    &   ⊢ (𝜑 → 𝐹:𝑋⟶𝑋)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦)))    ⇒   ⊢ (𝜑 → ∃!𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑧)
21.22.11  Euclidean space
Syntax	crrn 37429	Extend class notation with the n-dimensional Euclidean space.
class ℝn
Definition	df-rrn 37430*	Define n-dimensional Euclidean space as a metric space with the standard Euclidean norm given by the quadratic mean. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ℝn = (𝑖 ∈ Fin ↦ (𝑥 ∈ (ℝ ↑m 𝑖), 𝑦 ∈ (ℝ ↑m 𝑖) ↦ (√‘Σ𝑘 ∈ 𝑖 (((𝑥‘𝑘) − (𝑦‘𝑘))↑2))))
Theorem	rrnval 37431*	The n-dimensional Euclidean space. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.)
⊢ 𝑋 = (ℝ ↑m 𝐼)    ⇒   ⊢ (𝐼 ∈ Fin → (ℝn‘𝐼) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ 𝐼 (((𝑥‘𝑘) − (𝑦‘𝑘))↑2))))
Theorem	rrnmval 37432*	The value of the Euclidean metric. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.)
⊢ 𝑋 = (ℝ ↑m 𝐼)    ⇒   ⊢ ((𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹(ℝn‘𝐼)𝐺) = (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)))
Theorem	rrnmet 37433	Euclidean space is a metric space. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.)
⊢ 𝑋 = (ℝ ↑m 𝐼)    ⇒   ⊢ (𝐼 ∈ Fin → (ℝn‘𝐼) ∈ (Met‘𝑋))
Theorem	rrndstprj1 37434	The distance between two points in Euclidean space is greater than the distance between the projections onto one coordinate. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.)
⊢ 𝑋 = (ℝ ↑m 𝐼)    &   ⊢ 𝑀 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ (((𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐼) ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ((𝐹‘𝐴)𝑀(𝐺‘𝐴)) ≤ (𝐹(ℝn‘𝐼)𝐺))
Theorem	rrndstprj2 37435*	Bound on the distance between two points in Euclidean space given bounds on the distances in each coordinate. This theorem and rrndstprj1 37434 can be used to show that the supremum norm and Euclidean norm are equivalent. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.)
⊢ 𝑋 = (ℝ ↑m 𝐼)    &   ⊢ 𝑀 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝐹(ℝn‘𝐼)𝐺) < (𝑅 · (√‘(♯‘𝐼))))
Theorem	rrncmslem 37436*	Lemma for rrncms 37437. (Contributed by Jeff Madsen, 6-Jun-2014.) (Revised by Mario Carneiro, 13-Sep-2015.)
⊢ 𝑋 = (ℝ ↑m 𝐼)    &   ⊢ 𝑀 = ((abs ∘ − ) ↾ (ℝ × ℝ))    &   ⊢ 𝐽 = (MetOpen‘(ℝn‘𝐼))    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐹 ∈ (Cau‘(ℝn‘𝐼)))    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑋)    &   ⊢ 𝑃 = (𝑚 ∈ 𝐼 ↦ ( ⇝ ‘(𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑚))))    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽))
Theorem	rrncms 37437	Euclidean space is complete. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.)
⊢ 𝑋 = (ℝ ↑m 𝐼)    ⇒   ⊢ (𝐼 ∈ Fin → (ℝn‘𝐼) ∈ (CMet‘𝑋))
Theorem	repwsmet 37438	The supremum metric on ℝ↑𝐼 is a metric. (Contributed by Jeff Madsen, 15-Sep-2015.)
⊢ 𝑌 = ((ℂfld ↾s ℝ) ↑s 𝐼)    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ 𝑋 = (ℝ ↑m 𝐼)    ⇒   ⊢ (𝐼 ∈ Fin → 𝐷 ∈ (Met‘𝑋))
Theorem	rrnequiv 37439	The supremum metric on ℝ↑𝐼 is equivalent to the ℝn metric. (Contributed by Jeff Madsen, 15-Sep-2015.)
⊢ 𝑌 = ((ℂfld ↾s ℝ) ↑s 𝐼)    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ 𝑋 = (ℝ ↑m 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    ⇒   ⊢ ((𝜑 ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ((𝐹𝐷𝐺) ≤ (𝐹(ℝn‘𝐼)𝐺) ∧ (𝐹(ℝn‘𝐼)𝐺) ≤ ((√‘(♯‘𝐼)) · (𝐹𝐷𝐺))))
Theorem	rrntotbnd 37440	A set in Euclidean space is totally bounded iff its is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 16-Sep-2015.)
⊢ 𝑋 = (ℝ ↑m 𝐼)    &   ⊢ 𝑀 = ((ℝn‘𝐼) ↾ (𝑌 × 𝑌))    ⇒   ⊢ (𝐼 ∈ Fin → (𝑀 ∈ (TotBnd‘𝑌) ↔ 𝑀 ∈ (Bnd‘𝑌)))
Theorem	rrnheibor 37441	Heine-Borel theorem for Euclidean space. A subset of Euclidean space is compact iff it is closed and bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ 𝑋 = (ℝ ↑m 𝐼)    &   ⊢ 𝑀 = ((ℝn‘𝐼) ↾ (𝑌 × 𝑌))    &   ⊢ 𝑇 = (MetOpen‘𝑀)    &   ⊢ 𝑈 = (MetOpen‘(ℝn‘𝐼))    ⇒   ⊢ ((𝐼 ∈ Fin ∧ 𝑌 ⊆ 𝑋) → (𝑇 ∈ Comp ↔ (𝑌 ∈ (Clsd‘𝑈) ∧ 𝑀 ∈ (Bnd‘𝑌))))
21.22.12  Intervals (continued)
Theorem	ismrer1 37442*	An isometry between ℝ and ℝ↑1. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ 𝑅 = ((abs ∘ − ) ↾ (ℝ × ℝ))    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ({𝐴} × {𝑥}))    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐹 ∈ (𝑅 Ismty (ℝn‘{𝐴})))
Theorem	reheibor 37443	Heine-Borel theorem for real numbers. A subset of ℝ is compact iff it is closed and bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ 𝑀 = ((abs ∘ − ) ↾ (𝑌 × 𝑌))    &   ⊢ 𝑇 = (MetOpen‘𝑀)    &   ⊢ 𝑈 = (topGen‘ran (,))    ⇒   ⊢ (𝑌 ⊆ ℝ → (𝑇 ∈ Comp ↔ (𝑌 ∈ (Clsd‘𝑈) ∧ 𝑀 ∈ (Bnd‘𝑌))))
Theorem	iccbnd 37444	A closed interval in ℝ is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐽 = (𝐴[,]𝐵)    &   ⊢ 𝑀 = ((abs ∘ − ) ↾ (𝐽 × 𝐽))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑀 ∈ (Bnd‘𝐽))
Theorem	icccmpALT 37445	A closed interval in ℝ is compact. Alternate proof of icccmp 24785 using the Heine-Borel theorem heibor 37425. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Aug-2014.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐽 = (𝐴[,]𝐵)    &   ⊢ 𝑀 = ((abs ∘ − ) ↾ (𝐽 × 𝐽))    &   ⊢ 𝑇 = (MetOpen‘𝑀)    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑇 ∈ Comp)
21.22.13  Operation properties
Syntax	cass 37446	Extend class notation with a device to add associativity to internal operations.
class Ass
Definition	df-ass 37447*	A device to add associativity to various sorts of internal operations. The definition is meaningful when 𝑔 is a magma at least. (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.)
⊢ Ass = {𝑔 ∣ ∀𝑥 ∈ dom dom 𝑔∀𝑦 ∈ dom dom 𝑔∀𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))}
Syntax	cexid 37448	Extend class notation with the class of all the internal operations with an identity element.
class ExId
Definition	df-exid 37449*	A device to add an identity element to various sorts of internal operations. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
⊢ ExId = {𝑔 ∣ ∃𝑥 ∈ dom dom 𝑔∀𝑦 ∈ dom dom 𝑔((𝑥𝑔𝑦) = 𝑦 ∧ (𝑦𝑔𝑥) = 𝑦)}
Theorem	isass 37450*	The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.)
⊢ 𝑋 = dom dom 𝐺    ⇒   ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ Ass ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))))
Theorem	isexid 37451*	The predicate 𝐺 has a left and right identity element. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = dom dom 𝐺    ⇒   ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ ExId ↔ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝑥) = 𝑦)))
21.22.14  Groups and related structures
Syntax	cmagm 37452	Extend class notation with the class of all magmas.
class Magma
Definition	df-mgmOLD 37453*	Obsolete version of df-mgm 18603 as of 3-Feb-2020. A magma is a binary internal operation. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
⊢ Magma = {𝑔 ∣ ∃𝑡 𝑔:(𝑡 × 𝑡)⟶𝑡}
Theorem	ismgmOLD 37454	Obsolete version of ismgm 18604 as of 3-Feb-2020. The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑋 = dom dom 𝐺    ⇒   ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ Magma ↔ 𝐺:(𝑋 × 𝑋)⟶𝑋))
Theorem	clmgmOLD 37455	Obsolete version of mgmcl 18606 as of 3-Feb-2020. Closure of a magma. (Contributed by FL, 14-Sep-2010.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑋 = dom dom 𝐺    ⇒   ⊢ ((𝐺 ∈ Magma ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)
Theorem	opidonOLD 37456	Obsolete version of mndpfo 18720 as of 23-Jan-2020. An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑋 = dom dom 𝐺    ⇒   ⊢ (𝐺 ∈ (Magma ∩ ExId ) → 𝐺:(𝑋 × 𝑋)–onto→𝑋)
Theorem	rngopidOLD 37457	Obsolete version of mndpfo 18720 as of 23-Jan-2020. Range of an operation with a left and right identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐺 ∈ (Magma ∩ ExId ) → ran 𝐺 = dom dom 𝐺)
Theorem	opidon2OLD 37458	Obsolete version of mndpfo 18720 as of 23-Jan-2020. An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ (Magma ∩ ExId ) → 𝐺:(𝑋 × 𝑋)–onto→𝑋)
Theorem	isexid2 37459*	If 𝐺 ∈ (Magma ∩ ExId ), then it has a left and right identity element that belongs to the range of the operation. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ (Magma ∩ ExId ) → ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥))
Theorem	exidu1 37460*	Uniqueness of the left and right identity element of a magma when it exists. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ (Magma ∩ ExId ) → ∃!𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥))
Theorem	idrval 37461*	The value of the identity element. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝐴 → 𝑈 = (℩𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)))
Theorem	iorlid 37462	A magma right and left identity belongs to the underlying set of the operation. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    ⇒   ⊢ (𝐺 ∈ (Magma ∩ ExId ) → 𝑈 ∈ 𝑋)
Theorem	cmpidelt 37463	A magma right and left identity element keeps the other elements unchanged. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    ⇒   ⊢ ((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝐴 ∈ 𝑋) → ((𝑈𝐺𝐴) = 𝐴 ∧ (𝐴𝐺𝑈) = 𝐴))
Syntax	csem 37464	Extend class notation with the class of all semigroups.
class SemiGrp
Definition	df-sgrOLD 37465	Obsolete version of df-sgrp 18682 as of 3-Feb-2020. A semigroup is an associative magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
⊢ SemiGrp = (Magma ∩ Ass)
Theorem	smgrpismgmOLD 37466	Obsolete version of sgrpmgm 18687 as of 3-Feb-2020. A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐺 ∈ SemiGrp → 𝐺 ∈ Magma)
Theorem	issmgrpOLD 37467*	Obsolete version of issgrp 18683 as of 3-Feb-2020. The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑋 = dom dom 𝐺    ⇒   ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ SemiGrp ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))))
Theorem	smgrpmgm 37468	A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
⊢ 𝑋 = dom dom 𝐺    ⇒   ⊢ (𝐺 ∈ SemiGrp → 𝐺:(𝑋 × 𝑋)⟶𝑋)
Theorem	smgrpassOLD 37469*	Obsolete version of sgrpass 18688 as of 3-Feb-2020. A semigroup is associative. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑋 = dom dom 𝐺    ⇒   ⊢ (𝐺 ∈ SemiGrp → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))
Syntax	cmndo 37470	Extend class notation with the class of all monoids.
class MndOp
Definition	df-mndo 37471	A monoid is a semigroup with an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
⊢ MndOp = (SemiGrp ∩ ExId )
Theorem	mndoissmgrpOLD 37472	Obsolete version of mndsgrp 18703 as of 3-Feb-2020. A monoid is a semigroup. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐺 ∈ MndOp → 𝐺 ∈ SemiGrp)
Theorem	mndoisexid 37473	A monoid has an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
⊢ (𝐺 ∈ MndOp → 𝐺 ∈ ExId )
Theorem	mndoismgmOLD 37474	Obsolete version of mndmgm 18704 as of 3-Feb-2020. A monoid is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐺 ∈ MndOp → 𝐺 ∈ Magma)
Theorem	mndomgmid 37475	A monoid is a magma with an identity element. (Contributed by FL, 18-Feb-2010.) (New usage is discouraged.)
⊢ (𝐺 ∈ MndOp → 𝐺 ∈ (Magma ∩ ExId ))
Theorem	ismndo 37476*	The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = dom dom 𝐺    ⇒   ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ MndOp ↔ (𝐺 ∈ SemiGrp ∧ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝑥) = 𝑦))))
Theorem	ismndo1 37477*	The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = dom dom 𝐺    ⇒   ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ MndOp ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝑥) = 𝑦))))
Theorem	ismndo2 37478*	The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ MndOp ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝑥) = 𝑦))))
Theorem	grpomndo 37479	A group is a monoid. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
⊢ (𝐺 ∈ GrpOp → 𝐺 ∈ MndOp)
Theorem	exidcl 37480	Closure of the binary operation of a magma with identity. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)
Theorem	exidreslem 37481*	Lemma for exidres 37482 and exidresid 37483. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾ (𝑌 × 𝑌))    ⇒   ⊢ ((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → (𝑈 ∈ dom dom 𝐻 ∧ ∀𝑥 ∈ dom dom 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥)))
Theorem	exidres 37482	The restriction of a binary operation with identity to a subset containing the identity has an identity element. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾ (𝑌 × 𝑌))    ⇒   ⊢ ((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → 𝐻 ∈ ExId )
Theorem	exidresid 37483	The restriction of a binary operation with identity to a subset containing the identity has the same identity element. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾ (𝑌 × 𝑌))    ⇒   ⊢ (((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) ∧ 𝐻 ∈ Magma) → (GId‘𝐻) = 𝑈)
Theorem	ablo4pnp 37484	A commutative/associative law for Abelian groups. (Contributed by Jeff Madsen, 11-Jun-2010.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ AbelOp ∧ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐹 ∈ 𝑋))) → ((𝐴𝐺𝐵)𝐷(𝐶𝐺𝐹)) = ((𝐴𝐷𝐶)𝐺(𝐵𝐷𝐹)))
Theorem	grpoeqdivid 37485	Two group elements are equal iff their quotient is the identity. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 = 𝐵 ↔ (𝐴𝐷𝐵) = 𝑈))
Theorem	grposnOLD 37486	The group operation for the singleton group. Obsolete, use grp1 19011. instead. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ∈ GrpOp
21.22.15  Group homomorphism and isomorphism
Syntax	cghomOLD 37487	Obsolete version of cghm 19175 as of 15-Mar-2020. Extend class notation to include the class of group homomorphisms. (New usage is discouraged.)
class GrpOpHom
Definition	df-ghomOLD 37488*	Obsolete version of df-ghm 19176 as of 15-Mar-2020. Define the set of group homomorphisms from 𝑔 to ℎ. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.)
⊢ GrpOpHom = (𝑔 ∈ GrpOp, ℎ ∈ GrpOp ↦ {𝑓 ∣ (𝑓:ran 𝑔⟶ran ℎ ∧ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔((𝑓‘𝑥)ℎ(𝑓‘𝑦)) = (𝑓‘(𝑥𝑔𝑦)))})
Theorem	elghomlem1OLD 37489*	Obsolete as of 15-Mar-2020. Lemma for elghomOLD 37491. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑆 = {𝑓 ∣ (𝑓:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑓‘𝑥)𝐻(𝑓‘𝑦)) = (𝑓‘(𝑥𝐺𝑦)))}    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → (𝐺 GrpOpHom 𝐻) = 𝑆)
Theorem	elghomlem2OLD 37490*	Obsolete as of 15-Mar-2020. Lemma for elghomOLD 37491. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑆 = {𝑓 ∣ (𝑓:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑓‘𝑥)𝐻(𝑓‘𝑦)) = (𝑓‘(𝑥𝐺𝑦)))}    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → (𝐹 ∈ (𝐺 GrpOpHom 𝐻) ↔ (𝐹:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝐹‘𝑥)𝐻(𝐹‘𝑦)) = (𝐹‘(𝑥𝐺𝑦)))))
Theorem	elghomOLD 37491*	Obsolete version of isghm 19178 as of 15-Mar-2020. Membership in the set of group homomorphisms from 𝐺 to 𝐻. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑊 = ran 𝐻    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → (𝐹 ∈ (𝐺 GrpOpHom 𝐻) ↔ (𝐹:𝑋⟶𝑊 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘𝑥)𝐻(𝐹‘𝑦)) = (𝐹‘(𝑥𝐺𝑦)))))
Theorem	ghomlinOLD 37492	Obsolete version of ghmlin 19184 as of 15-Mar-2020. Linearity of a group homomorphism. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐹‘𝐴)𝐻(𝐹‘𝐵)) = (𝐹‘(𝐴𝐺𝐵)))
Theorem	ghomidOLD 37493	Obsolete version of ghmid 19185 as of 15-Mar-2020. A group homomorphism maps identity element to identity element. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑈 = (GId‘𝐺)    &   ⊢ 𝑇 = (GId‘𝐻)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → (𝐹‘𝑈) = 𝑇)
Theorem	ghomf 37494	Mapping property of a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑊 = ran 𝐻    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → 𝐹:𝑋⟶𝑊)
Theorem	ghomco 37495	The composition of two group homomorphisms is a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009.) (Revised by Mario Carneiro, 27-Dec-2014.)
⊢ (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp) ∧ (𝑆 ∈ (𝐺 GrpOpHom 𝐻) ∧ 𝑇 ∈ (𝐻 GrpOpHom 𝐾))) → (𝑇 ∘ 𝑆) ∈ (𝐺 GrpOpHom 𝐾))
Theorem	ghomdiv 37496	Group homomorphisms preserve division. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    &   ⊢ 𝐶 = ( /𝑔 ‘𝐻)    ⇒   ⊢ (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐷𝐵)) = ((𝐹‘𝐴)𝐶(𝐹‘𝐵)))
Theorem	grpokerinj 37497	A group homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑊 = (GId‘𝐺)    &   ⊢ 𝑌 = ran 𝐻    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → (𝐹:𝑋–1-1→𝑌 ↔ (◡𝐹 “ {𝑈}) = {𝑊}))
21.22.16  Rings
Syntax	crngo 37498	Extend class notation with the class of all unital rings.
class RingOps
Definition	df-rngo 37499*	Define the class of all unital rings. (Contributed by Jeff Hankins, 21-Nov-2006.) (New usage is discouraged.)
⊢ RingOps = {⟨𝑔, ℎ⟩ ∣ ((𝑔 ∈ AbelOp ∧ ℎ:(ran 𝑔 × ran 𝑔)⟶ran 𝑔) ∧ (∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔∀𝑧 ∈ ran 𝑔(((𝑥ℎ𝑦)ℎ𝑧) = (𝑥ℎ(𝑦ℎ𝑧)) ∧ (𝑥ℎ(𝑦𝑔𝑧)) = ((𝑥ℎ𝑦)𝑔(𝑥ℎ𝑧)) ∧ ((𝑥𝑔𝑦)ℎ𝑧) = ((𝑥ℎ𝑧)𝑔(𝑦ℎ𝑧))) ∧ ∃𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔((𝑥ℎ𝑦) = 𝑦 ∧ (𝑦ℎ𝑥) = 𝑦)))}
Theorem	relrngo 37500	The class of all unital rings is a relation. (Contributed by FL, 31-Aug-2009.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
⊢ Rel RingOps