Theorem lsm01

Description: Subgroup sum with the zero subgroup. (Contributed by NM, 27-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2016)

	Ref	Expression
Hypotheses	lsm01.z	|- .0. = ( 0g ` G )
	lsm01.p	|- .(+) = ( LSSum ` G )
Assertion	lsm01	|- ( X e. ( SubGrp ` G ) -> ( X .(+) { .0. } ) = X )

Proof

Step	Hyp	Ref	Expression
1		lsm01.z	|- .0. = ( 0g ` G )
2		lsm01.p	|- .(+) = ( LSSum ` G )
3		subgrcl	|- ( X e. ( SubGrp ` G ) -> G e. Grp )
4	1	0subg	|- ( G e. Grp -> { .0. } e. ( SubGrp ` G ) )
5	3 4	syl	|- ( X e. ( SubGrp ` G ) -> { .0. } e. ( SubGrp ` G ) )
6	1	subg0cl	|- ( X e. ( SubGrp ` G ) -> .0. e. X )
7	6	snssd	|- ( X e. ( SubGrp ` G ) -> { .0. } C_ X )
8	2	lsmss2	|- ( ( X e. ( SubGrp ` G ) /\ { .0. } e. ( SubGrp ` G ) /\ { .0. } C_ X ) -> ( X .(+) { .0. } ) = X )
9	5 7 8	mpd3an23	|- ( X e. ( SubGrp ` G ) -> ( X .(+) { .0. } ) = X )