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	ablfacrp 15301*	A finite abelian group whose order factors into relatively prime integers, itself "factors" into two subgroups K , L that have trivial intersection and whose product is the whole group. Lemma 6.1C.2 of [Shapiro], p. 199. (Contributed by Mario Carneiro, 19-Apr-2016.)
|- B = ( Base ` G )   &    |- O = ( od ` G )   &    |- K = { x e. B | ( O ` x ) || M }   &    |- L = { x e. B | ( O ` x ) || N }   &    |- ( ph -> G e. Abel )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N e. NN )   &    |- ( ph -> ( M gcd N ) = 1 )   &    |- ( ph -> ( # ` B ) = ( M x. N ) )   &    |- .0. = ( 0g ` G )   &    |- .(+) = ( LSSum ` G )   =>    |- ( ph -> ( ( K i^i L ) = { .0. } /\ ( K .(+) L ) = B ) )
Theorem	ablfacrp2 15302*	The factors K , L of ablfacrp 15301 have the expected orders (which allows for repeated application to decompose G into subgroups of prime-power order). Lemma 6.1C.2 of [Shapiro], p. 199. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- O = ( od ` G )   &    |- K = { x e. B | ( O ` x ) || M }   &    |- L = { x e. B | ( O ` x ) || N }   &    |- ( ph -> G e. Abel )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N e. NN )   &    |- ( ph -> ( M gcd N ) = 1 )   &    |- ( ph -> ( # ` B ) = ( M x. N ) )   =>    |- ( ph -> ( ( # ` K ) = M /\ ( # ` L ) = N ) )
Theorem	ablfac1lem 15303*	Lemma for ablfac1b 15305. Satisfy the assumptions of ablfacrp. (Contributed by Mario Carneiro, 26-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 )   &    |- M = ( P ^ ( P pCnt ( # ` B ) ) )   &    |- N = ( ( # ` B ) / M )   =>    |- ( ( ph /\ P e. A ) -> ( ( M e. NN /\ N e. NN ) /\ ( M gcd N ) = 1 /\ ( # ` B ) = ( M x. N ) ) )
Theorem	ablfac1a 15304*	The factors of ablfac1b 15305 are of prime power order. (Contributed by Mario Carneiro, 26-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 )   =>    |- ( ( ph /\ P e. A ) -> ( # ` ( S ` P ) ) = ( P ^ ( P pCnt ( # ` B ) ) ) )
Theorem	ablfac1b 15305*	Any abelian group is the direct product of factors of prime power order (with the exact order further matching the prime factorization of the group order). (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 )   =>    |- ( ph -> G dom DProd S )
Theorem	ablfac1c 15306*	The factors of ablfac1b 15305 cover the entire group. (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 DProd S ) = B )
Theorem	ablfac1eulem 15307*	Lemma for ablfac1eu 15308. (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 15308*	The factorization of ablfac1b 15305 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 15309*	Lemma for pgpfac1 15315. (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 15310*	Lemma for pgpfac1 15315. (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 15311*	Lemma for pgpfac1 15315. (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 15312*	Lemma for pgpfac1 15315. (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 15313*	Lemma for pgpfac1 15315. (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 15314*	Lemma for pgpfac1 15315 (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 15315*	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 15316*	Lemma for pgpfac 15319. (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 15317*	Lemma for pgpfac 15319. (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 15318*	Lemma for pgpfac 15319. (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 15319*	Full factorization of a finite abelian p-group, by iterating pgpfac1 15315. 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 15320*	Lemma for ablfac 15323. (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 15321*	Lemma for ablfac 15323. (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 15322*	Lemma for ablfac 15323. (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 15323*	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 15324*	Choose generators for each cyclic group in ablfac 15323. (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 15325	Multiplicative group.
class mulGrp
Definition	df-mgp 15326	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 15449 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 15347) or "the multiplicative identity" in terms of the identity of a monoid (df-1r 8687). (Contributed by Mario Carneiro, 21-Dec-2014.)
|- mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
Theorem	fnmgp 15327	The multiplicative group operator is a function. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- mulGrp Fn _V
Theorem	mgpval 15328	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 15329	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 15330	Lemma for mgpbas 15331. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- M = (mulGrp ` R )   &    |- E = Slot N   &    |- N e. NN   &    |- N =/= 2   =>    |- ( E ` R ) = ( E ` M )
Theorem	mgpbas 15331	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 15332	The multiplication monoid has the same (if any) scalars as the original ring. Mostly to simplify pwsmgp 15401. (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 15333	Topology component of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- M = (mulGrp ` R )   =>    |- (TopSet ` R ) = (TopSet ` M )
Theorem	mgptopn 15334	Topology of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- M = (mulGrp ` R )   &    |- J = ( TopOpen ` R )   =>    |- J = ( TopOpen ` M )
Theorem	mgpds 15335	Distance function of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- M = (mulGrp ` R )   &    |- B = ( dist ` R )   =>    |- B = ( dist ` M )
Theorem	mgpress 15336	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 15337	Extend class notation with class of all (unital) rings.
class Ring
Syntax	ccrg 15338	Extend class notation with class of all (unital) commutative rings.
class CRing
Syntax	cur 15339	Extend class notation with ring unit.
class 1r
Definition	df-rng 15340*	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 15369), 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 15341	Define class of all commutative rings. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- CRing = { f e. Ring | (mulGrp ` f ) e. CMnd }
Definition	df-ur 15342	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 15326). See also dfur2 15344, 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 15343	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 15344*	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 15345*	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 15346	A ring is a group. (Contributed by NM, 15-Sep-2011.)
|- ( R e. Ring -> R e. Grp )
Theorem	rngmgp 15347	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 15348	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 15349	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 15350	A ring is a monoid under addition. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- ( R e. Ring -> R e. Mnd )
Theorem	crngrng 15351	A commutative ring is a ring. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- ( R e. CRing -> R e. Ring )
Theorem	mgpf 15352	Restricted functionality of the multiplicative group on rings. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- (mulGrp |` Ring ) : Ring --> Mnd
Theorem	rngi 15353	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 15354	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 15355	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 15356*	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 15357	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 15358*	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 15359	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 15360	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 15361	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 15362	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 15363	Lemma for rnglidm 15364 and rngridm 15365. (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 15364	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 15365	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 15366*	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 15367	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 15368	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 15369	Commutativity of the additive group of a ring. (See also lmodcom 15671.) (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 15370	A ring is an Abelian group. (Contributed by NM, 26-Aug-2011.)
|- ( R e. Ring -> R e. Abel )
Theorem	rngcmn 15371	A ring is a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.)
|- ( R e. Ring -> R e. CMnd )
Theorem	rngpropd 15372*	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 15373*	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 15374	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 15375*	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 15376*	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 15377	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 15378	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 15379	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 15380	Negation in a ring is the same as left multiplication by -1. (rngonegmn1l 26580 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 15381	Negation in a ring is the same as right multiplication by -1. (rngonegmn1r 26581 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 15382	Negation of a product in a ring. (mulneg1 9216 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 15383	Negation of a product in a ring. (mulneg2 9217 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 15384	Double negation of a product in a ring. (mul2neg 9219 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 15385	Ring multiplication distributes over subtraction. (subdi 9213 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 15386	Ring multiplication distributes over subtraction. (subdir 9214 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 15387	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 15388*	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 15389*	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 15390*	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 15391*	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 15392*	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 15393	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 15394	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 15395	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 15396	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 15397	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 15398	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 15399	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 15400	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 )