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