P. 181 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18001-18100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	gexod 18001	Any group element is annihilated by any multiple of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016.)
|- X = ( Base ` G )   &    |- E = (gEx ` G )   &    |- O = ( od ` G )   =>    |- ( ( G e. Grp /\ A e. X ) -> ( O ` A ) || E )
Theorem	gexcl3 18002*	If the order of every group element is bounded by N, the group has finite exponent. (Contributed by Mario Carneiro, 24-Apr-2016.)
|- X = ( Base ` G )   &    |- E = (gEx ` G )   &    |- O = ( od ` G )   =>    |- ( ( G e. Grp /\ A. x e. X ( O ` x ) e. ( 1 ... N ) ) -> E e. NN )
Theorem	gexnnod 18003	Every group element has finite order if the exponent is finite. (Contributed by Mario Carneiro, 24-Apr-2016.)
|- X = ( Base ` G )   &    |- E = (gEx ` G )   &    |- O = ( od ` G )   =>    |- ( ( G e. Grp /\ E e. NN /\ A e. X ) -> ( O ` A ) e. NN )
Theorem	gexcl2 18004	The exponent of a finite group is finite. (Contributed by Mario Carneiro, 24-Apr-2016.)
|- X = ( Base ` G )   &    |- E = (gEx ` G )   =>    |- ( ( G e. Grp /\ X e. Fin ) -> E e. NN )
Theorem	gexdvds3 18005	The exponent of a finite group divides the order (cardinality) of the group. Corollary of Lagrange's theorem for the order of a subgroup. (Contributed by Mario Carneiro, 24-Apr-2016.)
|- X = ( Base ` G )   &    |- E = (gEx ` G )   =>    |- ( ( G e. Grp /\ X e. Fin ) -> E || ( # ` X ) )
Theorem	gex1 18006	A group or monoid has exponent 1 iff it is trivial. (Contributed by Mario Carneiro, 24-Apr-2016.)
|- X = ( Base ` G )   &    |- E = (gEx ` G )   =>    |- ( G e. Mnd -> ( E = 1 <-> X ~~ 1o ) )
Theorem	ispgp 18007*	A group is a P-group if every element has some power of P as its order. (Contributed by Mario Carneiro, 15-Jan-2015.)
|- X = ( Base ` G )   &    |- O = ( od ` G )   =>    |- ( P pGrp G <-> ( P e. Prime /\ G e. Grp /\ A. x e. X E. n e. NN0 ( O ` x ) = ( P ^ n ) ) )
Theorem	pgpprm 18008	Reverse closure for the first argument of pGrp. (Contributed by Mario Carneiro, 15-Jan-2015.)
|- ( P pGrp G -> P e. Prime )
Theorem	pgpgrp 18009	Reverse closure for the second argument of pGrp. (Contributed by Mario Carneiro, 15-Jan-2015.)
|- ( P pGrp G -> G e. Grp )
Theorem	pgpfi1 18010	A finite group with order a power of a prime P is a P-group. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- X = ( Base ` G )   =>    |- ( ( G e. Grp /\ P e. Prime /\ N e. NN0 ) -> ( ( # ` X ) = ( P ^ N ) -> P pGrp G ) )
Theorem	pgp0 18011	The identity subgroup is a P-group for every prime P. (Contributed by Mario Carneiro, 19-Jan-2015.)
|- .0. = ( 0g ` G )   =>    |- ( ( G e. Grp /\ P e. Prime ) -> P pGrp ( G ↾s { .0. } ) )
Theorem	subgpgp 18012	A subgroup of a p-group is a p-group. (Contributed by Mario Carneiro, 27-Apr-2016.)
|- ( ( P pGrp G /\ S e. (SubGrp ` G ) ) -> P pGrp ( G ↾s S ) )
Theorem	sylow1lem1 18013*	Lemma for sylow1 18018. The p-adic valuation of the size of S is equal to the number of excess powers of P in ( # ` X ) / ( P ^ N ). (Contributed by Mario Carneiro, 15-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 ) }   =>    |- ( ph -> ( ( # ` S ) e. NN /\ ( P pCnt ( # ` S ) ) = ( ( P pCnt ( # ` X ) ) - N ) ) )
Theorem	sylow1lem2 18014*	Lemma for sylow1 18018. The function .(+) is a group action on S. (Contributed by Mario Carneiro, 15-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 ) ) )   =>    |- ( ph -> .(+) e. ( G GrpAct S ) )
Theorem	sylow1lem3 18015*	Lemma for sylow1 18018. One of the orbits of the group action has p-adic valuation less than the prime count of the set S. (Contributed by Mario Carneiro, 15-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 -> E. w e. S ( P pCnt ( # ` [ w ] .~ ) ) <_ ( ( P pCnt ( # ` X ) ) - N ) )
Theorem	sylow1lem4 18016*	Lemma for sylow1 18018. The stabilizer subgroup of any element of S is at most P ^ N in size. (Contributed by Mario Carneiro, 15-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 -> ( # ` H ) <_ ( P ^ N ) )
Theorem	sylow1lem5 18017*	Lemma for sylow1 18018. 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 18018*	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 18019*	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 18020*	The converse to pgpfi1 18010. 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 18021	Alternate version of pgpfi 18020. (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 18022	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 18023*	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 18024	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 18025	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 18026	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 18027	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 18028	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 18029*	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 18030	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 18031	A Sylow subgroup that is contained in a larger subgroup is also Sylow with respect to the subgroup. (The converse need not be true.) (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 18032*	Lemma for sylow2a 18034. 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 18033*	Lemma for sylow2a 18034. 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 18034*	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 18035*	Lemma for sylow2b 18038. 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 18036*	Lemma for sylow2b 18038. 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 18037*	Sylow's second theorem. Putting together the results of sylow2a 18034 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 18038*	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 18039	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 18040	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 18041*	Sylow's second theorem. See also sylow2b 18038 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 18040). 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 18042*	Lemma for sylow3 18048, 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 18043*	Lemma for sylow3 18048, 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 18044*	Lemma for sylow3 18048, 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 18045*	Lemma for sylow3 18048, 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 18046*	Lemma for sylow3 18048, second part. Reduce the group action of sylow3lem1 18042 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 18047*	Lemma for sylow3 18048, second part. Using the lemma sylow2a 18034, 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 18048	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.11  Direct products
Syntax	clsm 18049	Extend class notation with subgroup sum.
class LSSum
Syntax	cpj1 18050	Extend class notation with left projection.
class proj1
Definition	df-lsm 18051*	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 18052*	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 18053*	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 18054*	Subspace sum value (for a group or vector space). Extended domain version of lsmval 18063. (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 18055*	Subspace sum membership (for a group or vector space). Extended domain version of lsmelval 18064. (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 18056	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 18057	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 18058	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 18059	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 18060	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 18061	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 18062	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 18063*	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 18064*	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 18065	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 18066*	Subgroup sum membership analogue of lsmelval 18064 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 18067	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 18068	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 18069	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 18070	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 18071	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 18072	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 18073	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 18074	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 18075	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 18076	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 18077	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 18078	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 18079	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 18080	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 18081	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 18082	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 18083	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 18084	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 18085	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 18086	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 18087	Equivalent expressions for "not less than". (chnlei 28344 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 18088	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 18089	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 18090*	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 18091	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 18092	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 18093	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 18094	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 18095	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 18096	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 18097	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 18098	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 18099	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 18100	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. } ) ) )