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 SubGrp G U SubGrp G U T T ˙ U = T

Proof

Step Hyp Ref Expression
1 lsmub1.p ˙ = LSSum G
2 1 lsmss2 T SubGrp G U SubGrp G U T T ˙ U = T
3 2 3expia T SubGrp G U SubGrp G U T T ˙ U = T
4 1 lsmub2 T SubGrp G U SubGrp G U T ˙ U
5 sseq2 T ˙ U = T U T ˙ U U T
6 4 5 syl5ibcom T SubGrp G U SubGrp G T ˙ U = T U T
7 3 6 impbid T SubGrp G U SubGrp G U T T ˙ U = T