Theorem lsmssv

Description: Subgroup sum is a subset of the base. (Contributed by Mario Carneiro, 19-Apr-2016)

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

Proof

Step	Hyp	Ref	Expression
1		lsmless2.v	|- B = ( Base ` G )
2		lsmless2.s	|- .(+) = ( LSSum ` G )
3		eqid	|- ( +g ` G ) = ( +g ` G )
4	1 3 2	lsmvalx	|- ( ( G e. Mnd /\ T C_ B /\ U C_ B ) -> ( T .(+) U ) = ran ( x e. T , y e. U |-> ( x ( +g ` G ) y ) ) )
5		simpl1	|- ( ( ( G e. Mnd /\ T C_ B /\ U C_ B ) /\ ( x e. T /\ y e. U ) ) -> G e. Mnd )
6		simp2	|- ( ( G e. Mnd /\ T C_ B /\ U C_ B ) -> T C_ B )
7	6	sselda	|- ( ( ( G e. Mnd /\ T C_ B /\ U C_ B ) /\ x e. T ) -> x e. B )
8	7	adantrr	|- ( ( ( G e. Mnd /\ T C_ B /\ U C_ B ) /\ ( x e. T /\ y e. U ) ) -> x e. B )
9		simp3	|- ( ( G e. Mnd /\ T C_ B /\ U C_ B ) -> U C_ B )
10	9	sselda	|- ( ( ( G e. Mnd /\ T C_ B /\ U C_ B ) /\ y e. U ) -> y e. B )
11	10	adantrl	|- ( ( ( G e. Mnd /\ T C_ B /\ U C_ B ) /\ ( x e. T /\ y e. U ) ) -> y e. B )
12	1 3	mndcl	|- ( ( G e. Mnd /\ x e. B /\ y e. B ) -> ( x ( +g ` G ) y ) e. B )
13	5 8 11 12	syl3anc	|- ( ( ( G e. Mnd /\ T C_ B /\ U C_ B ) /\ ( x e. T /\ y e. U ) ) -> ( x ( +g ` G ) y ) e. B )
14	13	ralrimivva	|- ( ( G e. Mnd /\ T C_ B /\ U C_ B ) -> A. x e. T A. y e. U ( x ( +g ` G ) y ) e. B )
15		eqid	|- ( x e. T , y e. U |-> ( x ( +g ` G ) y ) ) = ( x e. T , y e. U |-> ( x ( +g ` G ) y ) )
16	15	fmpo	|- ( A. x e. T A. y e. U ( x ( +g ` G ) y ) e. B <-> ( x e. T , y e. U |-> ( x ( +g ` G ) y ) ) : ( T X. U ) --> B )
17	14 16	sylib	|- ( ( G e. Mnd /\ T C_ B /\ U C_ B ) -> ( x e. T , y e. U |-> ( x ( +g ` G ) y ) ) : ( T X. U ) --> B )
18	17	frnd	|- ( ( G e. Mnd /\ T C_ B /\ U C_ B ) -> ran ( x e. T , y e. U |-> ( x ( +g ` G ) y ) ) C_ B )
19	4 18	eqsstrd	|- ( ( G e. Mnd /\ T C_ B /\ U C_ B ) -> ( T .(+) U ) C_ B )