Metamath Proof Explorer


Theorem lsmless1x

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

Ref Expression
Hypotheses lsmless2.v
|- B = ( Base ` G )
lsmless2.s
|- .(+) = ( LSSum ` G )
Assertion lsmless1x
|- ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ R C_ T ) -> ( R .(+) U ) C_ ( T .(+) U ) )

Proof

Step Hyp Ref Expression
1 lsmless2.v
 |-  B = ( Base ` G )
2 lsmless2.s
 |-  .(+) = ( LSSum ` G )
3 ssrexv
 |-  ( R C_ T -> ( E. y e. R E. z e. U x = ( y ( +g ` G ) z ) -> E. y e. T E. z e. U x = ( y ( +g ` G ) z ) ) )
4 3 adantl
 |-  ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ R C_ T ) -> ( E. y e. R E. z e. U x = ( y ( +g ` G ) z ) -> E. y e. T E. z e. U x = ( y ( +g ` G ) z ) ) )
5 simpl1
 |-  ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ R C_ T ) -> G e. V )
6 simpr
 |-  ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ R C_ T ) -> R C_ T )
7 simpl2
 |-  ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ R C_ T ) -> T C_ B )
8 6 7 sstrd
 |-  ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ R C_ T ) -> R C_ B )
9 simpl3
 |-  ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ R C_ T ) -> U C_ B )
10 eqid
 |-  ( +g ` G ) = ( +g ` G )
11 1 10 2 lsmelvalx
 |-  ( ( G e. V /\ R C_ B /\ U C_ B ) -> ( x e. ( R .(+) U ) <-> E. y e. R E. z e. U x = ( y ( +g ` G ) z ) ) )
12 5 8 9 11 syl3anc
 |-  ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ R C_ T ) -> ( x e. ( R .(+) U ) <-> E. y e. R E. z e. U x = ( y ( +g ` G ) z ) ) )
13 1 10 2 lsmelvalx
 |-  ( ( G e. V /\ T C_ B /\ U C_ B ) -> ( x e. ( T .(+) U ) <-> E. y e. T E. z e. U x = ( y ( +g ` G ) z ) ) )
14 13 adantr
 |-  ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ R C_ T ) -> ( x e. ( T .(+) U ) <-> E. y e. T E. z e. U x = ( y ( +g ` G ) z ) ) )
15 4 12 14 3imtr4d
 |-  ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ R C_ T ) -> ( x e. ( R .(+) U ) -> x e. ( T .(+) U ) ) )
16 15 ssrdv
 |-  ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ R C_ T ) -> ( R .(+) U ) C_ ( T .(+) U ) )