Theorem lsm02

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	lsm02	|- ( X e. ( SubGrp ` G ) -> ( { .0. } .(+) X ) = 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		id	|- ( X e. ( SubGrp ` G ) -> X e. ( SubGrp ` G ) )
7	1	subg0cl	|- ( X e. ( SubGrp ` G ) -> .0. e. X )
8	7	snssd	|- ( X e. ( SubGrp ` G ) -> { .0. } C_ X )
9	2	lsmss1	|- ( ( { .0. } e. ( SubGrp ` G ) /\ X e. ( SubGrp ` G ) /\ { .0. } C_ X ) -> ( { .0. } .(+) X ) = X )
10	5 6 8 9	syl3anc	|- ( X e. ( SubGrp ` G ) -> ( { .0. } .(+) X ) = X )