lsmss1b

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

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

Metamath Proof Explorer