Metamath Proof Explorer

Theorem lsmss2

Description: Subgroup sum with a subset. (Contributed by NM, 27-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypothesis lsmub1.p 
|- .(+) = ( LSSum ` G )
Assertion lsmss2 
|- ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ U C_ T ) -> ( T .(+) U ) = T )

Proof

Step Hyp Ref Expression
1 lsmub1.p 
 |-  .(+) = ( LSSum ` G )
2 ssid 
 |-  T C_ T
3 1 lsmlub 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) ) -> ( ( T C_ T /\ U C_ T ) <-> ( T .(+) U ) C_ T ) )
4 3 3anidm13 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( ( T C_ T /\ U C_ T ) <-> ( T .(+) U ) C_ T ) )
5 4 biimpd 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( ( T C_ T /\ U C_ T ) -> ( T .(+) U ) C_ T ) )
6 2 5 mpani 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( U C_ T -> ( T .(+) U ) C_ T ) )
7 6 3impia 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ U C_ T ) -> ( T .(+) U ) C_ T )
8 1 lsmub1 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> T C_ ( T .(+) U ) )
9 8 3adant3 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ U C_ T ) -> T C_ ( T .(+) U ) )
10 7 9 eqssd 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ U C_ T ) -> ( T .(+) U ) = T )