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 | ||
---|---|---|---|
Hypothesis | lsmub1.p | |- .(+) = ( LSSum ` G ) |
|
Assertion | lsmub1 | |- ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> T C_ ( T .(+) U ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lsmub1.p | |- .(+) = ( LSSum ` G ) |
|
2 | eqid | |- ( Base ` G ) = ( Base ` G ) |
|
3 | 2 | subgss | |- ( T e. ( SubGrp ` G ) -> T C_ ( Base ` G ) ) |
4 | subgsubm | |- ( U e. ( SubGrp ` G ) -> U e. ( SubMnd ` G ) ) |
|
5 | 2 1 | lsmub1x | |- ( ( T C_ ( Base ` G ) /\ U e. ( SubMnd ` G ) ) -> T C_ ( T .(+) U ) ) |
6 | 3 4 5 | syl2an | |- ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> T C_ ( T .(+) U ) ) |