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 ) )