lsmss2

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	lsmss2	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land U \subseteq T) \to T \underset{˙}{\oplus} U = T$

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

Metamath Proof Explorer