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

Metamath Proof Explorer

Theorem lsmub1

Description: Subgroup sum is an upper bound of its arguments. (Contributed by NM, 6-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)

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

Step	Hyp	Ref	Expression
1		lsmub1.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
2		eqid	$⊢ {Base}_{G} = {Base}_{G}$
3	2	subgss	$⊢ T \in SubGrp (G) \to T \subseteq {Base}_{G}$
4		subgsubm	$⊢ U \in SubGrp (G) \to U \in SubMnd (G)$
5	2 1	lsmub1x	$⊢ (T \subseteq {Base}_{G} \land U \in SubMnd (G)) \to T \subseteq T \underset{˙}{\oplus} U$
6	3 4 5	syl2an	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G)) \to T \subseteq T \underset{˙}{\oplus} U$