Metamath Proof Explorer


Theorem lsmss1

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 lsmss1
|- ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ U ) -> ( T .(+) U ) = U )

Proof

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