lsmub2x

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
Hypotheses	lsmless2.v	$⊢ B = {Base}_{G}$
	lsmless2.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
Assertion	lsmub2x	$⊢ (T \in SubMnd (G) \land U \subseteq B) \to U \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	$⊢ T \in SubMnd (G) \to G \in Mnd$
4	3	ad2antrr	$⊢ ((T \in SubMnd (G) \land U \subseteq B) \land x \in U) \to G \in Mnd$
5		simpr	$⊢ (T \in SubMnd (G) \land U \subseteq B) \to U \subseteq B$
6	5	sselda	$⊢ ((T \in SubMnd (G) \land U \subseteq B) \land x \in U) \to x \in B$
7		eqid	$⊢ +_{G} = +_{G}$
8		eqid	$⊢ 0_{G} = 0_{G}$
9	1 7 8	mndlid	$⊢ (G \in Mnd \land x \in B) \to 0_{G} +_{G} x = x$
10	4 6 9	syl2anc	$⊢ ((T \in SubMnd (G) \land U \subseteq B) \land x \in U) \to 0_{G} +_{G} x = x$
11	1	submss	$⊢ T \in SubMnd (G) \to T \subseteq B$
12	11	ad2antrr	$⊢ ((T \in SubMnd (G) \land U \subseteq B) \land x \in U) \to T \subseteq B$
13		simplr	$⊢ ((T \in SubMnd (G) \land U \subseteq B) \land x \in U) \to U \subseteq B$
14	8	subm0cl	$⊢ T \in SubMnd (G) \to 0_{G} \in T$
15	14	ad2antrr	$⊢ ((T \in SubMnd (G) \land U \subseteq B) \land x \in U) \to 0_{G} \in T$
16		simpr	$⊢ ((T \in SubMnd (G) \land U \subseteq B) \land x \in U) \to x \in U$
17	1 7 2	lsmelvalix	$⊢ ((G \in Mnd \land T \subseteq B \land U \subseteq B) \land (0_{G} \in T \land x \in U)) \to 0_{G} +_{G} x \in (T \underset{˙}{\oplus} U)$
18	4 12 13 15 16 17	syl32anc	$⊢ ((T \in SubMnd (G) \land U \subseteq B) \land x \in U) \to 0_{G} +_{G} x \in (T \underset{˙}{\oplus} U)$
19	10 18	eqeltrrd	$⊢ ((T \in SubMnd (G) \land U \subseteq B) \land x \in U) \to x \in (T \underset{˙}{\oplus} U)$
20	19	ex	$⊢ (T \in SubMnd (G) \land U \subseteq B) \to (x \in U \to x \in (T \underset{˙}{\oplus} U))$
21	20	ssrdv	$⊢ (T \in SubMnd (G) \land U \subseteq B) \to U \subseteq T \underset{˙}{\oplus} U$

Metamath Proof Explorer

Theorem lsmub2x

Proof