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 ∈ Abel ∧ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G → T ⊕ ˙ U ∈ SubGrp ⁡ G

Proof

Step Hyp Ref Expression
1 lsmcom.s ⊢ ⊕ ˙ = LSSum ⁡ G
2 simp2 ⊢ G ∈ Abel ∧ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G → T ∈ SubGrp ⁡ G
3 simp3 ⊢ G ∈ Abel ∧ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G → U ∈ SubGrp ⁡ G
4 eqid ⊢ Cntz ⁡ G = Cntz ⁡ G
5 simp1 ⊢ G ∈ Abel ∧ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G → G ∈ Abel
6 4 5 2 3 ablcntzd ⊢ G ∈ Abel ∧ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G → T ⊆ Cntz ⁡ G ⁡ U
7 1 4 lsmsubg ⊢ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ T ⊆ Cntz ⁡ G ⁡ U → T ⊕ ˙ U ∈ SubGrp ⁡ G
8 2 3 6 7 syl3anc ⊢ G ∈ Abel ∧ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G → T ⊕ ˙ U ∈ SubGrp ⁡ G