Metamath Proof Explorer


Theorem lsmsubg2

Description: The sum of two subgroups is a subgroup. (Contributed by NM, 4-Feb-2014) (Proof shortened by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypothesis lsmcom.s
|- .(+) = ( LSSum ` G )
Assertion lsmsubg2
|- ( ( G e. Abel /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( T .(+) U ) e. ( SubGrp ` G ) )

Proof

Step Hyp Ref Expression
1 lsmcom.s
 |-  .(+) = ( LSSum ` G )
2 simp2
 |-  ( ( G e. Abel /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> T e. ( SubGrp ` G ) )
3 simp3
 |-  ( ( G e. Abel /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> U e. ( SubGrp ` G ) )
4 eqid
 |-  ( Cntz ` G ) = ( Cntz ` G )
5 simp1
 |-  ( ( G e. Abel /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> G e. Abel )
6 4 5 2 3 ablcntzd
 |-  ( ( G e. Abel /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> T C_ ( ( Cntz ` G ) ` U ) )
7 1 4 lsmsubg
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( ( Cntz ` G ) ` U ) ) -> ( T .(+) U ) e. ( SubGrp ` G ) )
8 2 3 6 7 syl3anc
 |-  ( ( G e. Abel /\ T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( T .(+) U ) e. ( SubGrp ` G ) )