![]() |
Metamath
Proof Explorer Theorem List (p. 233 of 437) | < 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-28351) |
![]() (28352-29876) |
![]() (29877-43667) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | phtpyco2 23201 | Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝑃 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺)) ⇒ ⊢ (𝜑 → (𝑃 ∘ 𝐻) ∈ ((𝑃 ∘ 𝐹)(PHtpy‘𝐾)(𝑃 ∘ 𝐺))) | ||
Theorem | phtpycc 23202* | Concatenate two path homotopies. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 7-Jun-2014.) |
⊢ 𝑀 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), (𝑥𝐾(2 · 𝑦)), (𝑥𝐿((2 · 𝑦) − 1)))) & ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐻 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐾 ∈ (𝐹(PHtpy‘𝐽)𝐺)) & ⊢ (𝜑 → 𝐿 ∈ (𝐺(PHtpy‘𝐽)𝐻)) ⇒ ⊢ (𝜑 → 𝑀 ∈ (𝐹(PHtpy‘𝐽)𝐻)) | ||
Definition | df-phtpc 23203* | 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 23204 | 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 23205 | 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 23206 | 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 23207 | Path homotopic paths have the same endpoints. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝐹( ≃ph‘𝐽)𝐺 → ((𝐹‘0) = (𝐺‘0) ∧ (𝐹‘1) = (𝐺‘1))) | ||
Theorem | reparphti 23208* | Lemma for reparpht 23209. (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 23209 | 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 23210 | Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 6-Jul-2015.) |
⊢ (𝜑 → 𝐹( ≃ph‘𝐽)𝐺) & ⊢ (𝜑 → 𝑃 ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → (𝑃 ∘ 𝐹)( ≃ph‘𝐾)(𝑃 ∘ 𝐺)) | ||
Syntax | cpco 23211 | Extend class notation with the concatenation operation for paths in a topological space. |
class *𝑝 | ||
Syntax | comi 23212 | Extend class notation with the loop space. |
class Ω1 | ||
Syntax | comn 23213 | Extend class notation with the higher loop spaces. |
class Ω𝑛 | ||
Syntax | cpi1 23214 | Extend class notation with the fundamental group. |
class π1 | ||
Syntax | cpin 23215 | Extend class notation with the higher homotopy groups. |
class πn | ||
Definition | df-pco 23216* | 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 23217* | 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 23218* | 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 23219* | 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 23220* | 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 23221* | 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.) |
⊢ (*𝑝‘𝐽) = (𝑓 ∈ (II Cn 𝐽), 𝑔 ∈ (II Cn 𝐽) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))) | ||
Theorem | pcoval 23222* | 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 23223 | 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 23224 | 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 23225 | The starting point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) ⇒ ⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)‘0) = (𝐹‘0)) | ||
Theorem | pco1 23226 | The ending point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) ⇒ ⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)‘1) = (𝐺‘1)) | ||
Theorem | pcoval2 23227 | 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 23228 | 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 23229 | 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 23230* | Lemma for pcohtpy 23231. (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 23231 | 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 23232 | 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 23233 | 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 23234 | Concatenation with a point does not affect homotopy class. (Contributed by Mario Carneiro, 12-Feb-2015.) |
⊢ 𝑃 = ((0[,]1) × {𝑌}) ⇒ ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘1) = 𝑌) → (𝐹(*𝑝‘𝐽)𝑃)( ≃ph‘𝐽)𝐹) | ||
Theorem | pcoass 23235* | 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 23236* | 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 23237* | Lemma for pcorev 23238. 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 23238* | 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 23239* | Concatenation with the reverse path. (Contributed by Mario Carneiro, 12-Feb-2015.) |
⊢ 𝐺 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥))) & ⊢ 𝑃 = ((0[,]1) × {(𝐹‘0)}) ⇒ ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐹(*𝑝‘𝐽)𝐺)( ≃ph‘𝐽)𝑃) | ||
Theorem | pcophtb 23240* | 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 23241* | 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 23242* | The base set of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝑂 = (𝐽 Ω1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 = (Base‘𝑂)) ⇒ ⊢ (𝜑 → 𝐵 = {𝑓 ∈ (II Cn 𝐽) ∣ ((𝑓‘0) = 𝑌 ∧ (𝑓‘1) = 𝑌)}) | ||
Theorem | om1elbas 23243 | 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 23244 | 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 23245 | 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 23246 | The topology of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝑂 = (𝐽 Ω1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐽 ^ko II) = (TopSet‘𝑂)) | ||
Theorem | om1opn 23247 | The topology of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝑂 = (𝐽 Ω1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ 𝐾 = (TopOpen‘𝑂) & ⊢ (𝜑 → 𝐵 = (Base‘𝑂)) ⇒ ⊢ (𝜑 → 𝐾 = ((𝐽 ^ko II) ↾t 𝐵)) | ||
Theorem | pi1val 23248 | 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 23249 | 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 23250 | Lemma for pi1buni 23251. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ 𝑂 = (𝐽 Ω1 𝑌) & ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → 𝐾 = (Base‘𝑂)) ⇒ ⊢ (𝜑 → ((( ≃ph‘𝐽) “ 𝐾) ⊆ 𝐾 ∧ 𝐾 ⊆ (II Cn 𝐽))) | ||
Theorem | pi1buni 23251 | 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 23252 | The base set of the fundamental group, written self-referentially. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) ⇒ ⊢ (𝜑 → 𝐵 = (∪ 𝐵 / ( ≃ph‘𝐽))) | ||
Theorem | pi1eluni 23253 | 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 23254 | The base set of the fundamental group. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ 𝑅 = (( ≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵)) ⇒ ⊢ (𝜑 → 𝐵 = (∪ 𝐵 / 𝑅)) | ||
Theorem | pi1cpbl 23255 | 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 23256* | 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 23257 | 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 23258 | 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 23259 | 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 23260 | Lemma for pi1grp 23261. (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 23261 | 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 23262 | 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 23263* | 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 23264* | 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 23265* | 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 23266* | 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 23267* | 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 23268* | 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 23269* | 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 23270* | 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 23271* | 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 23272* | 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 23273 | Syntax for the class of subcomplex modules. |
class ℂMod | ||
Definition | df-clm 23274* | Define the class of subcomplex modules, which are left modules over a subring of the field of complex numbers ℂfld, which allows us 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 19180), left modules over such subrings are the same as right modules, see rmodislmod 19327. 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 23275 | 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 23276 | 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 23277 | 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 23278 | A subcomplex module is a left module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ LMod) | ||
Theorem | clmgrp 23279 | A subcomplex module is an additive group. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ Grp) | ||
Theorem | clmabl 23280 | A subcomplex module is an abelian group. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ Abel) | ||
Theorem | clmring 23281 | The scalar ring of a subcomplex module is a ring. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → 𝐹 ∈ Ring) | ||
Theorem | clmfgrp 23282 | The scalar ring of a subcomplex module is a group. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → 𝐹 ∈ Grp) | ||
Theorem | clm0 23283 | The zero of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → 0 = (0g‘𝐹)) | ||
Theorem | clm1 23284 | The identity of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → 1 = (1r‘𝐹)) | ||
Theorem | clmadd 23285 | The addition of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → + = (+g‘𝐹)) | ||
Theorem | clmmul 23286 | The multiplication of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → · = (.r‘𝐹)) | ||
Theorem | clmcj 23287 | The conjugation of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → ∗ = (*𝑟‘𝐹)) | ||
Theorem | isclmi 23288 | Reverse direction of isclm 23275. (Contributed by Mario Carneiro, 30-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 ∈ (SubRing‘ℂfld)) → 𝑊 ∈ ℂMod) | ||
Theorem | clmzss 23289 | The scalar ring of a subcomplex module contains the integers. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂMod → ℤ ⊆ 𝐾) | ||
Theorem | clmsscn 23290 | 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 23291 | Subtraction in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾) → (𝐴 − 𝐵) = (𝐴(-g‘𝐹)𝐵)) | ||
Theorem | clmneg 23292 | Negation in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾) → -𝐴 = ((invg‘𝐹)‘𝐴)) | ||
Theorem | clmneg1 23293 | Minus one is in the scalar ring of a subcomplex module. (Contributed by AV, 28-Sep-2021.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂMod → -1 ∈ 𝐾) | ||
Theorem | clmabs 23294 | Norm in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾) → (abs‘𝐴) = ((norm‘𝐹)‘𝐴)) | ||
Theorem | clmacl 23295 | Closure of ring addition for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 + 𝑌) ∈ 𝐾) | ||
Theorem | clmmcl 23296 | Closure of ring multiplication for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 · 𝑌) ∈ 𝐾) | ||
Theorem | clmsubcl 23297 | Closure of ring subtraction for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 − 𝑌) ∈ 𝐾) | ||
Theorem | lmhmclm 23298 | 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 23299 | Closure of scalar product for a subcomplex module. Analogue of lmodvscl 19276. (Contributed by NM, 3-Nov-2006.) (Revised by AV, 28-Sep-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑄 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑄 · 𝑋) ∈ 𝑉) | ||
Theorem | clmvsass 23300 | Associative law for scalar product. Analogue of lmodvsass 19284. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 · 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |