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

Metamath Proof Explorer

Theorem lsmunss

Description: Union of subgroups is a subset of subgroup sum. (Contributed by NM, 6-Feb-2014) (Proof shortened by Mario Carneiro, 21-Jun-2014)

		Ref	Expression
	Hypothesis	lsmub1.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	Assertion	lsmunss	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G)) \to T \cup U \subseteq T \underset{˙}{\oplus} U$

Step	Hyp	Ref	Expression
1		lsmub1.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
2	1	lsmub1	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G)) \to T \subseteq T \underset{˙}{\oplus} U$
3	1	lsmub2	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G)) \to U \subseteq T \underset{˙}{\oplus} U$
4	2 3	unssd	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G)) \to T \cup U \subseteq T \underset{˙}{\oplus} U$