Theorem lsmcom

Description: Subgroup sum commutes. (Contributed by NM, 6-Feb-2014) (Revised by Mario Carneiro, 21-Jun-2014)

	Ref	Expression
Hypothesis	lsmcom.s	|- .(+) = ( LSSum ` G )
Assertion	lsmcom	|- ( ( G e. Abel /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( T .(+) U ) = ( U .(+) T ) )

Proof

Step	Hyp	Ref	Expression
1		lsmcom.s	|- .(+) = ( LSSum ` G )
2		id	|- ( G e. Abel -> G e. Abel )
3		eqid	|- ( Base ` G ) = ( Base ` G )
4	3	subgss	|- ( T e. ( SubGrp ` G ) -> T C_ ( Base ` G ) )
5	3	subgss	|- ( U e. ( SubGrp ` G ) -> U C_ ( Base ` G ) )
6	3 1	lsmcomx	|- ( ( G e. Abel /\ T C_ ( Base ` G ) /\ U C_ ( Base ` G ) ) -> ( T .(+) U ) = ( U .(+) T ) )
7	2 4 5 6	syl3an	|- ( ( G e. Abel /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( T .(+) U ) = ( U .(+) T ) )