Metamath Proof Explorer

Theorem lsmless1

Description: Subset implies subgroup sum subset. (Contributed by NM, 6-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)

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

Proof

Step Hyp Ref Expression
1 lsmub1.p 
 |-  .(+) = ( LSSum ` G )
2 subgrcl 
 |-  ( T e. ( SubGrp ` G ) -> G e. Grp )
3 2 3ad2ant1 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ S C_ T ) -> G e. Grp )
4 eqid 
 |-  ( Base ` G ) = ( Base ` G )
5 4 subgss 
 |-  ( T e. ( SubGrp ` G ) -> T C_ ( Base ` G ) )
6 5 3ad2ant1 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ S C_ T ) -> T C_ ( Base ` G ) )
7 4 subgss 
 |-  ( U e. ( SubGrp ` G ) -> U C_ ( Base ` G ) )
8 7 3ad2ant2 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ S C_ T ) -> U C_ ( Base ` G ) )
9 simp3 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ S C_ T ) -> S C_ T )
10 4 1 lsmless1x 
 |-  ( ( ( G e. Grp /\ T C_ ( Base ` G ) /\ U C_ ( Base ` G ) ) /\ S C_ T ) -> ( S .(+) U ) C_ ( T .(+) U ) )
11 3 6 8 9 10 syl31anc 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ S C_ T ) -> ( S .(+) U ) C_ ( T .(+) U ) )