Metamath Proof Explorer

Theorem lsmub1x

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

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

Proof

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