This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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