![]() |
Metamath
Proof Explorer Theorem List (p. 280 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-28347) |
![]() (28348-29872) |
![]() (29873-43657) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cplig 27901 | Extend class notation with the class of all planar incidence geometries. |
class Plig | ||
Definition | df-plig 27902* |
Define the class of planar incidence geometries. We use Hilbert's
axioms and adapt them to planar geometry. We use ∈ for the
incidence relation. We could have used a generic binary relation, but
using ∈ allows us to reuse previous
results. Much of what follows
is directly borrowed from Aitken, Incidence-Betweenness Geometry,
2008, http://public.csusm.edu/aitken_html/m410/betweenness.08.pdf.
The class Plig is the class of planar incidence geometries, where a planar incidence geometry is defined as a set of lines satisfying three axioms. In the definition below, 𝑥 denotes a planar incidence geometry, so ∪ 𝑥 denotes the union of its lines, that is, the set of points in the plane, 𝑙 denotes a line, and 𝑎, 𝑏, 𝑐 denote points. Therefore, the axioms are: 1) for all pairs of (distinct) points, there exists a unique line containing them; 2) all lines contain at least two points; 3) there exist three non-collinear points. (Contributed by FL, 2-Aug-2009.) |
⊢ Plig = {𝑥 ∣ (∀𝑎 ∈ ∪ 𝑥∀𝑏 ∈ ∪ 𝑥(𝑎 ≠ 𝑏 → ∃!𝑙 ∈ 𝑥 (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙)) ∧ ∀𝑙 ∈ 𝑥 ∃𝑎 ∈ ∪ 𝑥∃𝑏 ∈ ∪ 𝑥(𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙) ∧ ∃𝑎 ∈ ∪ 𝑥∃𝑏 ∈ ∪ 𝑥∃𝑐 ∈ ∪ 𝑥∀𝑙 ∈ 𝑥 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙))} | ||
Theorem | isplig 27903* | The predicate "is a planar incidence geometry" for sets. (Contributed by FL, 2-Aug-2009.) |
⊢ 𝑃 = ∪ 𝐺 ⇒ ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ Plig ↔ (∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 → ∃!𝑙 ∈ 𝐺 (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙)) ∧ ∀𝑙 ∈ 𝐺 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙) ∧ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙)))) | ||
Theorem | ispligb 27904* | The predicate "is a planar incidence geometry". (Contributed by BJ, 2-Dec-2021.) |
⊢ 𝑃 = ∪ 𝐺 ⇒ ⊢ (𝐺 ∈ Plig ↔ (𝐺 ∈ V ∧ (∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 → ∃!𝑙 ∈ 𝐺 (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙)) ∧ ∀𝑙 ∈ 𝐺 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙) ∧ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙)))) | ||
Theorem | tncp 27905* | In any planar incidence geometry, there exist three non-collinear points. (Contributed by FL, 3-Aug-2009.) |
⊢ 𝑃 = ∪ 𝐺 ⇒ ⊢ (𝐺 ∈ Plig → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙)) | ||
Theorem | l2p 27906* | For any line in a planar incidence geometry, there exist two different points on the line. (Contributed by AV, 28-Nov-2021.) |
⊢ 𝑃 = ∪ 𝐺 ⇒ ⊢ ((𝐺 ∈ Plig ∧ 𝐿 ∈ 𝐺) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝐿)) | ||
Theorem | lpni 27907* | For any line in a planar incidence geometry, there exists a point not on the line. (Contributed by Jeff Hankins, 15-Aug-2009.) |
⊢ 𝑃 = ∪ 𝐺 ⇒ ⊢ ((𝐺 ∈ Plig ∧ 𝐿 ∈ 𝐺) → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿) | ||
Theorem | nsnlplig 27908 | There is no "one-point line" in a planar incidence geometry. (Contributed by BJ, 2-Dec-2021.) (Proof shortened by AV, 5-Dec-2021.) |
⊢ (𝐺 ∈ Plig → ¬ {𝐴} ∈ 𝐺) | ||
Theorem | nsnlpligALT 27909 | Alternate version of nsnlplig 27908 using the predicate ∉ instead of ¬ ∈ and whose proof is shorter. (Contributed by AV, 5-Dec-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐺 ∈ Plig → {𝐴} ∉ 𝐺) | ||
Theorem | n0lplig 27910 | There is no "empty line" in a planar incidence geometry. (Contributed by AV, 28-Nov-2021.) (Proof shortened by BJ, 2-Dec-2021.) |
⊢ (𝐺 ∈ Plig → ¬ ∅ ∈ 𝐺) | ||
Theorem | n0lpligALT 27911 | Alternate version of n0lplig 27910 using the predicate ∉ instead of ¬ ∈ and whose proof bypasses nsnlplig 27908. (Contributed by AV, 28-Nov-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐺 ∈ Plig → ∅ ∉ 𝐺) | ||
Theorem | eulplig 27912* | Through two distinct points of a planar incidence geometry, there is a unique line. (Contributed by BJ, 2-Dec-2021.) |
⊢ 𝑃 = ∪ 𝐺 ⇒ ⊢ ((𝐺 ∈ Plig ∧ ((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ 𝐴 ≠ 𝐵)) → ∃!𝑙 ∈ 𝐺 (𝐴 ∈ 𝑙 ∧ 𝐵 ∈ 𝑙)) | ||
Theorem | pliguhgr 27913 | Any planar incidence geometry 𝐺 can be regarded as a hypergraph with its points as vertices and its lines as edges. See incistruhgr 26427 for a generalization of this case for arbitrary incidence structures (planar incidence geometries are such incidence structures). (Proposed by Gerard Lang, 24-Nov-2021.) (Contributed by AV, 28-Nov-2021.) |
⊢ (𝐺 ∈ Plig → 〈∪ 𝐺, ( I ↾ 𝐺)〉 ∈ UHGraph) | ||
This section contains a few aliases that we temporarily keep to prevent broken links. If you land on any of these, please let the originating site and/or us know that the link that made you land here should be changed. | ||
Theorem | dummylink 27914 |
Alias for a1ii 1 that may be referenced in some older works, and
kept
here to prevent broken links.
If you landed here, please let the originating site and/or us know that the link that made you land here should be changed to a link to a1ii 1. (Contributed by NM, 7-Feb-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 ⇒ ⊢ 𝜑 | ||
Theorem | id1 27915 |
Alias for idALT 23 that may be referenced in some older works, and
kept
here to prevent broken links.
If you landed here, please let the originating site and/or us know that the link that made you land here should be changed to a link to idALT 23. (Contributed by NM, 30-Sep-1992.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜑) | ||
The intent is for this deprecated section to be deleted once its theorems have extensible structure versions (or are not useful). You can make a list of "terminal" theorems (i.e., theorems not referenced by anything else) and for each theorem see if there exists an extensible structure version (or decide it is not useful), and if so, delete it. Then, repeat this recursively. One way to search for terminal theorems is to log the output ("MM> OPEN LOG xxx.txt") of "MM> SHOW USAGE <label-match>" in metamath.exe and search for "(None)". | ||
This section contains an earlier development of groups that was defined before extensible structures were introduced. The intent is for this deprecated section to be deleted once the corresponding definitions and theorems for complex topological vector spaces, which are using them, are revised accordingly. | ||
Syntax | cgr 27916 | Extend class notation with the class of all group operations. |
class GrpOp | ||
Syntax | cgi 27917 | Extend class notation with a function mapping a group operation to the group's identity element. |
class GId | ||
Syntax | cgn 27918 | Extend class notation with a function mapping a group operation to the inverse function for the group. |
class inv | ||
Syntax | cgs 27919 | Extend class notation with a function mapping a group operation to the division (or subtraction) operation for the group. |
class /𝑔 | ||
Definition | df-grpo 27920* | Define the class of all group operations. The base set for a group can be determined from its group operation. Based on the definition in Exercise 28 of [Herstein] p. 54. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) |
⊢ GrpOp = {𝑔 ∣ ∃𝑡(𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢))} | ||
Definition | df-gid 27921* | Define a function that maps a group operation to the group's identity element. (Contributed by FL, 5-Feb-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ GId = (𝑔 ∈ V ↦ (℩𝑢 ∈ ran 𝑔∀𝑥 ∈ ran 𝑔((𝑢𝑔𝑥) = 𝑥 ∧ (𝑥𝑔𝑢) = 𝑥))) | ||
Definition | df-ginv 27922* | Define a function that maps a group operation to the group's inverse function. (Contributed by NM, 26-Oct-2006.) (New usage is discouraged.) |
⊢ inv = (𝑔 ∈ GrpOp ↦ (𝑥 ∈ ran 𝑔 ↦ (℩𝑧 ∈ ran 𝑔(𝑧𝑔𝑥) = (GId‘𝑔)))) | ||
Definition | df-gdiv 27923* | Define a function that maps a group operation to the group's division (or subtraction) operation. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
⊢ /𝑔 = (𝑔 ∈ GrpOp ↦ (𝑥 ∈ ran 𝑔, 𝑦 ∈ ran 𝑔 ↦ (𝑥𝑔((inv‘𝑔)‘𝑦)))) | ||
Theorem | isgrpo 27924* | The predicate "is a group operation." Note that 𝑋 is the base set of the group. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ GrpOp ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢)))) | ||
Theorem | isgrpoi 27925* | Properties that determine a group operation. Read 𝑁 as 𝑁(𝑥). (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
⊢ 𝑋 ∈ V & ⊢ 𝐺:(𝑋 × 𝑋)⟶𝑋 & ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧))) & ⊢ 𝑈 ∈ 𝑋 & ⊢ (𝑥 ∈ 𝑋 → (𝑈𝐺𝑥) = 𝑥) & ⊢ (𝑥 ∈ 𝑋 → 𝑁 ∈ 𝑋) & ⊢ (𝑥 ∈ 𝑋 → (𝑁𝐺𝑥) = 𝑈) ⇒ ⊢ 𝐺 ∈ GrpOp | ||
Theorem | grpofo 27926 | A group operation maps onto the group's underlying set. (Contributed by NM, 30-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ GrpOp → 𝐺:(𝑋 × 𝑋)–onto→𝑋) | ||
Theorem | grpocl 27927 | Closure law for a group operation. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋) | ||
Theorem | grpolidinv 27928* | A group has a left identity element, and every member has a left inverse. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ GrpOp → ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢)) | ||
Theorem | grpon0 27929 | The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ GrpOp → 𝑋 ≠ ∅) | ||
Theorem | grpoass 27930 | A group operation is associative. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = (𝐴𝐺(𝐵𝐺𝐶))) | ||
Theorem | grpoidinvlem1 27931 | Lemma for grpoidinv 27935. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝐺 ∈ GrpOp ∧ (𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) ∧ ((𝑌𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝐴) = 𝐴)) → (𝑈𝐺𝐴) = 𝑈) | ||
Theorem | grpoidinvlem2 27932 | Lemma for grpoidinv 27935. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝐺 ∈ GrpOp ∧ (𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) ∧ ((𝑈𝐺𝑌) = 𝑌 ∧ (𝑌𝐺𝐴) = 𝑈)) → ((𝐴𝐺𝑌)𝐺(𝐴𝐺𝑌)) = (𝐴𝐺𝑌)) | ||
Theorem | grpoidinvlem3 27933* | Lemma for grpoidinv 27935. (Contributed by NM, 11-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥) & ⊢ (𝜓 ↔ ∀𝑥 ∈ 𝑋 ∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈) ⇒ ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)) | ||
Theorem | grpoidinvlem4 27934* | Lemma for grpoidinv 27935. (Contributed by NM, 14-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)) → (𝐴𝐺𝑈) = (𝑈𝐺𝐴)) | ||
Theorem | grpoidinv 27935* | A group has a left and right identity element, and every member has a left and right inverse. (Contributed by NM, 14-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ GrpOp → ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑥) = 𝑢 ∧ (𝑥𝐺𝑦) = 𝑢))) | ||
Theorem | grpoideu 27936* | The left identity element of a group is unique. Lemma 2.2.1(a) of [Herstein] p. 55. (Contributed by NM, 14-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ GrpOp → ∃!𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥) | ||
Theorem | grporndm 27937 | A group's range in terms of its domain. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.) |
⊢ (𝐺 ∈ GrpOp → ran 𝐺 = dom dom 𝐺) | ||
Theorem | 0ngrp 27938 | The empty set is not a group. (Contributed by NM, 25-Apr-2007.) (New usage is discouraged.) |
⊢ ¬ ∅ ∈ GrpOp | ||
Theorem | gidval 27939* | The value of the identity element of a group. (Contributed by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ 𝑉 → (GId‘𝐺) = (℩𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥))) | ||
Theorem | grpoidval 27940* | Lemma for grpoidcl 27941 and others. (Contributed by NM, 5-Feb-2010.) (Proof shortened by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ (𝐺 ∈ GrpOp → 𝑈 = (℩𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥)) | ||
Theorem | grpoidcl 27941 | The identity element of a group belongs to the group. (Contributed by NM, 24-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ (𝐺 ∈ GrpOp → 𝑈 ∈ 𝑋) | ||
Theorem | grpoidinv2 27942* | A group's properties using the explicit identity element. (Contributed by NM, 5-Feb-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (((𝑈𝐺𝐴) = 𝐴 ∧ (𝐴𝐺𝑈) = 𝐴) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈))) | ||
Theorem | grpolid 27943 | The identity element of a group is a left identity. (Contributed by NM, 24-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝑈𝐺𝐴) = 𝐴) | ||
Theorem | grporid 27944 | The identity element of a group is a right identity. (Contributed by NM, 24-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝑈) = 𝐴) | ||
Theorem | grporcan 27945 | Right cancellation law for groups. (Contributed by NM, 26-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐶) = (𝐵𝐺𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | grpoinveu 27946* | The left inverse element of a group is unique. Lemma 2.2.1(b) of [Herstein] p. 55. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → ∃!𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈) | ||
Theorem | grpoid 27947 | Two ways of saying that an element of a group is the identity element. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝐴 = 𝑈 ↔ (𝐴𝐺𝐴) = 𝐴)) | ||
Theorem | grporn 27948 | The range of a group operation. Useful for satisfying group base set hypotheses of the form 𝑋 = ran 𝐺. (Contributed by NM, 5-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 ∈ GrpOp & ⊢ dom 𝐺 = (𝑋 × 𝑋) ⇒ ⊢ 𝑋 = ran 𝐺 | ||
Theorem | grpoinvfval 27949* | The inverse function of a group. (Contributed by NM, 26-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ (𝐺 ∈ GrpOp → 𝑁 = (𝑥 ∈ 𝑋 ↦ (℩𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈))) | ||
Theorem | grpoinvval 27950* | The inverse of a group element. (Contributed by NM, 26-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (℩𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)) | ||
Theorem | grpoinvcl 27951 | A group element's inverse is a group element. (Contributed by NM, 27-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ 𝑋) | ||
Theorem | grpoinv 27952 | The properties of a group element's inverse. (Contributed by NM, 27-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (((𝑁‘𝐴)𝐺𝐴) = 𝑈 ∧ (𝐴𝐺(𝑁‘𝐴)) = 𝑈)) | ||
Theorem | grpolinv 27953 | The left inverse of a group element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → ((𝑁‘𝐴)𝐺𝐴) = 𝑈) | ||
Theorem | grporinv 27954 | The right inverse of a group element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺(𝑁‘𝐴)) = 𝑈) | ||
Theorem | grpoinvid1 27955 | The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘𝐴) = 𝐵 ↔ (𝐴𝐺𝐵) = 𝑈)) | ||
Theorem | grpoinvid2 27956 | The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐺) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘𝐴) = 𝐵 ↔ (𝐵𝐺𝐴) = 𝑈)) | ||
Theorem | grpolcan 27957 | Left cancellation law for groups. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐶𝐺𝐴) = (𝐶𝐺𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | grpo2inv 27958 | Double inverse law for groups. Lemma 2.2.1(c) of [Herstein] p. 55. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝑁‘(𝑁‘𝐴)) = 𝐴) | ||
Theorem | grpoinvf 27959 | Mapping of the inverse function of a group. (Contributed by NM, 29-Mar-2008.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ (𝐺 ∈ GrpOp → 𝑁:𝑋–1-1-onto→𝑋) | ||
Theorem | grpoinvop 27960 | The inverse of the group operation reverses the arguments. Lemma 2.2.1(d) of [Herstein] p. 55. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐺𝐵)) = ((𝑁‘𝐵)𝐺(𝑁‘𝐴))) | ||
Theorem | grpodivfval 27961* | Group division (or subtraction) operation. (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ (𝐺 ∈ GrpOp → 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝐺(𝑁‘𝑦)))) | ||
Theorem | grpodivval 27962 | Group division (or subtraction) operation value. (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐴𝐺(𝑁‘𝐵))) | ||
Theorem | grpodivinv 27963 | Group division by an inverse. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷(𝑁‘𝐵)) = (𝐴𝐺𝐵)) | ||
Theorem | grpoinvdiv 27964 | Inverse of a group division. (Contributed by NM, 24-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝑁 = (inv‘𝐺) & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐷𝐵)) = (𝐵𝐷𝐴)) | ||
Theorem | grpodivf 27965 | Mapping for group division. (Contributed by NM, 10-Apr-2008.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ (𝐺 ∈ GrpOp → 𝐷:(𝑋 × 𝑋)⟶𝑋) | ||
Theorem | grpodivcl 27966 | Closure of group division (or subtraction) operation. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ 𝑋) | ||
Theorem | grpodivdiv 27967 | Double group division. (Contributed by NM, 24-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷(𝐵𝐷𝐶)) = (𝐴𝐺(𝐶𝐷𝐵))) | ||
Theorem | grpomuldivass 27968 | Associative-type law for multiplication and division. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐷𝐶) = (𝐴𝐺(𝐵𝐷𝐶))) | ||
Theorem | grpodivid 27969 | Division of a group member by itself. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) & ⊢ 𝑈 = (GId‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝐴𝐷𝐴) = 𝑈) | ||
Theorem | grponpcan 27970 | Cancellation law for group division. (npcan 10632 analog.) (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐷𝐵)𝐺𝐵) = 𝐴) | ||
Syntax | cablo 27971 | Extend class notation with the class of all Abelian group operations. |
class AbelOp | ||
Definition | df-ablo 27972* | Define the class of all Abelian group operations. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) |
⊢ AbelOp = {𝑔 ∈ GrpOp ∣ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(𝑥𝑔𝑦) = (𝑦𝑔𝑥)} | ||
Theorem | isablo 27973* | The predicate "is an Abelian (commutative) group operation." (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝐺 ∈ AbelOp ↔ (𝐺 ∈ GrpOp ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐺𝑦) = (𝑦𝐺𝑥))) | ||
Theorem | ablogrpo 27974 | An Abelian group operation is a group operation. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) |
⊢ (𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp) | ||
Theorem | ablocom 27975 | An Abelian group operation is commutative. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝐺 ∈ AbelOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) = (𝐵𝐺𝐴)) | ||
Theorem | ablo32 27976 | Commutative/associative law for Abelian groups. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐺𝐵)) | ||
Theorem | ablo4 27977 | Commutative/associative law for Abelian groups. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺(𝐶𝐺𝐷)) = ((𝐴𝐺𝐶)𝐺(𝐵𝐺𝐷))) | ||
Theorem | isabloi 27978* | Properties that determine an Abelian group operation. (Contributed by NM, 5-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 ∈ GrpOp & ⊢ dom 𝐺 = (𝑋 × 𝑋) & ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥)) ⇒ ⊢ 𝐺 ∈ AbelOp | ||
Theorem | ablomuldiv 27979 | Law for group multiplication and division. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐷𝐶) = ((𝐴𝐷𝐶)𝐺𝐵)) | ||
Theorem | ablodivdiv 27980 | Law for double group division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷(𝐵𝐷𝐶)) = ((𝐴𝐷𝐵)𝐺𝐶)) | ||
Theorem | ablodivdiv4 27981 | Law for double group division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐷𝐶) = (𝐴𝐷(𝐵𝐺𝐶))) | ||
Theorem | ablodiv32 27982 | Swap the second and third terms in a double division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐷𝐶) = ((𝐴𝐷𝐶)𝐷𝐵)) | ||
Theorem | ablonncan 27983 | Cancellation law for group division. (nncan 10652 analog.) (Contributed by NM, 7-Mar-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ AbelOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷(𝐴𝐷𝐵)) = 𝐵) | ||
Theorem | ablonnncan1 27984 | Cancellation law for group division. (nnncan1 10659 analog.) (Contributed by NM, 7-Mar-2008.) (New usage is discouraged.) |
⊢ 𝑋 = ran 𝐺 & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐷(𝐴𝐷𝐶)) = (𝐶𝐷𝐵)) | ||
Syntax | cvc 27985 | Extend class notation with the class of all complex vector spaces. |
class CVecOLD | ||
Definition | df-vc 27986* | Define the class of all complex vector spaces. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) |
⊢ CVecOLD = {〈𝑔, 𝑠〉 ∣ (𝑔 ∈ AbelOp ∧ 𝑠:(ℂ × ran 𝑔)⟶ran 𝑔 ∧ ∀𝑥 ∈ ran 𝑔((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))))} | ||
Theorem | vcrel 27987 | The class of all complex vector spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
⊢ Rel CVecOLD | ||
Theorem | vciOLD 27988* | Obsolete version of cvsi 23337. The properties of a complex vector space, which is an Abelian group (i.e. the vectors, with the operation of vector addition) accompanied by a scalar multiplication operation on the field of complex numbers. The variable 𝑊 was chosen because V is already used for the universal class. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑆 = (2nd ‘𝑊) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑊 ∈ CVecOLD → (𝐺 ∈ AbelOp ∧ 𝑆:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ((1𝑆𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ 𝑋 (𝑦𝑆(𝑥𝐺𝑧)) = ((𝑦𝑆𝑥)𝐺(𝑦𝑆𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑆𝑥) = ((𝑦𝑆𝑥)𝐺(𝑧𝑆𝑥)) ∧ ((𝑦 · 𝑧)𝑆𝑥) = (𝑦𝑆(𝑧𝑆𝑥))))))) | ||
Theorem | vcsm 27989 | Functionality of th scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑆 = (2nd ‘𝑊) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑊 ∈ CVecOLD → 𝑆:(ℂ × 𝑋)⟶𝑋) | ||
Theorem | vccl 27990 | Closure of the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑆 = (2nd ‘𝑊) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑊 ∈ CVecOLD ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (𝐴𝑆𝐵) ∈ 𝑋) | ||
Theorem | vcidOLD 27991 | Identity element for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) Obsolete theorem, use clmvs1 23300 together with cvsclm 23333 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑆 = (2nd ‘𝑊) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋) → (1𝑆𝐴) = 𝐴) | ||
Theorem | vcdi 27992 | Distributive law for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑆 = (2nd ‘𝑊) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑊 ∈ CVecOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑆(𝐵𝐺𝐶)) = ((𝐴𝑆𝐵)𝐺(𝐴𝑆𝐶))) | ||
Theorem | vcdir 27993 | Distributive law for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑆 = (2nd ‘𝑊) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑊 ∈ CVecOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 + 𝐵)𝑆𝐶) = ((𝐴𝑆𝐶)𝐺(𝐵𝑆𝐶))) | ||
Theorem | vcass 27994 | Associative law for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑆 = (2nd ‘𝑊) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑊 ∈ CVecOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 · 𝐵)𝑆𝐶) = (𝐴𝑆(𝐵𝑆𝐶))) | ||
Theorem | vc2OLD 27995 | A vector plus itself is two times the vector. (Contributed by NM, 1-Feb-2007.) Obsolete theorem, use clmvs2 23301 together with cvsclm 23333 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑆 = (2nd ‘𝑊) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝐴) = (2𝑆𝐴)) | ||
Theorem | vcablo 27996 | Vector addition is an Abelian group operation. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) ⇒ ⊢ (𝑊 ∈ CVecOLD → 𝐺 ∈ AbelOp) | ||
Theorem | vcgrp 27997 | Vector addition is a group operation. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) ⇒ ⊢ (𝑊 ∈ CVecOLD → 𝐺 ∈ GrpOp) | ||
Theorem | vclcan 27998 | Left cancellation law for vector addition. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑊 ∈ CVecOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐶𝐺𝐴) = (𝐶𝐺𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | vczcl 27999 | The zero vector is a vector. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑊 ∈ CVecOLD → 𝑍 ∈ 𝑋) | ||
Theorem | vc0rid 28000 | The zero vector is a right identity element. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
⊢ 𝐺 = (1st ‘𝑊) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝑍) = 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |