Metamath Proof Explorer

Theorem lsmss2b

Description: Subgroup sum with a subset. (Contributed by NM, 10-Jan-2015) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypothesis lsmub1.p 
|- .(+) = ( LSSum ` G )
Assertion lsmss2b 
|- ( ( 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 1 lsmss2 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ U C_ T ) -> ( T .(+) U ) = T )
3 2 3expia 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( U C_ T -> ( T .(+) U ) = T ) )
4 1 lsmub2 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> U C_ ( T .(+) U ) )
5 sseq2 
 |-  ( ( T .(+) U ) = T -> ( U C_ ( T .(+) U ) <-> U C_ T ) )
6 4 5 syl5ibcom 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( ( T .(+) U ) = T -> U C_ T ) )
7 3 6 impbid 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( U C_ T <-> ( T .(+) U ) = T ) )