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