| Metamath
Proof Explorer Theorem List (p. 379 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | prdstotbnd 37801* | The product metric over finite index set is totally bounded if all the factors are totally bounded. (Contributed by Mario Carneiro, 20-Sep-2015.) |
| ⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑉 = (Base‘(𝑅‘𝑥)) & ⊢ 𝐸 = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) & ⊢ 𝐷 = (dist‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (TotBnd‘𝑉)) ⇒ ⊢ (𝜑 → 𝐷 ∈ (TotBnd‘𝐵)) | ||
| Theorem | prdsbnd2 37802* | If balls are totally bounded in each factor, then balls are bounded in a metric product. (Contributed by Mario Carneiro, 16-Sep-2015.) |
| ⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑉 = (Base‘(𝑅‘𝑥)) & ⊢ 𝐸 = ((dist‘(𝑅‘𝑥)) ↾ (𝑉 × 𝑉)) & ⊢ 𝐷 = (dist‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ 𝐶 = (𝐷 ↾ (𝐴 × 𝐴)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ↾ (𝑦 × 𝑦)) ∈ (TotBnd‘𝑦) ↔ (𝐸 ↾ (𝑦 × 𝑦)) ∈ (Bnd‘𝑦))) ⇒ ⊢ (𝜑 → (𝐶 ∈ (TotBnd‘𝐴) ↔ 𝐶 ∈ (Bnd‘𝐴))) | ||
| Theorem | cntotbnd 37803 | A subset of the complex numbers is totally bounded iff it is bounded. (Contributed by Mario Carneiro, 14-Sep-2015.) |
| ⊢ 𝐷 = ((abs ∘ − ) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝐷 ∈ (TotBnd‘𝑋) ↔ 𝐷 ∈ (Bnd‘𝑋)) | ||
| Theorem | cnpwstotbnd 37804 | 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‘𝑋))) | ||
| Syntax | cismty 37805 | Extend class notation with the class of metric space isometries. |
| class Ismty | ||
| Definition | df-ismty 37806* | 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 37807* | The set of isometries between two metric spaces. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝑀 Ismty 𝑁) = {𝑓 ∣ (𝑓:𝑋–1-1-onto→𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) = ((𝑓‘𝑥)𝑁(𝑓‘𝑦)))}) | ||
| Theorem | isismty 37808* | The condition "is an isometry". (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝐹 ∈ (𝑀 Ismty 𝑁) ↔ (𝐹:𝑋–1-1-onto→𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) = ((𝐹‘𝑥)𝑁(𝐹‘𝑦))))) | ||
| Theorem | ismtycnv 37809 | The inverse of an isometry is an isometry. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝐹 ∈ (𝑀 Ismty 𝑁) → ◡𝐹 ∈ (𝑁 Ismty 𝑀))) | ||
| Theorem | ismtyima 37810 | 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 37811 | Lemma for ismtyhmeo 37812. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
| ⊢ 𝐽 = (MetOpen‘𝑀) & ⊢ 𝐾 = (MetOpen‘𝑁) & ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) & ⊢ (𝜑 → 𝐹 ∈ (𝑀 Ismty 𝑁)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) | ||
| Theorem | ismtyhmeo 37812 | 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 37813 | Lemma for ismtybnd 37814. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 19-Jan-2014.) |
| ⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝐹 ∈ (𝑀 Ismty 𝑁)) → (𝑀 ∈ (Bnd‘𝑋) → 𝑁 ∈ (Bnd‘𝑌))) | ||
| Theorem | ismtybnd 37814 | Isometries preserve boundedness. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 19-Jan-2014.) |
| ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌) ∧ 𝐹 ∈ (𝑀 Ismty 𝑁)) → (𝑀 ∈ (Bnd‘𝑋) ↔ 𝑁 ∈ (Bnd‘𝑌))) | ||
| Theorem | ismtyres 37815 | 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 𝑇)) | ||
| Theorem | heibor1lem 37816 | Lemma for heibor1 37817. 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 37817 | One half of heibor 37828, that does not require any Choice. A compact metric space is complete and totally bounded. We prove completeness in cmpcmet 25353 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 37818* | Lemma for heibor 37828. 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 37819* | Lemma for heibor 37828. Substitutions for the set 𝐺. (Contributed by Jeff Madsen, 23-Jan-2014.) |
| ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣} & ⊢ 𝐺 = {〈𝑦, 𝑛〉 ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)} & ⊢ 𝐴 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴𝐺𝐶 ↔ (𝐶 ∈ ℕ0 ∧ 𝐴 ∈ (𝐹‘𝐶) ∧ (𝐴𝐵𝐶) ∈ 𝐾)) | ||
| Theorem | heiborlem3 37820* | Lemma for heibor 37828. Using countable choice ax-cc 10475, 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 37818 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 10475 via iunctb 10614), and so we can apply ax-cc 10475 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 37821* | Lemma for heibor 37828. Using the function 𝑇 constructed in heiborlem3 37820, 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 37822* | Lemma for heibor 37828. The function 𝑀 is a set of point-and-radius pairs suitable for application to caubl 25342. (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 37823* | Lemma for heibor 37828. 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 37824* | Lemma for heibor 37828. 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 37825* | Lemma for heibor 37828. 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 37826* | Lemma for heibor 37828. Discharge the hypotheses of heiborlem8 37825 by applying caubl 25342 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 37827* | Lemma for heibor 37828. 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 37818, 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 37828 | Generalized Heine-Borel Theorem. A metric space is compact iff it is complete and totally bounded. See heibor1 37817 and heiborlem1 37818 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‘𝑋))) | ||
| Theorem | bfplem1 37829* | Lemma for bfp 37831. 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 37830* | Lemma for bfp 37831. Using the point found in bfplem1 37829, 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 37831* | 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) & ⊢ (𝜑 → 𝐹:𝑋⟶𝑋) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦))) ⇒ ⊢ (𝜑 → ∃!𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑧) | ||
| Syntax | crrn 37832 | Extend class notation with the n-dimensional Euclidean space. |
| class ℝn | ||
| Definition | df-rrn 37833* | 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 37834* | 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 37835* | 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 37836 | 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 37837 | 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 37838* | Bound on the distance between two points in Euclidean space given bounds on the distances in each coordinate. This theorem and rrndstprj1 37837 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 37839* | Lemma for rrncms 37840. (Contributed by Jeff Madsen, 6-Jun-2014.) (Revised by Mario Carneiro, 13-Sep-2015.) |
| ⊢ 𝑋 = (ℝ ↑m 𝐼) & ⊢ 𝑀 = ((abs ∘ − ) ↾ (ℝ × ℝ)) & ⊢ 𝐽 = (MetOpen‘(ℝn‘𝐼)) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐹 ∈ (Cau‘(ℝn‘𝐼))) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑋) & ⊢ 𝑃 = (𝑚 ∈ 𝐼 ↦ ( ⇝ ‘(𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑚)))) ⇒ ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽)) | ||
| Theorem | rrncms 37840 | Euclidean space is complete. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.) |
| ⊢ 𝑋 = (ℝ ↑m 𝐼) ⇒ ⊢ (𝐼 ∈ Fin → (ℝn‘𝐼) ∈ (CMet‘𝑋)) | ||
| Theorem | repwsmet 37841 | The supremum metric on ℝ↑𝐼 is a metric. (Contributed by Jeff Madsen, 15-Sep-2015.) |
| ⊢ 𝑌 = ((ℂfld ↾s ℝ) ↑s 𝐼) & ⊢ 𝐷 = (dist‘𝑌) & ⊢ 𝑋 = (ℝ ↑m 𝐼) ⇒ ⊢ (𝐼 ∈ Fin → 𝐷 ∈ (Met‘𝑋)) | ||
| Theorem | rrnequiv 37842 | 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 37843 | 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 37844 | 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‘𝑌)))) | ||
| Theorem | ismrer1 37845* | An isometry between ℝ and ℝ↑1. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.) |
| ⊢ 𝑅 = ((abs ∘ − ) ↾ (ℝ × ℝ)) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ({𝐴} × {𝑥})) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹 ∈ (𝑅 Ismty (ℝn‘{𝐴}))) | ||
| Theorem | reheibor 37846 | 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 37847 | 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 37848 | A closed interval in ℝ is compact. Alternate proof of icccmp 24847 using the Heine-Borel theorem heibor 37828. (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) | ||
| Syntax | cass 37849 | Extend class notation with a device to add associativity to internal operations. |
| class Ass | ||
| Definition | df-ass 37850* | 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 37851 | Extend class notation with the class of all the internal operations with an identity element. |
| class ExId | ||
| Definition | df-exid 37852* | 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 37853* | The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.) |
| ⊢ 𝑋 = dom dom 𝐺 ⇒ ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ Ass ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))) | ||
| Theorem | isexid 37854* | 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 ↔ ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐺𝑦) = 𝑦 ∧ (𝑦𝐺𝑥) = 𝑦))) | ||
| Syntax | cmagm 37855 | Extend class notation with the class of all magmas. |
| class Magma | ||
| Definition | df-mgmOLD 37856* | Obsolete version of df-mgm 18653 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 37857 | Obsolete version of ismgm 18654 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 37858 | Obsolete version of mgmcl 18656 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 37859 | Obsolete version of mndpfo 18770 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 37860 | Obsolete version of mndpfo 18770 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 37861 | Obsolete version of mndpfo 18770 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 37862* | 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 37863* | 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 37864* | 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 37865 | 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 37866 | 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 37867 | Extend class notation with the class of all semigroups. |
| class SemiGrp | ||
| Definition | df-sgrOLD 37868 | Obsolete version of df-sgrp 18732 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 37869 | Obsolete version of sgrpmgm 18737 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 37870* | Obsolete version of issgrp 18733 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 37871 | A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
| ⊢ 𝑋 = dom dom 𝐺 ⇒ ⊢ (𝐺 ∈ SemiGrp → 𝐺:(𝑋 × 𝑋)⟶𝑋) | ||
| Theorem | smgrpassOLD 37872* | Obsolete version of sgrpass 18738 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 37873 | Extend class notation with the class of all monoids. |
| class MndOp | ||
| Definition | df-mndo 37874 | A monoid is a semigroup with an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
| ⊢ MndOp = (SemiGrp ∩ ExId ) | ||
| Theorem | mndoissmgrpOLD 37875 | Obsolete version of mndsgrp 18753 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 37876 | A monoid has an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
| ⊢ (𝐺 ∈ MndOp → 𝐺 ∈ ExId ) | ||
| Theorem | mndoismgmOLD 37877 | Obsolete version of mndmgm 18754 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 37878 | A monoid is a magma with an identity element. (Contributed by FL, 18-Feb-2010.) (New usage is discouraged.) |
| ⊢ (𝐺 ∈ MndOp → 𝐺 ∈ (Magma ∩ ExId )) | ||
| Theorem | ismndo 37879* | 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 37880* | 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 37881* | 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 37882 | 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 37883 | Closure of the binary operation of a magma with identity. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋) | ||
| Theorem | exidreslem 37884* | Lemma for exidres 37885 and exidresid 37886. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝐻 = (𝐺 ↾ (𝑌 × 𝑌)) ⇒ ⊢ ((𝐺 ∈ (Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌) → (𝑈 ∈ dom dom 𝐻 ∧ ∀𝑥 ∈ dom dom 𝐻((𝑈𝐻𝑥) = 𝑥 ∧ (𝑥𝐻𝑈) = 𝑥))) | ||
| Theorem | exidres 37885 | 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 37886 | 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 37887 | A commutative/associative law for Abelian groups. (Contributed by Jeff Madsen, 11-Jun-2010.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ AbelOp ∧ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐹 ∈ 𝑋))) → ((𝐴𝐺𝐵)𝐷(𝐶𝐺𝐹)) = ((𝐴𝐷𝐶)𝐺(𝐵𝐷𝐹))) | ||
| Theorem | grpoeqdivid 37888 | Two group elements are equal iff their quotient is the identity. (Contributed by Jeff Madsen, 6-Jan-2011.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 = 𝐵 ↔ (𝐴𝐷𝐵) = 𝑈)) | ||
| Theorem | grposnOLD 37889 | The group operation for the singleton group. Obsolete, use grp1 19065. instead. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ {〈〈𝐴, 𝐴〉, 𝐴〉} ∈ GrpOp | ||
| Syntax | cghomOLD 37890 | Obsolete version of cghm 19230 as of 15-Mar-2020. Extend class notation to include the class of group homomorphisms. (New usage is discouraged.) |
| class GrpOpHom | ||
| Definition | df-ghomOLD 37891* | Obsolete version of df-ghm 19231 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 37892* | Obsolete as of 15-Mar-2020. Lemma for elghomOLD 37894. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑆 = {𝑓 ∣ (𝑓:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺((𝑓‘𝑥)𝐻(𝑓‘𝑦)) = (𝑓‘(𝑥𝐺𝑦)))} ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → (𝐺 GrpOpHom 𝐻) = 𝑆) | ||
| Theorem | elghomlem2OLD 37893* | Obsolete as of 15-Mar-2020. Lemma for elghomOLD 37894. (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 37894* | Obsolete version of isghm 19233 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 37895 | Obsolete version of ghmlin 19239 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 37896 | Obsolete version of ghmid 19240 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 37897 | Mapping property of a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑊 = ran 𝐻 ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) → 𝐹:𝑋⟶𝑊) | ||
| Theorem | ghomco 37898 | 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 37899 | Group homomorphisms preserve division. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) & ⊢ 𝐶 = ( /𝑔 ‘𝐻) ⇒ ⊢ (((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ (𝐺 GrpOpHom 𝐻)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘(𝐴𝐷𝐵)) = ((𝐹‘𝐴)𝐶(𝐹‘𝐵))) | ||
| Theorem | grpokerinj 37900 | 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→𝑌 ↔ (◡𝐹 “ {𝑈}) = {𝑊})) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |