lsmub1x

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

	Ref	Expression
Hypotheses	lsmless2.v	$⊢ B = {Base}_{G}$
	lsmless2.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
Assertion	lsmub1x	$⊢ (T \subseteq B \land U \in SubMnd (G)) \to T \subseteq T \underset{˙}{\oplus} U$

Proof

Step	Hyp	Ref	Expression
1		lsmless2.v	$⊢ B = {Base}_{G}$
2		lsmless2.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
3		submrcl	$⊢ U \in SubMnd (G) \to G \in Mnd$
4	3	ad2antlr	$⊢ ((T \subseteq B \land U \in SubMnd (G)) \land x \in T) \to G \in Mnd$
5		simpll	$⊢ ((T \subseteq B \land U \in SubMnd (G)) \land x \in T) \to T \subseteq B$
6		simpr	$⊢ ((T \subseteq B \land U \in SubMnd (G)) \land x \in T) \to x \in T$
7	5 6	sseldd	$⊢ ((T \subseteq B \land U \in SubMnd (G)) \land x \in T) \to x \in B$
8		eqid	$⊢ +_{G} = +_{G}$
9		eqid	$⊢ 0_{G} = 0_{G}$
10	1 8 9	mndrid	$⊢ (G \in Mnd \land x \in B) \to x +_{G} 0_{G} = x$
11	4 7 10	syl2anc	$⊢ ((T \subseteq B \land U \in SubMnd (G)) \land x \in T) \to x +_{G} 0_{G} = x$
12	1	submss	$⊢ U \in SubMnd (G) \to U \subseteq B$
13	12	ad2antlr	$⊢ ((T \subseteq B \land U \in SubMnd (G)) \land x \in T) \to U \subseteq B$
14	9	subm0cl	$⊢ U \in SubMnd (G) \to 0_{G} \in U$
15	14	ad2antlr	$⊢ ((T \subseteq B \land U \in SubMnd (G)) \land x \in T) \to 0_{G} \in U$
16	1 8 2	lsmelvalix	$⊢ ((G \in Mnd \land T \subseteq B \land U \subseteq B) \land (x \in T \land 0_{G} \in U)) \to x +_{G} 0_{G} \in (T \underset{˙}{\oplus} U)$
17	4 5 13 6 15 16	syl32anc	$⊢ ((T \subseteq B \land U \in SubMnd (G)) \land x \in T) \to x +_{G} 0_{G} \in (T \underset{˙}{\oplus} U)$
18	11 17	eqeltrrd	$⊢ ((T \subseteq B \land U \in SubMnd (G)) \land x \in T) \to x \in (T \underset{˙}{\oplus} U)$
19	18	ex	$⊢ (T \subseteq B \land U \in SubMnd (G)) \to (x \in T \to x \in (T \underset{˙}{\oplus} U))$
20	19	ssrdv	$⊢ (T \subseteq B \land U \in SubMnd (G)) \to T \subseteq T \underset{˙}{\oplus} U$

Metamath Proof Explorer

Theorem lsmub1x

Proof