HomeTheorem List (p. 303 of 481)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 303 of 481) | < 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-30640) |
Hilbert Space Explorer
(30641-32163) |
Users' Mathboxes
(32164-48040) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | l2p 30201* | 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 30202* | 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 30203 | 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 30204 | Alternate version of nsnlplig 30203 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 30205 | 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 30206 | Alternate version of n0lplig 30205 using the predicate β instead of Β¬ β and whose proof bypasses nsnlplig 30203. (Contributed by AV, 28-Nov-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
| β’ (πΊ β Plig β β β πΊ) | ||
| Theorem | eulplig 30207* | Through two distinct points of a planar incidence geometry, there is a unique line. (Contributed by BJ, 2-Dec-2021.) |
| β’ π = βͺ πΊ β β’ ((πΊ β Plig β§ ((π΄ β π β§ π΅ β π) β§ π΄ β π΅)) β β!π β πΊ (π΄ β π β§ π΅ β π)) | ||
| Theorem | pliguhgr 30208 | Any planar incidence geometry πΊ can be regarded as a hypergraph with its points as vertices and its lines as edges. See incistruhgr 28808 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 30209 |
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 30210 |
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 30211 | Extend class notation with the class of all group operations. |
| class GrpOp | ||
| Syntax | cgi 30212 | Extend class notation with a function mapping a group operation to the group's identity element. |
| class GId | ||
| Syntax | cgn 30213 | Extend class notation with a function mapping a group operation to the inverse function for the group. |
| class inv | ||
| Syntax | cgs 30214 | Extend class notation with a function mapping a group operation to the division (or subtraction) operation for the group. |
| class /π | ||
| Definition | df-grpo 30215* | 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 30216* | 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 30217* | 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 30218* | 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 30219* | 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 30220* | Properties that determine a group operation. Read π as π(π₯). (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
| β’ π β V & β’ πΊ:(π Γ π)βΆπ & β’ ((π₯ β π β§ π¦ β π β§ π§ β π) β ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§))) & β’ π β π & β’ (π₯ β π β (ππΊπ₯) = π₯) & β’ (π₯ β π β π β π) & β’ (π₯ β π β (ππΊπ₯) = π) β β’ πΊ β GrpOp | ||
| Theorem | grpofo 30221 | 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 30222 | Closure law for a group operation. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) |
| β’ π = ran πΊ β β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) β π) | ||
| Theorem | grpolidinv 30223* | 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 30224 | The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (New usage is discouraged.) |
| β’ π = ran πΊ β β’ (πΊ β GrpOp β π β β ) | ||
| Theorem | grpoass 30225 | A group operation is associative. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) |
| β’ π = ran πΊ β β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)πΊπΆ) = (π΄πΊ(π΅πΊπΆ))) | ||
| Theorem | grpoidinvlem1 30226 | Lemma for grpoidinv 30230. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) |
| β’ π = ran πΊ β β’ (((πΊ β GrpOp β§ (π β π β§ π΄ β π)) β§ ((ππΊπ΄) = π β§ (π΄πΊπ΄) = π΄)) β (ππΊπ΄) = π) | ||
| Theorem | grpoidinvlem2 30227 | Lemma for grpoidinv 30230. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.) |
| β’ π = ran πΊ β β’ (((πΊ β GrpOp β§ (π β π β§ π΄ β π)) β§ ((ππΊπ) = π β§ (ππΊπ΄) = π)) β ((π΄πΊπ)πΊ(π΄πΊπ)) = (π΄πΊπ)) | ||
| Theorem | grpoidinvlem3 30228* | Lemma for grpoidinv 30230. (Contributed by NM, 11-Oct-2006.) (New usage is discouraged.) |
| β’ π = ran πΊ & β’ (π β βπ₯ β π (ππΊπ₯) = π₯) & β’ (π β βπ₯ β π βπ§ β π (π§πΊπ₯) = π) β β’ ((((πΊ β GrpOp β§ π β π) β§ (π β§ π)) β§ π΄ β π) β βπ¦ β π ((π¦πΊπ΄) = π β§ (π΄πΊπ¦) = π)) | ||
| Theorem | grpoidinvlem4 30229* | Lemma for grpoidinv 30230. (Contributed by NM, 14-Oct-2006.) (New usage is discouraged.) |
| β’ π = ran πΊ β β’ (((πΊ β GrpOp β§ π΄ β π) β§ βπ¦ β π ((π¦πΊπ΄) = π β§ (π΄πΊπ¦) = π)) β (π΄πΊπ) = (ππΊπ΄)) | ||
| Theorem | grpoidinv 30230* | 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 30231* | 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 30232 | 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 30233 | The empty set is not a group. (Contributed by NM, 25-Apr-2007.) (New usage is discouraged.) |
| β’ Β¬ β β GrpOp | ||
| Theorem | gidval 30234* | The value of the identity element of a group. (Contributed by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
| β’ π = ran πΊ β β’ (πΊ β π β (GIdβπΊ) = (β©π’ β π βπ₯ β π ((π’πΊπ₯) = π₯ β§ (π₯πΊπ’) = π₯))) | ||
| Theorem | grpoidval 30235* | Lemma for grpoidcl 30236 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 30236 | 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 30237* | 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 30238 | 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 30239 | 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 30240 | Right cancellation law for groups. (Contributed by NM, 26-Oct-2006.) (New usage is discouraged.) |
| β’ π = ran πΊ β β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπΆ) = (π΅πΊπΆ) β π΄ = π΅)) | ||
| Theorem | grpoinveu 30241* | 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 30242 | 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 30243 | 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 30244* | 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 30245* | 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 30246 | 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 30247 | 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 30248 | The left inverse of a group element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
| β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π = (invβπΊ) β β’ ((πΊ β GrpOp β§ π΄ β π) β ((πβπ΄)πΊπ΄) = π) | ||
| Theorem | grporinv 30249 | The right inverse of a group element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
| β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π = (invβπΊ) β β’ ((πΊ β GrpOp β§ π΄ β π) β (π΄πΊ(πβπ΄)) = π) | ||
| Theorem | grpoinvid1 30250 | 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 30251 | 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 30252 | Left cancellation law for groups. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.) |
| β’ π = ran πΊ β β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((πΆπΊπ΄) = (πΆπΊπ΅) β π΄ = π΅)) | ||
| Theorem | grpo2inv 30253 | 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 30254 | 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 30255 | 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 30256* | 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 30257 | 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 30258 | Group division by an inverse. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
| β’ π = ran πΊ & β’ π = (invβπΊ) & β’ π· = ( /π βπΊ) β β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β (π΄π·(πβπ΅)) = (π΄πΊπ΅)) | ||
| Theorem | grpoinvdiv 30259 | Inverse of a group division. (Contributed by NM, 24-Feb-2008.) (New usage is discouraged.) |
| β’ π = ran πΊ & β’ π = (invβπΊ) & β’ π· = ( /π βπΊ) β β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β (πβ(π΄π·π΅)) = (π΅π·π΄)) | ||
| Theorem | grpodivf 30260 | 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 30261 | Closure of group division (or subtraction) operation. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
| β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) β π) | ||
| Theorem | grpodivdiv 30262 | Double group division. (Contributed by NM, 24-Feb-2008.) (New usage is discouraged.) |
| β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·(π΅π·πΆ)) = (π΄πΊ(πΆπ·π΅))) | ||
| Theorem | grpomuldivass 30263 | Associative-type law for multiplication and division. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
| β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)π·πΆ) = (π΄πΊ(π΅π·πΆ))) | ||
| Theorem | grpodivid 30264 | Division of a group member by itself. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
| β’ π = ran πΊ & β’ π· = ( /π βπΊ) & β’ π = (GIdβπΊ) β β’ ((πΊ β GrpOp β§ π΄ β π) β (π΄π·π΄) = π) | ||
| Theorem | grponpcan 30265 | Cancellation law for group division. (npcan 11466 analog.) (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
| β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β ((π΄π·π΅)πΊπ΅) = π΄) | ||
| Syntax | cablo 30266 | Extend class notation with the class of all Abelian group operations. |
| class AbelOp | ||
| Definition | df-ablo 30267* | Define the class of all Abelian group operations. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) |
| β’ AbelOp = {π β GrpOp β£ βπ₯ β ran πβπ¦ β ran π(π₯ππ¦) = (π¦ππ₯)} | ||
| Theorem | isablo 30268* | The predicate "is an Abelian (commutative) group operation." (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) |
| β’ π = ran πΊ β β’ (πΊ β AbelOp β (πΊ β GrpOp β§ βπ₯ β π βπ¦ β π (π₯πΊπ¦) = (π¦πΊπ₯))) | ||
| Theorem | ablogrpo 30269 | An Abelian group operation is a group operation. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) |
| β’ (πΊ β AbelOp β πΊ β GrpOp) | ||
| Theorem | ablocom 30270 | An Abelian group operation is commutative. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.) |
| β’ π = ran πΊ β β’ ((πΊ β AbelOp β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) = (π΅πΊπ΄)) | ||
| Theorem | ablo32 30271 | Commutative/associative law for Abelian groups. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.) |
| β’ π = ran πΊ β β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)πΊπΆ) = ((π΄πΊπΆ)πΊπ΅)) | ||
| Theorem | ablo4 30272 | Commutative/associative law for Abelian groups. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.) |
| β’ π = ran πΊ β β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β ((π΄πΊπ΅)πΊ(πΆπΊπ·)) = ((π΄πΊπΆ)πΊ(π΅πΊπ·))) | ||
| Theorem | isabloi 30273* | Properties that determine an Abelian group operation. (Contributed by NM, 5-Nov-2006.) (New usage is discouraged.) |
| β’ πΊ β GrpOp & β’ dom πΊ = (π Γ π) & β’ ((π₯ β π β§ π¦ β π) β (π₯πΊπ¦) = (π¦πΊπ₯)) β β’ πΊ β AbelOp | ||
| Theorem | ablomuldiv 30274 | Law for group multiplication and division. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
| β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)π·πΆ) = ((π΄π·πΆ)πΊπ΅)) | ||
| Theorem | ablodivdiv 30275 | Law for double group division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.) |
| β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·(π΅π·πΆ)) = ((π΄π·π΅)πΊπΆ)) | ||
| Theorem | ablodivdiv4 30276 | Law for double group division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.) |
| β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π·π΅)π·πΆ) = (π΄π·(π΅πΊπΆ))) | ||
| Theorem | ablodiv32 30277 | Swap the second and third terms in a double division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.) |
| β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π·π΅)π·πΆ) = ((π΄π·πΆ)π·π΅)) | ||
| Theorem | ablonncan 30278 | Cancellation law for group division. (nncan 11486 analog.) (Contributed by NM, 7-Mar-2008.) (New usage is discouraged.) |
| β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β AbelOp β§ π΄ β π β§ π΅ β π) β (π΄π·(π΄π·π΅)) = π΅) | ||
| Theorem | ablonnncan1 30279 | Cancellation law for group division. (nnncan1 11493 analog.) (Contributed by NM, 7-Mar-2008.) (New usage is discouraged.) |
| β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π·π΅)π·(π΄π·πΆ)) = (πΆπ·π΅)) | ||
| Syntax | cvc 30280 | Extend class notation with the class of all complex vector spaces. |
| class CVecOLD | ||
| Definition | df-vc 30281* | 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 30282 | The class of all complex vector spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
| β’ Rel CVecOLD | ||
| Theorem | vciOLD 30283* | Obsolete version of cvsi 24979. 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 30284 | 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 30285 | 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 30286 | Identity element for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) Obsolete theorem, use clmvs1 24942 together with cvsclm 24975 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
| β’ πΊ = (1st βπ) & β’ π = (2nd βπ) & β’ π = ran πΊ β β’ ((π β CVecOLD β§ π΄ β π) β (1ππ΄) = π΄) | ||
| Theorem | vcdi 30287 | 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 30288 | 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 30289 | 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 30290 | A vector plus itself is two times the vector. (Contributed by NM, 1-Feb-2007.) Obsolete theorem, use clmvs2 24943 together with cvsclm 24975 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
| β’ πΊ = (1st βπ) & β’ π = (2nd βπ) & β’ π = ran πΊ β β’ ((π β CVecOLD β§ π΄ β π) β (π΄πΊπ΄) = (2ππ΄)) | ||
| Theorem | vcablo 30291 | Vector addition is an Abelian group operation. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) |
| β’ πΊ = (1st βπ) β β’ (π β CVecOLD β πΊ β AbelOp) | ||
| Theorem | vcgrp 30292 | Vector addition is a group operation. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
| β’ πΊ = (1st βπ) β β’ (π β CVecOLD β πΊ β GrpOp) | ||
| Theorem | vclcan 30293 | Left cancellation law for vector addition. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
| β’ πΊ = (1st βπ) & β’ π = ran πΊ β β’ ((π β CVecOLD β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((πΆπΊπ΄) = (πΆπΊπ΅) β π΄ = π΅)) | ||
| Theorem | vczcl 30294 | The zero vector is a vector. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
| β’ πΊ = (1st βπ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (π β CVecOLD β π β π) | ||
| Theorem | vc0rid 30295 | The zero vector is a right identity element. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
| β’ πΊ = (1st βπ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ ((π β CVecOLD β§ π΄ β π) β (π΄πΊπ) = π΄) | ||
| Theorem | vc0 30296 | Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) |
| β’ πΊ = (1st βπ) & β’ π = (2nd βπ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ ((π β CVecOLD β§ π΄ β π) β (0ππ΄) = π) | ||
| Theorem | vcz 30297 | Anything times the zero vector is the zero vector. Equation 1b of [Kreyszig] p. 51. (Contributed by NM, 24-Nov-2006.) (New usage is discouraged.) |
| β’ πΊ = (1st βπ) & β’ π = (2nd βπ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ ((π β CVecOLD β§ π΄ β β) β (π΄ππ) = π) | ||
| Theorem | vcm 30298 | Minus 1 times a vector is the underlying group's inverse element. Equation 2 of [Kreyszig] p. 51. (Contributed by NM, 25-Nov-2006.) (New usage is discouraged.) |
| β’ πΊ = (1st βπ) & β’ π = (2nd βπ) & β’ π = ran πΊ & β’ π = (invβπΊ) β β’ ((π β CVecOLD β§ π΄ β π) β (-1ππ΄) = (πβπ΄)) | ||
| Theorem | isvclem 30299* | Lemma for isvcOLD 30301. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
| β’ π = ran πΊ β β’ ((πΊ β V β§ π β V) β (β¨πΊ, πβ© β CVecOLD β (πΊ β AbelOp β§ π:(β Γ π)βΆπ β§ βπ₯ β π ((1ππ₯) = π₯ β§ βπ¦ β β (βπ§ β π (π¦π(π₯πΊπ§)) = ((π¦ππ₯)πΊ(π¦ππ§)) β§ βπ§ β β (((π¦ + π§)ππ₯) = ((π¦ππ₯)πΊ(π§ππ₯)) β§ ((π¦ Β· π§)ππ₯) = (π¦π(π§ππ₯)))))))) | ||
| Theorem | vcex 30300 | The components of a complex vector space are sets. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
| β’ (β¨πΊ, πβ© β CVecOLD β (πΊ β V β§ π β V)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |