Home | Metamath
Proof Explorer Theorem List (p. 237 of 450) | < 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: | Metamath Proof Explorer
(1-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | reparphti 23601* | Lemma for reparpht 23602. (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 23602 | 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 23603 | Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 6-Jul-2015.) |
⊢ (𝜑 → 𝐹( ≃ph‘𝐽)𝐺) & ⊢ (𝜑 → 𝑃 ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → (𝑃 ∘ 𝐹)( ≃ph‘𝐾)(𝑃 ∘ 𝐺)) | ||
Syntax | cpco 23604 | Extend class notation with the concatenation operation for paths in a topological space. |
class *𝑝 | ||
Syntax | comi 23605 | Extend class notation with the loop space. |
class Ω1 | ||
Syntax | comn 23606 | Extend class notation with the higher loop spaces. |
class Ω𝑛 | ||
Syntax | cpi1 23607 | Extend class notation with the fundamental group. |
class π1 | ||
Syntax | cpin 23608 | Extend class notation with the higher homotopy groups. |
class πn | ||
Definition | df-pco 23609* | 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 23610* | 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 23611* | 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 23612* | 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 23613* | 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 23614* | 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 23615* | 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 23616 | 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 23617 | 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 23618 | The starting point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) ⇒ ⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)‘0) = (𝐹‘0)) | ||
Theorem | pco1 23619 | The ending point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) ⇒ ⊢ (𝜑 → ((𝐹(*𝑝‘𝐽)𝐺)‘1) = (𝐺‘1)) | ||
Theorem | pcoval2 23620 | 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 23621 | 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 23622 | 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 23623* | Lemma for pcohtpy 23624. (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 23624 | 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 23625 | 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 23626 | 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 23627 | Concatenation with a point does not affect homotopy class. (Contributed by Mario Carneiro, 12-Feb-2015.) |
⊢ 𝑃 = ((0[,]1) × {𝑌}) ⇒ ⊢ ((𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘1) = 𝑌) → (𝐹(*𝑝‘𝐽)𝑃)( ≃ph‘𝐽)𝐹) | ||
Theorem | pcoass 23628* | 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 23629* | 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 23630* | Lemma for pcorev 23631. 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 23631* | 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 23632* | Concatenation with the reverse path. (Contributed by Mario Carneiro, 12-Feb-2015.) |
⊢ 𝐺 = (𝑥 ∈ (0[,]1) ↦ (𝐹‘(1 − 𝑥))) & ⊢ 𝑃 = ((0[,]1) × {(𝐹‘0)}) ⇒ ⊢ (𝐹 ∈ (II Cn 𝐽) → (𝐹(*𝑝‘𝐽)𝐺)( ≃ph‘𝐽)𝑃) | ||
Theorem | pcophtb 23633* | 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 23634* | 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 23635* | The base set of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝑂 = (𝐽 Ω1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 = (Base‘𝑂)) ⇒ ⊢ (𝜑 → 𝐵 = {𝑓 ∈ (II Cn 𝐽) ∣ ((𝑓‘0) = 𝑌 ∧ (𝑓‘1) = 𝑌)}) | ||
Theorem | om1elbas 23636 | 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 23637 | 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 23638 | 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 23639 | The topology of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝑂 = (𝐽 Ω1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐽 ↑ko II) = (TopSet‘𝑂)) | ||
Theorem | om1opn 23640 | The topology of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝑂 = (𝐽 Ω1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ 𝐾 = (TopOpen‘𝑂) & ⊢ (𝜑 → 𝐵 = (Base‘𝑂)) ⇒ ⊢ (𝜑 → 𝐾 = ((𝐽 ↑ko II) ↾t 𝐵)) | ||
Theorem | pi1val 23641 | 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 23642 | 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 23643 | Lemma for pi1buni 23644. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ 𝑂 = (𝐽 Ω1 𝑌) & ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → 𝐾 = (Base‘𝑂)) ⇒ ⊢ (𝜑 → ((( ≃ph‘𝐽) “ 𝐾) ⊆ 𝐾 ∧ 𝐾 ⊆ (II Cn 𝐽))) | ||
Theorem | pi1buni 23644 | 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 23645 | The base set of the fundamental group, written self-referentially. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) ⇒ ⊢ (𝜑 → 𝐵 = (∪ 𝐵 / ( ≃ph‘𝐽))) | ||
Theorem | pi1eluni 23646 | 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 23647 | The base set of the fundamental group. (Contributed by Mario Carneiro, 10-Jul-2015.) |
⊢ 𝐺 = (𝐽 π1 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ 𝑅 = (( ≃ph‘𝐽) ∩ (∪ 𝐵 × ∪ 𝐵)) ⇒ ⊢ (𝜑 → 𝐵 = (∪ 𝐵 / 𝑅)) | ||
Theorem | pi1cpbl 23648 | 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 23649* | 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 23650 | 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 23651 | 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 23652 | 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 23653 | Lemma for pi1grp 23654. (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 23654 | 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 23655 | 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 23656* | 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 23657* | 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 23658* | 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 23659* | 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 23660* | 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 23661* | 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 23662* | 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 23663* | 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 23664* | 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 23665* | 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 23666 | Syntax for the class of subcomplex modules. |
class ℂMod | ||
Definition | df-clm 23667* | 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 19539), left modules over such subrings are the same as right modules, see rmodislmod 19702. 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 23668 | 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 23669 | 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 23670 | 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 23671 | A subcomplex module is a left module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ LMod) | ||
Theorem | clmgrp 23672 | A subcomplex module is an additive group. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ Grp) | ||
Theorem | clmabl 23673 | A subcomplex module is an abelian group. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ Abel) | ||
Theorem | clmring 23674 | The scalar ring of a subcomplex module is a ring. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → 𝐹 ∈ Ring) | ||
Theorem | clmfgrp 23675 | The scalar ring of a subcomplex module is a group. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → 𝐹 ∈ Grp) | ||
Theorem | clm0 23676 | The zero of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → 0 = (0g‘𝐹)) | ||
Theorem | clm1 23677 | The identity of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → 1 = (1r‘𝐹)) | ||
Theorem | clmadd 23678 | The addition of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → + = (+g‘𝐹)) | ||
Theorem | clmmul 23679 | The multiplication of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → · = (.r‘𝐹)) | ||
Theorem | clmcj 23680 | The conjugation of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → ∗ = (*𝑟‘𝐹)) | ||
Theorem | isclmi 23681 | Reverse direction of isclm 23668. (Contributed by Mario Carneiro, 30-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐹 = (ℂfld ↾s 𝐾) ∧ 𝐾 ∈ (SubRing‘ℂfld)) → 𝑊 ∈ ℂMod) | ||
Theorem | clmzss 23682 | The scalar ring of a subcomplex module contains the integers. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂMod → ℤ ⊆ 𝐾) | ||
Theorem | clmsscn 23683 | 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 23684 | Subtraction in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾) → (𝐴 − 𝐵) = (𝐴(-g‘𝐹)𝐵)) | ||
Theorem | clmneg 23685 | Negation in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾) → -𝐴 = ((invg‘𝐹)‘𝐴)) | ||
Theorem | clmneg1 23686 | Minus one is in the scalar ring of a subcomplex module. (Contributed by AV, 28-Sep-2021.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂMod → -1 ∈ 𝐾) | ||
Theorem | clmabs 23687 | Norm in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾) → (abs‘𝐴) = ((norm‘𝐹)‘𝐴)) | ||
Theorem | clmacl 23688 | Closure of ring addition for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 + 𝑌) ∈ 𝐾) | ||
Theorem | clmmcl 23689 | Closure of ring multiplication for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 · 𝑌) ∈ 𝐾) | ||
Theorem | clmsubcl 23690 | Closure of ring subtraction for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑋 − 𝑌) ∈ 𝐾) | ||
Theorem | lmhmclm 23691 | 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 23692 | Closure of scalar product for a subcomplex module. Analogue of lmodvscl 19651. (Contributed by NM, 3-Nov-2006.) (Revised by AV, 28-Sep-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑄 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑄 · 𝑋) ∈ 𝑉) | ||
Theorem | clmvsass 23693 | Associative law for scalar product. Analogue of lmodvsass 19659. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 · 𝑅) · 𝑋) = (𝑄 · (𝑅 · 𝑋))) | ||
Theorem | clmvscom 23694 | Commutative law for the scalar product. (Contributed by NM, 14-Feb-2008.) (Revised by AV, 7-Oct-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → (𝑄 · (𝑅 · 𝑋)) = (𝑅 · (𝑄 · 𝑋))) | ||
Theorem | clmvsdir 23695 | Distributive law for scalar product (right-distributivity). (lmodvsdir 19658 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ (𝑄 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑄 + 𝑅) · 𝑋) = ((𝑄 · 𝑋) + (𝑅 · 𝑋))) | ||
Theorem | clmvsdi 23696 | Distributive law for scalar product (left-distributivity). (lmodvsdi 19657 analog.) (Contributed by NM, 3-Nov-2006.) (Revised by AV, 28-Sep-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ (𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝐴 · (𝑋 + 𝑌)) = ((𝐴 · 𝑋) + (𝐴 · 𝑌))) | ||
Theorem | clmvs1 23697 | Scalar product with ring unit. (lmodvs1 19662 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉) → (1 · 𝑋) = 𝑋) | ||
Theorem | clmvs2 23698 | A vector plus itself is two times the vector. (Contributed by NM, 1-Feb-2007.) (Revised by AV, 21-Sep-2021.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉) → (𝐴 + 𝐴) = (2 · 𝐴)) | ||
Theorem | clm0vs 23699 | Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (lmod0vs 19667 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉) → (0 · 𝑋) = 0 ) | ||
Theorem | clmopfne 23700 | The (functionalized) operations of addition and multiplication by a scalar of a subcomplex module cannot be identical. (Contributed by NM, 31-May-2008.) (Revised by AV, 3-Oct-2021.) |
⊢ · = ( ·sf ‘𝑊) & ⊢ + = (+𝑓‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂMod → + ≠ · ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |