Metamath Proof Explorer


Theorem lsmub2x

Description: Subgroup sum is an upper bound of its arguments. (Contributed by NM, 6-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)

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

Proof

Step Hyp Ref Expression
1 lsmless2.v
 |-  B = ( Base ` G )
2 lsmless2.s
 |-  .(+) = ( LSSum ` G )
3 submrcl
 |-  ( T e. ( SubMnd ` G ) -> G e. Mnd )
4 3 ad2antrr
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U C_ B ) /\ x e. U ) -> G e. Mnd )
5 simpr
 |-  ( ( T e. ( SubMnd ` G ) /\ U C_ B ) -> U C_ B )
6 5 sselda
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U C_ B ) /\ x e. U ) -> x e. B )
7 eqid
 |-  ( +g ` G ) = ( +g ` G )
8 eqid
 |-  ( 0g ` G ) = ( 0g ` G )
9 1 7 8 mndlid
 |-  ( ( G e. Mnd /\ x e. B ) -> ( ( 0g ` G ) ( +g ` G ) x ) = x )
10 4 6 9 syl2anc
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U C_ B ) /\ x e. U ) -> ( ( 0g ` G ) ( +g ` G ) x ) = x )
11 1 submss
 |-  ( T e. ( SubMnd ` G ) -> T C_ B )
12 11 ad2antrr
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U C_ B ) /\ x e. U ) -> T C_ B )
13 simplr
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U C_ B ) /\ x e. U ) -> U C_ B )
14 8 subm0cl
 |-  ( T e. ( SubMnd ` G ) -> ( 0g ` G ) e. T )
15 14 ad2antrr
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U C_ B ) /\ x e. U ) -> ( 0g ` G ) e. T )
16 simpr
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U C_ B ) /\ x e. U ) -> x e. U )
17 1 7 2 lsmelvalix
 |-  ( ( ( G e. Mnd /\ T C_ B /\ U C_ B ) /\ ( ( 0g ` G ) e. T /\ x e. U ) ) -> ( ( 0g ` G ) ( +g ` G ) x ) e. ( T .(+) U ) )
18 4 12 13 15 16 17 syl32anc
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U C_ B ) /\ x e. U ) -> ( ( 0g ` G ) ( +g ` G ) x ) e. ( T .(+) U ) )
19 10 18 eqeltrrd
 |-  ( ( ( T e. ( SubMnd ` G ) /\ U C_ B ) /\ x e. U ) -> x e. ( T .(+) U ) )
20 19 ex
 |-  ( ( T e. ( SubMnd ` G ) /\ U C_ B ) -> ( x e. U -> x e. ( T .(+) U ) ) )
21 20 ssrdv
 |-  ( ( T e. ( SubMnd ` G ) /\ U C_ B ) -> U C_ ( T .(+) U ) )