Metamath Proof Explorer

Theorem lsmunss

Description: Union of subgroups is a subset of subgroup sum. (Contributed by NM, 6-Feb-2014) (Proof shortened by Mario Carneiro, 21-Jun-2014)

Ref Expression
Hypothesis lsmub1.p 
|- .(+) = ( LSSum ` G )
Assertion lsmunss 
|- ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( T u. U ) C_ ( T .(+) U ) )

Proof

Step Hyp Ref Expression
1 lsmub1.p 
 |-  .(+) = ( LSSum ` G )
2 1 lsmub1 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> T C_ ( T .(+) U ) )
3 1 lsmub2 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> U C_ ( T .(+) U ) )
4 2 3 unssd 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( T u. U ) C_ ( T .(+) U ) )