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 ‘ 𝐺 )
Assertion lsmsubg2 ( ( 𝐺 ∈ Abel ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑇 𝑈 ) ∈ ( SubGrp ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 lsmcom.s = ( LSSum ‘ 𝐺 )
2 simp2 ( ( 𝐺 ∈ Abel ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
3 simp3 ( ( 𝐺 ∈ Abel ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
4 eqid ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
5 simp1 ( ( 𝐺 ∈ Abel ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐺 ∈ Abel )
6 4 5 2 3 ablcntzd ( ( 𝐺 ∈ Abel ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑇 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ 𝑈 ) )
7 1 4 lsmsubg ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ 𝑈 ) ) → ( 𝑇 𝑈 ) ∈ ( SubGrp ‘ 𝐺 ) )
8 2 3 6 7 syl3anc ( ( 𝐺 ∈ Abel ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑇 𝑈 ) ∈ ( SubGrp ‘ 𝐺 ) )