mmtheorems84 - 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-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

Statement List for Metamath Proof Explorer - 8301-8400 - Page 84 of 123

Type	Label	Description
Statement
Theorem	grpdivinv 8301	Group division by an inverse.
|- X = ran G   &   |- N = (inv` G)   &   |- D = ( /g ` G)   =>   |- ((G e. Grp /\ A e. X /\ B e. X) -> (AD(N` B)) = (AGB))
Theorem	grpinvdiv 8302	Inverse of a group division.
|- X = ran G   &   |- N = (inv` G)   &   |- D = ( /g ` G)   =>   |- ((G e. Grp /\ A e. X /\ B e. X) -> (N` (ADB)) = (BDA))
Theorem	grpdivf 8303	Mapping for group division.
|- X = ran G   &   |- D = ( /g ` G)   =>   |- (G e. Grp -> D:(X X. X)-->X)
Theorem	grpdivcl 8304	Closure of group division (or subtraction) operation.
|- X = ran G   &   |- D = ( /g ` G)   =>   |- ((G e. Grp /\ A e. X /\ B e. X) -> (ADB) e. X)
Theorem	grpdivdiv 8305	Double group division.
|- X = ran G   &   |- D = ( /g ` G)   =>   |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> (AD(BDC)) = (AG(CDB)))
Theorem	grpmuldivass 8306	Associative-type law for multiplication and division.
|- X = ran G   &   |- D = ( /g ` G)   =>   |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGB)DC) = (AG(BDC)))
Theorem	grpdivid 8307	Division of a group member by itself.
|- X = ran G   &   |- D = ( /g ` G)   &   |- U = (Id` G)   =>   |- ((G e. Grp /\ A e. X) -> (ADA) = U)
Theorem	grppncan 8308	Group theory analog of pncan 5551.
|- X = ran G   &   |- D = ( /g ` G)   =>   |- ((G e. Grp /\ A e. X /\ B e. X) -> ((AGB)DB) = A)
Theorem	grpnpcan 8309	Group theory analog of npcan 5553.
|- X = ran G   &   |- D = ( /g ` G)   =>   |- ((G e. Grp /\ A e. X /\ B e. X) -> ((ADB)GB) = A)
Theorem	grppnpcan2 8310	Group theory analog of pnpcan2 5633.
|- X = ran G   &   |- D = ( /g ` G)   =>   |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGC)D(BGC)) = (ADB))
Theorem	grpnnncan2 8311	Group theory analog of nnncan2 5622.
|- X = ran G   &   |- D = ( /g ` G)   =>   |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> ((ADC)D(BDC)) = (ADB))
Theorem	grpnpncan 8312	Group theory analog of npncan 5554.
|- X = ran G   &   |- D = ( /g ` G)   =>   |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> ((ADB)G(BDC)) = (ADC))
Theorem	gxoprval 8313	The value of the group power operator function. (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- U = (Id` G)   &   |- N = (inv` G)   &   |- P = (^g` G)   =>   |- (G e. Grp -> P = {<.<.x, y>., z>. | ((x e. X /\ y e. ZZ) /\ z = if(y = 0, U, if(0 < y, ((G seq1 (NN X. {x}))` y), (N` ((G seq1 (NN X. {x}))` -uy)))))})
Theorem	gxval 8314	The result of the group power operator. (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- U = (Id` G)   &   |- N = (inv` G)   &   |- P = (^g` G)   =>   |- ((G e. Grp /\ A e. X /\ K e. ZZ) -> (APK) = if(K = 0, U, if(0 < K, ((G seq1 (NN X. {A}))` K), (N` ((G seq1 (NN X. {A}))` -uK)))))
Theorem	gxpval 8315	The result of the group power operator when the exponent is positive. (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- P = (^g` G)   =>   |- ((G e. Grp /\ A e. X /\ K e. NN) -> (APK) = ((G seq1 (NN X. {A}))` K))
Theorem	gxnval 8316	The result of the group power operator when the exponent is negative. (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- P = (^g` G)   &   |- N = (inv` G)   =>   |- ((G e. Grp /\ A e. X /\ (K e. ZZ /\ K < 0)) -> (APK) = (N` ((G seq1 (NN X. {A}))` -uK)))
Theorem	gx0 8317	The result of the group power operator when the exponent is zero. (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- U = (Id` G)   &   |- P = (^g` G)   =>   |- ((G e. Grp /\ A e. X) -> (AP0) = U)
Theorem	gx1 8318	The result of the group power operator when the exponent is one. (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- P = (^g` G)   =>   |- ((G e. Grp /\ A e. X) -> (AP1) = A)
Theorem	gxnn0neg 8319	A negative group power is the inverse of the positive power (lemma with nonnegative exponent - use gxneg 8322 instead). (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- N = (inv` G)   &   |- P = (^g` G)   =>   |- ((G e. Grp /\ A e. X /\ K e. NN0) -> (AP-uK) = (N` (APK)))
Theorem	gxnn0suc 8320	Induction on group power (lemma with nonnegative exponent - use gxsuc 8328 instead). (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- P = (^g` G)   =>   |- ((G e. Grp /\ A e. X /\ K e. NN0) -> (AP(K + 1)) = ((APK)GA))
Theorem	gxcl 8321	Closure of the group power operator. (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- P = (^g` G)   =>   |- ((G e. Grp /\ A e. X /\ K e. ZZ) -> (APK) e. X)
Theorem	gxneg 8322	A negative group power is the inverse of the positive power. (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- N = (inv` G)   &   |- P = (^g` G)   =>   |- ((G e. Grp /\ A e. X /\ K e. ZZ) -> (AP-uK) = (N` (APK)))
Theorem	gxneg2 8323	The inverse of a negative group power is the positive power. (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- N = (inv` G)   &   |- P = (^g` G)   =>   |- ((G e. Grp /\ A e. X /\ K e. ZZ) -> (N` (AP-uK)) = (APK))
Theorem	gxm1 8324	The result of the group power operator when the exponent is minus one. (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- N = (inv` G)   &   |- P = (^g` G)   =>   |- ((G e. Grp /\ A e. X) -> (AP-u1) = (N` A))
Theorem	gxcom 8325	The group power operator commutes with the group operation. (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- P = (^g` G)   =>   |- ((G e. Grp /\ A e. X /\ K e. ZZ) -> ((APK)GA) = (AG(APK)))
Theorem	gxinv 8326	The group power operator commutes with the group inverse function. (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- N = (inv` G)   &   |- P = (^g` G)   =>   |- ((G e. Grp /\ A e. X /\ K e. ZZ) -> ((N` A)PK) = (N` (APK)))
Theorem	gxinv2 8327	The group power operator commutes with the group inverse function. (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- N = (inv` G)   &   |- P = (^g` G)   =>   |- ((G e. Grp /\ A e. X /\ K e. ZZ) -> (N` ((N` A)PK)) = (APK))
Theorem	gxsuc 8328	Induction on group power. (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- P = (^g` G)   =>   |- ((G e. Grp /\ A e. X /\ K e. ZZ) -> (AP(K + 1)) = ((APK)GA))
Theorem	gxid 8329	The identity element of a group to any power remains unchanged. (Contributed by Paul Chapman, 17-Apr-2009.)
|- U = (Id` G)   &   |- P = (^g` G)   =>   |- ((G e. Grp /\ K e. ZZ) -> (UPK) = U)
Theorem	gxnn0add 8330	The group power of a sum is the group product of the powers (lemma with nonnegative exponent - use gxadd 8331 instead). (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- P = (^g` G)   =>   |- ((G e. Grp /\ A e. X /\ (J e. ZZ /\ K e. NN0)) -> (AP(J + K)) = ((APJ)G(APK)))
Theorem	gxadd 8331	The group power of a sum is the group product of the powers. (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- P = (^g` G)   =>   |- ((G e. Grp /\ A e. X /\ (J e. ZZ /\ K e. ZZ)) -> (AP(J + K)) = ((APJ)G(APK)))
Theorem	gxsub 8332	The group power of a difference is the group quotient of the powers. (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- N = (inv` G)   &   |- P = (^g` G)   =>   |- ((G e. Grp /\ A e. X /\ (J e. ZZ /\ K e. ZZ)) -> (AP(J - K)) = ((APJ)G(N` (APK))))
Theorem	gxnn0mul 8333	The group power of a product is the composition of the powers (lemma with nonnegative exponent - use gxmul 8334 instead). (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- P = (^g` G)   =>   |- ((G e. Grp /\ A e. X /\ (J e. ZZ /\ K e. NN0)) -> (AP(J x. K)) = ((APJ)PK))
Theorem	gxmul 8334	The group power of a product is the composition of the powers. (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- P = (^g` G)   =>   |- ((G e. Grp /\ A e. X /\ (J e. ZZ /\ K e. ZZ)) -> (AP(J x. K)) = ((APJ)PK))
Theorem	gxmodid 8335	Casting out powers of the identity element leaves the group power unchanged. (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- U = (Id` G)   &   |- P = (^g` G)   =>   |- ((G e. Grp /\ (K e. ZZ /\ M e. NN) /\ (A e. X /\ (APM) = U)) -> (AP(K mod M)) = (APK))
Theorem	resgrprn 8336	The underlying set of a group operation which is a restriction of a mapping. (Contributed by Paul Chapman, 25-Mar-2008.)
|- H = (G |` (Y X. Y))   =>   |- ((dom G = (X X. X) /\ H e. Grp /\ Y (_ X) -> Y = ran H)
Theorem	grplactfval 8337	The left group action of element A of group G. (Contributed by Paul Chapman, 18-Mar-2008.)
|- F = {<.g, h>. | (g e. X /\ h = {<.a, b>. | (a e. X /\ b = (gGa))})}   &   |- X = ran G   =>   |- ((G e. Grp /\ A e. X) -> (F` A) = {<.a, b>. | (a e. X /\ b = (AGa))})
Theorem	grplactval 8338	The value of the left group action of element A of group G at B. (Contributed by Paul Chapman, 18-Mar-2008.)
|- F = {<.g, h>. | (g e. X /\ h = {<.a, b>. | (a e. X /\ b = (gGa))})}   &   |- X = ran G   =>   |- ((G e. Grp /\ A e. X /\ B e. X) -> ((F` A)` B) = (AGB))
Theorem	grplactf1o 8339	The left group action of element A of group G maps the underlying set X of G one-to-one onto itself. (Contributed by Paul Chapman, 18-Mar-2008.)
|- F = {<.g, h>. | (g e. X /\ h = {<.a, b>. | (a e. X /\ b = (gGa))})}   &   |- X = ran G   =>   |- ((G e. Grp /\ A e. X) -> (F` A):X-1-1-onto->X)
Definition and basic properties of Abelian groups
Syntax	cabl 8340	Extend class notation with the class of all Abelian group operations.
class Abel
Definition	df-abl 8341	Define the class of all Abelian group operations.
|- Abel = {g e. Grp | A.x e. ran gA.y e. ran g(xgy) = (ygx)}
Theorem	isabl 8342	The predicate "is an Abelian (commutative) group operation."
|- X = ran G   =>   |- (G e. Abel <-> (G e. Grp /\ A.x e. X A.y e. X (xGy) = (yGx)))
Theorem	ablgrp 8343	An Abelian group operation is a group operation.
|- (G e. Abel -> G e. Grp)
Theorem	ablcom 8344	An Abelian group operation is commutative.
|- X = ran G   =>   |- ((G e. Abel /\ A e. X /\ B e. X) -> (AGB) = (BGA))
Theorem	abl23 8345	Commutative/associative law for Abelian groups.
|- X = ran G   =>   |- ((G e. Abel /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGB)GC) = ((AGC)GB))
Theorem	abl4 8346	Commutative/associative law for Abelian groups.
|- X = ran G   =>   |- ((G e. Abel /\ (A e. X /\ B e. X) /\ (C e. X /\ D e. X)) -> ((AGB)G(CGD)) = ((AGC)G(BGD)))
Theorem	isabli 8347	Properties that determine an Abelian group operation.
|- G e. Grp   &   |- dom G = (X X. X)   &   |- ((x e. X /\ y e. X) -> (xGy) = (yGx))   =>   |- G e. Abel
Theorem	ablmuldiv 8348	Law for group multiplication and division.
|- X = ran G   &   |- D = ( /g ` G)   =>   |- ((G e. Abel /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGB)DC) = ((ADC)GB))
Theorem	abldivdiv 8349	Law for double group division.
|- X = ran G   &   |- D = ( /g ` G)   =>   |- ((G e. Abel /\ (A e. X /\ B e. X /\ C e. X)) -> (AD(BDC)) = ((ADB)GC))
Theorem	abldivdiv4 8350	Law for double group division.
|- X = ran G   &   |- D = ( /g ` G)   =>   |- ((G e. Abel /\ (A e. X /\ B e. X /\ C e. X)) -> ((ADB)DC) = (AD(BGC)))
Theorem	abldiv23 8351	Swap the second and third terms in a double division.
|- X = ran G   &   |- D = ( /g ` G)   =>   |- ((G e. Abel /\ (A e. X /\ B e. X /\ C e. X)) -> ((ADB)DC) = ((ADC)DB))
Theorem	ablnnncan 8352	Group theory analog of nnncan 5620.
|- X = ran G   &   |- D = ( /g ` G)   =>   |- ((G e. Abel /\ (A e. X /\ B e. X /\ C e. X)) -> ((AD(BDC))DC) = (ADB))
Theorem	ablnncan 8353	Group theory analog of nncan 5623.
|- X = ran G   &   |- D = ( /g ` G)   =>   |- ((G e. Abel /\ A e. X /\ B e. X) -> (AD(ADB)) = B)
Theorem	ablnnncan1 8354	Group theory analog of nnncan1 5621.
|- X = ran G   &   |- D = ( /g ` G)   =>   |- ((G e. Abel /\ (A e. X /\ B e. X /\ C e. X)) -> ((ADB)D(ADC)) = (CDB))
Theorem	gxdi 8355	Distribution of group power over group operation for abelian groups. (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- P = (^g` G)   =>   |- ((G e. Abel /\ (A e. X /\ B e. X) /\ K e. ZZ) -> ((AGB)PK) = ((APK)G(BPK)))
Subgroups
Syntax	csubg 8356	Extend class notation to include the class of subgroups.
class SubGrp
Definition	df-subg 8357	Define the set of subgroups of g.
|- SubGrp = {<.g, s>. | (g e. Grp /\ s = {h e. Grp | h (_ g})}
Theorem	issubg 8358	The predicate "is a subgroup of G." (Contributed by Paul Chapman, 3-Mar-2008.)
|- (H e. (SubGrp` G) <-> (G e. Grp /\ H e. Grp /\ H (_ G))
Theorem	subgres 8359	A subgroup operation is the restriction of its parent group operation to its underlying set. (Contributed by Paul Chapman, 3-Mar-2008.)
|- W = ran H   =>   |- (H e. (SubGrp` G) -> H = (G |` (W X. W)))
Theorem	subgopr 8360	The result of a subgroup operation is the same as the result of its parent operation. (Contributed by Paul Chapman, 3-Mar-2008.)
|- W = ran H   =>   |- (H e. (SubGrp` G) -> ((A e. W /\ B e. W) -> (AHB) = (AGB)))
Theorem	subgrnss 8361	The underlying set of a subgroup is a subset of its parent group's underlying set. (Contributed by Paul Chapman, 3-Mar-2008.)
|- X = ran G   &   |- W = ran H   =>   |- (H e. (SubGrp` G) -> W (_ X)
Theorem	subgid 8362	The identity element of a subgroup is the same as its parent's. (Contributed by Paul Chapman, 3-Mar-2008.)
|- U = (Id` G)   &   |- T = (Id` H)   =>   |- (H e. (SubGrp` G) -> T = U)
Theorem	issubgilem 8363	Lemma for issubgi 8364.
Theorem	issubgi 8364	Properties that determine a subgroup. (Contributed by Paul Chapman, 25-Feb-2008.)
|- G e. Grp   &   |- X = ran G   &   |- U = (Id` G)   &   |- N = (inv` G)   &   |- Y (_ X   &   |- H = (G |` (Y X. Y))   &   |- ((x e. Y /\ y e. Y) -> (xGy) e. Y)   &   |- U e. Y   &   |- (x e. Y -> (N` x) e. Y)   =>   |- H e. (SubGrp` G)
Theorem	subgabl 8365	A subgroup of an Abelian group is Abelian. (Contributed by Paul Chapman, 25-Apr-2008.)
|- ((G e. Abel /\ H e. (SubGrp` G)) -> H e. Abel)
Examples of Abelian groups
Theorem	ablsn 8366	The Abelian group operation for the singleton group.
|- A e. V   =>   |- {<.<.A, A>., A>.} e. Abel
Theorem	cnaddabl 8367	Complex number addition is an Abelian group operation.
|- + e. Abel
Theorem	cnid 8368	The group identity element of complex number addition is zero. (Contributed by Steve Rodriguez, 3-Dec-2006.)
|- 0 = (Id` + )
Theorem	addinv 8369	Value of the group inverse of complex number addition. (Contributed by Steve Rodriguez, 3-Dec-2006.)
|- (A e. CC -> ((inv` + )` A) = -uA)
Theorem	readdsubg 8370	The real numbers under addition comprise a subgroup of the complex numbers under addition. (Contributed by Paul Chapman, 25-Apr-2008.)
|- ( + |` (RR X. RR)) e. (SubGrp` + )
Theorem	zaddsubg 8371	The integers under addition comprise a subgroup of the complex numbers under addition. (Contributed by Paul Chapman, 25-Apr-2008.)
|- ( + |` (ZZ X. ZZ)) e. (SubGrp` + )
Theorem	ablmul 8372	Nonzero complex number multiplication is an Abelian group operation. (Contributed by Steve Rodriguez, 12-Feb-2007.)
|- ( x. |` ((CC \ {0}) X. (CC \ {0}))) e. Abel
Theorem	mulid 8373	The group identity element of nonzero complex number multiplication is one. (Contributed by Steve Rodriguez, 23-Feb-2007.)
|- (Id` ( x. |` ((CC \ {0}) X. (CC \ {0})))) = 1
Group homomorphism
Theorem	ghgrpilem1 8374	Lemma for ghgrpi 8378.
Theorem	ghgrpilem2 8375	Lemma for ghgrpi 8378.
Theorem	ghgrpilem3 8376	Lemma for ghgrpi 8378.
Theorem	ghgrpilem4 8377	Lemma for ghgrpi 8378.
Theorem	ghgrpi 8378	The image of a group G under a group homomorphism F is a group, and furthermore is Abelian if G is Abelian. This is a stronger result than that usually found in the literature, since the target of the homomorphism (operator O in our model) need not have any of the properties of a group as a prerequisite. (Contributed by Paul Chapman, 25-Apr-2008.)
|- G e. Grp   &   |- X = ran G   &   |- F:X-onto->Y   &   |- Y (_ A   &   |- O Fn (A X. A)   &   |- ((x e. X /\ y e. X) -> (F` (xGy)) = ((F` x)O(F` y)))   &   |- H = (O |` (Y X. Y))   =>   |- (H e. Grp /\ (G e. Abel -> H e. Abel))
Theorem	ghsubgi 8379	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 8380	Extend class notation with the class of all unital rings.
class Ring
Definition	df-ring 8381	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 8382	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 8383	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 8384	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 8385	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 8386	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.u e. X ((AHu) = A /\ (uHA) = A))
Theorem	ringideu 8387	The unit element of a ring is unique.
|- G = (1st` R)   &   |- H = (2nd` R)   &   |- X = ran G   =>   |- (R e. Ring -> E!u e. X A.x e. X ((xHu) = x /\ (uHx) = x))
Theorem	ringdi 8388	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 8389	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 8390	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 8391	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 8392	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 8393	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 8394	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 8395	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 8396	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 8397	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 8398	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 8399	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 8400	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))