mmtheorems82 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10687

Statement List for Metamath Proof Explorer - 8101-8200 - Page 82 of 107

Type	Label	Description
Statement
Theorem	ghsubgi 8101	The image of a subgroup S of group G under a group homomorphism F on G is a group, and furthermore is Abelian if S is Abelian. (Contributed by Paul Chapman, 25-Apr-2008.)
|- S e. (SubGrp` G)   &   |- X = ran G   &   |- F:X-->Y   &   |- Y (_ A   &   |- O Fn (A X. A)   &   |- ((x e. X /\ y e. X) -> (F` (xGy)) = ((F` x)O(F` y)))   &   |- Z = ran S   &   |- W = (F"Z)   &   |- H = (O |` (W X. W))   =>   |- (H e. Grp /\ (S e. Abel -> H e. Abel))
Ring theory
Definition and basic properties
Syntax	cring 8102	Extend class notation with the class of all unital rings.
class Ring
Definition	df-ring 8103	Define the class of all unital rings.
|- Ring = {<.g, h>. | ((g e. Abel /\ h:(ran g X. ran g)-->ran g) /\ (A.x e. ran gA.y e. ran gA.z e. ran g(((xhy)hz) = (xh(yhz)) /\ (xh(ygz)) = ((xhy)g(xhz)) /\ ((xgy)hz) = ((xhz)g(yhz))) /\ E.x e. ran gA.y e. ran g((yhx) = y /\ (xhy) = y)))}
Theorem	isring 8104	The predicate "is a (unital) ring." Definition of ring with unit in [Schechter] p. 187. (Contributed by Jeffrey Hankins, 21-Nov-2006.)
|- X = ran G   =>   |- (H e. A -> (<.G, H>. e. Ring <-> ((G e. Abel /\ H:(X X. X)-->X) /\ (A.x e. X A.y e. X A.z e. X (((xHy)Hz) = (xH(yHz)) /\ (xH(yGz)) = ((xHy)G(xHz)) /\ ((xGy)Hz) = ((xHz)G(yHz))) /\ E.x e. X A.y e. X ((yHx) = y /\ (xHy) = y)))))
Theorem	ringi 8105	The properties of a unital ring. (Contributed by Steve Rodriguez, 8-Sep-2007.)
|- G = (1st` R)   &   |- H = (2nd` R)   &   |- X = ran G   =>   |- (R e. Ring -> ((G e. Abel /\ H:(X X. X)-->X) /\ (A.x e. X A.y e. X A.z e. X (((xHy)Hz) = (xH(yHz)) /\ (xH(yGz)) = ((xHy)G(xHz)) /\ ((xGy)Hz) = ((xHz)G(yHz))) /\ E.x e. X A.y e. X ((yHx) = y /\ (xHy) = y))))
Theorem	ringsm 8106	Functionality of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- G = (1st` R)   &   |- H = (2nd` R)   &   |- X = ran G   =>   |- (R e. Ring -> H:(X X. X)-->X)
Theorem	ringcl 8107	Closure of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- G = (1st` R)   &   |- H = (2nd` R)   &   |- X = ran G   =>   |- ((R e. Ring /\ A e. X /\ B e. X) -> (AHB) e. X)
Theorem	ringid 8108	The multiplication operation of a unital ring has (one or more) identity elements. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- G = (1st` R)   &   |- H = (2nd` R)   &   |- X = ran G   =>   |- ((R e. Ring /\ A e. X) -> E.x e. X ((AHx) = A /\ (xHA) = A))
Theorem	ringdi 8109	Distributive law for the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- G = (1st` R)   &   |- H = (2nd` R)   &   |- X = ran G   =>   |- ((R e. Ring /\ (A e. X /\ B e. X /\ C e. X)) -> (AH(BGC)) = ((AHB)G(AHC)))
Theorem	ringdir 8110	Distributive law for the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- G = (1st` R)   &   |- H = (2nd` R)   &   |- X = ran G   =>   |- ((R e. Ring /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGB)HC) = ((AHC)G(BHC)))
Theorem	ringass 8111	Associative law for the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- G = (1st` R)   &   |- H = (2nd` R)   &   |- X = ran G   =>   |- ((R e. Ring /\ (A e. X /\ B e. X /\ C e. X)) -> ((AHB)HC) = (AH(BHC)))
Theorem	ring2 8112	A ring element plus itself is two times the element. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- G = (1st` R)   &   |- H = (2nd` R)   &   |- X = ran G   =>   |- ((R e. Ring /\ A e. X) -> E.x e. X (AGA) = ((xGx)HA))
Theorem	ringabl 8113	A ring's addition operation is an Abelian group operation. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- G = (1st` R)   =>   |- (R e. Ring -> G e. Abel)
Theorem	ringgrp 8114	A ring's addition operation is a group operation. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- G = (1st` R)   =>   |- (R e. Ring -> G e. Grp)
Theorem	ringgcl 8115	Closure law for the addition (group) operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- G = (1st` R)   &   |- X = ran G   =>   |- ((R e. Ring /\ A e. X /\ B e. X) -> (AGB) e. X)
Theorem	ringcom 8116	The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- G = (1st` R)   &   |- X = ran G   =>   |- ((R e. Ring /\ A e. X /\ B e. X) -> (AGB) = (BGA))
Theorem	ringaass 8117	The addition operation of a ring is associative. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- G = (1st` R)   &   |- X = ran G   =>   |- ((R e. Ring /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGB)GC) = (AG(BGC)))
Theorem	ringa23 8118	The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- G = (1st` R)   &   |- X = ran G   =>   |- ((R e. Ring /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGB)GC) = ((AGC)GB))
Theorem	ringa4 8119	Rearrangement of 4 terms in a sum of ring elements. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- G = (1st` R)   &   |- X = ran G   =>   |- ((R e. Ring /\ (A e. X /\ B e. X) /\ (C e. X /\ D e. X)) -> ((AGB)G(CGD)) = ((AGC)G(BGD)))
Theorem	ringrcan 8120	Right cancellation law for the addition operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- G = (1st` R)   &   |- X = ran G   =>   |- ((R e. Ring /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGC) = (BGC) <-> A = B))
Theorem	ringlcan 8121	Left cancellation law for the addition operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- G = (1st` R)   &   |- X = ran G   =>   |- ((R e. Ring /\ (A e. X /\ B e. X /\ C e. X)) -> ((CGA) = (CGB) <-> A = B))
Theorem	ring0cl 8122	A ring has an additive identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- G = (1st` R)   &   |- X = ran G   &   |- Z = (Id` G)   =>   |- (R e. Ring -> Z e. X)
Theorem	ring0rid 8123	The additive identity of a ring is a right identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- G = (1st` R)   &   |- X = ran G   &   |- Z = (Id` G)   =>   |- ((R e. Ring /\ A e. X) -> (AGZ) = A)
Theorem	ring0lid 8124	The additive identity of a ring is a left identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- G = (1st` R)   &   |- X = ran G   &   |- Z = (Id` G)   =>   |- ((R e. Ring /\ A e. X) -> (ZGA) = A)
Examples of rings
Theorem	cnring 8125	The set of complex numbers is a (unital) ring. (Contributed by Steve Rodriguez, 2-Feb-2007.)
|- <. + , x. >. e. Ring
Theorem	ringsn 8126	The trivial or zero ring defined on a singleton set {A} (see http://en.wikipedia.org/wiki/Trivial_ring). (Contributed by Steve Rodriguez, 10-Feb-2007.)
|- A e. V   =>   |- <.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>. e. Ring
Complex vector spaces
Definition and basic properties
Syntax	cvc 8127	Extend class notation with the class of all complex vector spaces.
class CVec
Definition	df-vc 8128	Define the class of all complex vector spaces.
|- CVec = {<.g, s>. | (g e. Abel /\ s:(CC X. ran g)-->ran g /\ A.x e. ran g((1sx) = x /\ A.y e. CC (A.z e. ran g(ys(xgz)) = ((ysx)g(ysz)) /\ A.z e. CC (((y + z)sx) = ((ysx)g(zsx)) /\ ((y x. z)sx) = (ys(zsx))))))}
Theorem	vcrel 8129	The class of all complex vector spaces is a relation.
|- Rel CVec
Theorem	vci 8130	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 W was chosen because V is already used for the universal class.
|- G = (1st` W)   &   |- S = (2nd` W)   &   |- X = ran G   =>   |- (W e. CVec -> (G e. Abel /\ S:(CC X. X)-->X /\