P. 185 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18401-18500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dprdval0prc 18401	The internal direct product of a family of subgroups indexed by a proper class is empty. (Contributed by AV, 13-Jul-2019.)
|- ( dom S e/ _V -> ( G DProd S ) = (/) )
Theorem	dprdval 18402*	The value of the internal direct product operation, which is a function mapping the (infinite, but finitely supported) cartesian product of subgroups (which mutually commute and have trivial intersections) to its (group) sum . (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.)
|- .0. = ( 0g ` G )   &    |- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }   =>    |- ( ( G dom DProd S /\ dom S = I ) -> ( G DProd S ) = ran ( f e. W |-> ( G gsumg f ) ) )
Theorem	eldprd 18403*	A class A is an internal direct product iff it is the (group) sum of an infinite, but finitely supported cartesian product of subgroups (which mutually commute and have trivial intersections). (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.)
|- .0. = ( 0g ` G )   &    |- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }   =>    |- ( dom S = I -> ( A e. ( G DProd S ) <-> ( G dom DProd S /\ E. f e. W A = ( G gsumg f ) ) ) )
Theorem	dprdgrp 18404	Reverse closure for the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- ( G dom DProd S -> G e. Grp )
Theorem	dprdf 18405	The function S is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- ( G dom DProd S -> S : dom S --> (SubGrp ` G ) )
Theorem	dprdf2 18406	The function S is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   =>    |- ( ph -> S : I --> (SubGrp ` G ) )
Theorem	dprdcntz 18407	The function S is a family having pairwise commuting values. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> X e. I )   &    |- ( ph -> Y e. I )   &    |- ( ph -> X =/= Y )   &    |- Z = (Cntz ` G )   =>    |- ( ph -> ( S ` X ) C_ ( Z ` ( S ` Y ) ) )
Theorem	dprddisj 18408	The function S is a family having trivial intersections. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> X e. I )   &    |- .0. = ( 0g ` G )   &    |- K = (mrCls ` (SubGrp ` G ) )   =>    |- ( ph -> ( ( S ` X ) i^i ( K ` U. ( S " ( I \ { X } ) ) ) ) = { .0. } )
Theorem	dprdw 18409*	The property of being a finitely supported function in the family S. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.)
|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }   &    |- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   =>    |- ( ph -> ( F e. W <-> ( F Fn I /\ A. x e. I ( F ` x ) e. ( S ` x ) /\ F finSupp .0. ) ) )
Theorem	dprdwd 18410*	A mapping being a finitely supported function in the family S. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.) (Proof shortened by OpenAI, 30-Mar-2020.)
|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }   &    |- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ( ph /\ x e. I ) -> A e. ( S ` x ) )   &    |- ( ph -> ( x e. I |-> A ) finSupp .0. )   =>    |- ( ph -> ( x e. I |-> A ) e. W )
Theorem	dprdff 18411*	A finitely supported function in S is a function into the base. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.)
|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }   &    |- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> F e. W )   &    |- B = ( Base ` G )   =>    |- ( ph -> F : I --> B )
Theorem	dprdfcl 18412*	A finitely supported function in S has its X-th element in S ( X ). (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.)
|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }   &    |- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> F e. W )   =>    |- ( ( ph /\ X e. I ) -> ( F ` X ) e. ( S ` X ) )
Theorem	dprdffsupp 18413*	A finitely supported function in S is a finitely supported function. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.)
|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }   &    |- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> F e. W )   =>    |- ( ph -> F finSupp .0. )
Theorem	dprdfcntz 18414*	A function on the elements of an internal direct product has pairwise commuting values. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.)
|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }   &    |- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> F e. W )   &    |- Z = (Cntz ` G )   =>    |- ( ph -> ran F C_ ( Z ` ran F ) )
Theorem	dprdssv 18415	The internal direct product of a family of subgroups is a subset of the base. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- B = ( Base ` G )   =>    |- ( G DProd S ) C_ B
Theorem	dprdfid 18416*	A function mapping all but one arguments to zero sums to the value of this argument in a direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.)
|- .0. = ( 0g ` G )   &    |- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }   &    |- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> X e. I )   &    |- ( ph -> A e. ( S ` X ) )   &    |- F = ( n e. I |-> if ( n = X , A , .0. ) )   =>    |- ( ph -> ( F e. W /\ ( G gsumg F ) = A ) )
Theorem	eldprdi 18417*	The domain of definition of the internal direct product, which states that S is a family of subgroups that mutually commute and have trivial intersections. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.)
|- .0. = ( 0g ` G )   &    |- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }   &    |- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> F e. W )   =>    |- ( ph -> ( G gsumg F ) e. ( G DProd S ) )
Theorem	dprdfinv 18418*	Take the inverse of a group sum over a family of elements of disjoint subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.)
|- .0. = ( 0g ` G )   &    |- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }   &    |- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> F e. W )   &    |- N = ( invg ` G )   =>    |- ( ph -> ( ( N o. F ) e. W /\ ( G gsumg ( N o. F ) ) = ( N ` ( G gsumg F ) ) ) )
Theorem	dprdfadd 18419*	Take the sum of group sums over two families of elements of disjoint subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.)
|- .0. = ( 0g ` G )   &    |- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }   &    |- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> F e. W )   &    |- ( ph -> H e. W )   &    |- .+ = ( +g ` G )   =>    |- ( ph -> ( ( F oF .+ H ) e. W /\ ( G gsumg ( F oF .+ H ) ) = ( ( G gsumg F ) .+ ( G gsumg H ) ) ) )
Theorem	dprdfsub 18420*	Take the difference of group sums over two families of elements of disjoint subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.)
|- .0. = ( 0g ` G )   &    |- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }   &    |- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> F e. W )   &    |- ( ph -> H e. W )   &    |- .- = ( -g ` G )   =>    |- ( ph -> ( ( F oF .- H ) e. W /\ ( G gsumg ( F oF .- H ) ) = ( ( G gsumg F ) .- ( G gsumg H ) ) ) )
Theorem	dprdfeq0 18421*	The zero function is the only function that sums to zero in a direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.)
|- .0. = ( 0g ` G )   &    |- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }   &    |- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> F e. W )   =>    |- ( ph -> ( ( G gsumg F ) = .0. <-> F = ( x e. I |-> .0. ) ) )
Theorem	dprdf11 18422*	Two group sums over a direct product that give the same value are equal as functions. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.)
|- .0. = ( 0g ` G )   &    |- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }   &    |- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> F e. W )   &    |- ( ph -> H e. W )   =>    |- ( ph -> ( ( G gsumg F ) = ( G gsumg H ) <-> F = H ) )
Theorem	dprdsubg 18423	The internal direct product of a family of subgroups is a subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- ( G dom DProd S -> ( G DProd S ) e. (SubGrp ` G ) )
Theorem	dprdub 18424	Each factor is a subset of the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> X e. I )   =>    |- ( ph -> ( S ` X ) C_ ( G DProd S ) )
Theorem	dprdlub 18425*	The direct product is smaller than any subgroup which contains the factors. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ( ph /\ k e. I ) -> ( S ` k ) C_ T )   =>    |- ( ph -> ( G DProd S ) C_ T )
Theorem	dprdspan 18426	The direct product is the span of the union of the factors. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- K = (mrCls ` (SubGrp ` G ) )   =>    |- ( G dom DProd S -> ( G DProd S ) = ( K ` U. ran S ) )
Theorem	dprdres 18427	Restriction of a direct product (dropping factors). (Contributed by Mario Carneiro, 25-Apr-2016.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> A C_ I )   =>    |- ( ph -> ( G dom DProd ( S |` A ) /\ ( G DProd ( S |` A ) ) C_ ( G DProd S ) ) )
Theorem	dprdss 18428*	Create a direct product by finding subgroups inside each factor of another direct product. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- ( ph -> G dom DProd T )   &    |- ( ph -> dom T = I )   &    |- ( ph -> S : I --> (SubGrp ` G ) )   &    |- ( ( ph /\ k e. I ) -> ( S ` k ) C_ ( T ` k ) )   =>    |- ( ph -> ( G dom DProd S /\ ( G DProd S ) C_ ( G DProd T ) ) )
Theorem	dprdz 18429*	A family consisting entirely of trivial groups is an internal direct product, the product of which is the trivial subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ I e. V ) -> ( G dom DProd ( x e. I |-> { .0. } ) /\ ( G DProd ( x e. I |-> { .0. } ) ) = { .0. } ) )
Theorem	dprd0 18430	The empty family is an internal direct product, the product of which is the trivial subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- .0. = ( 0g ` G )   =>    |- ( G e. Grp -> ( G dom DProd (/) /\ ( G DProd (/) ) = { .0. } ) )
Theorem	dprdf1o 18431	Rearrange the index set of a direct product family. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> F : J -1-1-onto-> I )   =>    |- ( ph -> ( G dom DProd ( S o. F ) /\ ( G DProd ( S o. F ) ) = ( G DProd S ) ) )
Theorem	dprdf1 18432	Rearrange the index set of a direct product family. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> F : J -1-1-> I )   =>    |- ( ph -> ( G dom DProd ( S o. F ) /\ ( G DProd ( S o. F ) ) C_ ( G DProd S ) ) )
Theorem	subgdmdprd 18433	A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.)
|- H = ( G ↾s A )   =>    |- ( A e. (SubGrp ` G ) -> ( H dom DProd S <-> ( G dom DProd S /\ ran S C_ ~P A ) ) )
Theorem	subgdprd 18434	A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.)
|- H = ( G ↾s A )   &    |- ( ph -> A e. (SubGrp ` G ) )   &    |- ( ph -> G dom DProd S )   &    |- ( ph -> ran S C_ ~P A )   =>    |- ( ph -> ( H DProd S ) = ( G DProd S ) )
Theorem	dprdsn 18435	A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- ( ( A e. V /\ S e. (SubGrp ` G ) ) -> ( G dom DProd { <. A , S >. } /\ ( G DProd { <. A , S >. } ) = S ) )
Theorem	dmdprdsplitlem 18436*	Lemma for dmdprdsplit 18446. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.)
|- .0. = ( 0g ` G )   &    |- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }   &    |- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> A C_ I )   &    |- ( ph -> F e. W )   &    |- ( ph -> ( G gsumg F ) e. ( G DProd ( S |` A ) ) )   =>    |- ( ( ph /\ X e. ( I \ A ) ) -> ( F ` X ) = .0. )
Theorem	dprdcntz2 18437	The function S is a family of subgroups. (Contributed by Mario Carneiro, 26-Apr-2016.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> C C_ I )   &    |- ( ph -> D C_ I )   &    |- ( ph -> ( C i^i D ) = (/) )   &    |- Z = (Cntz ` G )   =>    |- ( ph -> ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) )
Theorem	dprddisj2 18438	The function S is a family of subgroups. (Contributed by Mario Carneiro, 26-Apr-2016.) (Revised by AV, 14-Jul-2019.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> C C_ I )   &    |- ( ph -> D C_ I )   &    |- ( ph -> ( C i^i D ) = (/) )   &    |- .0. = ( 0g ` G )   =>    |- ( ph -> ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } )
Theorem	dprd2dlem2 18439*	The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016.)
|- ( ph -> Rel A )   &    |- ( ph -> S : A --> (SubGrp ` G ) )   &    |- ( ph -> dom A C_ I )   &    |- ( ( ph /\ i e. I ) -> G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) )   &    |- ( ph -> G dom DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )   &    |- K = (mrCls ` (SubGrp ` G ) )   =>    |- ( ( ph /\ X e. A ) -> ( S ` X ) C_ ( G DProd ( j e. ( A " { ( 1st ` X ) } ) |-> ( ( 1st ` X ) S j ) ) ) )
Theorem	dprd2dlem1 18440*	The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016.)
|- ( ph -> Rel A )   &    |- ( ph -> S : A --> (SubGrp ` G ) )   &    |- ( ph -> dom A C_ I )   &    |- ( ( ph /\ i e. I ) -> G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) )   &    |- ( ph -> G dom DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )   &    |- K = (mrCls ` (SubGrp ` G ) )   &    |- ( ph -> C C_ I )   =>    |- ( ph -> ( K ` U. ( S " ( A |` C ) ) ) = ( G DProd ( i e. C |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ) )
Theorem	dprd2da 18441*	The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016.)
|- ( ph -> Rel A )   &    |- ( ph -> S : A --> (SubGrp ` G ) )   &    |- ( ph -> dom A C_ I )   &    |- ( ( ph /\ i e. I ) -> G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) )   &    |- ( ph -> G dom DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )   &    |- K = (mrCls ` (SubGrp ` G ) )   =>    |- ( ph -> G dom DProd S )
Theorem	dprd2db 18442*	The direct product of a collection of direct products. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- ( ph -> Rel A )   &    |- ( ph -> S : A --> (SubGrp ` G ) )   &    |- ( ph -> dom A C_ I )   &    |- ( ( ph /\ i e. I ) -> G dom DProd ( j e. ( A " { i } ) |-> ( i S j ) ) )   &    |- ( ph -> G dom DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) )   &    |- K = (mrCls ` (SubGrp ` G ) )   =>    |- ( ph -> ( G DProd S ) = ( G DProd ( i e. I |-> ( G DProd ( j e. ( A " { i } ) |-> ( i S j ) ) ) ) ) )
Theorem	dprd2d2 18443*	The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016.)
|- ( ( ph /\ ( i e. I /\ j e. J ) ) -> S e. (SubGrp ` G ) )   &    |- ( ( ph /\ i e. I ) -> G dom DProd ( j e. J |-> S ) )   &    |- ( ph -> G dom DProd ( i e. I |-> ( G DProd ( j e. J |-> S ) ) ) )   =>    |- ( ph -> ( G dom DProd ( i e. I , j e. J |-> S ) /\ ( G DProd ( i e. I , j e. J |-> S ) ) = ( G DProd ( i e. I |-> ( G DProd ( j e. J |-> S ) ) ) ) ) )
Theorem	dmdprdsplit2lem 18444	Lemma for dmdprdsplit 18446. (Contributed by Mario Carneiro, 26-Apr-2016.)
|- ( ph -> S : I --> (SubGrp ` G ) )   &    |- ( ph -> ( C i^i D ) = (/) )   &    |- ( ph -> I = ( C u. D ) )   &    |- Z = (Cntz ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G dom DProd ( S |` C ) )   &    |- ( ph -> G dom DProd ( S |` D ) )   &    |- ( ph -> ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) )   &    |- ( ph -> ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } )   &    |- K = (mrCls ` (SubGrp ` G ) )   =>    |- ( ( ph /\ X e. C ) -> ( ( Y e. I -> ( X =/= Y -> ( S ` X ) C_ ( Z ` ( S ` Y ) ) ) ) /\ ( ( S ` X ) i^i ( K ` U. ( S " ( I \ { X } ) ) ) ) C_ { .0. } ) )
Theorem	dmdprdsplit2 18445	The direct product splits into the direct product of any partition of the index set. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- ( ph -> S : I --> (SubGrp ` G ) )   &    |- ( ph -> ( C i^i D ) = (/) )   &    |- ( ph -> I = ( C u. D ) )   &    |- Z = (Cntz ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G dom DProd ( S |` C ) )   &    |- ( ph -> G dom DProd ( S |` D ) )   &    |- ( ph -> ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) )   &    |- ( ph -> ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } )   =>    |- ( ph -> G dom DProd S )
Theorem	dmdprdsplit 18446	The direct product splits into the direct product of any partition of the index set. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- ( ph -> S : I --> (SubGrp ` G ) )   &    |- ( ph -> ( C i^i D ) = (/) )   &    |- ( ph -> I = ( C u. D ) )   &    |- Z = (Cntz ` G )   &    |- .0. = ( 0g ` G )   =>    |- ( ph -> ( G dom DProd S <-> ( ( G dom DProd ( S |` C ) /\ G dom DProd ( S |` D ) ) /\ ( G DProd ( S |` C ) ) C_ ( Z ` ( G DProd ( S |` D ) ) ) /\ ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } ) ) )
Theorem	dprdsplit 18447	The direct product is the binary subgroup product ("sum") of the direct products of the partition. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- ( ph -> S : I --> (SubGrp ` G ) )   &    |- ( ph -> ( C i^i D ) = (/) )   &    |- ( ph -> I = ( C u. D ) )   &    |- .(+) = ( LSSum ` G )   &    |- ( ph -> G dom DProd S )   =>    |- ( ph -> ( G DProd S ) = ( ( G DProd ( S |` C ) ) .(+) ( G DProd ( S |` D ) ) ) )
Theorem	dmdprdpr 18448	A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- Z = (Cntz ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   =>    |- ( ph -> ( G dom DProd `' ( { S } +c { T } ) <-> ( S C_ ( Z ` T ) /\ ( S i^i T ) = { .0. } ) ) )
Theorem	dprdpr 18449	A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 26-Apr-2016.)
|- Z = (Cntz ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- .(+) = ( LSSum ` G )   &    |- ( ph -> S C_ ( Z ` T ) )   &    |- ( ph -> ( S i^i T ) = { .0. } )   =>    |- ( ph -> ( G DProd `' ( { S } +c { T } ) ) = ( S .(+) T ) )
Theorem	dpjlem 18450	Lemma for theorems about direct product projection. (Contributed by Mario Carneiro, 26-Apr-2016.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> X e. I )   =>    |- ( ph -> ( G DProd ( S |` { X } ) ) = ( S ` X ) )
Theorem	dpjcntz 18451	The two subgroups that appear in dpjval 18455 commute. (Contributed by Mario Carneiro, 26-Apr-2016.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> X e. I )   &    |- Z = (Cntz ` G )   =>    |- ( ph -> ( S ` X ) C_ ( Z ` ( G DProd ( S |` ( I \ { X } ) ) ) ) )
Theorem	dpjdisj 18452	The two subgroups that appear in dpjval 18455 are disjoint. (Contributed by Mario Carneiro, 26-Apr-2016.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> X e. I )   &    |- .0. = ( 0g ` G )   =>    |- ( ph -> ( ( S ` X ) i^i ( G DProd ( S |` ( I \ { X } ) ) ) ) = { .0. } )
Theorem	dpjlsm 18453	The two subgroups that appear in dpjval 18455 add to the full direct product. (Contributed by Mario Carneiro, 26-Apr-2016.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- ( ph -> X e. I )   &    |- .(+) = ( LSSum ` G )   =>    |- ( ph -> ( G DProd S ) = ( ( S ` X ) .(+) ( G DProd ( S |` ( I \ { X } ) ) ) ) )
Theorem	dpjfval 18454*	Value of the direct product projection (defined in terms of binary projection). (Contributed by Mario Carneiro, 26-Apr-2016.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- P = ( GdProj S )   &    |- Q = ( proj1 ` G )   =>    |- ( ph -> P = ( i e. I |-> ( ( S ` i ) Q ( G DProd ( S |` ( I \ { i } ) ) ) ) ) )
Theorem	dpjval 18455	Value of the direct product projection (defined in terms of binary projection). (Contributed by Mario Carneiro, 26-Apr-2016.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- P = ( GdProj S )   &    |- Q = ( proj1 ` G )   &    |- ( ph -> X e. I )   =>    |- ( ph -> ( P ` X ) = ( ( S ` X ) Q ( G DProd ( S |` ( I \ { X } ) ) ) ) )
Theorem	dpjf 18456	The X-th index projection is a function from the direct product to the X-th factor. (Contributed by Mario Carneiro, 26-Apr-2016.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- P = ( GdProj S )   &    |- ( ph -> X e. I )   =>    |- ( ph -> ( P ` X ) : ( G DProd S ) --> ( S ` X ) )
Theorem	dpjidcl 18457*	The key property of projections: the sum of all the projections of A is A. (Contributed by Mario Carneiro, 26-Apr-2016.) (Revised by AV, 14-Jul-2019.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- P = ( GdProj S )   &    |- ( ph -> A e. ( G DProd S ) )   &    |- .0. = ( 0g ` G )   &    |- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }   =>    |- ( ph -> ( ( x e. I |-> ( ( P ` x ) ` A ) ) e. W /\ A = ( G gsumg ( x e. I |-> ( ( P ` x ) ` A ) ) ) ) )
Theorem	dpjeq 18458*	Decompose a group sum into projections. (Contributed by Mario Carneiro, 26-Apr-2016.) (Revised by AV, 14-Jul-2019.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- P = ( GdProj S )   &    |- ( ph -> A e. ( G DProd S ) )   &    |- .0. = ( 0g ` G )   &    |- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }   &    |- ( ph -> ( x e. I |-> C ) e. W )   =>    |- ( ph -> ( A = ( G gsumg ( x e. I |-> C ) ) <-> A. x e. I ( ( P ` x ) ` A ) = C ) )
Theorem	dpjid 18459*	The key property of projections: the sum of all the projections of A is A. (Contributed by Mario Carneiro, 26-Apr-2016.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- P = ( GdProj S )   &    |- ( ph -> A e. ( G DProd S ) )   =>    |- ( ph -> A = ( G gsumg ( x e. I |-> ( ( P ` x ) ` A ) ) ) )
Theorem	dpjlid 18460	The X-th index projection acts as the identity on elements of the X-th factor. (Contributed by Mario Carneiro, 26-Apr-2016.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- P = ( GdProj S )   &    |- ( ph -> X e. I )   &    |- ( ph -> A e. ( S ` X ) )   =>    |- ( ph -> ( ( P ` X ) ` A ) = A )
Theorem	dpjrid 18461	The Y-th index projection annihilates elements of other factors. (Contributed by Mario Carneiro, 26-Apr-2016.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- P = ( GdProj S )   &    |- ( ph -> X e. I )   &    |- ( ph -> A e. ( S ` X ) )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> Y e. I )   &    |- ( ph -> Y =/= X )   =>    |- ( ph -> ( ( P ` Y ) ` A ) = .0. )
Theorem	dpjghm 18462	The direct product is the binary subgroup product ("sum") of the direct products of the partition. (Contributed by Mario Carneiro, 26-Apr-2016.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- P = ( GdProj S )   &    |- ( ph -> X e. I )   =>    |- ( ph -> ( P ` X ) e. ( ( G ↾s ( G DProd S ) ) GrpHom G ) )
Theorem	dpjghm2 18463	The direct product is the binary subgroup product ("sum") of the direct products of the partition. (Contributed by Mario Carneiro, 26-Apr-2016.)
|- ( ph -> G dom DProd S )   &    |- ( ph -> dom S = I )   &    |- P = ( GdProj S )   &    |- ( ph -> X e. I )   =>    |- ( ph -> ( P ` X ) e. ( ( G ↾s ( G DProd S ) ) GrpHom ( G ↾s ( S ` X ) ) ) )
10.3.6  The Fundamental Theorem of Abelian Groups
Theorem	ablfacrplem 18464*	Lemma for ablfacrp2 18466. (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 ) )   =>    |- ( ph -> ( ( # ` K ) gcd N ) = 1 )
Theorem	ablfacrp 18465*	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 18466*	The factors K , L of ablfacrp 18465 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 18467*	Lemma for ablfac1b 18469. 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 18468*	The factors of ablfac1b 18469 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 18469*	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 18470*	The factors of ablfac1b 18469 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 18471*	Lemma for ablfac1eu 18472. (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 18472*	The factorization of ablfac1b 18469 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 18473*	Lemma for pgpfac1 18479. (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 18474*	Lemma for pgpfac1 18479. (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 18475*	Lemma for pgpfac1 18479. (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 18476*	Lemma for pgpfac1 18479. (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 18477*	Lemma for pgpfac1 18479. (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 18478*	Lemma for pgpfac1 18479. (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 18479*	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 18480*	Lemma for pgpfac 18483. (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 ++ <" ( K ` { X } ) "> )   =>    |- ( ph -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = U ) )
Theorem	pgpfaclem2 18481*	Lemma for pgpfac 18483. (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 18482*	Lemma for pgpfac 18483. (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 18483*	Full factorization of a finite abelian p-group, by iterating pgpfac1 18479. 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 18484*	Lemma for ablfac 18487. (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 18485*	Lemma for ablfac 18487. (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 18486*	Lemma for ablfac 18487. (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 18487*	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 18488*	Choose generators for each cyclic group in ablfac 18487. (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 18489	Multiplicative group.
class mulGrp
Definition	df-mgp 18490	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 18667 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" (ringmgp 18553) or "the multiplicative identity" in terms of the identity of a monoid (df-1r 9883). (Contributed by Mario Carneiro, 21-Dec-2014.)
|- mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
Theorem	fnmgp 18491	The multiplicative group operator is a function. (Contributed by Mario Carneiro, 11-Mar-2015.)
|- mulGrp Fn _V
Theorem	mgpval 18492	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 18493	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 18494	Lemma for mgpbas 18495. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- M = (mulGrp ` R )   &    |- E = Slot N   &    |- N e. NN   &    |- N =/= 2   =>    |- ( E ` R ) = ( E ` M )
Theorem	mgpbas 18495	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 18496	The multiplication monoid has the same (if any) scalars as the original ring. Mostly to simplify pwsmgp 18618. (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 18497	Topology component of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- M = (mulGrp ` R )   =>    |- (TopSet ` R ) = (TopSet ` M )
Theorem	mgptopn 18498	Topology of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- M = (mulGrp ` R )   &    |- J = ( TopOpen ` R )   =>    |- J = ( TopOpen ` M )
Theorem	mgpds 18499	Distance function of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- M = (mulGrp ` R )   &    |- B = ( dist ` R )   =>    |- B = ( dist ` M )
Theorem	mgpress 18500	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 ) )