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