![]() |
Metamath
Proof Explorer Theorem List (p. 244 of 472) | < 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-29705) |
![]() (29706-31228) |
![]() (31229-47147) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-phtpc 24301* | Define the function which takes a topology and returns the path homotopy relation on that topology. Definition of [Hatcher] p. 25. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Jun-2014.) |
⊢ ≃ph = (𝑥 ∈ Top ↦ {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ (II Cn 𝑥) ∧ (𝑓(PHtpy‘𝑥)𝑔) ≠ ∅)}) | ||
Theorem | phtpcrel 24302 | The path homotopy relation is a relation. (Contributed by Mario Carneiro, 7-Jun-2014.) (Revised by Mario Carneiro, 7-Aug-2014.) |
⊢ Rel ( ≃ph‘𝐽) | ||
Theorem | isphtpc 24303 | The relation "is path homotopic to". (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Sep-2015.) |
⊢ (𝐹( ≃ph‘𝐽)𝐺 ↔ (𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅)) | ||
Theorem | phtpcer 24304 | Path homotopy is an equivalence relation. Proposition 1.2 of [Hatcher] p. 26. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 6-Jul-2015.) (Proof shortened by AV, 1-May-2021.) |
⊢ ( ≃ph‘𝐽) Er (II Cn 𝐽) | ||
Theorem | phtpc01 24305 | Path homotopic paths have the same endpoints. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝐹( ≃ph‘𝐽)𝐺 → ((𝐹‘0) = (𝐺‘0) ∧ (𝐹‘1) = (𝐺‘1))) | ||
Theorem | reparphti 24306* | Lemma for reparpht 24307. (Contributed by NM, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn II)) & ⊢ (𝜑 → (𝐺‘0) = 0) & ⊢ (𝜑 → (𝐺‘1) = 1) & ⊢ 𝐻 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝐹‘(((1 − 𝑦) · (𝐺‘𝑥)) + (𝑦 · 𝑥)))) ⇒ ⊢ (𝜑 → 𝐻 ∈ ((𝐹 ∘ 𝐺)(PHtpy‘𝐽)𝐹)) | ||
Theorem | reparpht 24307 | Reparametrization lemma. The reparametrization of a path by any continuous map 𝐺:II⟶II with 𝐺(0) = 0 and 𝐺(1) = 1 is path-homotopic to the original path. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn II)) & ⊢ (𝜑 → (𝐺‘0) = 0) & ⊢ (𝜑 → (𝐺‘1) = 1) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺)( ≃ph‘𝐽)𝐹) | ||
Theorem | phtpcco2 24308 | Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 6-Jul-2015.) |
⊢ (𝜑 → 𝐹( ≃ph‘𝐽)𝐺) & ⊢ (𝜑 → 𝑃 ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → (𝑃 ∘ 𝐹)( ≃ph‘𝐾)(𝑃 ∘ 𝐺)) | ||
Syntax | cpco 24309 | Extend class notation with the concatenation operation for paths in a topological space. |
class *𝑝 | ||
Syntax | comi 24310 | Extend class notation with the loop space. |
class Ω1 | ||
Syntax | comn 24311 | Extend class notation with the higher loop spaces. |
class Ω𝑛 | ||
Syntax | cpi1 24312 | Extend class notation with the fundamental group. |
class π1 | ||
Syntax | cpin 24313 | Extend class notation with the higher homotopy groups. |
class πn | ||
Definition | df-pco 24314* | Define the concatenation of two paths in a topological space 𝐽. For simplicity of definition, we define it on all paths, not just those whose endpoints line up. Definition of [Hatcher] p. 26. Hatcher denotes path concatenation with a square dot; other authors, such as Munkres, use a star. (Contributed by Jeff Madsen, 15-Jun-2010.) |
⊢ *𝑝 = (𝑗 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))))) | ||
Definition | df-om1 24315* | Define the loop space of a topological space, with a magma structure on it given by concatenation of loops. This structure is not a group, but the operation is compatible with homotopy, which allows the homotopy groups to be defined based on this operation. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ Ω1 = (𝑗 ∈ Top, 𝑦 ∈ ∪ 𝑗 ↦ {〈(Base‘ndx), {𝑓 ∈ (II Cn 𝑗) ∣ ((𝑓‘0) = 𝑦 ∧ (𝑓‘1) = 𝑦)}〉, 〈(+g‘ndx), (*𝑝‘𝑗)〉, 〈(TopSet‘ndx), (𝑗 ↑ko II)〉}) | ||
Definition | df-omn 24316* | Define the n-th iterated loop space of a topological space. Unlike Ω1 this is actually a pointed topological space, which is to say a tuple of a topological space (a member of TopSp, not Top) and a point in the space. Higher loop spaces select the constant loop at the point from the lower loop space for the distinguished point. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ Ω𝑛 = (𝑗 ∈ Top, 𝑦 ∈ ∪ 𝑗 ↦ seq0(((𝑥 ∈ V, 𝑝 ∈ V ↦ 〈((TopOpen‘(1st ‘𝑥)) Ω1 (2nd ‘𝑥)), ((0[,]1) × {(2nd ‘𝑥)})〉) ∘ 1st ), 〈{〈(Base‘ndx), ∪ 𝑗〉, 〈(TopSet‘ndx), 𝑗〉}, 𝑦〉)) | ||
Definition | df-pi1 24317* | Define the fundamental group, whose operation is given by concatenation of homotopy classes of loops. Definition of [Hatcher] p. 26. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ π1 = (𝑗 ∈ Top, 𝑦 ∈ ∪ 𝑗 ↦ ((𝑗 Ω1 𝑦) /s ( ≃ph‘𝑗))) | ||
Definition | df-pin 24318* | Define the n-th homotopy group, which is formed by taking the 𝑛-th loop space and forming the quotient under the relation of path homotopy equivalence in the base space of the 𝑛-th loop space, which is the 𝑛 − 1-th loop space. For 𝑛 = 0, since this is not well-defined we replace this relation with the path-connectedness relation, so that the 0-th homotopy group is the set of path components of 𝑋. (Since the 0-th loop space does not have a group operation, neither does the 0-th homotopy group, but the rest are genuine groups.) (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ πn = (𝑗 ∈ Top, 𝑝 ∈ ∪ 𝑗 ↦ (𝑛 ∈ ℕ0 ↦ ((1st ‘((𝑗 Ω𝑛 𝑝)‘𝑛)) /s if(𝑛 = 0, {〈𝑥, 𝑦〉 ∣ ∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}, ( ≃ph‘(TopOpen‘(1st ‘((𝑗 Ω𝑛 𝑝)‘(𝑛 − 1))))))))) | ||
Theorem | pcofval 24319* | The value of the path concatenation function on a topological space. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.) (Proof shortened by AV, 2-Mar-2024.) |
⊢ (*𝑝‘𝐽) = (𝑓 ∈ (II Cn 𝐽), 𝑔 ∈ (II Cn 𝐽) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))) | ||
Theorem | pcoval 24320* | The concatenation of two paths. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) ⇒ ⊢ (𝜑 → (𝐹(*𝑝‘𝐽)𝐺) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝐹‘(2 · 𝑥)), (𝐺‘((2 · 𝑥) − 1))))) | ||
Theorem | pcovalg 24321 | Evaluate the concatenation of two paths. (Contributed by Mario Carneiro, 7-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ (0[,]1)) → ((𝐹(*𝑝‘𝐽)𝐺)‘𝑋) = if(𝑋 ≤ (1 / 2), (𝐹‘(2 · 𝑋)), (𝐺‘((2 · 𝑋) − 1)))) | ||
Theorem | pcoval1 24322 | Evaluate the concatenation of two paths on the first half. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ (0[,](1 / 2))) → ((𝐹(*𝑝‘𝐽)𝐺)‘𝑋) = (𝐹‘(2 · 𝑋))) | ||
Theorem | pco0 24323 | The starting point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) ⇒ ⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)‘0) = (𝐹‘0)) | ||
Theorem | pco1 24324 | The ending point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) ⇒ ⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)‘1) = (𝐺‘1)) | ||
Theorem | pcoval2 24325 | Evaluate the concatenation of two paths on the second half. (Contributed by Jeff Madsen, 15-Jun-2010.) (Proof shortened by Mario Carneiro, 7-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → (𝐹‘1) = (𝐺‘0)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ ((1 / 2)[,]1)) → ((𝐹(*𝑝‘𝐽)𝐺)‘𝑋) = (𝐺‘((2 · 𝑋) − 1))) | ||
Theorem | pcocn 24326 | The concatenation of two paths is a path. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof shortened by Mario Carneiro, 7-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → (𝐹‘1) = (𝐺‘0)) ⇒ ⊢ (𝜑 → (𝐹(*𝑝‘𝐽)𝐺) ∈ (II Cn 𝐽)) | ||
Theorem | copco 24327 | The composition of a concatenation of paths with a continuous function. (Contributed by Mario Carneiro, 9-Jul-2015.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → (𝐹‘1) = (𝐺‘0)) & ⊢ (𝜑 → 𝐻 ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → (𝐻 ∘ (𝐹(*𝑝‘𝐽)𝐺)) = ((𝐻 ∘ 𝐹)(*𝑝‘𝐾)(𝐻 ∘ 𝐺))) | ||
Theorem | pcohtpylem 24328* | Lemma for pcohtpy 24329. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝜑 → (𝐹‘1) = (𝐺‘0)) & ⊢ (𝜑 → 𝐹( ≃ph‘𝐽)𝐻) & ⊢ (𝜑 → 𝐺( ≃ph‘𝐽)𝐾) & ⊢ 𝑃 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), ((2 · 𝑥)𝑀𝑦), (((2 · 𝑥) − 1)𝑁𝑦))) & ⊢ (𝜑 → 𝑀 ∈ (𝐹(PHtpy‘𝐽)𝐻)) & ⊢ (𝜑 → 𝑁 ∈ (𝐺(PHtpy‘𝐽)𝐾)) ⇒ ⊢ (𝜑 → 𝑃 ∈ ((𝐹(*𝑝‘𝐽)𝐺)(PHtpy‘𝐽)(𝐻(*𝑝‘𝐽)𝐾))) | ||
Theorem | pcohtpy 24329 | Homotopy invariance of path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝜑 → (𝐹‘1) = (𝐺‘0)) & ⊢ (𝜑 → 𝐹( ≃ph‘𝐽)𝐻) & ⊢ (𝜑 → 𝐺( ≃ph‘𝐽)𝐾) ⇒ ⊢ (𝜑 → (𝐹(*𝑝‘𝐽)𝐺)( ≃ph‘𝐽)(𝐻(*𝑝‘𝐽)𝐾)) | ||
Theorem | pcoptcl 24330 | A constant function is a path from 𝑌 to itself. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝑃 = ((0[,]1) × {𝑌}) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑌 ∈ 𝑋) → (𝑃 ∈ (II Cn 𝐽) ∧ (𝑃‘0) = 𝑌 ∧ (𝑃‘1) = 𝑌)) | ||
Theorem | pcopt 24331 | Concatenation with a point does not affect homotopy class. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.) |
⊢ 𝑃 = ((0[,]1) × {𝑌}) ⇒ ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌) → (𝑃(*𝑝‘𝐽)𝐹)( ≃ph‘𝐽)𝐹) | ||
Theorem | pcopt2 24332 | Concatenation with a point does not affect homotopy class. (Contributed by Mario Carneiro, 12-Feb-2015.) |
⊢ 𝑃 = ((0[,]1) × {𝑌}) ⇒ ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘1) = 𝑌) → (𝐹(*𝑝‘𝐽)𝑃)( ≃ph‘𝐽)𝐹) | ||
Theorem | pcoass 24333* | Order of concatenation does not affect homotopy class. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof shortened by Mario Carneiro, 8-Jun-2014.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐻 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → (𝐹‘1) = (𝐺‘0)) & ⊢ (𝜑 → (𝐺‘1) = (𝐻‘0)) & ⊢ 𝑃 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), if(𝑥 ≤ (1 / 4), (2 · 𝑥), (𝑥 + (1 / 4))), ((𝑥 / 2) + (1 / 2)))) ⇒ ⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)(𝐹(*𝑝‘𝐽)(𝐺(*𝑝‘𝐽)𝐻))) | ||
Theorem | pcorevcl 24334* | Closure for a reversed path. (Contributed by Mario Carneiro, 12-Feb-2015.) |
⊢ 𝐺 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥))) ⇒ ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐺 ∈ (II Cn 𝐽) ∧ (𝐺‘0) = (𝐹‘1) ∧ (𝐺‘1) = (𝐹‘0))) | ||
Theorem | pcorevlem 24335* | Lemma for pcorev 24336. Prove continuity of the homotopy function. (Contributed by Jeff Madsen, 11-Jun-2010.) (Proof shortened by Mario Carneiro, 8-Jun-2014.) |
⊢ 𝐺 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥))) & ⊢ 𝑃 = ((0[,]1) × {(𝐹‘1)}) & ⊢ 𝐻 = (𝑠 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ (𝐹‘if(𝑠 ≤ (1 / 2), (1 − ((1 − 𝑡) · (2 · 𝑠))), (1 − ((1 − 𝑡) · (1 − ((2 · 𝑠) − 1))))))) ⇒ ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐻 ∈ ((𝐺(*𝑝‘𝐽)𝐹)(PHtpy‘𝐽)𝑃) ∧ (𝐺(*𝑝‘𝐽)𝐹)( ≃ph‘𝐽)𝑃)) | ||
Theorem | pcorev 24336* | Concatenation with the reverse path. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.) |
⊢ 𝐺 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥))) & ⊢ 𝑃 = ((0[,]1) × {(𝐹‘1)}) ⇒ ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐺(*𝑝‘𝐽)𝐹)( ≃ph‘𝐽)𝑃) | ||
Theorem | pcorev2 24337* | Concatenation with the reverse path. (Contributed by Mario Carneiro, 12-Feb-2015.) |
⊢ 𝐺 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥))) & ⊢ 𝑃 = ((0[,]1) × {(𝐹‘0)}) ⇒ ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐹(*𝑝‘𝐽)𝐺)( ≃ph‘𝐽)𝑃) | ||
Theorem | pcophtb 24338* | The path homotopy equivalence relation on two paths 𝐹, 𝐺 with the same start and end point can be written in terms of the loop 𝐹 − 𝐺 formed by concatenating 𝐹 with the inverse of 𝐺. Thus, all the homotopy information in ≃ph‘𝐽 is available if we restrict our attention to closed loops, as in the definition of the fundamental group. (Contributed by Mario Carneiro, 12-Feb-2015.) |
⊢ 𝐻 = (𝑥 ∈ (0[,]1) ↦ (𝐺‘(1 − 𝑥))) & ⊢ 𝑃 = ((0[,]1) × {(𝐹‘0)}) & ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → (𝐹‘0) = (𝐺‘0)) & ⊢ (𝜑 → (𝐹‘1) = (𝐺‘1)) ⇒ ⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐻)( ≃ph‘𝐽)𝑃 ↔ 𝐹( ≃ph‘𝐽)𝐺)) | ||
Theorem | om1val 24339* | The definition of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝑂 = (𝐽 Ω1 𝑌) & ⊢ (𝜑 → 𝐵 = {𝑓 ∈ (II Cn 𝐽) ∣ ((𝑓‘0) = 𝑌 ∧ (𝑓‘1) = 𝑌)}) & ⊢ (𝜑 → + = (*𝑝‘𝐽)) & ⊢ (𝜑 → 𝐾 = (𝐽 ↑ko II)) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝑂 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(TopSet‘ndx), 𝐾〉}) | ||
Theorem | om1bas 24340* | The base set of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝑂 = (𝐽 Ω1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 = (Base‘𝑂)) ⇒ ⊢ (𝜑 → 𝐵 = {𝑓 ∈ (II Cn 𝐽) ∣ ((𝑓‘0) = 𝑌 ∧ (𝑓‘1) = 𝑌)}) | ||
Theorem | om1elbas 24341 | Elementhood in the base set of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝑂 = (𝐽 Ω1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 = (Base‘𝑂)) ⇒ ⊢ (𝜑 → (𝐹 ∈ 𝐵 ↔ (𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌 ∧ (𝐹‘1) = 𝑌))) | ||
Theorem | om1addcl 24342 | Closure of the group operation of the loop space. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 5-Sep-2015.) |
⊢ 𝑂 = (𝐽 Ω1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 = (Base‘𝑂)) & ⊢ (𝜑 → 𝐻 ∈ 𝐵) & ⊢ (𝜑 → 𝐾 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐻(*𝑝‘𝐽)𝐾) ∈ 𝐵) | ||
Theorem | om1plusg 24343 | The group operation (which isn't much more than a magma) of the loop space. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝑂 = (𝐽 Ω1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) ⇒ ⊢ (𝜑 → (*𝑝‘𝐽) = (+g‘𝑂)) | ||
Theorem | om1tset 24344 | The topology of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝑂 = (𝐽 Ω1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐽 ↑ko II) = (TopSet‘𝑂)) | ||
Theorem | om1opn 24345 | The topology of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝑂 = (𝐽 Ω1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ 𝐾 = (TopOpen‘𝑂) & ⊢ (𝜑 → 𝐵 = (Base‘𝑂)) ⇒ ⊢ (𝜑 → 𝐾 = ((𝐽 ↑ko II) ↾t 𝐵)) | ||
Theorem | pi1val 24346 | The definition of the fundamental group. (Contributed by Mario Carneiro, 11-Feb-2015.) (Revised by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ 𝑂 = (𝐽 Ω1 𝑌) ⇒ ⊢ (𝜑 → 𝐺 = (𝑂 /s ( ≃ph‘𝐽))) | ||
Theorem | pi1bas 24347 | The base set of the fundamental group of a topological space at a given base point. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ 𝑂 = (𝐽 Ω1 𝑌) & ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → 𝐾 = (Base‘𝑂)) ⇒ ⊢ (𝜑 → 𝐵 = (𝐾 / ( ≃ph‘𝐽))) | ||
Theorem | pi1blem 24348 | Lemma for pi1buni 24349. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ 𝑂 = (𝐽 Ω1 𝑌) & ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → 𝐾 = (Base‘𝑂)) ⇒ ⊢ (𝜑 → ((( ≃ph‘𝐽) “ 𝐾) ⊆ 𝐾 ∧ 𝐾 ⊆ (II Cn 𝐽))) | ||
Theorem | pi1buni 24349 | Another way to write the loop space base in terms of the base of the fundamental group. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ 𝑂 = (𝐽 Ω1 𝑌) & ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → 𝐾 = (Base‘𝑂)) ⇒ ⊢ (𝜑 → ∪ 𝐵 = 𝐾) | ||
Theorem | pi1bas2 24350 | The base set of the fundamental group, written self-referentially. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) ⇒ ⊢ (𝜑 → 𝐵 = (∪ 𝐵 / ( ≃ph‘𝐽))) | ||
Theorem | pi1eluni 24351 | Elementhood in the base set of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) ⇒ ⊢ (𝜑 → (𝐹 ∈ ∪ 𝐵 ↔ (𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = 𝑌 ∧ (𝐹‘1) = 𝑌))) | ||
Theorem | pi1bas3 24352 | The base set of the fundamental group. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ 𝑅 = (( ≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵)) ⇒ ⊢ (𝜑 → 𝐵 = (∪ 𝐵 / 𝑅)) | ||
Theorem | pi1cpbl 24353 | The group operation, loop concatenation, is compatible with homotopy equivalence. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ 𝑅 = (( ≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵)) & ⊢ 𝑂 = (𝐽 Ω1 𝑌) & ⊢ + = (+g‘𝑂) ⇒ ⊢ (𝜑 → ((𝑀𝑅𝑁 ∧ 𝑃𝑅𝑄) → (𝑀 + 𝑃)𝑅(𝑁 + 𝑄))) | ||
Theorem | elpi1 24354* | The elements of the fundamental group. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐹 ∈ 𝐵 ↔ ∃𝑓 ∈ (II Cn 𝐽)(((𝑓‘0) = 𝑌 ∧ (𝑓‘1) = 𝑌) ∧ 𝐹 = [𝑓]( ≃ph‘𝐽)))) | ||
Theorem | elpi1i 24355 | The elements of the fundamental group. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → (𝐹‘0) = 𝑌) & ⊢ (𝜑 → (𝐹‘1) = 𝑌) ⇒ ⊢ (𝜑 → [𝐹]( ≃ph‘𝐽) ∈ 𝐵) | ||
Theorem | pi1addf 24356 | The group operation of π1 is a binary operation. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝜑 → + :(𝐵 × 𝐵)⟶𝐵) | ||
Theorem | pi1addval 24357 | The concatenation of two path-homotopy classes in the fundamental group. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝑀 ∈ ∪ 𝐵) & ⊢ (𝜑 → 𝑁 ∈ ∪ 𝐵) ⇒ ⊢ (𝜑 → ([𝑀]( ≃ph‘𝐽) + [𝑁]( ≃ph‘𝐽)) = [(𝑀(*𝑝‘𝐽)𝑁)]( ≃ph‘𝐽)) | ||
Theorem | pi1grplem 24358 | Lemma for pi1grp 24359. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 10-Aug-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ 0 = ((0[,]1) × {𝑌}) ⇒ ⊢ (𝜑 → (𝐺 ∈ Grp ∧ [ 0 ]( ≃ph‘𝐽) = (0g‘𝐺))) | ||
Theorem | pi1grp 24359 | The fundamental group is a group. Proposition 1.3 of [Hatcher] p. 26. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof shortened by Mario Carneiro, 8-Jun-2014.) (Revised by Mario Carneiro, 10-Aug-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑌 ∈ 𝑋) → 𝐺 ∈ Grp) | ||
Theorem | pi1id 24360 | The identity element of the fundamental group. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 10-Aug-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ 0 = ((0[,]1) × {𝑌}) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑌 ∈ 𝑋) → [ 0 ]( ≃ph‘𝐽) = (0g‘𝐺)) | ||
Theorem | pi1inv 24361* | An inverse in the fundamental group. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 10-Aug-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → (𝐹‘0) = 𝑌) & ⊢ (𝜑 → (𝐹‘1) = 𝑌) & ⊢ 𝐼 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥))) ⇒ ⊢ (𝜑 → (𝑁‘[𝐹]( ≃ph‘𝐽)) = [𝐼]( ≃ph‘𝐽)) | ||
Theorem | pi1xfrf 24362* | Functionality of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝑃 = (𝐽 π1 (𝐹‘0)) & ⊢ 𝑄 = (𝐽 π1 (𝐹‘1)) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝐵 ↦ 〈[𝑔]( ≃ph‘𝐽), [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)〉) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐼 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → (𝐹‘1) = (𝐼‘0)) & ⊢ (𝜑 → (𝐼‘1) = (𝐹‘0)) ⇒ ⊢ (𝜑 → 𝐺:𝐵⟶(Base‘𝑄)) | ||
Theorem | pi1xfrval 24363* | The value of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝑃 = (𝐽 π1 (𝐹‘0)) & ⊢ 𝑄 = (𝐽 π1 (𝐹‘1)) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝐵 ↦ 〈[𝑔]( ≃ph‘𝐽), [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)〉) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐼 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → (𝐹‘1) = (𝐼‘0)) & ⊢ (𝜑 → (𝐼‘1) = (𝐹‘0)) & ⊢ (𝜑 → 𝐴 ∈ ∪ 𝐵) ⇒ ⊢ (𝜑 → (𝐺‘[𝐴]( ≃ph‘𝐽)) = [(𝐼(*𝑝‘𝐽)(𝐴(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)) | ||
Theorem | pi1xfr 24364* | Given a path 𝐹 and its inverse 𝐼 between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015.) |
⊢ 𝑃 = (𝐽 π1 (𝐹‘0)) & ⊢ 𝑄 = (𝐽 π1 (𝐹‘1)) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝐵 ↦ 〈[𝑔]( ≃ph‘𝐽), [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)〉) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ 𝐼 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥))) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝑃 GrpHom 𝑄)) | ||
Theorem | pi1xfrcnvlem 24365* | Given a path 𝐹 between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝑃 = (𝐽 π1 (𝐹‘0)) & ⊢ 𝑄 = (𝐽 π1 (𝐹‘1)) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝐵 ↦ 〈[𝑔]( ≃ph‘𝐽), [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)〉) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ 𝐼 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥))) & ⊢ 𝐻 = ran (ℎ ∈ ∪ (Base‘𝑄) ↦ 〈[ℎ]( ≃ph‘𝐽), [(𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉) ⇒ ⊢ (𝜑 → ◡𝐺 ⊆ 𝐻) | ||
Theorem | pi1xfrcnv 24366* | Given a path 𝐹 between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝑃 = (𝐽 π1 (𝐹‘0)) & ⊢ 𝑄 = (𝐽 π1 (𝐹‘1)) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝐵 ↦ 〈[𝑔]( ≃ph‘𝐽), [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)〉) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ 𝐼 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥))) & ⊢ 𝐻 = ran (ℎ ∈ ∪ (Base‘𝑄) ↦ 〈[ℎ]( ≃ph‘𝐽), [(𝐹(*𝑝‘𝐽)(ℎ(*𝑝‘𝐽)𝐼))]( ≃ph‘𝐽)〉) ⇒ ⊢ (𝜑 → (◡𝐺 = 𝐻 ∧ ◡𝐺 ∈ (𝑄 GrpHom 𝑃))) | ||
Theorem | pi1xfrgim 24367* | The mapping 𝐺 between fundamental groups is an isomorphism. (Contributed by Mario Carneiro, 12-Feb-2015.) |
⊢ 𝑃 = (𝐽 π1 (𝐹‘0)) & ⊢ 𝑄 = (𝐽 π1 (𝐹‘1)) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝐵 ↦ 〈[𝑔]( ≃ph‘𝐽), [(𝐼(*𝑝‘𝐽)(𝑔(*𝑝‘𝐽)𝐹))]( ≃ph‘𝐽)〉) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ 𝐼 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥))) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝑃 GrpIso 𝑄)) | ||
Theorem | pi1cof 24368* | Functionality of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝑃 = (𝐽 π1 𝐴) & ⊢ 𝑄 = (𝐾 π1 𝐵) & ⊢ 𝑉 = (Base‘𝑃) & ⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝑉 ↦ 〈[𝑔]( ≃ph‘𝐽), [(𝐹 ∘ 𝑔)]( ≃ph‘𝐾)〉) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → (𝐹‘𝐴) = 𝐵) ⇒ ⊢ (𝜑 → 𝐺:𝑉⟶(Base‘𝑄)) | ||
Theorem | pi1coval 24369* | The value of the loop transfer function on the equivalence class of a path. (Contributed by Mario Carneiro, 10-Aug-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝑃 = (𝐽 π1 𝐴) & ⊢ 𝑄 = (𝐾 π1 𝐵) & ⊢ 𝑉 = (Base‘𝑃) & ⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝑉 ↦ 〈[𝑔]( ≃ph‘𝐽), [(𝐹 ∘ 𝑔)]( ≃ph‘𝐾)〉) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → (𝐹‘𝐴) = 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝑇 ∈ ∪ 𝑉) → (𝐺‘[𝑇]( ≃ph‘𝐽)) = [(𝐹 ∘ 𝑇)]( ≃ph‘𝐾)) | ||
Theorem | pi1coghm 24370* | The mapping 𝐺 between fundamental groups is a group homomorphism. (Contributed by Mario Carneiro, 10-Aug-2015.) (Revised by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝑃 = (𝐽 π1 𝐴) & ⊢ 𝑄 = (𝐾 π1 𝐵) & ⊢ 𝑉 = (Base‘𝑃) & ⊢ 𝐺 = ran (𝑔 ∈ ∪ 𝑉 ↦ 〈[𝑔]( ≃ph‘𝐽), [(𝐹 ∘ 𝑔)]( ≃ph‘𝐾)〉) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → (𝐹‘𝐴) = 𝐵) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝑃 GrpHom 𝑄)) | ||
Syntax | cclm 24371 | Syntax for the class of subcomplex modules. |
class ℂMod | ||
Definition | df-clm 24372* | Define the class of subcomplex modules, which are left modules over a subring of the field of complex numbers ℂfld, which allows to use the complex addition, multiplication, etc. in theorems about subcomplex modules. Since the field of complex numbers is commutative and so are its subrings (see subrgcrng 20173), left modules over such subrings are the same as right modules, see rmodislmod 20337. Therefore, we drop the word "left" from "subcomplex left module". (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ ℂMod = {𝑤 ∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ 𝑘 ∈ (SubRing‘ℂfld))} | ||
Theorem | isclm 24373 | A subcomplex module is a left module over a subring of the field of complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂMod ↔ (𝑊 ∈ LMod ∧ 𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 ∈ (SubRing‘ℂfld))) | ||
Theorem | clmsca 24374 | The ring of scalars 𝐹 of a subcomplex module is the restriction of the field of complex numbers to the base set of 𝐹. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂMod → 𝐹 = (ℂfld ↾s 𝐾)) | ||
Theorem | clmsubrg 24375 | The base set of the ring of scalars of a subcomplex module is the base set of a subring of the field of complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂMod → 𝐾 ∈ (SubRing‘ℂfld)) | ||
Theorem | clmlmod 24376 | A subcomplex module is a left module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ LMod) | ||
Theorem | clmgrp 24377 | A subcomplex module is an additive group. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ Grp) | ||
Theorem | clmabl 24378 | A subcomplex module is an abelian group. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ Abel) | ||
Theorem | clmring 24379 | The scalar ring of a subcomplex module is a ring. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → 𝐹 ∈ Ring) | ||
Theorem | clmfgrp 24380 | The scalar ring of a subcomplex module is a group. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → 𝐹 ∈ Grp) | ||
Theorem | clm0 24381 | The zero of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → 0 = (0g‘𝐹)) | ||
Theorem | clm1 24382 | The identity of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → 1 = (1r‘𝐹)) | ||
Theorem | clmadd 24383 | The addition of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → + = (+g‘𝐹)) | ||
Theorem | clmmul 24384 | The multiplication of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → · = (.r‘𝐹)) | ||
Theorem | clmcj 24385 | The conjugation of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → ∗ = (*𝑟‘𝐹)) | ||
Theorem | isclmi 24386 | Reverse direction of isclm 24373. (Contributed by Mario Carneiro, 30-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 ∈ (SubRing‘ℂfld)) → 𝑊 ∈ ℂMod) | ||
Theorem | clmzss 24387 | The scalar ring of a subcomplex module contains the integers. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂMod → ℤ ⊆ 𝐾) | ||
Theorem | clmsscn 24388 | The scalar ring of a subcomplex module is a subset of the complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂMod → 𝐾 ⊆ ℂ) | ||
Theorem | clmsub 24389 | Subtraction in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾) → (𝐴 − 𝐵) = (𝐴(-g‘𝐹)𝐵)) | ||
Theorem | clmneg 24390 | Negation in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾) → -𝐴 = ((invg‘𝐹)‘𝐴)) | ||
Theorem | clmneg1 24391 | Minus one is in the scalar ring of a subcomplex module. (Contributed by AV, 28-Sep-2021.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂMod → -1 ∈ 𝐾) | ||
Theorem | clmabs 24392 | Norm in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾) → (abs‘𝐴) = ((norm‘𝐹)‘𝐴)) | ||
Theorem | clmacl 24393 | Closure of ring addition for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 + 𝑌) ∈ 𝐾) | ||
Theorem | clmmcl 24394 | Closure of ring multiplication for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 · 𝑌) ∈ 𝐾) | ||
Theorem | clmsubcl 24395 | Closure of ring subtraction for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 − 𝑌) ∈ 𝐾) | ||
Theorem | lmhmclm 24396 | The domain of a linear operator is a subcomplex module iff the range is. (Contributed by Mario Carneiro, 21-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝑆 ∈ ℂMod ↔ 𝑇 ∈ ℂMod)) | ||
Theorem | clmvscl 24397 | Closure of scalar product for a subcomplex module. Analogue of lmodvscl 20286. (Contributed by NM, 3-Nov-2006.) (Revised by AV, 28-Sep-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑄 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑄 · 𝑋) ∈ 𝑉) | ||
Theorem | clmvsass 24398 | Associative law for scalar product. Analogue of lmodvsass 20294. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 · 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋))) | ||
Theorem | clmvscom 24399 | Commutative law for the scalar product. (Contributed by NM, 14-Feb-2008.) (Revised by AV, 7-Oct-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → (𝑄 · (𝑅 · 𝑋)) = (𝑅 · (𝑄 · 𝑋))) | ||
Theorem | clmvsdir 24400 | Distributive law for scalar product (right-distributivity). (lmodvsdir 20293 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 + 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |