Metamath Proof Explorer

Theorem lsmless12

Description: Subset implies subgroup sum subset. (Contributed by NM, 14-Jan-2015) (Revised by Mario Carneiro, 19-Apr-2016)

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

Proof

Step Hyp Ref Expression
1 lsmub1.p 
 |-  .(+) = ( LSSum ` G )
2 subgrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
3 2 ad2antrr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ ( R C_ S /\ T C_ U ) ) -> G e. Grp )
4 eqid 
 |-  ( Base ` G ) = ( Base ` G )
5 4 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ ( Base ` G ) )
6 5 ad2antrr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ ( R C_ S /\ T C_ U ) ) -> S C_ ( Base ` G ) )
7 simprr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ ( R C_ S /\ T C_ U ) ) -> T C_ U )
8 4 subgss 
 |-  ( U e. ( SubGrp ` G ) -> U C_ ( Base ` G ) )
9 8 ad2antlr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ ( R C_ S /\ T C_ U ) ) -> U C_ ( Base ` G ) )
10 7 9 sstrd 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ ( R C_ S /\ T C_ U ) ) -> T C_ ( Base ` G ) )
11 simprl 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ ( R C_ S /\ T C_ U ) ) -> R C_ S )
12 4 1 lsmless1x 
 |-  ( ( ( G e. Grp /\ S C_ ( Base ` G ) /\ T C_ ( Base ` G ) ) /\ R C_ S ) -> ( R .(+) T ) C_ ( S .(+) T ) )
13 3 6 10 11 12 syl31anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ ( R C_ S /\ T C_ U ) ) -> ( R .(+) T ) C_ ( S .(+) T ) )
14 simpll 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ ( R C_ S /\ T C_ U ) ) -> S e. ( SubGrp ` G ) )
15 simplr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ ( R C_ S /\ T C_ U ) ) -> U e. ( SubGrp ` G ) )
16 1 lsmless2 
 |-  ( ( S e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ U ) -> ( S .(+) T ) C_ ( S .(+) U ) )
17 14 15 7 16 syl3anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ ( R C_ S /\ T C_ U ) ) -> ( S .(+) T ) C_ ( S .(+) U ) )
18 13 17 sstrd 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ ( R C_ S /\ T C_ U ) ) -> ( R .(+) T ) C_ ( S .(+) U ) )