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