This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lsmless2x

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

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

Proof

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