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	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	Assertion	lsmsubg2	$⊢ (G \in Abel \land T \in SubGrp (G) \land U \in SubGrp (G)) \to T \underset{˙}{\oplus} U \in SubGrp (G)$

Step	Hyp	Ref	Expression
1		lsmcom.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
2		simp2	$⊢ (G \in Abel \land T \in SubGrp (G) \land U \in SubGrp (G)) \to T \in SubGrp (G)$
3		simp3	$⊢ (G \in Abel \land T \in SubGrp (G) \land U \in SubGrp (G)) \to U \in SubGrp (G)$
4		eqid	$⊢ Cntz (G) = Cntz (G)$
5		simp1	$⊢ (G \in Abel \land T \in SubGrp (G) \land U \in SubGrp (G)) \to G \in Abel$
6	4 5 2 3	ablcntzd	$⊢ (G \in Abel \land T \in SubGrp (G) \land U \in SubGrp (G)) \to T \subseteq Cntz (G) (U)$
7	1 4	lsmsubg	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Cntz (G) (U)) \to T \underset{˙}{\oplus} U \in SubGrp (G)$
8	2 3 6 7	syl3anc	$⊢ (G \in Abel \land T \in SubGrp (G) \land U \in SubGrp (G)) \to T \underset{˙}{\oplus} U \in SubGrp (G)$

Metamath Proof Explorer