lsmss2b

Description: Subgroup sum with a subset. (Contributed by NM, 10-Jan-2015) (Revised by Mario Carneiro, 19-Apr-2016)

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

Step	Hyp	Ref	Expression
1		lsmub1.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
2	1	lsmss2	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land U \subseteq T) \to T \underset{˙}{\oplus} U = T$
3	2	3expia	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G)) \to (U \subseteq T \to T \underset{˙}{\oplus} U = T)$
4	1	lsmub2	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G)) \to U \subseteq T \underset{˙}{\oplus} U$
5		sseq2	$⊢ T \underset{˙}{\oplus} U = T \to (U \subseteq T \underset{˙}{\oplus} U \leftrightarrow U \subseteq T)$
6	4 5	syl5ibcom	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G)) \to (T \underset{˙}{\oplus} U = T \to U \subseteq T)$
7	3 6	impbid	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G)) \to (U \subseteq T \leftrightarrow T \underset{˙}{\oplus} U = T)$

Metamath Proof Explorer