P. 154 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 15301-15400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ablfac1eulem 15301*	Lemma for ablfac1eu 15302. (Contributed by Mario Carneiro, 27-Apr-2016.)
|- B = ( Base ` G )   &    |- O = ( od ` G )   &    |- S = ( p e. A |-> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> A C_ Prime )   &    |- D = { w e. Prime | w || ( # ` B ) }   &    |- ( ph -> D C_ A )   &    |- ( ph -> ( G dom DProd T /\ ( G DProd T ) = B ) )   &    |- ( ph -> dom T = A )   &    |- ( ( ph /\ q e. A ) -> C e. NN0 )   &    |- ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) = ( q ^ C ) )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> A e. Fin )   =>    |- ( ph -> -. P || ( # ` ( G DProd ( T |` ( A \ { P } ) ) ) ) )
Theorem	ablfac1eu 15302*	The factorization of ablfac1b 15299 is unique, in that any other factorization into prime power factors (even if the exponents are different) must be equal to S. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- O = ( od ` G )   &    |- S = ( p e. A |-> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> A C_ Prime )   &    |- D = { w e. Prime | w || ( # ` B ) }   &    |- ( ph -> D C_ A )   &    |- ( ph -> ( G dom DProd T /\ ( G DProd T ) = B ) )   &    |- ( ph -> dom T = A )   &    |- ( ( ph /\ q e. A ) -> C e. NN0 )   &    |- ( ( ph /\ q e. A ) -> ( # ` ( T ` q ) ) = ( q ^ C ) )   =>    |- ( ph -> T = S )
Theorem	pgpfac1lem1 15303*	Lemma for pgpfac1 15309. (Contributed by Mario Carneiro, 27-Apr-2016.)
|- K = (mrCls ` (SubGrp ` G ) )   &    |- S = ( K ` { A } )   &    |- B = ( Base ` G )   &    |- O = ( od ` G )   &    |- E = (gEx ` G )   &    |- .0. = ( 0g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- ( ph -> P pGrp G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> ( O ` A ) = E )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> A e. U )   &    |- ( ph -> W e. (SubGrp ` G ) )   &    |- ( ph -> ( S i^i W ) = { .0. } )   &    |- ( ph -> ( S .(+) W ) C_ U )   &    |- ( ph -> A. w e. (SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. ( S .(+) W ) C. w ) )   =>    |- ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> ( ( S .(+) W ) .(+) ( K ` { C } ) ) = U )
Theorem	pgpfac1lem2 15304*	Lemma for pgpfac1 15309. (Contributed by Mario Carneiro, 27-Apr-2016.)
|- K = (mrCls ` (SubGrp ` G ) )   &    |- S = ( K ` { A } )   &    |- B = ( Base ` G )   &    |- O = ( od ` G )   &    |- E = (gEx ` G )   &    |- .0. = ( 0g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- ( ph -> P pGrp G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> ( O ` A ) = E )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> A e. U )   &    |- ( ph -> W e. (SubGrp ` G ) )   &    |- ( ph -> ( S i^i W ) = { .0. } )   &    |- ( ph -> ( S .(+) W ) C_ U )   &    |- ( ph -> A. w e. (SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. ( S .(+) W ) C. w ) )   &    |- ( ph -> C e. ( U \ ( S .(+) W ) ) )   &    |- .x. = (.g ` G )   =>    |- ( ph -> ( P .x. C ) e. ( S .(+) W ) )
Theorem	pgpfac1lem3a 15305*	Lemma for pgpfac1 15309. (Contributed by Mario Carneiro, 4-Jun-2016.)
|- K = (mrCls ` (SubGrp ` G ) )   &    |- S = ( K ` { A } )   &    |- B = ( Base ` G )   &    |- O = ( od ` G )   &    |- E = (gEx ` G )   &    |- .0. = ( 0g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- ( ph -> P pGrp G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> ( O ` A ) = E )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> A e. U )   &    |- ( ph -> W e. (SubGrp ` G ) )   &    |- ( ph -> ( S i^i W ) = { .0. } )   &    |- ( ph -> ( S .(+) W ) C_ U )   &    |- ( ph -> A. w e. (SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. ( S .(+) W ) C. w ) )   &    |- ( ph -> C e. ( U \ ( S .(+) W ) ) )   &    |- .x. = (.g ` G )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> ( ( P .x. C ) ( +g ` G ) ( M .x. A ) ) e. W )   =>    |- ( ph -> ( P || E /\ P || M ) )
Theorem	pgpfac1lem3 15306*	Lemma for pgpfac1 15309. (Contributed by Mario Carneiro, 27-Apr-2016.)
|- K = (mrCls ` (SubGrp ` G ) )   &    |- S = ( K ` { A } )   &    |- B = ( Base ` G )   &    |- O = ( od ` G )   &    |- E = (gEx ` G )   &    |- .0. = ( 0g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- ( ph -> P pGrp G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> ( O ` A ) = E )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> A e. U )   &    |- ( ph -> W e. (SubGrp ` G ) )   &    |- ( ph -> ( S i^i W ) = { .0. } )   &    |- ( ph -> ( S .(+) W ) C_ U )   &    |- ( ph -> A. w e. (SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. ( S .(+) W ) C. w ) )   &    |- ( ph -> C e. ( U \ ( S .(+) W ) ) )   &    |- .x. = (.g ` G )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> ( ( P .x. C ) ( +g ` G ) ( M .x. A ) ) e. W )   &    |- D = ( C ( +g ` G ) ( ( M / P ) .x. A ) )   =>    |- ( ph -> E. t e. (SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) )
Theorem	pgpfac1lem4 15307*	Lemma for pgpfac1 15309. (Contributed by Mario Carneiro, 27-Apr-2016.)
|- K = (mrCls ` (SubGrp ` G ) )   &    |- S = ( K ` { A } )   &    |- B = ( Base ` G )   &    |- O = ( od ` G )   &    |- E = (gEx ` G )   &    |- .0. = ( 0g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- ( ph -> P pGrp G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> ( O ` A ) = E )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> A e. U )   &    |- ( ph -> W e. (SubGrp ` G ) )   &    |- ( ph -> ( S i^i W ) = { .0. } )   &    |- ( ph -> ( S .(+) W ) C_ U )   &    |- ( ph -> A. w e. (SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. ( S .(+) W ) C. w ) )   &    |- ( ph -> C e. ( U \ ( S .(+) W ) ) )   &    |- .x. = (.g ` G )   =>    |- ( ph -> E. t e. (SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) )
Theorem	pgpfac1lem5 15308*	Lemma for pgpfac1 15309 (Contributed by Mario Carneiro, 27-Apr-2016.)
|- K = (mrCls ` (SubGrp ` G ) )   &    |- S = ( K ` { A } )   &    |- B = ( Base ` G )   &    |- O = ( od ` G )   &    |- E = (gEx ` G )   &    |- .0. = ( 0g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- ( ph -> P pGrp G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> ( O ` A ) = E )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> A e. U )   &    |- ( ph -> A. s e. (SubGrp ` G ) ( ( s C. U /\ A e. s ) -> E. t e. (SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) )   =>    |- ( ph -> E. t e. (SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) )
Theorem	pgpfac1 15309*	Factorization of a finite abelian p-group. There is a direct product decomposition of any abelian group of prime-power order where one of the factors is cyclic and generated by an element of maximal order. (Contributed by Mario Carneiro, 27-Apr-2016.)
|- K = (mrCls ` (SubGrp ` G ) )   &    |- S = ( K ` { A } )   &    |- B = ( Base ` G )   &    |- O = ( od ` G )   &    |- E = (gEx ` G )   &    |- .0. = ( 0g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- ( ph -> P pGrp G )   &    |- ( ph -> G e. Abel )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> ( O ` A ) = E )   &    |- ( ph -> A e. B )   =>    |- ( ph -> E. t e. (SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = B ) )
Theorem	pgpfaclem1 15310*	Lemma for pgpfac 15313. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.)
|- B = ( Base ` G )   &    |- C = { r e. (SubGrp ` G ) | ( G ↾s r ) e. (CycGrp i^i ran pGrp ) }   &    |- ( ph -> G e. Abel )   &    |- ( ph -> P pGrp G )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> A. t e. (SubGrp ` G ) ( t C. U -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) )   &    |- H = ( G ↾s U )   &    |- K = (mrCls ` (SubGrp ` H ) )   &    |- O = ( od ` H )   &    |- E = (gEx ` H )   &    |- .0. = ( 0g ` H )   &    |- .(+) = ( LSSum ` H )   &    |- ( ph -> E =/= 1 )   &    |- ( ph -> X e. U )   &    |- ( ph -> ( O ` X ) = E )   &    |- ( ph -> W e. (SubGrp ` H ) )   &    |- ( ph -> ( ( K ` { X } ) i^i W ) = { .0. } )   &    |- ( ph -> ( ( K ` { X } ) .(+) W ) = U )   &    |- ( ph -> S e. Word C )   &    |- ( ph -> G dom DProd S )   &    |- ( ph -> ( G DProd S ) = W )   &    |- T = ( S concat <" ( K ` { X } ) "> )   =>    |- ( ph -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = U ) )
Theorem	pgpfaclem2 15311*	Lemma for pgpfac 15313. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.)
|- B = ( Base ` G )   &    |- C = { r e. (SubGrp ` G ) | ( G ↾s r ) e. (CycGrp i^i ran pGrp ) }   &    |- ( ph -> G e. Abel )   &    |- ( ph -> P pGrp G )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> A. t e. (SubGrp ` G ) ( t C. U -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) )   &    |- H = ( G ↾s U )   &    |- K = (mrCls ` (SubGrp ` H ) )   &    |- O = ( od ` H )   &    |- E = (gEx ` H )   &    |- .0. = ( 0g ` H )   &    |- .(+) = ( LSSum ` H )   &    |- ( ph -> E =/= 1 )   &    |- ( ph -> X e. U )   &    |- ( ph -> ( O ` X ) = E )   &    |- ( ph -> W e. (SubGrp ` H ) )   &    |- ( ph -> ( ( K ` { X } ) i^i W ) = { .0. } )   &    |- ( ph -> ( ( K ` { X } ) .(+) W ) = U )   =>    |- ( ph -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = U ) )
Theorem	pgpfaclem3 15312*	Lemma for pgpfac 15313. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.)
|- B = ( Base ` G )   &    |- C = { r e. (SubGrp ` G ) | ( G ↾s r ) e. (CycGrp i^i ran pGrp ) }   &    |- ( ph -> G e. Abel )   &    |- ( ph -> P pGrp G )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> A. t e. (SubGrp ` G ) ( t C. U -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) )   =>    |- ( ph -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = U ) )
Theorem	pgpfac 15313*	Full factorization of a finite abelian p-group, by iterating pgpfac1 15309. There is a direct product decomposition of any abelian group of prime-power order into cyclic subgroups. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.)
|- B = ( Base ` G )   &    |- C = { r e. (SubGrp ` G ) | ( G ↾s r ) e. (CycGrp i^i ran pGrp ) }   &    |- ( ph -> G e. Abel )   &    |- ( ph -> P pGrp G )   &    |- ( ph -> B e. Fin )   =>    |- ( ph -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = B ) )
Theorem	ablfaclem1 15314*	Lemma for ablfac 15317. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.)
|- B = ( Base ` G )   &    |- C = { r e. (SubGrp ` G ) | ( G ↾s r ) e. (CycGrp i^i ran pGrp ) }   &    |- ( ph -> G e. Abel )   &    |- ( ph -> B e. Fin )   &    |- O = ( od ` G )   &    |- A = { w e. Prime | w || ( # ` B ) }   &    |- S = ( p e. A |-> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } )   &    |- W = ( g e. (SubGrp ` G ) |-> { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = g ) } )   =>    |- ( U e. (SubGrp ` G ) -> ( W ` U ) = { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = U ) } )
Theorem	ablfaclem2 15315*	Lemma for ablfac 15317. (Contributed by Mario Carneiro, 27-Apr-2016.) (Proof shortened by Mario Carneiro, 3-May-2016.)
|- B = ( Base ` G )   &    |- C = { r e. (SubGrp ` G ) | ( G ↾s r ) e. (CycGrp i^i ran pGrp ) }   &    |- ( ph -> G e. Abel )   &    |- ( ph -> B e. Fin )   &    |- O = ( od ` G )   &    |- A = { w e. Prime | w || ( # ` B ) }   &    |- S = ( p e. A |-> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } )   &    |- W = ( g e. (SubGrp ` G ) |-> { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = g ) } )   &    |- ( ph -> F : A -->Word C )   &    |- ( ph -> A. y e. A ( F ` y ) e. ( W ` ( S ` y ) ) )   &    |- L = U_ y e. A ( { y } X. dom ( F ` y ) )   &    |- ( ph -> H : ( 0..^ ( # ` L ) ) -1-1-onto-> L )   =>    |- ( ph -> ( W ` B ) =/= (/) )
Theorem	ablfaclem3 15316*	Lemma for ablfac 15317. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.)
|- B = ( Base ` G )   &    |- C = { r e. (SubGrp ` G ) | ( G ↾s r ) e. (CycGrp i^i ran pGrp ) }   &    |- ( ph -> G e. Abel )   &    |- ( ph -> B e. Fin )   &    |- O = ( od ` G )   &    |- A = { w e. Prime | w || ( # ` B ) }   &    |- S = ( p e. A |-> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } )   &    |- W = ( g e. (SubGrp ` G ) |-> { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = g ) } )   =>    |- ( ph -> ( W ` B ) =/= (/) )
Theorem	ablfac 15317*	The Fundamental Theorem of (finite) Abelian Groups. Any finite abelian group is a direct product of cyclic p-groups. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.)
|- B = ( Base ` G )   &    |- C = { r e. (SubGrp ` G ) | ( G ↾s r ) e. (CycGrp i^i ran pGrp ) }   &    |- ( ph -> G e. Abel )   &    |- ( ph -> B e. Fin )   =>    |- ( ph -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = B ) )
Theorem	ablfac2 15318*	Choose generators for each cyclic group in ablfac 15317. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- B = ( Base ` G )   &    |- C = { r e. (SubGrp ` G ) | ( G ↾s r ) e. (CycGrp i^i ran pGrp ) }   &    |- ( ph -> G e. Abel )   &    |- ( ph -> B e. Fin )   &    |- .x. = (.g ` G )   &    |- S = ( k e. dom w |-> ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) )   =>    |- ( ph -> E. w e. Word B ( S : dom w --> C /\ G dom DProd S /\ ( G DProd S ) = B ) )
10.4  Rings
10.4.1  Multiplicative Group
Syntax	cmgp 15319	Multiplicative group.
class mulGrp
Definition	df-mgp 15320	Define a structure that puts the multiplication operation of a ring in the addition slot. Note that this will not actually be a group for the average ring, or even for a field, but it will be a monoid, and unitgrp 15443 shows that we get a group if we restrict to the elements that have inverses. This allows us to formalize such notions as "the multiplication operation of a ring is a monoid" (rngmgp 15341) or "the multiplicative identity" in terms of the identity of a monoid (df-1r 8682). (Contributed by Mario Carneiro, 21-Dec-2014.)
|- mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
Theorem	fnmgp 15321	The multiplicative group operator is a function. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- mulGrp Fn _V
Theorem	mgpval 15322	Value of the multiplication group operation. (Contributed by Mario Carneiro, 21-Dec-2014.)
|- M = (mulGrp ` R )   &    |- .x. = ( .r ` R )   =>    |- M = ( R sSet <. ( +g ` ndx ) , .x. >. )
Theorem	mgpplusg 15323	Value of the group operation of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.)
|- M = (mulGrp ` R )   &    |- .x. = ( .r ` R )   =>    |- .x. = ( +g ` M )
Theorem	mgplem 15324	Lemma for mgpbas 15325. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- M = (mulGrp ` R )   &    |- E = Slot N   &    |- N e. NN   &    |- N =/= 2   =>    |- ( E ` R ) = ( E ` M )
Theorem	mgpbas 15325	Base set of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.) (Revised by Mario Carneiro, 5-Oct-2015.)
|- M = (mulGrp ` R )   &    |- B = ( Base ` R )   =>    |- B = ( Base ` M )
Theorem	mgpsca 15326	The multiplication monoid has the same (if any) scalars as the original ring. Mostly to simplify pwsmgp 15395. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 5-May-2015.)
|- M = (mulGrp ` R )   &    |- S = (Scalar ` R )   =>    |- S = (Scalar ` M )
Theorem	mgptset 15327	Topology component of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- M = (mulGrp ` R )   =>    |- (TopSet ` R ) = (TopSet ` M )
Theorem	mgptopn 15328	Topology of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- M = (mulGrp ` R )   &    |- J = ( TopOpen ` R )   =>    |- J = ( TopOpen ` M )
Theorem	mgpds 15329	Distance function of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- M = (mulGrp ` R )   &    |- B = ( dist ` R )   =>    |- B = ( dist ` M )
Theorem	mgpress 15330	Subgroup commutes with the multiplication group operator. (Contributed by Mario Carneiro, 10-Jan-2015.)
|- S = ( R ↾s A )   &    |- M = (mulGrp ` R )   =>    |- ( ( R e. V /\ A e. W ) -> ( M ↾s A ) = (mulGrp ` S ) )
10.4.2  Definition and basic properties
Syntax	crg 15331	Extend class notation with class of all (unital) rings.
class Ring
Syntax	ccrg 15332	Extend class notation with class of all (unital) commutative rings.
class CRing
Syntax	cur 15333	Extend class notation with ring unit.
class 1r
Definition	df-rng 15334*	Define class of all (unital) rings. A unital ring is a set equipped with two everywhere-defined internal operations, whose first one is an additive group structure and the second one is a multiplicative monoid structure, and where the addition is left- and right-distributive for the multiplication. So that the additive structure must be abelian (see rngcom 15363), care must be taken that in the case of a non-unital ring, the commutativity of addition must be postulated and cannot be proved from the other conditions. (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- Ring = { f e. Grp | ( (mulGrp ` f ) e. Mnd /\ [. ( Base ` f ) / r ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. A. x e. r A. y e. r A. z e. r ( ( x t ( y p z ) ) = ( ( x t y ) p ( x t z ) ) /\ ( ( x p y ) t z ) = ( ( x t z ) p ( y t z ) ) ) ) }
Definition	df-cring 15335	Define class of all commutative rings. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- CRing = { f e. Ring | (mulGrp ` f ) e. CMnd }
Definition	df-ur 15336	Define the multiplicative neutral element of a ring. This definition works by extracting the 0g element, i.e. the neutral element in a group or monoid, and transfering it to the multiplicative monoid via the mulGrp function (df-mgp 15320). See also dfur2 15338, which derives the "traditional" definition as the unique element of a ring which is left- and right-neutral under multiplication. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- 1r = ( 0g o. mulGrp )
Theorem	rngidval 15337	The value of the unity element of a ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- G = (mulGrp ` R )   &    |- .1. = ( 1r ` R )   =>    |- .1. = ( 0g ` G )
Theorem	dfur2 15338*	The multiplicative identity is the unique element of the ring that is left- and right-neutral on all elements under multiplication. (Contributed by Mario Carneiro, 10-Jan-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   =>    |- .1. = ( iota e ( e e. B /\ A. x e. B ( ( e .x. x ) = x /\ ( x .x. e ) = x ) ) )
Theorem	isrng 15339*	The predicate "is a (unital) ring." Definition of ring with unit in [Schechter] p. 187. (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` R )   &    |- G = (mulGrp ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   =>    |- ( R e. Ring <-> ( R e. Grp /\ G e. Mnd /\ A. x e. B A. y e. B A. z e. B ( ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) /\ ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) ) )
Theorem	rnggrp 15340	A ring is a group. (Contributed by NM, 15-Sep-2011.)
|- ( R e. Ring -> R e. Grp )
Theorem	rngmgp 15341	A ring is a monoid under multiplication. (Contributed by Mario Carneiro, 6-Jan-2015.)
|- G = (mulGrp ` R )   =>    |- ( R e. Ring -> G e. Mnd )
Theorem	iscrng 15342	A commutative ring is a ring whose multiplication is a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- G = (mulGrp ` R )   =>    |- ( R e. CRing <-> ( R e. Ring /\ G e. CMnd ) )
Theorem	crngmgp 15343	A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- G = (mulGrp ` R )   =>    |- ( R e. CRing -> G e. CMnd )
Theorem	rngmnd 15344	A ring is a monoid under addition. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- ( R e. Ring -> R e. Mnd )
Theorem	crngrng 15345	A commutative ring is a ring. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- ( R e. CRing -> R e. Ring )
Theorem	mgpf 15346	Restricted functionality of the multiplicative group on rings. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- (mulGrp |` Ring ) : Ring --> Mnd
Theorem	rngi 15347	Properties of a unital ring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .x. ( Y .+ Z ) ) = ( ( X .x. Y ) .+ ( X .x. Z ) ) /\ ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) ) )
Theorem	rngcl 15348	Closure of the multiplication operation of a ring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( X .x. Y ) e. B )
Theorem	crngcom 15349	A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( X .x. Y ) = ( Y .x. X ) )
Theorem	iscrng2 15350*	A commutative ring is a ring whose multiplication is a commutative monoid. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( R e. CRing <-> ( R e. Ring /\ A. x e. B A. y e. B ( x .x. y ) = ( y .x. x ) ) )
Theorem	rngass 15351	Associative law for the multiplication operation of a ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .x. Y ) .x. Z ) = ( X .x. ( Y .x. Z ) ) )
Theorem	rngideu 15352*	The unit element of a ring is unique. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( R e. Ring -> E! u e. B A. x e. B ( ( u .x. x ) = x /\ ( x .x. u ) = x ) )
Theorem	rngdi 15353	Distributive law for the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .x. ( Y .+ Z ) ) = ( ( X .x. Y ) .+ ( X .x. Z ) ) )
Theorem	rngdir 15354	Distributive law for the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) )
Theorem	rngidcl 15355	The unit element of a ring belongs to the base set of the ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- B = ( Base ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> .1. e. B )
Theorem	rng0cl 15356	The zero element of a ring belongs to its base set. (Contributed by Mario Carneiro, 12-Jan-2014.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. Ring -> .0. e. B )
Theorem	rngidmlem 15357	Lemma for rnglidm 15358 and rngridm 15359. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> ( ( .1. .x. X ) = X /\ ( X .x. .1. ) = X ) )
Theorem	rnglidm 15358	The unit element of a ring is a left multiplicative identity. (Contributed by NM, 15-Sep-2011.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> ( .1. .x. X ) = X )
Theorem	rngridm 15359	The unit element of a ring is a right multiplicative identity. (Contributed by NM, 15-Sep-2011.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> ( X .x. .1. ) = X )
Theorem	isrngid 15360*	Properties showing that an element I is the unity element of a ring. (Contributed by NM, 7-Aug-2013.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> ( ( I e. B /\ A. x e. B ( ( I .x. x ) = x /\ ( x .x. I ) = x ) ) <-> .1. = I ) )
Theorem	rngidss 15361	A subset of the multiplicative group has the multiplicative identity as its identity if the identity is in the subset. (Contributed by Mario Carneiro, 27-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- M = ( (mulGrp ` R ) ↾s A )   &    |- B = ( Base ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ A C_ B /\ .1. e. A ) -> .1. = ( 0g ` M ) )
Theorem	rngacl 15362	Closure of the addition operation of a ring. (Contributed by Mario Carneiro, 14-Jan-2014.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   =>    |- ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
Theorem	rngcom 15363	Commutativity of the additive group of a ring. (See also lmodcom 15665.) (Contributed by Gérard Lang, 4-Dec-2014.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   =>    |- ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( X .+ Y ) = ( Y .+ X ) )
Theorem	rngabl 15364	A ring is an Abelian group. (Contributed by NM, 26-Aug-2011.)
|- ( R e. Ring -> R e. Abel )
Theorem	rngcmn 15365	A ring is a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- ( R e. Ring -> R e. CMnd )
Theorem	rngpropd 15366*	If two structures have the same group components (properties), one is a ring iff the other one is. (Contributed by Mario Carneiro, 6-Dec-2014.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )   =>    |- ( ph -> ( K e. Ring <-> L e. Ring ) )
Theorem	crngpropd 15367*	If two structures have the same group components (properties), one is a commutative ring iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )   =>    |- ( ph -> ( K e. CRing <-> L e. CRing ) )
Theorem	rngprop 15368	If two structures have the same ring components (properties), one is a ring iff the other one is. (Contributed by Mario Carneiro, 11-Oct-2013.)
|- ( Base ` K ) = ( Base ` L )   &    |- ( +g ` K ) = ( +g ` L )   &    |- ( .r ` K ) = ( .r ` L )   =>    |- ( K e. Ring <-> L e. Ring )
Theorem	isrngd 15369*	Properties that determine a ring. (Contributed by NM, 2-Aug-2013.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> .+ = ( +g ` R ) )   &    |- ( ph -> .x. = ( .r ` R ) )   &    |- ( ph -> R e. Grp )   &    |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .x. y ) e. B )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )   &    |- ( ph -> .1. e. B )   &    |- ( ( ph /\ x e. B ) -> ( .1. .x. x ) = x )   &    |- ( ( ph /\ x e. B ) -> ( x .x. .1. ) = x )   =>    |- ( ph -> R e. Ring )
Theorem	iscrngd 15370*	Properties that determine a commutative ring. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> .+ = ( +g ` R ) )   &    |- ( ph -> .x. = ( .r ` R ) )   &    |- ( ph -> R e. Grp )   &    |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .x. y ) e. B )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )   &    |- ( ph -> .1. e. B )   &    |- ( ( ph /\ x e. B ) -> ( .1. .x. x ) = x )   &    |- ( ( ph /\ x e. B ) -> ( x .x. .1. ) = x )   &    |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .x. y ) = ( y .x. x ) )   =>    |- ( ph -> R e. CRing )
Theorem	rnglz 15371	The zero of a unital ring is a left absorbing element. (Contributed by FL, 31-Aug-2009.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> ( .0. .x. X ) = .0. )
Theorem	rngrz 15372	The zero of a unital ring is a right absorbing element. (Contributed by FL, 31-Aug-2009.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> ( X .x. .0. ) = .0. )
Theorem	rng1eq0 15373	If one and zero are equal, then any two elements of a ring are equal. Alternatively, every ring has one distinct from zero except the zero ring containing the single element { 0 }. (Contributed by Mario Carneiro, 10-Sep-2014.)
|- B = ( Base ` R )   &    |- .1. = ( 1r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( .1. = .0. -> X = Y ) )
Theorem	rngnegl 15374	Negation in a ring is the same as left multiplication by -1. (rngonegmn1l 25979 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   &    |- N = ( inv g ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( ( N ` .1. ) .x. X ) = ( N ` X ) )
Theorem	rngnegr 15375	Negation in a ring is the same as right multiplication by -1. (rngonegmn1r 25980 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   &    |- N = ( inv g ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( X .x. ( N ` .1. ) ) = ( N ` X ) )
Theorem	rngmneg1 15376	Negation of a product in a ring. (mulneg1 9211 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- N = ( inv g ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( ( N ` X ) .x. Y ) = ( N ` ( X .x. Y ) ) )
Theorem	rngmneg2 15377	Negation of a product in a ring. (mulneg2 9212 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- N = ( inv g ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X .x. ( N ` Y ) ) = ( N ` ( X .x. Y ) ) )
Theorem	rngm2neg 15378	Double negation of a product in a ring. (mul2neg 9214 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- N = ( inv g ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( ( N ` X ) .x. ( N ` Y ) ) = ( X .x. Y ) )
Theorem	rngsubdi 15379	Ring multiplication distributes over subtraction. (subdi 9208 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .- = ( -g ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( X .x. ( Y .- Z ) ) = ( ( X .x. Y ) .- ( X .x. Z ) ) )
Theorem	rngsubdir 15380	Ring multiplication distributes over subtraction. (subdir 9209 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .- = ( -g ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .- Y ) .x. Z ) = ( ( X .x. Z ) .- ( Y .x. Z ) ) )
Theorem	mulgass2 15381	An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- B = ( Base ` R )   &    |- .x. = (.g ` R )   &    |- .X. = ( .r ` R )   =>    |- ( ( R e. Ring /\ ( N e. ZZ /\ X e. B /\ Y e. B ) ) -> ( ( N .x. X ) .X. Y ) = ( N .x. ( X .X. Y ) ) )
Theorem	rnglghm 15382*	Left-multiplication in a ring by a fixed element of the ring is a group homomorphism. (It is not usually a ring homomorphism.) (Contributed by Mario Carneiro, 4-May-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> ( x e. B |-> ( X .x. x ) ) e. ( R GrpHom R ) )
Theorem	rngrghm 15383*	Right-multiplication in a ring by a fixed element of the ring is a group homomorphism. (It is not usually a ring homomorphism.) (Contributed by Mario Carneiro, 4-May-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> ( x e. B |-> ( x .x. X ) ) e. ( R GrpHom R ) )
Theorem	gsummulc1 15384*	A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> A e. V )   &    |- ( ph -> Y e. B )   &    |- ( ( ph /\ k e. A ) -> X e. B )   &    |- ( ph -> ( `' ( k e. A |-> X ) " ( _V \ { .0. } ) ) e. Fin )   =>    |- ( ph -> ( R gsumg ( k e. A |-> ( X .x. Y ) ) ) = ( ( R gsumg ( k e. A |-> X ) ) .x. Y ) )
Theorem	gsummulc2 15385*	A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> A e. V )   &    |- ( ph -> Y e. B )   &    |- ( ( ph /\ k e. A ) -> X e. B )   &    |- ( ph -> ( `' ( k e. A |-> X ) " ( _V \ { .0. } ) ) e. Fin )   =>    |- ( ph -> ( R gsumg ( k e. A |-> ( Y .x. X ) ) ) = ( Y .x. ( R gsumg ( k e. A |-> X ) ) ) )
Theorem	gsumdixp 15386*	Distribute a binary product of sums to a sum of binary products in a ring. (Contributed by Mario Carneiro, 8-Mar-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   &    |- ( ph -> I e. V )   &    |- ( ph -> J e. W )   &    |- ( ph -> R e. Ring )   &    |- ( ( ph /\ x e. I ) -> X e. B )   &    |- ( ( ph /\ y e. J ) -> Y e. B )   &    |- ( ph -> ( `' ( x e. I |-> X ) " ( _V \ { .0. } ) ) e. Fin )   &    |- ( ph -> ( `' ( y e. J |-> Y ) " ( _V \ { .0. } ) ) e. Fin )   =>    |- ( ph -> ( ( R gsumg ( x e. I |-> X ) ) .x. ( R gsumg ( y e. J |-> Y ) ) ) = ( R gsumg ( x e. I , y e. J |-> ( X .x. Y ) ) ) )
Theorem	prdsmgp 15387	The multiplicative monoid of a product is the product of the multiplicative monoids of the factors. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- Y = ( S X_s R )   &    |- M = (mulGrp ` Y )   &    |- Z = ( S X_s (mulGrp o. R ) )   &    |- ( ph -> I e. V )   &    |- ( ph -> S e. W )   &    |- ( ph -> R Fn I )   =>    |- ( ph -> ( ( Base ` M ) = ( Base ` Z ) /\ ( +g ` M ) = ( +g ` Z ) ) )
Theorem	prdsmulrcl 15388	A structure product of rings has closed binary operation. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- Y = ( S X_s R )   &    |- B = ( Base ` Y )   &    |- .x. = ( .r ` Y )   &    |- ( ph -> S e. V )   &    |- ( ph -> I e. W )   &    |- ( ph -> R : I --> Ring )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. B )   =>    |- ( ph -> ( F .x. G ) e. B )
Theorem	prdsrngd 15389	A product of rings is a ring. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- Y = ( S X_s R )   &    |- ( ph -> I e. W )   &    |- ( ph -> S e. V )   &    |- ( ph -> R : I --> Ring )   =>    |- ( ph -> Y e. Ring )
Theorem	prdscrngd 15390	A product of commutative rings is a commutative ring. Since the resulting ring will have zero divisors in all nontrivial cases, this cannot be strengthened much further. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- Y = ( S X_s R )   &    |- ( ph -> I e. W )   &    |- ( ph -> S e. V )   &    |- ( ph -> R : I --> CRing )   =>    |- ( ph -> Y e. CRing )
Theorem	prds1 15391	Value of the ring unit in a structure family product. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- Y = ( S X_s R )   &    |- ( ph -> I e. W )   &    |- ( ph -> S e. V )   &    |- ( ph -> R : I --> Ring )   =>    |- ( ph -> ( 1r o. R ) = ( 1r ` Y ) )
Theorem	pwsrng 15392	A structure power of a ring is a ring. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- Y = ( R ^s I )   =>    |- ( ( R e. Ring /\ I e. V ) -> Y e. Ring )
Theorem	pws1 15393	Value of the ring unit in a structure power. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- Y = ( R ^s I )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ I e. V ) -> ( I X. { .1. } ) = ( 1r ` Y ) )
Theorem	pwscrng 15394	A structure power of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- Y = ( R ^s I )   =>    |- ( ( R e. CRing /\ I e. V ) -> Y e. CRing )
Theorem	pwsmgp 15395	The multiplicative group of the power structure resembles the power of the multiplicative group. (Contributed by Mario Carneiro, 12-Mar-2015.)
|- Y = ( R ^s I )   &    |- M = (mulGrp ` R )   &    |- Z = ( M ^s I )   &    |- N = (mulGrp ` Y )   &    |- B = ( Base ` N )   &    |- C = ( Base ` Z )   &    |- .+ = ( +g ` N )   &    |- .+b = ( +g ` Z )   =>    |- ( ( R e. V /\ I e. W ) -> ( B = C /\ .+ = .+b ) )
Theorem	imasrng 15396*	The image structure of a ring is a ring. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) ) )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> R e. Ring )   =>    |- ( ph -> ( U e. Ring /\ ( F ` .1. ) = ( 1r ` U ) ) )
Theorem	divsrng2 15397*	The quotient structure of a ring is a ring. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   &    |- ( ph -> .~ Er V )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .+ b ) .~ ( p .+ q ) ) )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )   &    |- ( ph -> R e. Ring )   =>    |- ( ph -> ( U e. Ring /\ [ .1. ] .~ = ( 1r ` U ) ) )
10.4.3  Opposite ring
Syntax	coppr 15398	The opposite ring operation.
class oppr
Definition	df-oppr 15399	Define an opposite ring, which is the same as the original ring but with multiplication written the other way around. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- oppr = ( f e. _V |-> ( f sSet <. ( .r ` ndx ) , tpos ( .r ` f ) >. ) )
Theorem	opprval 15400	Value of the opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- O = (oppr ` R )   =>    |- O = ( R sSet <. ( .r ` ndx ) , tpos .x. >. )