lsmss1

Description: Subgroup sum with a subset. (Contributed by NM, 27-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2016)

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

Step	Hyp	Ref	Expression
1		lsmub1.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
2		ssid	$⊢ U \subseteq U$
3	1	lsmlub	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land U \in SubGrp (G)) \to ((T \subseteq U \land U \subseteq U) \leftrightarrow T \underset{˙}{\oplus} U \subseteq U)$
4	3	3anidm23	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G)) \to ((T \subseteq U \land U \subseteq U) \leftrightarrow T \underset{˙}{\oplus} U \subseteq U)$
5	4	biimpd	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G)) \to ((T \subseteq U \land U \subseteq U) \to T \underset{˙}{\oplus} U \subseteq U)$
6	2 5	mpan2i	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G)) \to (T \subseteq U \to T \underset{˙}{\oplus} U \subseteq U)$
7	6	3impia	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq U) \to T \underset{˙}{\oplus} U \subseteq U$
8	1	lsmub2	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G)) \to U \subseteq T \underset{˙}{\oplus} U$
9	8	3adant3	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq U) \to U \subseteq T \underset{˙}{\oplus} U$
10	7 9	eqssd	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq U) \to T \underset{˙}{\oplus} U = U$

Metamath Proof Explorer