Theorem 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	⊢ ⊕ = ( LSSum ‘ 𝐺 )
Assertion	lsmss1b	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑇 ⊆ 𝑈 ↔ ( 𝑇 ⊕ 𝑈 ) = 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		lsmub1.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
2	1	lsmss1	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑈 ) → ( 𝑇 ⊕ 𝑈 ) = 𝑈 )
3	2	3expia	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑇 ⊆ 𝑈 → ( 𝑇 ⊕ 𝑈 ) = 𝑈 ) )
4	1	lsmub1	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑇 ⊆ ( 𝑇 ⊕ 𝑈 ) )
5		sseq2	⊢ ( ( 𝑇 ⊕ 𝑈 ) = 𝑈 → ( 𝑇 ⊆ ( 𝑇 ⊕ 𝑈 ) ↔ 𝑇 ⊆ 𝑈 ) )
6	4 5	syl5ibcom	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑇 ⊕ 𝑈 ) = 𝑈 → 𝑇 ⊆ 𝑈 ) )
7	3 6	impbid	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑇 ⊆ 𝑈 ↔ ( 𝑇 ⊕ 𝑈 ) = 𝑈 ) )