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