Home | Metamath
Proof Explorer Theorem List (p. 293 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 9p10ne21fool 29201 | 9 + 10 equals 21. This astonishing thesis lives as a meme on the internet, and may be believed by quite some people. At least repeated requests to falsify it are a permanent part of the story. Prof. Loof Lirpa did not rest until he finally came up with a computer verifiable mathematical proof, that only a fool can think so. (Contributed by Prof. Loof Lirpa, 26-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((9 + ;10) = ;21 β πΉβ (0 Β· 1)) | ||
Syntax | cplig 29202 | Extend class notation with the class of all planar incidence geometries. |
class Plig | ||
Definition | df-plig 29203* |
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 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 29204* | The predicate "is a planar incidence geometry" for sets. (Contributed by FL, 2-Aug-2009.) |
β’ π = βͺ πΊ β β’ (πΊ β π΄ β (πΊ β Plig β (βπ β π βπ β π (π β π β β!π β πΊ (π β π β§ π β π)) β§ βπ β πΊ βπ β π βπ β π (π β π β§ π β π β§ π β π) β§ βπ β π βπ β π βπ β π βπ β πΊ Β¬ (π β π β§ π β π β§ π β π)))) | ||
Theorem | ispligb 29205* | The predicate "is a planar incidence geometry". (Contributed by BJ, 2-Dec-2021.) |
β’ π = βͺ πΊ β β’ (πΊ β Plig β (πΊ β V β§ (βπ β π βπ β π (π β π β β!π β πΊ (π β π β§ π β π)) β§ βπ β πΊ βπ β π βπ β π (π β π β§ π β π β§ π β π) β§ βπ β π βπ β π βπ β π βπ β πΊ Β¬ (π β π β§ π β π β§ π β π)))) | ||
Theorem | tncp 29206* | In any planar incidence geometry, there exist three non-collinear points. (Contributed by FL, 3-Aug-2009.) |
β’ π = βͺ πΊ β β’ (πΊ β Plig β βπ β π βπ β π βπ β π βπ β πΊ Β¬ (π β π β§ π β π β§ π β π)) | ||
Theorem | l2p 29207* | 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 29208* | 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 29209 | 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 29210 | Alternate version of nsnlplig 29209 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 29211 | 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 29212 | Alternate version of n0lplig 29211 using the predicate β instead of Β¬ β and whose proof bypasses nsnlplig 29209. (Contributed by AV, 28-Nov-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (πΊ β Plig β β β πΊ) | ||
Theorem | eulplig 29213* | Through two distinct points of a planar incidence geometry, there is a unique line. (Contributed by BJ, 2-Dec-2021.) |
β’ π = βͺ πΊ β β’ ((πΊ β Plig β§ ((π΄ β π β§ π΅ β π) β§ π΄ β π΅)) β β!π β πΊ (π΄ β π β§ π΅ β π)) | ||
Theorem | pliguhgr 29214 | Any planar incidence geometry πΊ can be regarded as a hypergraph with its points as vertices and its lines as edges. See incistruhgr 27816 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 29215 |
Alias for a1ii 2 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 2. (Contributed by NM, 7-Feb-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π & β’ π β β’ π | ||
Theorem | id1 29216 |
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 the Metamath program 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 29217 | Extend class notation with the class of all group operations. |
class GrpOp | ||
Syntax | cgi 29218 | Extend class notation with a function mapping a group operation to the group's identity element. |
class GId | ||
Syntax | cgn 29219 | Extend class notation with a function mapping a group operation to the inverse function for the group. |
class inv | ||
Syntax | cgs 29220 | Extend class notation with a function mapping a group operation to the division (or subtraction) operation for the group. |
class /π | ||
Definition | df-grpo 29221* | 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 29222* | 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 29223* | 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 29224* | 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 29225* | 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 29226* | Properties that determine a group operation. Read π as π(π₯). (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
β’ π β V & β’ πΊ:(π Γ π)βΆπ & β’ ((π₯ β π β§ π¦ β π β§ π§ β π) β ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§))) & β’ π β π & β’ (π₯ β π β (ππΊπ₯) = π₯) & β’ (π₯ β π β π β π) & β’ (π₯ β π β (ππΊπ₯) = π) β β’ πΊ β GrpOp | ||
Theorem | grpofo 29227 | 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 29228 | Closure law for a group operation. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) |
β’ π = ran πΊ β β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) β π) | ||
Theorem | grpolidinv 29229* | 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 29230 | The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (New usage is discouraged.) |
β’ π = ran πΊ β β’ (πΊ β GrpOp β π β β ) | ||
Theorem | grpoass 29231 | A group operation is associative. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) |
β’ π = ran πΊ β β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)πΊπΆ) = (π΄πΊ(π΅πΊπΆ))) | ||
Theorem | grpoidinvlem1 29232 | Lemma for grpoidinv 29236. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) |
β’ π = ran πΊ β β’ (((πΊ β GrpOp β§ (π β π β§ π΄ β π)) β§ ((ππΊπ΄) = π β§ (π΄πΊπ΄) = π΄)) β (ππΊπ΄) = π) | ||
Theorem | grpoidinvlem2 29233 | Lemma for grpoidinv 29236. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) |
β’ π = ran πΊ β β’ (((πΊ β GrpOp β§ (π β π β§ π΄ β π)) β§ ((ππΊπ) = π β§ (ππΊπ΄) = π)) β ((π΄πΊπ)πΊ(π΄πΊπ)) = (π΄πΊπ)) | ||
Theorem | grpoidinvlem3 29234* | Lemma for grpoidinv 29236. (Contributed by NM, 11-Oct-2006.) (New usage is discouraged.) |
β’ π = ran πΊ & β’ (π β βπ₯ β π (ππΊπ₯) = π₯) & β’ (π β βπ₯ β π βπ§ β π (π§πΊπ₯) = π) β β’ ((((πΊ β GrpOp β§ π β π) β§ (π β§ π)) β§ π΄ β π) β βπ¦ β π ((π¦πΊπ΄) = π β§ (π΄πΊπ¦) = π)) | ||
Theorem | grpoidinvlem4 29235* | Lemma for grpoidinv 29236. (Contributed by NM, 14-Oct-2006.) (New usage is discouraged.) |
β’ π = ran πΊ β β’ (((πΊ β GrpOp β§ π΄ β π) β§ βπ¦ β π ((π¦πΊπ΄) = π β§ (π΄πΊπ¦) = π)) β (π΄πΊπ) = (ππΊπ΄)) | ||
Theorem | grpoidinv 29236* | 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 29237* | 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 29238 | 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 29239 | The empty set is not a group. (Contributed by NM, 25-Apr-2007.) (New usage is discouraged.) |
β’ Β¬ β β GrpOp | ||
Theorem | gidval 29240* | The value of the identity element of a group. (Contributed by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
β’ π = ran πΊ β β’ (πΊ β π β (GIdβπΊ) = (β©π’ β π βπ₯ β π ((π’πΊπ₯) = π₯ β§ (π₯πΊπ’) = π₯))) | ||
Theorem | grpoidval 29241* | Lemma for grpoidcl 29242 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 29242 | 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 29243* | 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 29244 | 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 29245 | 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 29246 | Right cancellation law for groups. (Contributed by NM, 26-Oct-2006.) (New usage is discouraged.) |
β’ π = ran πΊ β β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπΆ) = (π΅πΊπΆ) β π΄ = π΅)) | ||
Theorem | grpoinveu 29247* | 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 29248 | 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 29249 | 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 29250* | 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 29251* | 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 29252 | 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 29253 | 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 29254 | The left inverse of a group element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π = (invβπΊ) β β’ ((πΊ β GrpOp β§ π΄ β π) β ((πβπ΄)πΊπ΄) = π) | ||
Theorem | grporinv 29255 | The right inverse of a group element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π = (invβπΊ) β β’ ((πΊ β GrpOp β§ π΄ β π) β (π΄πΊ(πβπ΄)) = π) | ||
Theorem | grpoinvid1 29256 | 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 29257 | 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 29258 | Left cancellation law for groups. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
β’ π = ran πΊ β β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((πΆπΊπ΄) = (πΆπΊπ΅) β π΄ = π΅)) | ||
Theorem | grpo2inv 29259 | 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 29260 | 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 29261 | 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 29262* | 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 29263 | 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 29264 | Group division by an inverse. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
β’ π = ran πΊ & β’ π = (invβπΊ) & β’ π· = ( /π βπΊ) β β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β (π΄π·(πβπ΅)) = (π΄πΊπ΅)) | ||
Theorem | grpoinvdiv 29265 | Inverse of a group division. (Contributed by NM, 24-Feb-2008.) (New usage is discouraged.) |
β’ π = ran πΊ & β’ π = (invβπΊ) & β’ π· = ( /π βπΊ) β β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β (πβ(π΄π·π΅)) = (π΅π·π΄)) | ||
Theorem | grpodivf 29266 | 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 29267 | Closure of group division (or subtraction) operation. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) β π) | ||
Theorem | grpodivdiv 29268 | Double group division. (Contributed by NM, 24-Feb-2008.) (New usage is discouraged.) |
β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·(π΅π·πΆ)) = (π΄πΊ(πΆπ·π΅))) | ||
Theorem | grpomuldivass 29269 | Associative-type law for multiplication and division. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)π·πΆ) = (π΄πΊ(π΅π·πΆ))) | ||
Theorem | grpodivid 29270 | Division of a group member by itself. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
β’ π = ran πΊ & β’ π· = ( /π βπΊ) & β’ π = (GIdβπΊ) β β’ ((πΊ β GrpOp β§ π΄ β π) β (π΄π·π΄) = π) | ||
Theorem | grponpcan 29271 | Cancellation law for group division. (npcan 11344 analog.) (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β ((π΄π·π΅)πΊπ΅) = π΄) | ||
Syntax | cablo 29272 | Extend class notation with the class of all Abelian group operations. |
class AbelOp | ||
Definition | df-ablo 29273* | Define the class of all Abelian group operations. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) |
β’ AbelOp = {π β GrpOp β£ βπ₯ β ran πβπ¦ β ran π(π₯ππ¦) = (π¦ππ₯)} | ||
Theorem | isablo 29274* | The predicate "is an Abelian (commutative) group operation." (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) |
β’ π = ran πΊ β β’ (πΊ β AbelOp β (πΊ β GrpOp β§ βπ₯ β π βπ¦ β π (π₯πΊπ¦) = (π¦πΊπ₯))) | ||
Theorem | ablogrpo 29275 | An Abelian group operation is a group operation. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) |
β’ (πΊ β AbelOp β πΊ β GrpOp) | ||
Theorem | ablocom 29276 | An Abelian group operation is commutative. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) |
β’ π = ran πΊ β β’ ((πΊ β AbelOp β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) = (π΅πΊπ΄)) | ||
Theorem | ablo32 29277 | Commutative/associative law for Abelian groups. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.) |
β’ π = ran πΊ β β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)πΊπΆ) = ((π΄πΊπΆ)πΊπ΅)) | ||
Theorem | ablo4 29278 | Commutative/associative law for Abelian groups. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.) |
β’ π = ran πΊ β β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β ((π΄πΊπ΅)πΊ(πΆπΊπ·)) = ((π΄πΊπΆ)πΊ(π΅πΊπ·))) | ||
Theorem | isabloi 29279* | Properties that determine an Abelian group operation. (Contributed by NM, 5-Nov-2006.) (New usage is discouraged.) |
β’ πΊ β GrpOp & β’ dom πΊ = (π Γ π) & β’ ((π₯ β π β§ π¦ β π) β (π₯πΊπ¦) = (π¦πΊπ₯)) β β’ πΊ β AbelOp | ||
Theorem | ablomuldiv 29280 | Law for group multiplication and division. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)π·πΆ) = ((π΄π·πΆ)πΊπ΅)) | ||
Theorem | ablodivdiv 29281 | Law for double group division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.) |
β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·(π΅π·πΆ)) = ((π΄π·π΅)πΊπΆ)) | ||
Theorem | ablodivdiv4 29282 | Law for double group division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.) |
β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π·π΅)π·πΆ) = (π΄π·(π΅πΊπΆ))) | ||
Theorem | ablodiv32 29283 | Swap the second and third terms in a double division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.) |
β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π·π΅)π·πΆ) = ((π΄π·πΆ)π·π΅)) | ||
Theorem | ablonncan 29284 | Cancellation law for group division. (nncan 11364 analog.) (Contributed by NM, 7-Mar-2008.) (New usage is discouraged.) |
β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β AbelOp β§ π΄ β π β§ π΅ β π) β (π΄π·(π΄π·π΅)) = π΅) | ||
Theorem | ablonnncan1 29285 | Cancellation law for group division. (nnncan1 11371 analog.) (Contributed by NM, 7-Mar-2008.) (New usage is discouraged.) |
β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π·π΅)π·(π΄π·πΆ)) = (πΆπ·π΅)) | ||
Syntax | cvc 29286 | Extend class notation with the class of all complex vector spaces. |
class CVecOLD | ||
Definition | df-vc 29287* | 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 29288 | The class of all complex vector spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
β’ Rel CVecOLD | ||
Theorem | vciOLD 29289* | Obsolete version of cvsi 24415. 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 29290 | 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 29291 | 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 29292 | Identity element for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) Obsolete theorem, use clmvs1 24378 together with cvsclm 24411 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
β’ πΊ = (1st βπ) & β’ π = (2nd βπ) & β’ π = ran πΊ β β’ ((π β CVecOLD β§ π΄ β π) β (1ππ΄) = π΄) | ||
Theorem | vcdi 29293 | 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 29294 | 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 29295 | 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 29296 | A vector plus itself is two times the vector. (Contributed by NM, 1-Feb-2007.) Obsolete theorem, use clmvs2 24379 together with cvsclm 24411 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
β’ πΊ = (1st βπ) & β’ π = (2nd βπ) & β’ π = ran πΊ β β’ ((π β CVecOLD β§ π΄ β π) β (π΄πΊπ΄) = (2ππ΄)) | ||
Theorem | vcablo 29297 | Vector addition is an Abelian group operation. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) |
β’ πΊ = (1st βπ) β β’ (π β CVecOLD β πΊ β AbelOp) | ||
Theorem | vcgrp 29298 | Vector addition is a group operation. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
β’ πΊ = (1st βπ) β β’ (π β CVecOLD β πΊ β GrpOp) | ||
Theorem | vclcan 29299 | Left cancellation law for vector addition. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
β’ πΊ = (1st βπ) & β’ π = ran πΊ β β’ ((π β CVecOLD β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((πΆπΊπ΄) = (πΆπΊπ΅) β π΄ = π΅)) | ||
Theorem | vczcl 29300 | The zero vector is a vector. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
β’ πΊ = (1st βπ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (π β CVecOLD β π β π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |