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 ) )