P. 167 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 16601-16700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sylow1lem5 16601*	Lemma for sylow1 16602. Using Lagrange's theorem and the orbit-stabilizer theorem, show that there is a subgroup with size exactly P ^ N. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- X = ( Base ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> ( P ^ N ) || ( # ` X ) )   &    |- .+ = ( +g ` G )   &    |- S = { s e. ~P X | ( # ` s ) = ( P ^ N ) }   &    |- .(+) = ( x e. X , y e. S |-> ran ( z e. y |-> ( x .+ z ) ) )   &    |- .~ = { <. x , y >. | ( { x , y } C_ S /\ E. g e. X ( g .(+) x ) = y ) }   &    |- ( ph -> B e. S )   &    |- H = { u e. X | ( u .(+) B ) = B }   &    |- ( ph -> ( P pCnt ( # ` [ B ] .~ ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) )   =>    |- ( ph -> E. h e. (SubGrp ` G ) ( # ` h ) = ( P ^ N ) )
Theorem	sylow1 16602*	Sylow's first theorem. If P ^ N is a prime power that divides the cardinality of G, then G has a supgroup with size P ^ N. This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- X = ( Base ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> ( P ^ N ) || ( # ` X ) )   =>    |- ( ph -> E. g e. (SubGrp ` G ) ( # ` g ) = ( P ^ N ) )
Theorem	odcau 16603*	Cauchy's theorem for the order of an element in a group. A finite group whose order divides a prime P contains an element of order P. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- X = ( Base ` G )   &    |- O = ( od ` G )   =>    |- ( ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) /\ P || ( # ` X ) ) -> E. g e. X ( O ` g ) = P )
Theorem	pgpfi 16604*	The converse to pgpfi1 16594. A finite group is a P-group iff it has size some power of P. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- X = ( Base ` G )   =>    |- ( ( G e. Grp /\ X e. Fin ) -> ( P pGrp G <-> ( P e. Prime /\ E. n e. NN0 ( # ` X ) = ( P ^ n ) ) ) )
Theorem	pgpfi2 16605	Alternate version of pgpfi 16604. (Contributed by Mario Carneiro, 27-Apr-2016.)
|- X = ( Base ` G )   =>    |- ( ( G e. Grp /\ X e. Fin ) -> ( P pGrp G <-> ( P e. Prime /\ ( # ` X ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) )
Theorem	pgphash 16606	The order of a p-group. (Contributed by Mario Carneiro, 27-Apr-2016.)
|- X = ( Base ` G )   =>    |- ( ( P pGrp G /\ X e. Fin ) -> ( # ` X ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
Theorem	isslw 16607*	The property of being a Sylow subgroup. A Sylow P-subgroup is a P-group which has no proper supersets that are also P-groups. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- ( H e. ( P pSyl G ) <-> ( P e. Prime /\ H e. (SubGrp ` G ) /\ A. k e. (SubGrp ` G ) ( ( H C_ k /\ P pGrp ( G ↾s k ) ) <-> H = k ) ) )
Theorem	slwprm 16608	Reverse closure for the first argument of a Sylow P-subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.) (Revised by Mario Carneiro, 2-May-2015.)
|- ( H e. ( P pSyl G ) -> P e. Prime )
Theorem	slwsubg 16609	A Sylow P-subgroup is a subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- ( H e. ( P pSyl G ) -> H e. (SubGrp ` G ) )
Theorem	slwispgp 16610	Defining property of a Sylow P-subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- S = ( G ↾s K )   =>    |- ( ( H e. ( P pSyl G ) /\ K e. (SubGrp ` G ) ) -> ( ( H C_ K /\ P pGrp S ) <-> H = K ) )
Theorem	slwpss 16611	A proper superset of a Sylow subgroup is not a P-group. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- S = ( G ↾s K )   =>    |- ( ( H e. ( P pSyl G ) /\ K e. (SubGrp ` G ) /\ H C. K ) -> -. P pGrp S )
Theorem	slwpgp 16612	A Sylow P-subgroup is a P-group. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- S = ( G ↾s H )   =>    |- ( H e. ( P pSyl G ) -> P pGrp S )
Theorem	pgpssslw 16613*	Every P-subgroup is contained in a Sylow P-subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- X = ( Base ` G )   &    |- S = ( G ↾s H )   &    |- F = ( x e. { y e. (SubGrp ` G ) | ( P pGrp ( G ↾s y ) /\ H C_ y ) } |-> ( # ` x ) )   =>    |- ( ( H e. (SubGrp ` G ) /\ X e. Fin /\ P pGrp S ) -> E. k e. ( P pSyl G ) H C_ k )
Theorem	slwn0 16614	Every finite group contains a Sylow P-subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- X = ( Base ` G )   =>    |- ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) -> ( P pSyl G ) =/= (/) )
Theorem	subgslw 16615	A Sylow subgroup that is contained in a larger subgroup is also Sylow with respect to the subgroup. (The converse may not be true, though.) (Contributed by Mario Carneiro, 19-Jan-2015.)
|- H = ( G ↾s S )   =>    |- ( ( S e. (SubGrp ` G ) /\ K e. ( P pSyl G ) /\ K C_ S ) -> K e. ( P pSyl H ) )
Theorem	sylow2alem1 16616*	Lemma for sylow2a 16618. An equivalence class of fixed points is a singleton. (Contributed by Mario Carneiro, 17-Jan-2015.)
|- X = ( Base ` G )   &    |- ( ph -> .(+) e. ( G GrpAct Y ) )   &    |- ( ph -> P pGrp G )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> Y e. Fin )   &    |- Z = { u e. Y | A. h e. X ( h .(+) u ) = u }   &    |- .~ = { <. x , y >. | ( { x , y } C_ Y /\ E. g e. X ( g .(+) x ) = y ) }   =>    |- ( ( ph /\ A e. Z ) -> [ A ] .~ = { A } )
Theorem	sylow2alem2 16617*	Lemma for sylow2a 16618. All the orbits which are not for fixed points have size | G | / | G x | (where G x is the stabilizer subgroup) and thus are powers of P. And since they are all nontrivial (because any orbit which is a singleton is a fixed point), they all divide P, and so does the sum of all of them. (Contributed by Mario Carneiro, 17-Jan-2015.)
|- X = ( Base ` G )   &    |- ( ph -> .(+) e. ( G GrpAct Y ) )   &    |- ( ph -> P pGrp G )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> Y e. Fin )   &    |- Z = { u e. Y | A. h e. X ( h .(+) u ) = u }   &    |- .~ = { <. x , y >. | ( { x , y } C_ Y /\ E. g e. X ( g .(+) x ) = y ) }   =>    |- ( ph -> P || sum_ z e. ( ( Y /. .~ ) \ ~P Z ) ( # ` z ) )
Theorem	sylow2a 16618*	A named lemma of Sylow's second and third theorems. If G is a finite P-group that acts on the finite set Y, then the set Z of all points of Y fixed by every element of G has cardinality equivalent to the cardinality of Y, mod P. (Contributed by Mario Carneiro, 17-Jan-2015.)
|- X = ( Base ` G )   &    |- ( ph -> .(+) e. ( G GrpAct Y ) )   &    |- ( ph -> P pGrp G )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> Y e. Fin )   &    |- Z = { u e. Y | A. h e. X ( h .(+) u ) = u }   &    |- .~ = { <. x , y >. | ( { x , y } C_ Y /\ E. g e. X ( g .(+) x ) = y ) }   =>    |- ( ph -> P || ( ( # ` Y ) - ( # ` Z ) ) )
Theorem	sylow2blem1 16619*	Lemma for sylow2b 16622. Evaluate the group action on a left coset. (Contributed by Mario Carneiro, 17-Jan-2015.)
|- X = ( Base ` G )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> H e. (SubGrp ` G ) )   &    |- ( ph -> K e. (SubGrp ` G ) )   &    |- .+ = ( +g ` G )   &    |- .~ = ( G ~QG K )   &    |- .x. = ( x e. H , y e. ( X /. .~ ) |-> ran ( z e. y |-> ( x .+ z ) ) )   =>    |- ( ( ph /\ B e. H /\ C e. X ) -> ( B .x. [ C ] .~ ) = [ ( B .+ C ) ] .~ )
Theorem	sylow2blem2 16620*	Lemma for sylow2b 16622. Left multiplication in a subgroup H is a group action on the set of all left cosets of K. (Contributed by Mario Carneiro, 17-Jan-2015.)
|- X = ( Base ` G )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> H e. (SubGrp ` G ) )   &    |- ( ph -> K e. (SubGrp ` G ) )   &    |- .+ = ( +g ` G )   &    |- .~ = ( G ~QG K )   &    |- .x. = ( x e. H , y e. ( X /. .~ ) |-> ran ( z e. y |-> ( x .+ z ) ) )   =>    |- ( ph -> .x. e. ( ( G ↾s H ) GrpAct ( X /. .~ ) ) )
Theorem	sylow2blem3 16621*	Sylow's second theorem. Putting together the results of sylow2a 16618 and the orbit-stabilizer theorem to show that P does not divide the set of all fixed points under the group action, we get that there is a fixed point of the group action, so that there is some g e. X with h g K = g K for all h e. H. This implies that invg ( g ) h g e. K, so h is in the conjugated subgroup g K invg ( g ). (Contributed by Mario Carneiro, 18-Jan-2015.)
|- X = ( Base ` G )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> H e. (SubGrp ` G ) )   &    |- ( ph -> K e. (SubGrp ` G ) )   &    |- .+ = ( +g ` G )   &    |- .~ = ( G ~QG K )   &    |- .x. = ( x e. H , y e. ( X /. .~ ) |-> ran ( z e. y |-> ( x .+ z ) ) )   &    |- ( ph -> P pGrp ( G ↾s H ) )   &    |- ( ph -> ( # ` K ) = ( P ^ ( P pCnt ( # ` X ) ) ) )   &    |- .- = ( -g ` G )   =>    |- ( ph -> E. g e. X H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )
Theorem	sylow2b 16622*	Sylow's second theorem. Any P-group H is a subgroup of a conjugated P-group K of order P ^ n || ( # ` X ) with n maximal. This is usually stated under the assumption that K is a Sylow subgroup, but we use a slightly different definition, whose equivalence to this one requires this theorem. This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 18-Jan-2015.)
|- X = ( Base ` G )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> H e. (SubGrp ` G ) )   &    |- ( ph -> K e. (SubGrp ` G ) )   &    |- .+ = ( +g ` G )   &    |- ( ph -> P pGrp ( G ↾s H ) )   &    |- ( ph -> ( # ` K ) = ( P ^ ( P pCnt ( # ` X ) ) ) )   &    |- .- = ( -g ` G )   =>    |- ( ph -> E. g e. X H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )
Theorem	slwhash 16623	A sylow subgroup has cardinality equal to the maximum power of P dividing the group. (Contributed by Mario Carneiro, 18-Jan-2015.)
|- X = ( Base ` G )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> H e. ( P pSyl G ) )   =>    |- ( ph -> ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
Theorem	fislw 16624	The sylow subgroups of a finite group are exactly the groups which have cardinality equal to the maximum power of P dividing the group. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- X = ( Base ` G )   =>    |- ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) -> ( H e. ( P pSyl G ) <-> ( H e. (SubGrp ` G ) /\ ( # ` H ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) )
Theorem	sylow2 16625*	Sylow's second theorem. See also sylow2b 16622 for the "hard" part of the proof. Any two Sylow P-subgroups are conjugate to one another, and hence the same size, namely P ^ ( P pCnt | X | ) (see fislw 16624). This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 18-Jan-2015.)
|- X = ( Base ` G )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> H e. ( P pSyl G ) )   &    |- ( ph -> K e. ( P pSyl G ) )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   =>    |- ( ph -> E. g e. X H = ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )
Theorem	sylow3lem1 16626*	Lemma for sylow3 16632, first part. (Contributed by Mario Carneiro, 19-Jan-2015.)
|- X = ( Base ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> P e. Prime )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- .(+) = ( x e. X , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) )   =>    |- ( ph -> .(+) e. ( G GrpAct ( P pSyl G ) ) )
Theorem	sylow3lem2 16627*	Lemma for sylow3 16632, first part. The stabilizer of a given Sylow subgroup K in the group action .(+) acting on all of G is the normalizer NG(K). (Contributed by Mario Carneiro, 19-Jan-2015.)
|- X = ( Base ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> P e. Prime )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- .(+) = ( x e. X , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) )   &    |- ( ph -> K e. ( P pSyl G ) )   &    |- H = { u e. X | ( u .(+) K ) = K }   &    |- N = { x e. X | A. y e. X ( ( x .+ y ) e. K <-> ( y .+ x ) e. K ) }   =>    |- ( ph -> H = N )
Theorem	sylow3lem3 16628*	Lemma for sylow3 16632, first part. The number of Sylow subgroups is the same as the index (number of cosets) of the normalizer of the Sylow subgroup K. (Contributed by Mario Carneiro, 19-Jan-2015.)
|- X = ( Base ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> P e. Prime )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- .(+) = ( x e. X , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) )   &    |- ( ph -> K e. ( P pSyl G ) )   &    |- H = { u e. X | ( u .(+) K ) = K }   &    |- N = { x e. X | A. y e. X ( ( x .+ y ) e. K <-> ( y .+ x ) e. K ) }   =>    |- ( ph -> ( # ` ( P pSyl G ) ) = ( # ` ( X /. ( G ~QG N ) ) ) )
Theorem	sylow3lem4 16629*	Lemma for sylow3 16632, first part. The number of Sylow subgroups is a divisor of the size of G reduced by the size of a Sylow subgroup of G. (Contributed by Mario Carneiro, 19-Jan-2015.)
|- X = ( Base ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> P e. Prime )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- .(+) = ( x e. X , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) )   &    |- ( ph -> K e. ( P pSyl G ) )   &    |- H = { u e. X | ( u .(+) K ) = K }   &    |- N = { x e. X | A. y e. X ( ( x .+ y ) e. K <-> ( y .+ x ) e. K ) }   =>    |- ( ph -> ( # ` ( P pSyl G ) ) || ( ( # ` X ) / ( P ^ ( P pCnt ( # ` X ) ) ) ) )
Theorem	sylow3lem5 16630*	Lemma for sylow3 16632, second part. Reduce the group action of sylow3lem1 16626 to a given Sylow subgroup. (Contributed by Mario Carneiro, 19-Jan-2015.)
|- X = ( Base ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> P e. Prime )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> K e. ( P pSyl G ) )   &    |- .(+) = ( x e. K , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) )   =>    |- ( ph -> .(+) e. ( ( G ↾s K ) GrpAct ( P pSyl G ) ) )
Theorem	sylow3lem6 16631*	Lemma for sylow3 16632, second part. Using the lemma sylow2a 16618, show that the number of sylow subgroups is equivalent mod P to the number of fixed points under the group action. But K is the unique element of the set of Sylow subgroups that is fixed under the group action, so there is exactly one fixed point and so ( ( # ` ( P pSyl G ) ) mod P ) = 1. (Contributed by Mario Carneiro, 19-Jan-2015.)
|- X = ( Base ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> P e. Prime )   &    |- .+ = ( +g ` G )   &    |- .- = ( -g ` G )   &    |- ( ph -> K e. ( P pSyl G ) )   &    |- .(+) = ( x e. K , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) )   &    |- N = { x e. X | A. y e. X ( ( x .+ y ) e. s <-> ( y .+ x ) e. s ) }   =>    |- ( ph -> ( ( # ` ( P pSyl G ) ) mod P ) = 1 )
Theorem	sylow3 16632	Sylow's third theorem. The number of Sylow subgroups is a divisor of | G | / d, where d is the common order of a Sylow subgroup, and is equivalent to 1 mod P. This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 19-Jan-2015.)
|- X = ( Base ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> P e. Prime )   &    |- N = ( # ` ( P pSyl G ) )   =>    |- ( ph -> ( N || ( ( # ` X ) / ( P ^ ( P pCnt ( # ` X ) ) ) ) /\ ( N mod P ) = 1 ) )
10.2.10  Direct products
Syntax	clsm 16633	Extend class notation with subgroup sum.
class LSSum
Syntax	cpj1 16634	Extend class notation with left projection.
class proj1
Definition	df-lsm 16635*	Define subgroup sum (inner direct product of subgroups). (Contributed by NM, 28-Jan-2014.)
|- LSSum = ( w e. _V |-> ( t e. ~P ( Base ` w ) , u e. ~P ( Base ` w ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` w ) y ) ) ) )
Definition	df-pj1 16636*	Define the left projection function, which takes two subgroups t , u with trivial intersection and returns a function mapping the elements of the subgroup sum t + u to their projections onto t. (The other projection function can be obtained by swapping the roles of t and u.) (Contributed by Mario Carneiro, 15-Oct-2015.)
|- proj1 = ( w e. _V |-> ( t e. ~P ( Base ` w ) , u e. ~P ( Base ` w ) |-> ( z e. ( t ( LSSum ` w ) u ) |-> ( iota_ x e. t E. y e. u z = ( x ( +g ` w ) y ) ) ) ) )
Theorem	lsmfval 16637*	The subgroup sum function (for a group or vector space). (Contributed by NM, 28-Jan-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   =>    |- ( G e. V -> .(+) = ( t e. ~P B , u e. ~P B |-> ran ( x e. t , y e. u |-> ( x .+ y ) ) ) )
Theorem	lsmvalx 16638*	Subspace sum value (for a group or vector space). Extended domain version of lsmval 16647. (Contributed by NM, 28-Jan-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   =>    |- ( ( G e. V /\ T C_ B /\ U C_ B ) -> ( T .(+) U ) = ran ( x e. T , y e. U |-> ( x .+ y ) ) )
Theorem	lsmelvalx 16639*	Subspace sum membership (for a group or vector space). Extended domain version of lsmelval 16648. (Contributed by NM, 28-Jan-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   =>    |- ( ( G e. V /\ T C_ B /\ U C_ B ) -> ( X e. ( T .(+) U ) <-> E. y e. T E. z e. U X = ( y .+ z ) ) )
Theorem	lsmelvalix 16640	Subspace sum membership (for a group or vector space). (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   =>    |- ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ ( X e. T /\ Y e. U ) ) -> ( X .+ Y ) e. ( T .(+) U ) )
Theorem	oppglsm 16641	The subspace sum operation in the opposite group. (Contributed by Mario Carneiro, 19-Apr-2016.)
|- O = (oppg ` G )   &    |- .(+) = ( LSSum ` G )   =>    |- ( T ( LSSum ` O ) U ) = ( U .(+) T )
Theorem	lsmssv 16642	Subgroup sum is a subset of the base. (Contributed by Mario Carneiro, 19-Apr-2016.)
|- B = ( Base ` G )   &    |- .(+) = ( LSSum ` G )   =>    |- ( ( G e. Mnd /\ T C_ B /\ U C_ B ) -> ( T .(+) U ) C_ B )
Theorem	lsmless1x 16643	Subset implies subgroup sum subset (extended domain version). (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- B = ( Base ` G )   &    |- .(+) = ( LSSum ` G )   =>    |- ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ R C_ T ) -> ( R .(+) U ) C_ ( T .(+) U ) )
Theorem	lsmless2x 16644	Subset implies subgroup sum subset (extended domain version). (Contributed by NM, 25-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- B = ( Base ` G )   &    |- .(+) = ( LSSum ` G )   =>    |- ( ( ( G e. V /\ R C_ B /\ U C_ B ) /\ T C_ U ) -> ( R .(+) T ) C_ ( R .(+) U ) )
Theorem	lsmub1x 16645	Subgroup sum is an upper bound of its arguments. (Contributed by Mario Carneiro, 19-Apr-2016.)
|- B = ( Base ` G )   &    |- .(+) = ( LSSum ` G )   =>    |- ( ( T C_ B /\ U e. (SubMnd ` G ) ) -> T C_ ( T .(+) U ) )
Theorem	lsmub2x 16646	Subgroup sum is an upper bound of its arguments. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- B = ( Base ` G )   &    |- .(+) = ( LSSum ` G )   =>    |- ( ( T e. (SubMnd ` G ) /\ U C_ B ) -> U C_ ( T .(+) U ) )
Theorem	lsmval 16647*	Subgroup sum value (for a left module or left vector space). (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   =>    |- ( ( T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) ) -> ( T .(+) U ) = ran ( x e. T , y e. U |-> ( x .+ y ) ) )
Theorem	lsmelval 16648*	Subgroup sum membership (for a left module or left vector space). (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   =>    |- ( ( T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) ) -> ( X e. ( T .(+) U ) <-> E. y e. T E. z e. U X = ( y .+ z ) ) )
Theorem	lsmelvali 16649	Subgroup sum membership (for a left module or left vector space). (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   =>    |- ( ( ( T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) ) /\ ( X e. T /\ Y e. U ) ) -> ( X .+ Y ) e. ( T .(+) U ) )
Theorem	lsmelvalm 16650*	Subgroup sum membership analog of lsmelval 16648 using vector subtraction. TODO: any way to shorten proof? (Contributed by NM, 16-Mar-2015.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .- = ( -g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   =>    |- ( ph -> ( X e. ( T .(+) U ) <-> E. y e. T E. z e. U X = ( y .- z ) ) )
Theorem	lsmelvalmi 16651	Membership of vector subtraction in subgroup sum. (Contributed by NM, 27-Apr-2015.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .- = ( -g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> X e. T )   &    |- ( ph -> Y e. U )   =>    |- ( ph -> ( X .- Y ) e. ( T .(+) U ) )
Theorem	lsmsubm 16652	The sum of two commuting submonoids is a submonoid. (Contributed by Mario Carneiro, 19-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- Z = (Cntz ` G )   =>    |- ( ( T e. (SubMnd ` G ) /\ U e. (SubMnd ` G ) /\ T C_ ( Z ` U ) ) -> ( T .(+) U ) e. (SubMnd ` G ) )
Theorem	lsmsubg 16653	The sum of two commuting subgroups is a subgroup. (Contributed by Mario Carneiro, 19-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- Z = (Cntz ` G )   =>    |- ( ( T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( T .(+) U ) e. (SubGrp ` G ) )
Theorem	lsmcom2 16654	Subgroup sum commutes. (Contributed by Mario Carneiro, 22-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- Z = (Cntz ` G )   =>    |- ( ( T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( T .(+) U ) = ( U .(+) T ) )
Theorem	lsmub1 16655	Subgroup sum is an upper bound of its arguments. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .(+) = ( LSSum ` G )   =>    |- ( ( T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) ) -> T C_ ( T .(+) U ) )
Theorem	lsmub2 16656	Subgroup sum is an upper bound of its arguments. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .(+) = ( LSSum ` G )   =>    |- ( ( T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) ) -> U C_ ( T .(+) U ) )
Theorem	lsmunss 16657	Union of subgroups is a subset of subgroup sum. (Contributed by NM, 6-Feb-2014.) (Proof shortened by Mario Carneiro, 21-Jun-2014.)
|- .(+) = ( LSSum ` G )   =>    |- ( ( T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) ) -> ( T u. U ) C_ ( T .(+) U ) )
Theorem	lsmless1 16658	Subset implies subgroup sum subset. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .(+) = ( LSSum ` G )   =>    |- ( ( T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) /\ S C_ T ) -> ( S .(+) U ) C_ ( T .(+) U ) )
Theorem	lsmless2 16659	Subset implies subgroup sum subset. (Contributed by NM, 25-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .(+) = ( LSSum ` G )   =>    |- ( ( S e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) /\ T C_ U ) -> ( S .(+) T ) C_ ( S .(+) U ) )
Theorem	lsmless12 16660	Subset implies subgroup sum subset. (Contributed by NM, 14-Jan-2015.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .(+) = ( LSSum ` G )   =>    |- ( ( ( S e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) ) /\ ( R C_ S /\ T C_ U ) ) -> ( R .(+) T ) C_ ( S .(+) U ) )
Theorem	lsmidm 16661	Subgroup sum is idempotent. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.)
|- .(+) = ( LSSum ` G )   =>    |- ( U e. (SubGrp ` G ) -> ( U .(+) U ) = U )
Theorem	lsmlub 16662	The least upper bound property of subgroup sum. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.)
|- .(+) = ( LSSum ` G )   =>    |- ( ( S e. (SubGrp ` G ) /\ T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) ) -> ( ( S C_ U /\ T C_ U ) <-> ( S .(+) T ) C_ U ) )
Theorem	lsmss1 16663	Subgroup sum with a subset. (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .(+) = ( LSSum ` G )   =>    |- ( ( T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) /\ T C_ U ) -> ( T .(+) U ) = U )
Theorem	lsmss1b 16664	Subgroup sum with a subset. (Contributed by NM, 10-Jan-2015.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .(+) = ( LSSum ` G )   =>    |- ( ( T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) ) -> ( T C_ U <-> ( T .(+) U ) = U ) )
Theorem	lsmss2 16665	Subgroup sum with a subset. (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .(+) = ( LSSum ` G )   =>    |- ( ( T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) /\ U C_ T ) -> ( T .(+) U ) = T )
Theorem	lsmss2b 16666	Subgroup sum with a subset. (Contributed by NM, 10-Jan-2015.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .(+) = ( LSSum ` G )   =>    |- ( ( T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) ) -> ( U C_ T <-> ( T .(+) U ) = T ) )
Theorem	lsmass 16667	Subgroup sum is associative. (Contributed by NM, 2-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .(+) = ( LSSum ` G )   =>    |- ( ( R e. (SubGrp ` G ) /\ T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) ) -> ( ( R .(+) T ) .(+) U ) = ( R .(+) ( T .(+) U ) ) )
Theorem	lsm01 16668	Subgroup sum with the zero subgroup. (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .0. = ( 0g ` G )   &    |- .(+) = ( LSSum ` G )   =>    |- ( X e. (SubGrp ` G ) -> ( X .(+) { .0. } ) = X )
Theorem	lsm02 16669	Subgroup sum with the zero subgroup. (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .0. = ( 0g ` G )   &    |- .(+) = ( LSSum ` G )   =>    |- ( X e. (SubGrp ` G ) -> ( { .0. } .(+) X ) = X )
Theorem	subglsm 16670	The subgroup sum evaluated within a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.)
|- H = ( G ↾s S )   &    |- .(+) = ( LSSum ` G )   &    |- A = ( LSSum ` H )   =>    |- ( ( S e. (SubGrp ` G ) /\ T C_ S /\ U C_ S ) -> ( T .(+) U ) = ( T A U ) )
Theorem	lssnle 16671	Equivalent expressions for "not less than". (chnlei 26381 analog.) (Contributed by NM, 10-Jan-2015.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   =>    |- ( ph -> ( -. U C_ T <-> T C. ( T .(+) U ) ) )
Theorem	lsmmod 16672	The modular law holds for subgroup sum. Similar to part of Theorem 16.9 of [MaedaMaeda] p. 70. (Contributed by NM, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .(+) = ( LSSum ` G )   =>    |- ( ( ( S e. (SubGrp ` G ) /\ T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) ) /\ S C_ U ) -> ( S .(+) ( T i^i U ) ) = ( ( S .(+) T ) i^i U ) )
Theorem	lsmmod2 16673	Modular law dual for subgroup sum. Similar to part of Theorem 16.9 of [MaedaMaeda] p. 70. (Contributed by NM, 8-Jan-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
|- .(+) = ( LSSum ` G )   =>    |- ( ( ( S e. (SubGrp ` G ) /\ T e. (SubGrp ` G ) /\ U e. (SubGrp ` G ) ) /\ U C_ S ) -> ( S i^i ( T .(+) U ) ) = ( ( S i^i T ) .(+) U ) )
Theorem	lsmpropd 16674*	If two structures have the same components (properties), they have the same subspace structure. (Contributed by Mario Carneiro, 29-Jun-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 -> K e. _V )   &    |- ( ph -> L e. _V )   =>    |- ( ph -> ( LSSum ` K ) = ( LSSum ` L ) )
Theorem	cntzrecd 16675	Commute the "subgroups commute" predicate. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> T C_ ( Z ` U ) )   =>    |- ( ph -> U C_ ( Z ` T ) )
Theorem	lsmcntz 16676	The "subgroups commute" predicate applied to a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- Z = (Cntz ` G )   =>    |- ( ph -> ( ( S .(+) T ) C_ ( Z ` U ) <-> ( S C_ ( Z ` U ) /\ T C_ ( Z ` U ) ) ) )
Theorem	lsmcntzr 16677	The "subgroups commute" predicate applied to a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- Z = (Cntz ` G )   =>    |- ( ph -> ( S C_ ( Z ` ( T .(+) U ) ) <-> ( S C_ ( Z ` T ) /\ S C_ ( Z ` U ) ) ) )
Theorem	lsmdisj 16678	Disjointness from a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> ( ( S .(+) T ) i^i U ) = { .0. } )   =>    |- ( ph -> ( ( S i^i U ) = { .0. } /\ ( T i^i U ) = { .0. } ) )
Theorem	lsmdisj2 16679	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 22-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> ( ( S .(+) T ) i^i U ) = { .0. } )   &    |- ( ph -> ( S i^i T ) = { .0. } )   =>    |- ( ph -> ( T i^i ( S .(+) U ) ) = { .0. } )
Theorem	lsmdisj3 16680	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> ( ( S .(+) T ) i^i U ) = { .0. } )   &    |- ( ph -> ( S i^i T ) = { .0. } )   &    |- Z = (Cntz ` G )   &    |- ( ph -> S C_ ( Z ` T ) )   =>    |- ( ph -> ( S i^i ( T .(+) U ) ) = { .0. } )
Theorem	lsmdisjr 16681	Disjointness from a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> ( S i^i ( T .(+) U ) ) = { .0. } )   =>    |- ( ph -> ( ( S i^i T ) = { .0. } /\ ( S i^i U ) = { .0. } ) )
Theorem	lsmdisj2r 16682	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 22-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> ( S i^i ( T .(+) U ) ) = { .0. } )   &    |- ( ph -> ( T i^i U ) = { .0. } )   =>    |- ( ph -> ( ( S .(+) U ) i^i T ) = { .0. } )
Theorem	lsmdisj3r 16683	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 22-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> ( S i^i ( T .(+) U ) ) = { .0. } )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T C_ ( Z ` U ) )   =>    |- ( ph -> ( ( S .(+) T ) i^i U ) = { .0. } )
Theorem	lsmdisj2a 16684	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- .0. = ( 0g ` G )   =>    |- ( ph -> ( ( ( ( S .(+) T ) i^i U ) = { .0. } /\ ( S i^i T ) = { .0. } ) <-> ( ( T i^i ( S .(+) U ) ) = { .0. } /\ ( S i^i U ) = { .0. } ) ) )
Theorem	lsmdisj2b 16685	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- .0. = ( 0g ` G )   =>    |- ( ph -> ( ( ( ( S .(+) U ) i^i T ) = { .0. } /\ ( S i^i U ) = { .0. } ) <-> ( ( S i^i ( T .(+) U ) ) = { .0. } /\ ( T i^i U ) = { .0. } ) ) )
Theorem	lsmdisj3a 16686	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> S C_ ( Z ` T ) )   =>    |- ( ph -> ( ( ( ( S .(+) T ) i^i U ) = { .0. } /\ ( S i^i T ) = { .0. } ) <-> ( ( S i^i ( T .(+) U ) ) = { .0. } /\ ( T i^i U ) = { .0. } ) ) )
Theorem	lsmdisj3b 16687	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- .(+) = ( LSSum ` G )   &    |- ( ph -> S e. (SubGrp ` G ) )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T C_ ( Z ` U ) )   =>    |- ( ph -> ( ( ( ( S .(+) T ) i^i U ) = { .0. } /\ ( S i^i T ) = { .0. } ) <-> ( ( S i^i ( T .(+) U ) ) = { .0. } /\ ( T i^i U ) = { .0. } ) ) )
Theorem	subgdisj1 16688	Vectors belonging to disjoint commuting subgroups are uniquely determined by their sum. (Contributed by NM, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   &    |- ( ph -> A e. T )   &    |- ( ph -> C e. T )   &    |- ( ph -> B e. U )   &    |- ( ph -> D e. U )   &    |- ( ph -> ( A .+ B ) = ( C .+ D ) )   =>    |- ( ph -> A = C )
Theorem	subgdisj2 16689	Vectors belonging to disjoint subgroups are uniquely determined by their sum. (Contributed by NM, 12-Jul-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   &    |- ( ph -> A e. T )   &    |- ( ph -> C e. T )   &    |- ( ph -> B e. U )   &    |- ( ph -> D e. U )   &    |- ( ph -> ( A .+ B ) = ( C .+ D ) )   =>    |- ( ph -> B = D )
Theorem	subgdisjb 16690	Vectors belonging to disjoint subgroups are uniquely determined by their sum. Analogous to opth 4711, this theorem shows a way of representing a pair of vectors. (Contributed by NM, 5-Jul-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- .+ = ( +g ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   &    |- ( ph -> A e. T )   &    |- ( ph -> C e. T )   &    |- ( ph -> B e. U )   &    |- ( ph -> D e. U )   =>    |- ( ph -> ( ( A .+ B ) = ( C .+ D ) <-> ( A = C /\ B = D ) ) )
Theorem	pj1fval 16691*	The left projection function (for a direct product of group subspaces). (Contributed by Mario Carneiro, 15-Oct-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- P = ( proj1 ` G )   =>    |- ( ( G e. V /\ T C_ B /\ U C_ B ) -> ( T P U ) = ( z e. ( T .(+) U ) |-> ( iota_ x e. T E. y e. U z = ( x .+ y ) ) ) )
Theorem	pj1val 16692*	The left projection function (for a direct product of group subspaces). (Contributed by Mario Carneiro, 15-Oct-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- P = ( proj1 ` G )   =>    |- ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ X e. ( T .(+) U ) ) -> ( ( T P U ) ` X ) = ( iota_ x e. T E. y e. U X = ( x .+ y ) ) )
Theorem	pj1eu 16693*	Uniqueness of a left projection. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   =>    |- ( ( ph /\ X e. ( T .(+) U ) ) -> E! x e. T E. y e. U X = ( x .+ y ) )
Theorem	pj1f 16694	The left projection function maps a direct subspace sum onto the left factor. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   &    |- P = ( proj1 ` G )   =>    |- ( ph -> ( T P U ) : ( T .(+) U ) --> T )
Theorem	pj2f 16695	The right projection function maps a direct subspace sum onto the right factor. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   &    |- P = ( proj1 ` G )   =>    |- ( ph -> ( U P T ) : ( T .(+) U ) --> U )
Theorem	pj1id 16696	Any element of a direct subspace sum can be decomposed into projections onto the left and right factors. (Contributed by Mario Carneiro, 15-Oct-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
|- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   &    |- P = ( proj1 ` G )   =>    |- ( ( ph /\ X e. ( T .(+) U ) ) -> X = ( ( ( T P U ) ` X ) .+ ( ( U P T ) ` X ) ) )
Theorem	pj1eq 16697	Any element of a direct subspace sum can be decomposed uniquely into projections onto the left and right factors. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   &    |- P = ( proj1 ` G )   &    |- ( ph -> X e. ( T .(+) U ) )   &    |- ( ph -> B e. T )   &    |- ( ph -> C e. U )   =>    |- ( ph -> ( X = ( B .+ C ) <-> ( ( ( T P U ) ` X ) = B /\ ( ( U P T ) ` X ) = C ) ) )
Theorem	pj1lid 16698	The left projection function is the identity on the left subspace. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   &    |- P = ( proj1 ` G )   =>    |- ( ( ph /\ X e. T ) -> ( ( T P U ) ` X ) = X )
Theorem	pj1rid 16699	The left projection function is the zero operator on the right subspace. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   &    |- P = ( proj1 ` G )   =>    |- ( ( ph /\ X e. U ) -> ( ( T P U ) ` X ) = .0. )
Theorem	pj1ghm 16700	The left projection function is a group homomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.)
|- .+ = ( +g ` G )   &    |- .(+) = ( LSSum ` G )   &    |- .0. = ( 0g ` G )   &    |- Z = (Cntz ` G )   &    |- ( ph -> T e. (SubGrp ` G ) )   &    |- ( ph -> U e. (SubGrp ` G ) )   &    |- ( ph -> ( T i^i U ) = { .0. } )   &    |- ( ph -> T C_ ( Z ` U ) )   &    |- P = ( proj1 ` G )   =>    |- ( ph -> ( T P U ) e. ( ( G ↾s ( T .(+) U ) ) GrpHom G ) )