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

Metamath Proof Explorer

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 )