Metamath Proof Explorer

Theorem lsmub2

Description: Subgroup sum is an upper bound of its arguments. (Contributed by NM, 6-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)

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

Proof

Step Hyp Ref Expression
1 lsmub1.p 
 |-  .(+) = ( LSSum ` G )
2 subgsubm 
 |-  ( T e. ( SubGrp ` G ) -> T e. ( SubMnd ` G ) )
3 eqid 
 |-  ( Base ` G ) = ( Base ` G )
4 3 subgss 
 |-  ( U e. ( SubGrp ` G ) -> U C_ ( Base ` G ) )
5 3 1 lsmub2x 
 |-  ( ( T e. ( SubMnd ` G ) /\ U C_ ( Base ` G ) ) -> U C_ ( T .(+) U ) )
6 2 4 5 syl2an 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> U C_ ( T .(+) U ) )